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,17 @@
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  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,26 @@
+#include <assert.h>
+
+int idx = 4;
+
+int nextIdx() __CPROVER_assigns(idx)
+{
+  idx++;
+  return idx;
+}
+
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(idx, a[2 .. 5])
+/* clang-format on */
+{
+  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,16 @@
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  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,28 @@
+void assigns_single(int a[], int len) __CPROVER_assigns(a[8])
+{
+  a[8] = 20;
+}
+
+/* clang-format off */
+void assigns_upper_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  a[5] = 10;
+}
+
+/* clang-format off */
+void assigns_lower_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format oon */
+{
+  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,14 @@
+/* clang-format off */
+void assign_out_under(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  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,14 @@
+/* clang-format off */
+void assign_out_over(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  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,14 @@
+/* clang-format off */
+void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2 .. last_idx])
+/* clang-format on */
+{
+  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,15 @@
+/* clang-format off */
+void assigns_in_range(int a[], int last_idx) __CPROVER_assigns(a[2 .. last_idx])
+/* clang-format on */
+{
+  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,25 @@
+void assigns_single(int a[], int len) __CPROVER_assigns(a[7])
+{
+}
+
+/* clang-format off */
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+}
+
+/* clang-format off */
+void assigns_big_range(int a[], int len) __CPROVER_assigns(a[2 .. 7])
+/* clang-format on */
+{
+  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,20 @@
+/* clang-format off */
+void assign_25(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+}
+
+/* clang-format off */
+void assign_37(int a[], int len) __CPROVER_assigns(a[3 .. 7])
+/* clang-format on */
+{
+  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,20 @@
+void assigns_ptr(int *x) __CPROVER_assigns(*x)
+{
+  *x = 200;
+}
+
+/* clang-format off */
+void assigns_range(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
+{
+  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.