Cleans-up all regression tests for assigns clauses

feliperodri · feliperodri · commit 9678a3d0a159 · 2020-10-15T01:21:34.000-04:00
Signed-off-by: Felipe R. Monteiro &lt;felisous@amazon.com&gt;
diff --git a/regression/contracts/assigns_enforce_01/main.c b/regression/contracts/assigns_enforce_01/main.c
@@ -1,11 +1,4 @@
-#include <assert.h>
-
-int z;
-
-// z is not assigned, but it *may* be assigned.
-// The assigns clause does not need to exactly match the
-// set of variables which are assigned in the function.
-int foo(int *x) __CPROVER_assigns(z, *x)
+int foo(int *x) __CPROVER_assigns(*x)
   __CPROVER_ensures(__CPROVER_return_value == *x + 5)
 {
   *x = *x + 0;
diff --git a/regression/contracts/assigns_enforce_02/main.c b/regression/contracts/assigns_enforce_02/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int z;
 
 int foo(int *x) __CPROVER_assigns(z)
diff --git a/regression/contracts/assigns_enforce_03/main.c b/regression/contracts/assigns_enforce_03/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_04/main.c b/regression/contracts/assigns_enforce_04/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_05/main.c b/regression/contracts/assigns_enforce_05/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_06/main.c b/regression/contracts/assigns_enforce_06/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_07/main.c b/regression/contracts/assigns_enforce_07/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_08/main.c b/regression/contracts/assigns_enforce_08/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x) __CPROVER_assigns(*x)
 {
   int *a = x;
diff --git a/regression/contracts/assigns_enforce_08/test.desc b/regression/contracts/assigns_enforce_08/test.desc
@@ -6,4 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification succeeds when a function with an assigns clause calls another with an additional level of indirection, and that functions respects the assigns clause of the caller.
+This test checks that verification succeeds when a function with an assigns
+clause calls another with an additional level of indirection, and that
+functions respects the assigns clause of the caller.
diff --git a/regression/contracts/assigns_enforce_09/main.c b/regression/contracts/assigns_enforce_09/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int **x) __CPROVER_assigns(*x)
 {
   f2(x);
diff --git a/regression/contracts/assigns_enforce_10/main.c b/regression/contracts/assigns_enforce_10/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_11/main.c b/regression/contracts/assigns_enforce_11/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
 {
   f2(x1, y1, z1);
diff --git a/regression/contracts/assigns_enforce_12/main.c b/regression/contracts/assigns_enforce_12/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x) __CPROVER_assigns(*x)
 {
   int *a = x;
diff --git a/regression/contracts/assigns_enforce_13/main.c b/regression/contracts/assigns_enforce_13/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void f1(int *x, int *y) __CPROVER_assigns(*y)
 {
   int *a = x;
diff --git a/regression/contracts/assigns_enforce_14/main.c b/regression/contracts/assigns_enforce_14/main.c
@@ -0,0 +1,19 @@
+int z;
+
+// z is not assigned, but it *may* be assigned.
+// The assigns clause does not need to exactly match the
+// set of variables which are assigned in the function.
+int foo(int *x) __CPROVER_assigns(z, *x)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}
diff --git a/regression/contracts/assigns_enforce_14/test.desc b/regression/contracts/assigns_enforce_14/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
+
+Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).
+
+To make such assumptions would cause verification to fail.
diff --git a/regression/contracts/assigns_enforce_malloc_01/main.c b/regression/contracts/assigns_enforce_malloc_01/main.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <stdlib.h>
 
 int f1(int *a, int *b) __CPROVER_assigns(*a)
 {
diff --git a/regression/contracts/assigns_enforce_malloc_02/main.c b/regression/contracts/assigns_enforce_malloc_02/main.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <stdlib.h>
 
 int f1(int *a, int *b) __CPROVER_assigns(*a)
 {
diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc
@@ -3,6 +3,8 @@ main.c
 --enforce-all-contracts
 ^EXIT=6$
 ^SIGNAL=0$
+Call to malloc at location 18 falls between goto source location 23 and it's
+destination at location 15. Unable to complete instrumentation, as this
 malloc may be in a loop.$
 --
 --
diff --git a/regression/contracts/assigns_enforce_scoping_01/main.c b/regression/contracts/assigns_enforce_scoping_01/main.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int f1(int *a, int *b) __CPROVER_assigns(*a)
 {
   if(*a > 0)
diff --git a/regression/contracts/assigns_enforce_scoping_02/main.c b/regression/contracts/assigns_enforce_scoping_02/main.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <stdlib.h>
 
 int f1(int *a, int *b) __CPROVER_assigns(*a)
 {
diff --git a/regression/contracts/assigns_replace_01/main.c b/regression/contracts/assigns_replace_01/main.c
@@ -9,7 +9,7 @@ int main()
 {
   int n = 6;
   foo(&n);
+  assert(n == 7);
   assert(n == 6);
-
   return 0;
 }
diff --git a/regression/contracts/assigns_replace_01/test.desc b/regression/contracts/assigns_replace_01/test.desc
@@ -3,6 +3,8 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=10$
 ^SIGNAL=0$
+assertion n == 7: FAILURE
+assertion n == 6: FAILURE
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_replace_05/test.desc b/regression/contracts/assigns_replace_05/test.desc
@@ -6,6 +6,7 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-This test checks that verification fails when assigns clauses are combined with function contracts in a loop improperly.
+This test checks that verification fails when assigns clauses are combined with function contracts
+in a loop improperly, i.e., always assumes memory not mention in ensures clauses are unchanged.
 
 BUG: Currently, function call replacement using 'ensures' specifications encodes an implicit assumption that any memory not mentioned in the ensures clause remains unchanged throughout the function, even when an 'assigns' clause is not present.
diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc
@@ -6,4 +6,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
---replace-all-calls-with-contracts is the current name for the flag. This should be updated as the flag changes.
+This tests a simple example of a function with requires and ensures which should both be satisfied.

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-#include <assert.h>`
`2`		`-`
`3`	`1`	`int z;`
`4`	`2`
`5`	`3`	`int foo(int *x) __CPROVER_assigns(z)`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-#include <assert.h>`
`2`		`-`
`3`	`1`	`void f1(int x1, int y1, int z1) __CPROVER_assigns(x1, y1, z1)`
`4`	`2`	`{`
`5`	`3`	`f2(x1, y1, z1);`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-#include <assert.h>`
`2`		`-`
`3`	`1`	`void f1(int x) __CPROVER_assigns(x)`
`4`	`2`	`{`
`5`	`3`	`int *a = x;`
Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,3 @@`
`1`		`-#include <assert.h>`
`2`		`-`
`3`	`1`	`void f1(int *x) __CPROVER_assigns(x)`
`4`	`2`	`{`
`5`	`3`	`f2(x);`