Skip to content

Commit 5750c68

Browse files
tautschnigtautschnig
authored
Merge pull request #6447 from remi-delmas-3000/fix-local-statics-detection
Fix local static variables detection in assigns clauses
2 parents faaf50e + 5fb8ee5 commit 5750c68

File tree

15 files changed

+278
-99
lines changed

15 files changed

+278
-99
lines changed

‎regression/contracts/assigns_enforce_detect_local_statics/main.c

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
static int x;
5+
static int xx;
6+
7+
void foo()
8+
{
9+
int *y = &x;
10+
int *yy = &xx;
11+
12+
static int x;
13+
// must pass (modifies local static)
14+
x++;
15+
16+
// must pass (modifies assignable global static )
17+
(*y)++;
18+
19+
// must fail (modifies non-assignable global static)
20+
(*yy)++;
21+
}
22+
23+
void bar() __CPROVER_assigns(x)
24+
{
25+
foo();
26+
}
27+
28+
int main()
29+
{
30+
bar();
31+
}

‎regression/contracts/assigns_enforce_detect_local_statics/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--enforce-contract bar
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
7+
^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
8+
^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
9+
^\[foo.\d+\] line \d+ Check that \*yy is assignable: FAILURE$
10+
^VERIFICATION FAILED$
11+
--
12+
--
13+
Checks whether static local and global variables are correctly tracked
14+
in assigns clause verification, accross subfunction calls.

‎regression/contracts/assigns_enforce_statics/main.c

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
1-
#include <assert.h>
2-
#include <stdlib.h>
3-
4-
static int x;
1+
static int x = 0;
52

63
void foo() __CPROVER_assigns(x)
74
{
85
int *y = &x;
96

10-
static int x;
7+
static int x = 0;
8+
9+
// should pass (assigns local x)
1110
x++;
1211

12+
// should fail (assigns global x)
1313
(*y)++;
1414
}
1515

‎regression/contracts/function-calls-03-1/test-enf-f1.desc

Lines changed: 6 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,12 @@
11
CORE
22
main.c
33
--enforce-contract f1 _ --unwind 20 --unwinding-assertions
4-
^EXIT=10$
4+
^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$
5+
^Invariant check failed$
6+
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7+
^Reason: Recursive functions found during inlining$
8+
^EXIT=(127|134|137)$
59
^SIGNAL=0$
6-
^file main.c line \d+ function f2: recursion is ignored on call to \'f2\'$
7-
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
8-
^VERIFICATION FAILED$
910
--
1011
--
11-
Verification:
12-
function | pre-cond | post-cond
13-
---------|----------|----------
14-
f1 | assumed | asserted
15-
16-
Test should fail:
17-
The postcondition of f2 is incorrect, considering the recursion particularity.
18-
19-
Recursion:
20-
The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions).
12+
Test should fail because a recursive function is found during inlining.

‎regression/contracts/function-calls-03-1/test-enf-f2.desc

Lines changed: 6 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,12 @@
11
CORE
22
main.c
33
--enforce-contract f2 _ --unwind 20 --unwinding-assertions
4-
^EXIT=10$
4+
^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$
5+
^Invariant check failed$
6+
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7+
^Reason: Recursive functions found during inlining$
8+
^EXIT=(127|134|137)$
59
^SIGNAL=0$
6-
^file main.c line \d+ function f2: recursion is ignored on call to \'f2\'$
7-
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
8-
^\[f2.\d+\] line \d+ Check that loc is assignable: SUCCESS$
9-
^VERIFICATION FAILED$
1010
--
1111
--
12-
Verification:
13-
function | pre-cond | post-cond
14-
---------|----------|----------
15-
f2 | assumed | asserted
16-
17-
Test should fail:
18-
The postcondition of f2 is incorrect, considering the recursion particularity.
19-
20-
Recursion:
21-
The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions).
12+
Test should fail because a recursive function is found during inlining.

‎regression/contracts/function-calls-04-1/test-enf-f1.desc

