Fixing tests where inferred clause does not pass verification

Author: Remi Delmas

regression/contracts/invar_havoc_dynamic_array/main.c

@@ -9,6 +9,7 @@ void main()
   data[5] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
     __CPROVER_loop_invariant(i <= SIZE)
     {
       data[i] = 1;

regression/contracts/invar_havoc_dynamic_array/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-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 data\[5\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c

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

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-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 data\[1\]\[2\]\[3\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long int\)4\]\[\(signed long int\)i\]\[\(signed long int\)6\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/quantifiers-loop-01/main.c

@@ -9,6 +9,7 @@ void main()
 
   for(int i = 0; i < N; ++i)
     // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
       __CPROVER_forall {

regression/contracts/quantifiers-loop-01/test.desc

@@ -1,11 +1,13 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --trace
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] line .* Check loop invariant before entry: SUCCESS
-^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.1\] line .* assertion a\[10\] == 1: SUCCESS
+^\[main\.\d+\] line .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] line .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] line .* assertion a\[10\] == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-loop-02/main.c

@@ -1,12 +1,14 @@
 #include <assert.h>
 
+const int MAX = 3;
 void main()
 {
-  int N, a[64];
-  __CPROVER_assume(0 <= N && N < 64);
+  int N, a[MAX];
+  __CPROVER_assume(0 <= N && N < MAX);
 
   for(int i = 0; i < N; ++i)
     // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
       __CPROVER_forall {

regression/contracts/quantifiers-loop-02/test.desc

@@ -1,11 +1,13 @@
-CORE smt-backend broken-cprover-smt-backend
+CORE smt-backend broken-cprover-smt-backend thorough-smt-backend
 main.c
 --apply-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS
-^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.\d+\] line .* assertion .*: SUCCESS
+^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-loop-03/main.c

@@ -6,12 +6,13 @@
 void main()
 {
   unsigned N;
-  __CPROVER_assume(N <= MAX_SIZE);
+  __CPROVER_assume(0 < N && N <= MAX_SIZE);
 
   int *a = malloc(N * sizeof(int));
 
   for(int i = 0; i < N; ++i)
     // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
       (i != 0 ==> __CPROVER_exists {

regression/contracts/quantifiers-loop-03/test.desc

@@ -1,11 +1,13 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --trace
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] line .* Check loop invariant before entry: SUCCESS
-^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.1\] line .* assertion .*: SUCCESS
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] line .* assertion .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring