Fix havocing of struct members when enforcing invariants

Members expressions were ignored when computing the modified set of
loops, and were therefore not being havoc'ed correctly.

In this change we fix this behavior by adding these expressions to the
`modified` set.

Author: SaswatPadhi

regression/contracts/invar_dynamic_struct_member/main.c

@@ -0,0 +1,30 @@
+typedef struct test
+{
+  int x;
+} test;
+
+void main()
+{
+  struct test *t = malloc(sizeof(test));
+  t->x = 0;
+
+  unsigned n;
+  for(unsigned i = 0; i < n; ++i)
+    __CPROVER_loop_invariant(i <= n)
+    {
+      switch(i % 4)
+      {
+      case 0:
+        break;
+
+      case 1:
+      case 2:
+        t->x += 1;
+
+      default:
+        t->x += 2;
+      }
+    }
+
+  assert(t->x == 0 || t->x == 1 || t->x == 2);
+}

regression/contracts/invar_dynamic_struct_member/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion .*: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that  members of typedef'd and dynamically allocated structs
+are correctly havoced when enforcing loop invariants.
+The assertion is expected to fail when `t->x` is correctly havoced (so would be
+set to a nondet value).
+However, it `t->x` is not havoced then it stays at value `0` and would satisfy
+the assertion when the loop is replaced by a single nondet iteration.
+

regression/contracts/invar_struct_member/main.c

@@ -0,0 +1,19 @@
+struct test
+{
+  int x;
+};
+
+void main()
+{
+  struct test t;
+  t.x = 0;
+
+  unsigned n;
+  for(unsigned i = 0; i < n; ++i)
+    __CPROVER_loop_invariant(i <= n)
+    {
+      t.x += 2;
+    }
+
+  assert(t.x == 0 || t.x == 2);
+}

regression/contracts/invar_struct_member/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion t.x == 0 || t.x == 2: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that members of statically allocated are correctly havoced
+when enforcing loop invariants.
+The `t.x == 0 || t.x == 2` assertion is expected to fail when `t.x` is correctly
+havoced (so would be set to a nondet value).
+However, it `t.x` is not havoced then it stays at value `0` and would satisfy
+the assertion when the loop is replaced by a single nondet iteration.

src/goto-instrument/loop_utils.cpp

@@ -61,17 +61,14 @@ void get_modifies_lhs(
   const exprt &lhs,
   modifiest &modifies)
 {
-  if(lhs.id()==ID_symbol)
+  if(lhs.id() == ID_symbol || lhs.id() == ID_member)
     modifies.insert(lhs);
   else if(lhs.id()==ID_dereference)
   {
     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)
-  {
-  }
   else if(lhs.id()==ID_index)
   {
   }