Lines changed: 6 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,12 @@
11
CORE
22
main.c
33
--enforce-contract f1 _ --unwind 20 --unwinding-assertions
4-
^EXIT=10$
4+
^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
5+
^Invariant check failed$
6+
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7+
^Reason: Recursive functions found during inlining$
8+
^EXIT=(127|134|137)$
59
^SIGNAL=0$
6-
^file main.c line \d+ function f2\_in: recursion is ignored on call to \'f2\_out\'$
7-
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
8-
^VERIFICATION FAILED$
910
--
1011
--
11-
Verification:
12-
function | pre-cond | post-cond
13-
---------|----------|----------
14-
f1 | assumed | asserted
15-
16-
Test should fail:
17-
The postcondition of f2_out is incorrect, considering the recursion particularity.
18-
19-
Recursion:
20-
The base case for the recursive call to f2_out provides different behavior
21-
than the general case (given the pre-conditions).
12+
Test should fail because a recursive function is found during inlining.

‎regression/contracts/function-calls-04-1/test-enf-f2_in.desc

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,12 @@
11
CORE
22
main.c
33
--enforce-contract f2_in _ --unwind 20 --unwinding-assertions
4-
^EXIT=10$
4+
^file main\.c line 13 function f2_out: recursion is ignored on call to 'f2_in'$
5+
^Invariant check failed$
6+
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7+
^Reason: Recursive functions found during inlining$
8+
^EXIT=(127|134|137)$
59
^SIGNAL=0$
6-
^file main.c line \d+ function f2\_out: recursion is ignored on call to \'f2\_in\'$
7-
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
8-
^\[f2\_out.\d+\] line \d+ Check that loc2 is assignable: SUCCESS$
9-
^VERIFICATION FAILED$
1010
--
1111
--
12-
Verification:
13-
function | pre-cond | post-cond
14-
---------|----------|----------
15-
f2_in | assumed | asserted
16-
17-
Test should fail:
18-
The postcondition of f2_out is incorrect, considering the recursion particularity.
19-
20-
Recursion:
21-
The base case for the recursive call to f2_out provides different behavior
22-
than the general case (given the pre-conditions).
12+
Test should fail because a recursive function is found during inlining.

‎regression/contracts/function-calls-04-1/test-enf-f2_out.desc

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,12 @@
11
CORE
22
main.c
33
--enforce-contract f2_out _ --unwind 20 --unwinding-assertions
4-
^EXIT=10$
4+
^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
5+
^Invariant check failed$
6+
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7+
^Reason: Recursive functions found during inlining$
8+
^EXIT=(127|134|137)$
59
^SIGNAL=0$
6-
^file main.c line \d+ function f2\_in: recursion is ignored on call to \'f2\_out\'$
7-
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
8-
^\[f2\_out.\d+\] line \d+ Check that loc2 is assignable: SUCCESS$
9-
^VERIFICATION FAILED$
1010
--
1111
--
12-
Verification:
13-
function | pre-cond | post-cond
14-
---------|----------|----------
15-
f2_out | assumed | asserted
16-
17-
Test should fail:
18-
The postcondition of f2 is incorrect, considering the recursion particularity.
19-
20-
Recursion:
21-
The base case for the recursive call to f2_out provides different behavior
22-
than the general case (given the pre-conditions).
12+
Test should fail because a recursive function is found during inlining.

‎regression/contracts/function-calls-recursive-01/main.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <stdlib.h>
2+
3+
int sum_rec(int i, int acc)
4+
{
5+
if(i >= 0)
6+
return sum_rec(i - 1, acc + i);
7+
return acc;
8+
}
9+
10+
int sum(int i) __CPROVER_requires(0 <= i && i <= 50)
11+
__CPROVER_ensures(__CPROVER_return_value >= 0) __CPROVER_assigns()
12+
{
13+
int j = i;
14+
int res = sum_rec(j, 0);
15+
return res;
16+
}
17+
18+
int main()
19+
{
20+
int result = sum(10);
21+
__CPROVER_assert(result == 55, "result == 55");
22+
return 0;
23+
}

‎regression/contracts/function-calls-recursive-01/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-contract sum _ --trace
4+
^file main\.c line 6 function sum_rec: recursion is ignored on call to 'sum_rec'$
5+
^Invariant check failed$
6+
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7+
^Reason: Recursive functions found during inlining$
8+
^EXIT=(127|134|137)$
9+
^SIGNAL=0$
10+
--
11+
--
12+
Test should fail because a recursive function is found during inlining.

0 commit comments

Comments
 (0)