Skip to content

Commit 11441e8

Browse files
committed
Adds support for pointer history variables in function contracts
This adds support for history variables in function contracts. History variables are (1) declared and (2) assigned to the value that their corresponding variable has at function call time. Currently, only pointers are supported.
1 parent d79e5f0 commit 11441e8

File tree

30 files changed

+595
-14
lines changed

30 files changed

+595
-14
lines changed

regression/.gitignore

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,9 @@
11
tests.log
2+
contracts-*
3+
1.txt
4+
2.txt
5+
sym-tab*.txt
6+
parMap.txt
7+
ass.txt
8+
ensures.txt
9+
Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
=
2+
* type: bool
3+
* #source_location:
4+
* file: main.c
5+
* line: 1
6+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
7+
0: dereference
8+
* type: signedbv
9+
* width: 32
10+
* #c_type: signed_int
11+
* #source_location:
12+
* file: main.c
13+
* line: 1
14+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
15+
* #lvalue: 1
16+
0: symbol
17+
* type: pointer
18+
* #source_location:
19+
* file: main.c
20+
* line: 1
21+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
22+
* width: 64
23+
0: signedbv
24+
* width: 32
25+
* #c_type: signed_int
26+
* identifier: foo::tmp_cc::tmp_cc$0
27+
1: +
28+
* type: signedbv
29+
* width: 32
30+
* #c_type: signed_int
31+
* #source_location:
32+
* file: main.c
33+
* line: 1
34+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
35+
0: typecast
36+
* type: signedbv
37+
* width: 32
38+
* #c_type: signed_int
39+
0: old
40+
* type: bool
41+
* #source_location:
42+
* file: main.c
43+
* line: 1
44+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
45+
0: dereference
46+
* type: signedbv
47+
* width: 32
48+
* #c_type: signed_int
49+
* #source_location:
50+
* file: main.c
51+
* line: 1
52+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
53+
* #lvalue: 1
54+
0: symbol
55+
* type: pointer
56+
* #source_location:
57+
* file: main.c
58+
* line: 1
59+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
60+
* width: 64
61+
0: signedbv
62+
* width: 32
63+
* #c_type: signed_int
64+
* identifier: foo::tmp_cc::tmp_cc$0
65+
1: constant
66+
* type: signedbv
67+
* width: 32
68+
* #c_type: signed_int
69+
* #source_location:
70+
* file: main.c
71+
* line: 1
72+
* working_directory: /local/home/babikian/git/cbmc/regression/contracts/ghost-pointer-enforce-01
73+
* value: 5
74+
* #base: 10
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
void foo(int *x) __CPROVER_assigns(*x)
2+
__CPROVER_ensures(*x == __CPROVER_old(*x) + 5)
3+
{
4+
*x = *x + 5;
5+
}
6+
7+
int main()
8+
{
9+
int n;
10+
foo(&n);
11+
12+
return 0;
13+
}
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+
Verification:
10+
This test checks that history variables are supported for parameters of the
11+
the function under test. By using the --enforce-all-contracts flag,
12+
the post-condition (which contains the history variable) is asserted.
13+
In this case, this assertion should pass.
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
void foo(int *x) __CPROVER_assigns(*x)
2+
__CPROVER_ensures(*x < __CPROVER_old(*x) + 5)
3+
{
4+
*x = *x + 5;
5+
}
6+
7+
int main()
8+
{
9+
int n;
10+
foo(&n);
11+
12+
return 0;
13+
}
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=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables are supported for parameters of the
11+
the function under test. By using the --enforce-all-contracts flag,
12+
the post-condition (which contains the history variable) is asserted.
13+
In this case, this assertion should fail.
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
void foo(int *x) __CPROVER_assigns(*x)
2+
__CPROVER_requires(*x > 0 && *x < __INT_MAX__ - 5) __CPROVER_ensures(
3+
*x >= __CPROVER_old(*x) + 4 && *x <= __CPROVER_old(*x) + 6)
4+
{
5+
*x = *x + 5;
6+
}
7+
8+
int main()
9+
{
10+
int n;
11+
foo(&n);
12+
13+
return 0;
14+
}
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 _ --trace
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables are supported in the case where a
11+
history variable is referred to multiple times within an ensures clause.
12+
By using the --enforce-all-contracts flag, the post-condition (which contains
13+
the history variable) is asserted. In this case, this assertion should pass.
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
2+
__CPROVER_ensures(*x == __CPROVER_old(*y) + 1 && *y == __CPROVER_old(*x) + 2)
3+
{
4+
int x_initial = *x;
5+
*x = *y + 1;
6+
*y = x_initial + 2;
7+
}
8+
9+
int main()
10+
{
11+
int x, y;
12+
foo(&x, &y);
13+
14+
return 0;
15+
}
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+
Verification:
10+
This test checks that history variables are supported in the case where the
11+
function under test has multiple parameters. By using the
12+
--enforce-all-contracts flag, the post-condition (which contains the history
13+
variables) is asserted. In this case, this assertion should pass.
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
2+
__CPROVER_ensures(*x == __CPROVER_old(*x) + 2 || *y == __CPROVER_old(*y) + 3)
3+
{
4+
*x = *x + 1;
5+
*y = *y + 2;
6+
}
7+
8+
int main()
9+
{
10+
int x, y;
11+
foo(&x, &y);
12+
13+
return 0;
14+
}
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=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables are supported in the case where the
11+
function under test has multiple parameters. By using the
12+
--enforce-all-contracts flag, the post-condition (which contains the history
13+
variables) is asserted. In this case, this assertion should fail.
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
void foo(int *x) __CPROVER_assigns(*x)
4+
__CPROVER_ensures(*x == __CPROVER_old(*x) + 5)
5+
{
6+
assert(__CPROVER_old(*x) == *x);
7+
*x = *x + 5;
8+
}
9+
10+
int main()
11+
{
12+
int n;
13+
foo(&n);
14+
15+
return 0;
16+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables are not supported when referred to from
11+
a function body. In such a case, verification should fail.
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
void foo(int *x) __CPROVER_assigns(*x)
2+
__CPROVER_ensures(*x == __CPROVER_old(*y) + 5)
3+
{
4+
*x = *x + 5;
5+
}
6+
7+
int main()
8+
{
9+
int n;
10+
foo(&n);
11+
12+
return 0;
13+
}
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=1$
5+
^SIGNAL=0$
6+
^CONVERSION ERROR$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables may only be used with existing
11+
symbols. In other words, including a new symbol as part of __CPROVER_old()
12+
is not alowed. In such a case, the program should not parse and there
13+
should be a conversion error.
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
3+
void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
4+
__CPROVER_ensures(*x == __CPROVER_old(*x) + 2)
5+
{
6+
*x = *x + 2;
7+
}
8+
9+
int main()
10+
{
11+
int n;
12+
__CPROVER_assume(n > 0 && n < __INT_MAX__ - 2);
13+
foo(&n);
14+
15+
assert(n > 2);
16+
17+
return 0;
18+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables are supported with the use of the
11+
--replace-all-calls-with-contracts flag. In this case, the post-condition
12+
(which contains the history variable) becomes an assumption. We then manually
13+
assert this assumption. For this test, the assertion should succeed.
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
3+
void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x == 0)
4+
__CPROVER_ensures(*x > __CPROVER_old(*x) + 2)
5+
{
6+
*x = *x + 2;
7+
}
8+
9+
int main()
10+
{
11+
int n = 0;
12+
foo(&n);
13+
14+
assert(n > 2);
15+
16+
return 0;
17+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables are supported with the use of the
11+
--replace-all-calls-with-contracts flag. In this case, the post-condition
12+
(which contains the history variable) becomes an assumption. We then manually
13+
assert this assumption. For this test, the assertion should succeed.
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
3+
void foo(int *x) __CPROVER_assigns(*x)
4+
__CPROVER_requires(*x == __CPROVER_old(*x))
5+
__CPROVER_ensures(*x == __CPROVER_old(*x) + 2)
6+
{
7+
*x = *x + 2;
8+
}
9+
10+
int main()
11+
{
12+
int n = 0;
13+
foo(&n);
14+
15+
assert(n == 2);
16+
17+
return 0;
18+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Verification:
10+
This test checks that history variables cannot be used as part of the
11+
pre-condition contract. In this case, verification should fail.

0 commit comments

Comments
 (0)