Skip to content

Commit 5762a10

Browse files
feliperodrifeliperodri
committed
Updates parser and type checking to properly handle code contracts
We move the contracts specification from the function body to the function signature. We also want to be able to handle contracts when verifying multiple source files (e.g., contracts specified in .h files). Finally, we must prepare the parser and the type-checking engine to handle new assigns clause constructs, which enables support for arrays and structs. Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 947fb8f commit 5762a10

File tree

43 files changed

+489
-121
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+489
-121
lines changed

‎regression/contracts/assigns_enforce_01/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
int foo(int *x) __CPROVER_assigns(*x)
2-
__CPROVER_ensures(__CPROVER_return_value == *x + 5)
2+
__CPROVER_ensures(__CPROVER_return_value == *x + 5);
3+
4+
int foo(int *x)
35
{
46
*x = *x + 0;
57
return *x + 5;

‎regression/contracts/assigns_enforce_02/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
int z;
22

33
int foo(int *x) __CPROVER_assigns(z)
4-
__CPROVER_ensures(__CPROVER_return_value == *x + 5)
4+
__CPROVER_ensures(__CPROVER_return_value == *x + 5);
5+
6+
int foo(int *x)
57
{
68
*x = *x + 0;
79
return *x + 5;

‎regression/contracts/assigns_enforce_03/main.c

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,20 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2);
4+
5+
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3);
6+
7+
void f1(int *x1, int *y1, int *z1)
28
{
39
f2(x1, y1, z1);
410
}
511

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
12+
void f2(int *x2, int *y2, int *z2)
713
{
814
f3(x2, y2, z2);
915
}
1016

11-
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
17+
void f3(int *x3, int *y3, int *z3)
1218
{
1319
*x3 = *x3 + 1;
1420
*y3 = *y3 + 1;

‎regression/contracts/assigns_enforce_04/main.c

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,20 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2);
4+
5+
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3);
6+
7+
void f1(int *x1, int *y1, int *z1)
28
{
39
f2(x1, y1, z1);
410
}
511

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
12+
void f2(int *x2, int *y2, int *z2)
713
{
814
f3(x2, y2, z2);
915
}
1016

11-
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
17+
void f3(int *x3, int *y3, int *z3)
1218
{
1319
*x3 = *x3 + 1;
1420
*y3 = *y3 + 1;

‎regression/contracts/assigns_enforce_05/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2);
4+
5+
void f1(int *x1, int *y1, int *z1)
26
{
37
f2(x1, y1, z1);
48
}
59

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
10+
void f2(int *x2, int *y2, int *z2)
711
{
812
f3(x2, y2, z2);
913
}

‎regression/contracts/assigns_enforce_06/main.c

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,20 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2);
4+
5+
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3);
6+
7+
void f1(int *x1, int *y1, int *z1)
28
{
39
f2(x1, y1, z1);
410
}
511

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
12+
void f2(int *x2, int *y2, int *z2)
713
{
814
f3(x2, y2, z2);
915
}
1016

11-
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
17+
void f3(int *x3, int *y3, int *z3)
1218
{
1319
*x3 = *x3 + 1;
1420
*y3 = *y3 + 1;

‎regression/contracts/assigns_enforce_07/main.c

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,20 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2);
4+
5+
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3);
6+
7+
void f1(int *x1, int *y1, int *z1)
28
{
39
f2(x1, y1, z1);
410
}
511

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
12+
void f2(int *x2, int *y2, int *z2)
713
{
814
f3(x2, y2, z2);
915
}
1016

