Skip to content

Commit 31eef04

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 985f1a7 commit 31eef04

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
@@ -206,8 +206,6 @@ void rw_range_sett::get_objects_dereference(
206206
{
207207
const exprt &pointer=deref.pointer();
208208
get_objects_rec(READ, pointer);
209-
if(mode!=READ)
210-
get_objects_rec(mode, pointer);
211209
}
212210

213211
/*******************************************************************\
@@ -586,14 +584,13 @@ Function: rw_range_sett::get_objects_address_of
586584

587585
void rw_range_sett::get_objects_address_of(const exprt &object)
588586
{
589-
if(object.id()==ID_string_constant ||
587+
if(object.id()==ID_symbol ||
588+
object.id()==ID_string_constant ||
590589
object.id()==ID_label ||
591590
object.id()==ID_array ||
592591
object.id()=="NULL-object")
593592
// constant, nothing to do
594593
return;
595-
else if(object.id()==ID_symbol)
596-
get_objects_rec(READ, object);
597594
else if(object.id()==ID_dereference)
598595
get_objects_rec(READ, object);
599596
else if(object.id()==ID_index)
@@ -757,11 +754,6 @@ void rw_range_sett::get_objects_rec(
757754
{
758755
// dereferencing may yield some weird ones, ignore these
759756
}
760-
else if(mode==LHS_W)
761-
{
762-
forall_operands(it, expr)
763-
get_objects_rec(mode, *it);
764-
}
765757
else
766758
throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
767759
}

0 commit comments

Comments
 (0)