Merge pull request #5961 from padhi-aws-forks/loop_modifies_fix

Author: feliperodri

regression/contracts/invar_check_pointer_modifies-01/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *data = malloc(1);
+  *data = 42;
+
+  unsigned i;
+  while(i > 0)
+    __CPROVER_loop_invariant(*data == 42)
+    {
+      *data = 42;
+      i--;
+    }
+
+  assert(*data = 42);
+}

regression/contracts/invar_check_pointer_modifies-01/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion \*data = 42: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
+--
+This test checks that modifications to deref-ed pointers are correctly handled.
+In such cases, pointers should not be havoc'ed, only the value should be.

regression/contracts/invar_check_pointer_modifies-02/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  char *copy, *data = malloc(1);
+
+  copy = data;
+  *data = 42;
+
+  unsigned i;
+  while(i > 0)
+    __CPROVER_loop_invariant(*data == 42)
+    {
+      *data = 42;
+      i--;
+    }
+
+  assert(data == copy);
+  assert(*copy = 42);
+}

regression/contracts/invar_check_pointer_modifies-02/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion data == copy: SUCCESS$
+^\[main.assertion.2\] .* assertion \*copy = 42: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
+--
+This test checks that modifications to aliased pointers are correctly handled.

src/goto-instrument/loop_utils.cpp

@@ -65,10 +65,9 @@ void get_modifies_lhs(
     modifies.insert(lhs);
   else if(lhs.id()==ID_dereference)
   {
-    modifiest m=local_may_alias.get(t, to_dereference_expr(lhs).pointer());
-    for(modifiest::const_iterator m_it=m.begin();
-        m_it!=m.end(); m_it++)
-      get_modifies_lhs(local_may_alias, t, *m_it, modifies);
+    const auto &pointer = to_dereference_expr(lhs).pointer();
+    for(const auto &mod : local_may_alias.get(t, pointer))
+      modifies.insert(dereference_exprt{mod});
   }
   else if(lhs.id()==ID_member)
   {