11-
void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
17+
void f3(int *x3, int *y3, int *z3)
1218
{
1319
*x3 = *x3 + 1;
1420
*y3 = *y3 + 1;

‎regression/contracts/assigns_enforce_08/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1-
void f1(int *x) __CPROVER_assigns(*x)
1+
void f1(int *x) __CPROVER_assigns(*x);
2+
3+
void f2(int **y) __CPROVER_assigns(**y);
4+
5+
void f1(int *x)
26
{
37
int *a = x;
48
f2(&a);
59
}
6-
void f2(int **y) __CPROVER_assigns(**y)
10+
void f2(int **y)
711
{
812
**y = 5;
913
}

‎regression/contracts/assigns_enforce_09/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
1-
void f1(int **x) __CPROVER_assigns(*x)
1+
void f1(int **x) __CPROVER_assigns(*x);
2+
3+
void f2(int **y) __CPROVER_assigns(**y);
4+
5+
void f1(int **x)
26
{
37
f2(x);
48
}
5-
void f2(int **y) __CPROVER_assigns(**y)
9+
void f2(int **y)
610
{
711
**y = 5;
812
}

‎regression/contracts/assigns_enforce_10/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*y2, *z2);
4+
5+
void f1(int *x1, int *y1, int *z1)
26
{
37
f2(x1, y1, z1);
48
}
59

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*y2, *z2)
10+
void f2(int *x2, int *y2, int *z2)
711
{
812
*y2 = 5;
913
*z2 = 5;

‎regression/contracts/assigns_enforce_11/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1-
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1)
1+
void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1);
2+
3+
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2);
4+
5+
void f1(int *x1, int *y1, int *z1)
26
{
37
f2(x1, y1, z1);
48
}
59

6-
void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2)
10+
void f2(int *x2, int *y2, int *z2)
711
{
812
*y2 = 5;
913
*z2 = 5;

‎regression/contracts/assigns_enforce_12/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
void f1(int *x) __CPROVER_assigns(*x)
1+
void f1(int *x) __CPROVER_assigns(*x);
2+
3+
void f1(int *x)
24
{
35
int *a = x;
46
*a = 5;

‎regression/contracts/assigns_enforce_13/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
void f1(int *x, int *y) __CPROVER_assigns(*y)
1+
void f1(int *x, int *y) __CPROVER_assigns(*y);
2+
3+
void f1(int *x, int *y)
24
{
35
int *a = x;
46
*a = 5;

‎regression/contracts/assigns_enforce_14/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,9 @@ int z;
44
// The assigns clause does not need to exactly match the
55
// set of variables which are assigned in the function.
66
int foo(int *x) __CPROVER_assigns(z, *x)
7-
__CPROVER_ensures(__CPROVER_return_value == *x + 5)
7+
__CPROVER_ensures(__CPROVER_return_value == *x + 5);
8+
9+
int foo(int *x)
810
{
911
*x = *x + 0;
1012
return *x + 5;

‎regression/contracts/assigns_enforce_malloc_01/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#include <stdlib.h>
22

3-
int f1(int *a, int *b) __CPROVER_assigns(*a)
3+
int f1(int *a, int *b) __CPROVER_assigns(*a);
4+
5+
int f1(int *a, int *b)
46
{
57
b = (int *)malloc(sizeof(int));
68
*b = 5;

‎regression/contracts/assigns_enforce_malloc_02/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#include <stdlib.h>
22

3-
int f1(int *a, int *b) __CPROVER_assigns(*a)
3+
int f1(int *a, int *b) __CPROVER_assigns(*a);
4+
5+
int f1(int *a, int *b)
46
{
57
while(*a > 0)
68
{

‎regression/contracts/assigns_enforce_scoping_01/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
1-
int f1(int *a, int *b) __CPROVER_assigns(*a)
1+
int f1(int *a, int *b) __CPROVER_assigns(*a);
2+
3+
int f1(int *a, int *b)
24
{
35
if(*a > 0)
46
{

‎regression/contracts/assigns_enforce_scoping_02/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
#include <stdlib.h>
1+
int f1(int *a, int *b) __CPROVER_assigns(*a);
22

3-
int f1(int *a, int *b) __CPROVER_assigns(*a)
3+
int f1(int *a, int *b)
44
{
55
if(*a > 0)
66
{

‎regression/contracts/assigns_replace_01/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#include <assert.h>
22

3-
void foo(int *x) __CPROVER_assigns(*x)
3+
void foo(int *x) __CPROVER_assigns(*x);
4+
5+
void foo(int *x)
46
{
57
*x = 7;
68
}

‎regression/contracts/assigns_replace_02/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#include <assert.h>
22

3-
void foo(int *x, int *y) __CPROVER_assigns(*x)
3+
void foo(int *x, int *y) __CPROVER_assigns(*x);
4+
5+
void foo(int *x, int *y)
46
{
57
*x = 7;
68
}

‎regression/contracts/assigns_replace_03/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@
33
int y;
44
double z;
55

6-
void bar(char **c) __CPROVER_assigns(y, z, **c) __CPROVER_ensures(**c == 6)
6+
void bar(char **c) __CPROVER_assigns(y, z, **c) __CPROVER_ensures(**c == 6);
7+
8+
void bar(char **c)
79
{
810
}
911

‎regression/contracts/assigns_replace_04/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
#include <assert.h>
22

3-
void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5)
3+
void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5);
4+
5+
void f3(int *x3, int *y3) __CPROVER_assigns(*x3) __CPROVER_ensures(*x3 > 100);
6+
7+
void f2(int *x2, int *y2)
48
{
59
*x2 = 10;
610
}
711

8-
void f3(int *x3, int *y3) __CPROVER_assigns(*x3) __CPROVER_ensures(*x3 > 100)
12+
void f3(int *x3, int *y3)
913
{
1014
*x3 = 101;
1115
}

‎regression/contracts/assigns_replace_05/main.c

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
11
#include <assert.h>
22

3-
void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5)
3+
void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5);
4+
5+
void f3(int *x3, int *y3) __CPROVER_ensures(*x3 > 100);
6+
7+
void f2(int *x2, int *y2)
48
{
59
*x2 = 10;
610
}
711

8-
void f3(int *x3, int *y3) __CPROVER_ensures(*x3 > 100)
12+
void f3(int *x3, int *y3)
913
{
1014
*x3 = 101;
1115
}

‎regression/contracts/function_apply_01/main.c

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@
66

77
#include <assert.h>
88

9-
int foo() __CPROVER_ensures(__CPROVER_return_value == 0)
9+
int foo() __CPROVER_ensures(__CPROVER_return_value == 0);
10+
11+
int foo()
1012
{
1113
return 1;
1214
}

‎regression/contracts/function_check_01/main.c

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,11 @@
55

66
#include <assert.h>
77

8+
int min(int a, int b) __CPROVER_requires(a >= 0 && b >= 0) __CPROVER_ensures(
9+
__CPROVER_return_value <= a && __CPROVER_return_value <= b &&
10+
(__CPROVER_return_value == a || __CPROVER_return_value == b));
11+
812
int min(int a, int b)
9-
__CPROVER_requires(a >= 0 && b >= 0)
10-
__CPROVER_ensures(__CPROVER_return_value <= a &&
11-
__CPROVER_return_value <= b &&
12-
(__CPROVER_return_value == a || __CPROVER_return_value == b)
13-
)
1413
{
1514
if(a <= b)
1615
{

‎regression/contracts/function_check_02/main.c

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,12 @@
44
// A known bug (resolved in PR #2278) causes the use of quantifiers
55
// in ensures to fail.
66

7+
int initialize(int *arr) __CPROVER_ensures(__CPROVER_forall {
8+
int i;
9+
(0 <= i && i < 10) == > arr[i] == i
10+
});
11+
712
int initialize(int *arr)
8-
__CPROVER_ensures(
9-
__CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
10-
)
1113
{
1214
for(int i = 0; i < 10; i++)
1315
{

‎regression/contracts/function_check_03/main.c

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,12 @@
55
// This currently fails because side-effect checking in loop invariants is
66
// incorrect.
77

8+
void initialize(int *arr, int len) __CPROVER_ensures(__CPROVER_forall {
9+
int i;
10+
(0 <= i && i < len) == > arr[i] == i
11+
});
12+
813
void initialize(int *arr, int len)
9-
__CPROVER_ensures(
10-
__CPROVER_forall {int i; (0 <= i && i < len) ==> arr[i] == i}
11-
)
1214
{
1315
for(int i = 0; i < len; i++)
1416
__CPROVER_loop_invariant(

‎regression/contracts/function_check_04/main.c

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,9 @@
55

66
#include <assert.h>
77

8-
int foo()
9-
__CPROVER_ensures(__CPROVER_return_value == 0)
8+
int foo() __CPROVER_ensures(__CPROVER_return_value == 0);
9+
10+
int foo()
1011
{
1112
return 1;
1213
}

0 commit comments

Comments
 (0)