Adds support for range annotation in assigns clauses

regression/contracts/assigns_enforce_arrays_01/main.c

@@ -1,4 +1,6 @@
-void f1(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
   int b[10];
   a = b;

regression/contracts/assigns_enforce_arrays_02/main.c

@@ -8,7 +8,9 @@ int nextIdx() __CPROVER_assigns(idx)
   return idx;
 }
 
-void f1(int a[], int len)
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(idx, a[2 .. 5])
+/* clang-format on */
 {
   a[nextIdx()] = 5;
 }

regression/contracts/assigns_enforce_arrays_03/main.c

@@ -1,12 +1,16 @@
-void assign_out_under(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void f1(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
-  a[1] = 5;
+  int *indr;
+  indr = a + 3;
+  *indr = 5;
 }
 
 int main()
 {
   int arr[10];
-  assign_out_under(arr, 10);
+  f1(arr, 10);
 
   return 0;
 }

regression/contracts/assigns_enforce_arrays_03/test.desc

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

regression/contracts/assigns_enforce_arrays_04/main.c

@@ -1,21 +1,28 @@
-void assigns_single(int a[], int len) __CPROVER_assigns(a)
+void assigns_single(int a[], int len) __CPROVER_assigns(a[8])
 {
+  a[8] = 20;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void assigns_upper_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format on */
 {
+  a[5] = 10;
 }
 
-void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
+/* clang-format off */
+void assigns_lower_bound(int a[], int len) __CPROVER_assigns(a[2 .. 5])
+/* clang-format oon */
 {
-  assigns_single(a, len);
-  assigns_range(a, len);
+  a[2] = 10;
 }
 
 int main()
 {
   int arr[10];
-  assigns_big_range(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

@@ -6,6 +6,6 @@ main.c
 ^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.
+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

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

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -6,6 +6,5 @@ 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 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.

regression/contracts/assigns_enforce_arrays_14/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[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.