Adds regression test to cover code contracts support

Code contracts now supports assigns clause with structs and array ranges.
It also supports contracts specified across multiple source files.
So, we added regression tests to cover these capabilites.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_arrays_01/main.c

@@ -0,0 +1,15 @@
+void f1(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  int b[10];
+  a = b;
+  int *indr = a + 2;
+  *indr = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_01/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks their assigns clause behavior when it reasons (indirectly)
+over a freshly-allocated variable.

regression/contracts/assigns_enforce_arrays_02/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(idx, a[2, 5])
+{
+  a[nextIdx()] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  assert(idx == 5);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+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.

regression/contracts/assigns_enforce_arrays_03/main.c

@@ -0,0 +1,14 @@
+void f1(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  int *indr;
+  indr = a + 3;
+  *indr = 5;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned indirectly
+through a pointer.

regression/contracts/assigns_enforce_arrays_04/main.c

@@ -0,0 +1,24 @@
+void assigns_single(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[8] = 20;
+}
+
+void assigns_upper_bound(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  a[5] = 10;
+}
+
+void assigns_lower_bound(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  a[2] = 10;
+}
+
+int main()
+{
+  int arr[10];
+  assigns_upper_bound(arr, 10);
+  assigns_lower_bound(arr, 10);
+  assigns_single(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned at both upper
+and lower bounds of its assignable array range. Single-value array range
+assignment is checked as well.

regression/contracts/assigns_enforce_arrays_05/main.c

@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  a[1] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_under(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index
+below its lower bound.

regression/contracts/assigns_enforce_arrays_06/main.c

@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[7] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_under(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_06/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index below
+its allowed index and specification contains only a single cell
+instead of a range.

regression/contracts/assigns_enforce_arrays_07/main.c

@@ -0,0 +1,12 @@
+void assign_out_over(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  a[6] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_over(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_07/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index
+above its upper bound.

regression/contracts/assigns_enforce_arrays_08/main.c

@@ -0,0 +1,12 @@
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[9] = 5;
+}
+
+int main()
+{
+  int arr[10];
+  assign_out_under(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_08/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned at an index
+above its allowed index.

regression/contracts/assigns_enforce_arrays_09/main.c

@@ -0,0 +1,12 @@
+void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2, last_idx])
+{
+  a[last_idx] = 6;
+}
+
+int main()
+{
+  int arr[10];
+  assigns_in_range(arr, 9);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_09/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned at the upper
+bounds of its assignable array range, when the range has a non-constant bound.

regression/contracts/assigns_enforce_arrays_10/main.c

@@ -0,0 +1,13 @@
+void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2, last_idx])
+{
+  last_idx++;
+  a[last_idx] = 6;
+}
+
+int main()
+{
+  int arr[10];
+  assigns_in_range(arr, 9);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_10/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when an array is assigned past the upper
+bound of its assignable array range, using the symbol of the upper bound,
+after it has been incremented. This is intended to show that the bounds
+are determined at the time the function is called.

regression/contracts/assigns_enforce_arrays_11/main.c

@@ -0,0 +1,21 @@
+void assigns_single(int a[], int len) __CPROVER_assigns(a[7])
+{
+}
+
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+}
+
+void assigns_big_range(int a[], int len) __CPROVER_assigns(a[2, 7])
+{
+  assigns_single(a, len);
+  assigns_range(a, len);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_big_range(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_11/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned through
+calls to functions with array assigns clauses which are compatible with
+that of the caller.

regression/contracts/assigns_enforce_arrays_12/main.c

@@ -0,0 +1,16 @@
+void assign_25(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+}
+
+void assign_37(int a[], int len) __CPROVER_assigns(a[3, 7])
+{
+  assign_25(a, len);
+}
+
+int main()
+{
+  int arr[10];
+  assign_37(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_12/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Checks whether verification fails when a function with an array assigns target
+calls a function which may assign below the allowable range.

regression/contracts/assigns_enforce_arrays_13/main.c

@@ -0,0 +1,18 @@
+void assigns_ptr(int *x) __CPROVER_assigns(*x)
+{
+  *x = 200;
+}
+
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  int *ptr = &(a[3]);
+  assigns_ptr(ptr);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_range(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_13/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification succeeds when an array is assigned via a
+function call which assigns a pointer to one of its elements.

regression/contracts/assigns_enforce_arrays_14/main.c

@@ -0,0 +1,18 @@
+void assigns_ptr(int *x) __CPROVER_assigns(*x)
+{
+  *x = 200;
+}
+
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2, 5])
+{
+  int *ptr = &(a[7]);
+  assigns_ptr(ptr);
+}
+
+int main()
+{
+  int arr[10];
+  assigns_range(arr, 10);
+
+  return 0;
+}

regression/contracts/assigns_enforce_arrays_14/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^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.