Fixes regression tests for function contracts

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

regression/contracts/assigns_enforce_arrays_01/main.c

@@ -4,6 +4,7 @@ void f1(int a[], int len) __CPROVER_assigns(a)
   a = b;
   int *indr = a + 2;
   *indr = 5;
+  a[5] = 2;
 }
 
 int main()

regression/contracts/assigns_enforce_arrays_02/main.c

@@ -8,7 +8,7 @@ int nextIdx() __CPROVER_assigns(idx)
   return idx;
 }
 
-void f1(int a[], int len)
+void f1(int a[], int len) __CPROVER_assigns(*a, idx)
 {
   a[nextIdx()] = 5;
 }

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -10,3 +10,5 @@ Checks whether the instrumentation process does not duplicate function calls
 used as part of array-index operations, i.e., if a function call is used in
 the computation of the index of an array assignment, then instrumenting that
 statement with an assigns clause will not result in multiple function calls.
+This test also ensures that assigns clauses correctly check for global
+variables modified by subcalls.

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -6,5 +6,5 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an array is assigned at an index
-below its lower bound.
+Checks whether verification fails when an assigns clause contains pointer,
+but function only modifies its content.

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -6,6 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an array is assigned via a
-function call which assigns a pointer to an element out of the
-allowable range.
+Checks whether verification fails when an assigns clause of a function
+indicates the pointer might change, but one of its internal function only
+modified its content.

regression/contracts/assigns_enforce_arrays_10/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int idx = 4;
+
+int nextIdx() __CPROVER_assigns(idx)
+{
+  idx++;
+  return idx;
+}
+
+void f1(int a[], int len) __CPROVER_assigns(*a)
+{
+  a[nextIdx()] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  assert(idx == 5);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_10/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test also ensures that assigns clauses correctly check for global
+variables modified by subcalls. In this case, since the assigns clause
+doesn't include the modified global variable, the verification should failed.

regression/contracts/assigns_enforce_malloc_01/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-int f1(int *a, int *b) __CPROVER_assigns(*a)
+int f1(int *a, int *b) __CPROVER_assigns(*a, b)
 {
   b = (int *)malloc(sizeof(int));
   *b = 5;

regression/contracts/assigns_enforce_malloc_02/main.c

@@ -1,10 +1,10 @@
 #include <stdlib.h>
 
-int f1(int *a, int *b) __CPROVER_assigns(*a)
+int f1(int *a, int *b) __CPROVER_assigns(*a, b)
 {
   while(*a > 0)
   {
-    int *b = (int *)malloc(sizeof(int));
+    b = (int *)malloc(sizeof(int));
     *b = 5;
   }
 }

regression/contracts/assigns_enforce_multi_file_02/header.h

@@ -14,7 +14,7 @@ struct pair_of_pairs
 
 int f1(int *a, struct pair *b);
 
-int f1(int *a, struct pair *b) __CPROVER_assigns(*a)
+int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b)
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));