Skip function parameters and auxiliary variables when checking assigns clauses and check loop-freeness

regression/contracts/assigns_enforce_04/test.desc

@@ -3,12 +3,6 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$

regression/contracts/assigns_enforce_05/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.1\] line \d+ .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/assigns_enforce_18/test.desc

@@ -7,7 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
 ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$

regression/contracts/assigns_enforce_21/test.desc

@@ -6,9 +6,6 @@ main.c
 main.c function bar
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
-^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -10,7 +10,6 @@ main.c
 ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$
@@ -25,7 +24,6 @@ main.c
 ^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -6,7 +6,6 @@ main.c
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
 ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
 ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_subfunction_calls/test.desc

@@ -3,28 +3,15 @@ main.c
 --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^main.c function bar$
-^\[bar.1\] line \d+ Check that x is assignable: SUCCESS$
-^\[bar.2\] line \d+ Check that y is assignable: SUCCESS$
-^\[bar.3\] line \d+ Check that x is assignable: SUCCESS$
-^\[bar.4\] line \d+ Check that y is assignable: SUCCESS$
 ^main.c function baz$
 ^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$
 ^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$
 ^main.c function foo$
-^\[foo.1\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.2\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$
-^\[foo.3\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.4\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$
-^\[foo.5\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.6\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$
-^\[foo.7\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.8\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$
 ^VERIFICATION FAILED$
 --

regression/contracts/assigns_function_pointer/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract bar
 ^EXIT=0$
 ^SIGNAL=0$
-^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_type_checking_valid_cases/test.desc

@@ -3,13 +3,9 @@ main.c
 --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
 ^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$
-^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
-^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
-^\[foo4.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$
 ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$
@@ -28,7 +24,6 @@ main.c
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$
-^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 Checks whether CBMC parses correctly all standard cases for assigns clauses.

regression/contracts/assigns_validity_pointer_01/test.desc

@@ -8,7 +8,6 @@ SUCCESS
 // bar
 ASSERT \*foo::x > 0
 IF ¬\(\*foo::x = 3\) THEN GOTO \d
-IF ¬\(.*0.* = NULL\) THEN GOTO \d
 ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\)
 ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false
 ASSUME .*::tmp_if_expr\$\d

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -7,8 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/function_check_02/main.c

@@ -15,10 +15,16 @@ int initialize(int *arr)
   )
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }

regression/contracts/history-pointer-enforce-10/main.c

@@ -23,7 +23,7 @@ void bar(struct pair *p) __CPROVER_assigns(p->y)
   p->y = (p->y + 5);
 }
 
-void baz(struct pair p) __CPROVER_assigns(p)
+void baz(struct pair p) __CPROVER_assigns()
   __CPROVER_ensures(p == __CPROVER_old(p))
 {
   struct pair pp = p;

regression/contracts/history-pointer-enforce-10/test.desc

@@ -7,8 +7,6 @@ main.c
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$
@@ -19,3 +17,5 @@ main.c
 This test checks that history variables are supported for structs, symbols, and
 struct members. By using the --enforce-contract flag, the postcondition
 (with history variable) is asserted. In this case, this assertion should pass.
+Note: A function is always authorized to assign the variables that store
+its arguments, there is no need to mention them in the assigns clause.

regression/contracts/loop-freeness-check/main.c

@@ -0,0 +1,16 @@
+int foo(int *arr)
+  // clang-format off
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
+// clang-format off
+{
+  for(int i = 0; i < 10; i++)
+    arr[i] = i;
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  foo(arr);
+}

regression/contracts/loop-freeness-check/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo
+^--- begin invariant violation report ---$
+^Invariant check failed$
+^Condition: is_loop_free\(.*\)
+^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+This test checks that loops that remain in the program when attempting to 
+instrument assigns clauses are detected and trigger an INVARIANT.

regression/contracts/quantifiers-exists-ensures-enforce/main.c

@@ -7,10 +7,16 @@ int f1(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
@@ -24,10 +30,16 @@ int f2(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = 0;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }

regression/contracts/quantifiers-exists-requires-enforce/main.c

@@ -1,7 +1,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-#define MAX_LEN 64
+#define MAX_LEN 10
 
 // clang-format off
 bool f1(int *arr, int len)
@@ -18,11 +18,27 @@ bool f1(int *arr, int len)
 // clang-format on
 {
   bool found_four = false;
-  for(int i = 0; i <= MAX_LEN; i++)
-  {
-    if(i < len)
-      found_four |= (arr[i] == 4);
-  }
+  if(0 < len)
+    found_four |= (arr[0] == 4);
+  if(1 < len)
+    found_four |= (arr[1] == 4);
+  if(2 < len)
+    found_four |= (arr[2] == 4);
+  if(3 < len)
+    found_four |= (arr[3] == 4);
+  if(4 < len)
+    found_four |= (arr[4] == 4);
+  if(5 < len)
+    found_four |= (arr[5] == 4);
+  if(6 < len)
+    found_four |= (arr[6] == 4);
+  if(7 < len)
+    found_four |= (arr[7] == 4);
+  if(8 < len)
+    found_four |= (arr[8] == 4);
+
+  if(9 < len)
+    found_four |= (arr[9] == 4);
 
   // clang-format off
   return (len > 0 ==> found_four);

regression/contracts/quantifiers-forall-ensures-enforce/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-#define MAX_LEN 16
+#define MAX_LEN 10
 
 // clang-format off
 int f1(int *arr, int len)
@@ -12,11 +12,27 @@ int f1(int *arr, int len)
   })
 // clang-format on
 {
-  for(int i = 0; i < MAX_LEN; i++)
-  {
-    if(i < len)
-      arr[i] = 0;
-  }
+  if(0 < len)
+    arr[0] = 0;
+  if(1 < len)
+    arr[1] = 0;
+  if(2 < len)
+    arr[2] = 0;
+  if(3 < len)
+    arr[3] = 0;
+  if(4 < len)
+    arr[4] = 0;
+  if(5 < len)
+    arr[5] = 0;
+  if(6 < len)
+    arr[6] = 0;
+  if(7 < len)
+    arr[7] = 0;
+  if(8 < len)
+    arr[8] = 0;
+  if(9 < len)
+    arr[9] = 0;
+
   return 0;
 }
 

regression/contracts/quantifiers-forall-ensures-enforce/test.desc

@@ -4,10 +4,11 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$
 --
 The purpose of this test is to ensure that we can safely use __CPROVER_forall
 within positive contexts (enforced ENSURES clauses).

regression/contracts/quantifiers-forall-requires-enforce/main.c

@@ -12,8 +12,16 @@ bool f1(int *arr)
 // clang-format on
 {
   bool is_identity = true;
-  for(int i = 0; i < 10; ++i)
-    is_identity &= (arr[i] == i);
+  is_identity &= (arr[0] == 0);
+  is_identity &= (arr[1] == 1);
+  is_identity &= (arr[2] == 2);
+  is_identity &= (arr[3] == 3);
+  is_identity &= (arr[4] == 4);
+  is_identity &= (arr[5] == 5);
+  is_identity &= (arr[6] == 6);
+  is_identity &= (arr[7] == 7);
+  is_identity &= (arr[8] == 8);
+  is_identity &= (arr[9] == 9);
   return is_identity;
 }
 

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

@@ -11,10 +11,16 @@ int f1(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }