Merge pull request #6533 from remi-delmas-3000/function-contracts-prune-write-set

Function contracts: check loop freeness before instrumentation, skip assignments to locals and prune write set using CFG info.

Author: remi-delmas-3000

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,9 +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$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) 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_arrays_01/main.c

@@ -1,4 +1,4 @@
-void f1(int a[], int len) __CPROVER_assigns(a)
+void f1(int a[], int len) __CPROVER_assigns()
 {
   int b[10];
   a = b;

regression/contracts/assigns_enforce_arrays_03/main.c

@@ -1,4 +1,4 @@
-void assign_out_under(int a[], int len) __CPROVER_assigns(a)
+void assign_out_under(int a[], int len) __CPROVER_assigns()
 {
   a[1] = 5;
 }

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -6,5 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an assigns clause contains pointer,
-but function only modifies its content.
+Checks whether verification fails when a function has an array 
+as parameter, an empty assigns clause and attempts to modify the object
+pointed to by the pointer.

regression/contracts/assigns_enforce_arrays_04/main.c

@@ -1,21 +1,20 @@
-void assigns_single(int a[], int len) __CPROVER_assigns(a)
+void assigns_single(int a[], int len)
 {
+  int i;
+  __CPROVER_assume(0 <= i && i < len);
+  a[i] = 0;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
-{
-}
-
-void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
+void uses_assigns(int a[], int len)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
 {
   assigns_single(a, len);
-  assigns_range(a, len);
 }
 
 int main()
 {
   int arr[10];
-  assigns_big_range(arr, 10);
+  uses_assigns(arr, 10);
 
   return 0;
 }

regression/contracts/assigns_enforce_arrays_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract assigns_single --enforce-contract assigns_range --enforce-contract assigns_big_range
+--enforce-contract uses_assigns
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_05/main.c

@@ -1,18 +1,23 @@
-void assigns_ptr(int *x) __CPROVER_assigns(*x)
+void assigns_ptr(int *x)
 {
   *x = 200;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
+void uses_assigns(int a[], int i, int len)
+  // clang-format off
+ __CPROVER_requires(0 <= i && i < len)
+  __CPROVER_assigns(*(&a[i]))
+// clang-format on
 {
-  int *ptr = &(a[7]);
+  int *ptr = &(a[i]);
   assigns_ptr(ptr);
 }
 
 int main()
 {
   int arr[10];
-  assigns_range(arr, 10);
-
+  int i;
+  __CPROVER_assume(0 <= i && i < 10);
+  uses_assigns(arr, i, 10);
   return 0;
 }