Fixed some array and pointer reads\writes not appearing

Author: AnnaTrost

src/analyses/goto_rw.cpp

@@ -205,6 +205,8 @@ void rw_range_sett::get_objects_dereference(
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(READ, pointer);
+  if(mode!=READ)
+    get_objects_rec(mode, pointer);
 }
 
 /*******************************************************************\
@@ -583,13 +585,14 @@ Function: rw_range_sett::get_objects_address_of
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id()==ID_symbol ||
-     object.id()==ID_string_constant ||
+  if(object.id()==ID_string_constant ||
      object.id()==ID_label ||
      object.id()==ID_array ||
      object.id()=="NULL-object")
     // constant, nothing to do
     return;
+  else if(object.id()==ID_symbol)
+    get_objects_rec(READ, object);
   else if(object.id()==ID_dereference)
     get_objects_rec(READ, object);
   else if(object.id()==ID_index)
@@ -752,6 +755,11 @@ void rw_range_sett::get_objects_rec(
   {
     // dereferencing may yield some weird ones, ignore these
   }
+  else if(mode==LHS_W)
+  {
+    forall_operands(it, expr)
+      get_objects_rec(mode, *it);
+  }
   else
     throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
 }