Merge pull request #4920 from karkhaz/kk-goto-rw-less-conservative

Make goto_rw less conservative

Author: tautschnig

regression/goto-instrument/goto_rw_pointer_handling-2/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  char a = 'a';
+  char *b = &a;
+  *b = 'c';
+}

regression/goto-instrument/goto_rw_pointer_handling-2/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--show-dependence-graph
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Data dependencies: \d+$
+--
+^warning: ignoring
+^Data dependencies: \d+,\s*\d+$
+--
+This tests that the write-set of a pointer contains only the pointed-to
+object when the pointer is dereferenced and written to.
+
+There should therefore be no data dependence between the pointer itself
+and the write to the pointed-to object.

src/analyses/goto_rw.cpp

@@ -429,18 +429,14 @@ void rw_range_sett::get_objects_typecast(
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id() == ID_string_constant ||
-     object.id() == ID_label ||
-     object.id() == ID_array ||
-     object.id() == ID_null_object)
+  if(
+    object.id() == ID_string_constant || object.id() == ID_label ||
+    object.id() == ID_array || object.id() == ID_null_object ||
+    object.id() == ID_symbol)
   {
     // constant, nothing to do
     return;
   }
-  else if(object.id()==ID_symbol)
-  {
-    get_objects_rec(get_modet::READ, object);
-  }
   else if(object.id()==ID_dereference)
   {
     get_objects_rec(get_modet::READ, object);