Skip to content

Commit c5cc454

Browse files
feliperodrifeliperodri
authored
Merge pull request #5911 from ArenBabikian/contracts-recursion-reg-tests
Adds code contracts regression tests that involve function calls
2 parents 2c7d136 + 01444b7 commit c5cc454

File tree

25 files changed

+454
-3
lines changed

25 files changed

+454
-3
lines changed

‎regression/contracts/chain.sh

+11-3
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,14 @@ name=${*:$#}
1111
name=${name%.c}
1212

1313
args=${*:5:$#-5}
14+
if [[ "$args" != *" _ "* ]]
15+
then
16+
args_inst=$args
17+
args_cbmc=""
18+
else
19+
args_inst="${args%%" _ "*}"
20+
args_cbmc="${args#*" _ "}"
21+
fi
1422

1523
if [[ "${is_windows}" == "true" ]]; then
1624
$goto_cc "${name}.c"
@@ -20,10 +28,10 @@ else
2028
fi
2129

2230
rm -f "${name}-mod.gb"
23-
$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
31+
$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
2432
if [ ! -e "${name}-mod.gb" ] ; then
2533
cp "$name.gb" "${name}-mod.gb"
26-
elif echo $args | grep -q -- "--dump-c" ; then
34+
elif echo $args_inst | grep -q -- "--dump-c" ; then
2735
mv "${name}-mod.gb" "${name}-mod.c"
2836

2937
if [[ "${is_windows}" == "true" ]]; then
@@ -36,4 +44,4 @@ elif echo $args | grep -q -- "--dump-c" ; then
3644
rm "${name}-mod.c"
3745
fi
3846
$goto_instrument --show-goto-functions "${name}-mod.gb"
39-
$cbmc "${name}-mod.gb"
47+
$cbmc "${name}-mod.gb" ${args_cbmc}

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

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
2+
__CPROVER_ensures(__CPROVER_return_value == *x1 + 1)
3+
{
4+
return *x1 + 1;
5+
}
6+
7+
int main()
8+
{
9+
int p;
10+
__CPROVER_assume(p > 1 && p < 10000);
11+
f1(&p);
12+
13+
return 0;
14+
}

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

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted

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

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
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+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | asserted | assumed

‎regression/contracts/function-calls-02-1/main.c

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
2+
__CPROVER_ensures(__CPROVER_return_value == *x1 + 3)
3+
{
4+
int loc = *x1 + 1;
5+
return f2(&loc) + 1;
6+
}
7+
8+
int f2(int *x2) __CPROVER_requires(*x2 > 2 && *x2 < 10001)
9+
__CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
10+
{
11+
return *x2 + 1;
12+
}
13+
14+
int main()
15+
{
16+
int p;
17+
__CPROVER_assume(p > 1 && p < 10000);
18+
f1(&p);
19+
20+
return 0;
21+
}

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

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
14+
15+
Known bug:
16+
Enforce flag not handled correctly for function calls within functions.

‎regression/contracts/function-calls-02-1/test-mix.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-contract f1 --replace-call-with-contract f2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | asserted | assumed

‎regression/contracts/function-calls-02-1/test-rep.desc

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
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+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | asserted | assumed
13+
f2 | n/a | n/a
14+
15+
Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.

‎regression/contracts/function-calls-02/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
2+
__CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
3+
{
4+
return f2(x1) + 1;
5+
}
6+
7+
int f2(int *x2) __CPROVER_requires(*x2 > 1 && *x2 < 10000)
8+
__CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
9+
{
10+
return *x2 + 1;
11+
}
12+
13+
int main()
14+
{
15+
int p;
16+
__CPROVER_assume(p > 1 && p < 10000);
17+
f1(&p);
18+
19+
return 0;
20+
}

‎regression/contracts/function-calls-02/test-enf.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
14+
15+
Known bug:
16+
Enforce flag not handled correctly for function calls within functions.

‎regression/contracts/function-calls-02/test-mix.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-contract f1 --replace-call-with-contract f2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | asserted | assumed

‎regression/contracts/function-calls-02/test-rep.desc

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
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+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | asserted | assumed
13+
f2 | n/a | n/a
14+
15+
Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.

‎regression/contracts/function-calls-03-1/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
2+
__CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
3+
{
4+
return f2(x1) + 1;
5+
}
6+
7+
int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
8+
__CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
9+
{
10+
if(*x2 < 1)
11+
return -1; //Notice the change for the base case
12+
int loc = *x2 - 1;
13+
return f2(&loc) + 1;
14+
}
15+
16+
int main()
17+
{
18+
int p;
19+
__CPROVER_assume(p > 0 && p < 20);
20+
f1(&p);
21+
22+
return 0;
23+
}

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

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
14+
15+
Test should fail:
16+
The postcondition of f2 is incorrect, considering the recursion particularity.
17+
18+
Recursion:
19+
The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions).

‎regression/contracts/function-calls-03/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
2+
__CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
3+
{
4+
return f2(x1) + 1;
5+
}
6+
7+
int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
8+
__CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
9+
{
10+
if(*x2 < 1)
11+
return 1;
12+
int loc = *x2 - 1;
13+
return f2(&loc) + 1;
14+
}
15+
16+
int main()
17+
{
18+
int p;
19+
__CPROVER_assume(p > 0 && p < 20);
20+
f1(&p);
21+
22+
return 0;
23+
}

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

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
14+
15+
Recursion:
16+
The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
17+
18+
Known bug:
19+
Enforce flag not handled correctly for function calls within functions.

‎regression/contracts/function-calls-03/test-mix.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--enforce-contract f1 --replace-call-with-contract f2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | asserted | assumed
14+
15+
Recursion:
16+
The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

‎regression/contracts/function-calls-03/test-rep.desc

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
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+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | asserted | assumed
13+
f2 | n/a | n/a
14+
15+
Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.
16+
17+
Recursion:
18+
The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

‎regression/contracts/function-calls-04-1/main.c

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
2+
__CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
3+
{
4+
return f2_out(x1) + 1;
5+
}
6+
7+
int f2_out(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
8+
__CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
9+
{
10+
if(*x2 < 1)
11+
return -1; //Notice the change for the base case
12+
int loc2 = *x2 - 1;
13+
return f2_in(&loc2) + 1;
14+
}
15+
16+
int f2_in(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 19)
17+
__CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
18+
{
19+
return f2_out(x2);
20+
}
21+
22+
int main()
23+
{
24+
int p;
25+
__CPROVER_assume(p > 0 && p < 20);
26+
f1(&p);
27+
28+
return 0;
29+
}

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

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2_out | assumed | asserted
14+
f2_in | 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 general case (given the pre-conditions).

0 commit comments

Comments
 (0)