Skip to content

Commit 1b65ef9

Browse files
committed
Revert "Fixed some array and pointer reads\writes not appearing"
This reverts commit 55d1297. Pointers require dereferencing, and taking an address of an object does not induce any reads on the object.
1 parent 55d45a0 commit 1b65ef9

File tree

1 file changed

+2
-10
lines changed

1 file changed

+2
-10
lines changed

src/analyses/goto_rw.cpp

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -127,8 +127,6 @@ void rw_range_sett::get_objects_dereference(
127127
{
128128
const exprt &pointer=deref.pointer();
129129
get_objects_rec(get_modet::READ, pointer);
130-
if(mode!=get_modet::READ)
131-
get_objects_rec(mode, pointer);
132130
}
133131

134132
void rw_range_sett::get_objects_byte_extract(
@@ -413,14 +411,13 @@ void rw_range_sett::get_objects_typecast(
413411

414412
void rw_range_sett::get_objects_address_of(const exprt &object)
415413
{
416-
if(object.id()==ID_string_constant ||
414+
if(object.id()==ID_symbol ||
415+
object.id()==ID_string_constant ||
417416
object.id()==ID_label ||
418417
object.id()==ID_array ||
419418
object.id()=="NULL-object")
420419
// constant, nothing to do
421420
return;
422-
else if(object.id()==ID_symbol)
423-
get_objects_rec(get_modet::READ, object);
424421
else if(object.id()==ID_dereference)
425422
get_objects_rec(get_modet::READ, object);
426423
else if(object.id()==ID_index)
@@ -563,11 +560,6 @@ void rw_range_sett::get_objects_rec(
563560
{
564561
// dereferencing may yield some weird ones, ignore these
565562
}
566-
else if(mode==get_modet::LHS_W)
567-
{
568-
forall_operands(it, expr)
569-
get_objects_rec(mode, *it);
570-
}
571563
else
572564
throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
573565
}

0 commit comments

Comments
 (0)