Switch to a more aggressive loop-assigns widening strategy for DFCC

Author: qinheping

regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c

@@ -10,7 +10,7 @@ void main()
   data[4] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_assigns(data[1], i) __CPROVER_loop_invariant(i <= SIZE)
     {
       data[1] = i;
     }

regression/contracts-dfcc/loop_assigns_inference-05/main.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+#define SIZE 8
+
+int main()
+{
+  int i = 0;
+  int *j = malloc(SIZE * sizeof(int));
+  for(i = 0; i < SIZE; i++)
+    // __CPROVER_assigns(h.pos, i)
+    __CPROVER_loop_invariant(0 <= i && i <= SIZE)
+    {
+      int *k;
+      k = j + i;
+      *k = 1;
+    }
+}

regression/contracts-dfcc/loop_assigns_inference-05/test.desc

@@ -0,0 +1,15 @@
+CORE dfcc-only
+main.c
+--no-malloc-may-fail --dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line \d+ Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line \d+ Check step was unwound for loop .*: SUCCESS$
+^\[main.assigns.\d+\] line \d+ Check that \*k is assignable: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns __CPROVER_object_whole(k) is inferred correctly,
+which requires widening *k to the whole object.

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp

@@ -262,7 +262,9 @@ static assignst dfcc_infer_loop_assigns_for_loop(
     {
       address_of_exprt address_of_expr(expr);
       address_of_expr.add_source_location() = expr.source_location();
-      if(!is_constant(address_of_expr))
+      // Widen assigns targets to object_whole if `expr` is a dereference or
+      // with constant address.
+      if(expr.id() == ID_dereference || !is_constant(address_of_expr))
       {
         // Target address is not constant, widening to the whole object
         result.emplace(make_object_whole_call_expr(address_of_expr, ns));