Skip to content

Commit 9678a3d

Browse files
committed
Cleans-up all regression tests for assigns clauses
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent cf8e8cb commit 9678a3d

File tree

25 files changed

+47
-41
lines changed

25 files changed

+47
-41
lines changed

regression/contracts/assigns_enforce_01/main.c

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,4 @@
1-
#include <assert.h>
2-
3-
int z;
4-
5-
// z is not assigned, but it *may* be assigned.
6-
// The assigns clause does not need to exactly match the
7-
// set of variables which are assigned in the function.
8-
int foo(int *x) __CPROVER_assigns(z, *x)
1+
int foo(int *x) __CPROVER_assigns(*x)
92
__CPROVER_ensures(__CPROVER_return_value == *x + 5)
103
{
114
*x = *x + 0;

regression/contracts/assigns_enforce_02/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int z;
42

53
int foo(int *x) __CPROVER_assigns(z)

regression/contracts/assigns_enforce_03/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_04/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_05/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_06/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_07/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_08/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x) __CPROVER_assigns(*x)
42
{
53
int *a = x;

regression/contracts/assigns_enforce_08/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,6 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
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.
9+
This test checks that verification succeeds when a function with an assigns
10+
clause calls another with an additional level of indirection, and that
11+
functions respects the assigns clause of the caller.

regression/contracts/assigns_enforce_09/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int **x) __CPROVER_assigns(*x)
42
{
53
f2(x);

regression/contracts/assigns_enforce_10/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_11/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
42
{
53
f2(x1, y1, z1);

regression/contracts/assigns_enforce_12/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x) __CPROVER_assigns(*x)
42
{
53
int *a = x;

regression/contracts/assigns_enforce_13/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
void f1(int *x, int *y) __CPROVER_assigns(*y)
42
{
53
int *a = x;
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int z;
2+
3+
// z is not assigned, but it *may* be assigned.
4+
// The assigns clause does not need to exactly match the
5+
// set of variables which are assigned in the function.
6+
int foo(int *x) __CPROVER_assigns(z, *x)
7+
__CPROVER_ensures(__CPROVER_return_value == *x + 5)
8+
{
9+
*x = *x + 0;
10+
return *x + 5;
11+
}
12+
13+
int main()
14+
{
15+
int n = 4;
16+
n = foo(&n);
17+
18+
return 0;
19+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
10+
11+
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).
12+
13+
To make such assumptions would cause verification to fail.

regression/contracts/assigns_enforce_malloc_01/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
#include <stdlib.h>
22

33
int f1(int *a, int *b) __CPROVER_assigns(*a)
44
{

regression/contracts/assigns_enforce_malloc_02/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
#include <stdlib.h>
22

33
int f1(int *a, int *b) __CPROVER_assigns(*a)
44
{

regression/contracts/assigns_enforce_malloc_02/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ main.c
33
--enforce-all-contracts
44
^EXIT=6$
55
^SIGNAL=0$
6+
Call to malloc at location 18 falls between goto source location 23 and it's
7+
destination at location 15. Unable to complete instrumentation, as this
68
malloc may be in a loop.$
79
--
810
--

regression/contracts/assigns_enforce_scoping_01/main.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int f1(int *a, int *b) __CPROVER_assigns(*a)
42
{
53
if(*a > 0)

regression/contracts/assigns_enforce_scoping_02/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
#include <stdlib.h>
22

33
int f1(int *a, int *b) __CPROVER_assigns(*a)
44
{

regression/contracts/assigns_replace_01/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ int main()
99
{
1010
int n = 6;
1111
foo(&n);
12+
assert(n == 7);
1213
assert(n == 6);
13-
1414
return 0;
1515
}

regression/contracts/assigns_replace_01/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ main.c
33
--replace-all-calls-with-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6+
assertion n == 7: FAILURE
7+
assertion n == 6: FAILURE
68
^VERIFICATION FAILED$
79
--
810
--

regression/contracts/assigns_replace_05/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ main.c
66
^VERIFICATION FAILED$
77
--
88
--
9-
This test checks that verification fails when assigns clauses are combined with function contracts in a loop improperly.
9+
This test checks that verification fails when assigns clauses are combined with function contracts
10+
in a loop improperly, i.e., always assumes memory not mention in ensures clauses are unchanged.
1011

1112
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.

regression/contracts/function_check_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,4 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
--replace-all-calls-with-contracts is the current name for the flag. This should be updated as the flag changes.
9+
This tests a simple example of a function with requires and ensures which should both be satisfied.

0 commit comments

Comments
 (0)