Skip to content

Commit 01444b7

Browse files
author
Aren Babikian
committed
Assesses PR comments and adds handling for loop unwinding
1 parent 7166cd5 commit 01444b7

File tree

18 files changed

+117
-45
lines changed

18 files changed

+117
-45
lines changed

‎regression/contracts/chain.sh

Lines changed: 11 additions & 3 deletions
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/test-enf.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,7 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the postconditions.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,7 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | asserted | assumed

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

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,11 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the postconditions of both f1 and f2.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
1014

1115
Known bug:
1216
Enforce flag not handled correctly for function calls within functions.
13-
This bug is fixed in PR #5538.

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,8 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,10 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f1 (called from main).
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/test-enf.desc

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,11 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the postconditions of both f1 and f2.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
1014

1115
Known bug:
1216
Enforce flag not handled correctly for function calls within functions.
13-
This bug is fixed in PR #5538.

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,8 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,10 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f1 (called from main).
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/test-enf.desc

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,19 @@
1-
KNOWNBUG
1+
CORE
22
main.c
3-
--enforce-all-contracts
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
--
88
--
9-
This confirms the accuracy of the postconditions of both f1 and f2.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
1014

1115
Test should fail:
1216
The postcondition of f2 is incorrect, considering the recursion particularity.
1317

1418
Recursion:
1519
The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions).
16-
17-
Known bug 2:
18-
This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
11
KNOWNBUG
22
main.c
3-
--enforce-all-contracts
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the postconditions of both f1 and f2.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | assumed | asserted
1014

1115
Recursion:
1216
The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
1317

14-
Known bug 1:
18+
Known bug:
1519
Enforce flag not handled correctly for function calls within functions.
16-
This bug is fixed in PR #5538.
17-
18-
Known bug 2:
19-
This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,11 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2 | asserted | assumed
1014

1115
Recursion:
1216
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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,13 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f1 (called from main).
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.
1016

1117
Recursion:
1218
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/test-enf.desc

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,20 @@
1-
KNOWNBUG
1+
CORE
22
main.c
3-
--enforce-all-contracts
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
--
88
--
9-
This confirms the accuracy of the postconditions of f1, f2_out and f2_in.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2_out | assumed | asserted
14+
f2_in | assumed | asserted
1015

1116
Test should fail:
1217
The postcondition of f2 is incorrect, considering the recursion particularity.
1318

1419
Recursion:
1520
The base case for the recursive call to f2 provides different behavior than the general case (given the pre-conditions).
16-
17-
Known bug:
18-
This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.

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

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,20 @@
11
KNOWNBUG
22
main.c
3-
--enforce-all-contracts
3+
--enforce-all-contracts _ --unwind 20 --unwinding-assertions
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the postconditions of f1, f2_out and f2_in.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2_out | assumed | asserted
14+
f2_in | assumed | asserted
1015

1116
Recursion:
1217
The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
1318

14-
Known bug 1:
19+
Known bug:
1520
Enforce flag not handled correctly for function calls within functions.
16-
This bug is fixed in PR #5538.
17-
18-
Known bug 2:
19-
This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,14 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f2_out (called from f1) and of the postconditions of f1.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2_out | asserted | assumed
14+
f2_in | n/a | n/a
15+
16+
Note: the calls to f2_in does not occur because the call to f2_out is replaced by its contracts.
1017

1118
Recursion:
1219
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/test-mix-2.desc

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,12 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f2_in (called from f2_out) and of the postconditions of f1 and of f2_out.
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | assumed | asserted
13+
f2_out | assumed | asserted
14+
f2_in | asserted | assumed
1015

1116
Recursion
1217
(1) This test checks the mutualy recursive f2_out and f2-in functions by enforcing f2_out and replacing the internal f2_in call with its contract.
@@ -15,4 +20,3 @@ Recursion
1520

1621
Known bug:
1722
Enforce flag not handled correctly for function calls within functions.
18-
This bug is fixed in PR #5538.

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,14 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
--
9-
This confirms the accuracy of the preconditions of f1 (called from main).
9+
Verification:
10+
function | pre-cond | post-cond
11+
---------|----------|----------
12+
f1 | asserted | assumed
13+
f2_out | n/a | n/a
14+
f2_in | n/a | n/a
15+
16+
Note: the calls to f2_out and to f2_in do not occur because the call to f1 is replaced by its contracts.
1017

1118
Recursion:
1219
The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

0 commit comments

Comments
 (0)