Skip to content

Commit eeddb3f

Browse files
tautschnigtautschnig
authored
Merge pull request #6509 from remi-delmas-3000/dont-trust-inferred-loop-assigns-clauses
Check inferred loop assigns clauses instead of blindly trusting them
2 parents e783d13 + ef52bb9 commit eeddb3f

File tree

44 files changed

+270
-161
lines changed

Some content is hidden

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

44 files changed

+270
-161
lines changed

‎regression/contracts/github_6168_infinite_unwinding_bug/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
7-
^\[main.1\] line \d+ Check loop invariant before entry: SUCCESS$
8-
^\[main.2\] line \d+ Check that loop invariant is preserved: SUCCESS$
7+
^\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
8+
^\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
99
--
1010
--
1111
This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168.

‎regression/contracts/invar_check_break_fail/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ main.c
33
--apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion r == 0: FAILURE$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
9+
^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
910
^VERIFICATION FAILED$
1011
--
1112
This test is expected to fail along the code path where r is an even integer

‎regression/contracts/invar_check_break_pass/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ main.c
33
--apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion r == 0 || r == 1: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
9+
^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
910
^VERIFICATION SUCCESSFUL$
1011
--
1112
This test checks that conditionals and `break` are correctly handled.

‎regression/contracts/invar_check_continue/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ main.c
33
--apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
9+
^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
910
^VERIFICATION SUCCESSFUL$
1011
--
1112
This test checks that conditionals and `continue` are correctly handled.

‎regression/contracts/invar_check_multiple_loops/test.desc

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,17 @@ main.c
33
--apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
9-
^\[main.4\] .* Check loop invariant before entry: SUCCESS$
10-
^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
11-
^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
12-
^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
9+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
10+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
11+
^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
12+
^\[main\.assertion\.\d+\] .* assertion x == y \+ 2 \* n: SUCCESS$
13+
^\[main\.\d+\] line 8 Check that r is assignable: SUCCESS$
14+
^\[main\.\d+\] line 15 Check that x is assignable: SUCCESS$
15+
^\[main\.\d+\] line 23 Check that y is assignable: SUCCESS$
16+
^\[main\.\d+\] line 24 Check that r is assignable: SUCCESS$
1317
^VERIFICATION SUCCESSFUL$
1418
--
1519
This test checks that multiple loops and `for` loops are correctly handled.

‎regression/contracts/invar_check_nested_loops/test.desc

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,16 @@ main.c
33
--apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
9-
^\[main.2\] .* Check loop invariant before entry: SUCCESS$
10-
^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$
11-
^\[main.4\] .* Check decreases clause on loop iteration: SUCCESS$
12-
^\[main.assertion.1\] .* assertion s == n: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
9+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
10+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
11+
^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
12+
^\[main\.\d+] line 23 Check that s is assignable: SUCCESS$
13+
^\[main\.\d+] line 24 Check that a is assignable: SUCCESS$
14+
^\[main\.\d+] line 27 Check that s is assignable: SUCCESS$
15+
^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$
1316
^VERIFICATION SUCCESSFUL$
1417
--
1518
This test checks that nested loops, `for` loops,

‎regression/contracts/invar_check_pointer_modifies-01/test.desc

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,11 @@ main.c
33
--apply-loop-contracts --pointer-check
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion \*data = 42: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+] .* Check that \*data is assignable: SUCCESS$
9+
^\[main\.\d+] .* Check that i is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion \*data = 42: SUCCESS$
911
^VERIFICATION SUCCESSFUL$
1012
--
1113
^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE

‎regression/contracts/invar_check_pointer_modifies-02/test.desc

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,12 @@ main.c
33
--apply-loop-contracts --pointer-check
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion data == copy: SUCCESS$
9-
^\[main.assertion.2\] .* assertion \*copy = 42: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check that \*data is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion data == copy: SUCCESS$
11+
^\[main\.assertion\.\d+\] .* assertion \*copy = 42: SUCCESS$
1012
^VERIFICATION SUCCESSFUL$
1113
--
1214
^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE

‎regression/contracts/invar_check_sufficiency/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ main.c
33
--apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
8-
^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
9+
^\[main\.assertion\.1\] .* assertion r == 0: SUCCESS$
910
^VERIFICATION SUCCESSFUL$
1011
--
1112
This test checks that a loop invariant can be proven to be inductive,

‎regression/contracts/invar_dynamic_struct_member/test.desc

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,11 @@ main.c
33
--apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
9+
^\[main\.\d+\] line 22 Check that t->x is assignable: SUCCESS$
10+
^\[main\.\d+\] line 25 Check that t->x is assignable: SUCCESS$
811
^\[main.assertion.1\] .* assertion .*: FAILURE$
912
^VERIFICATION FAILED$
1013
--

0 commit comments

Comments
 (0)