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
--

‎regression/contracts/invar_havoc_dynamic_array/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,10 @@ void main()
99
data[5] = 0;
1010

1111
for(unsigned i = 0; i < SIZE; i++)
12+
// clang-format off
13+
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
1214
__CPROVER_loop_invariant(i <= SIZE)
15+
// clang-format on
1316
{
1417
data[i] = 1;
1518
}

‎regression/contracts/invar_havoc_dynamic_array/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
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 data\[5\] == 0: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[5\] == 1: 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 i is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
11+
^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
1012
^VERIFICATION FAILED$
1113
--
1214
--

‎regression/contracts/invar_havoc_dynamic_array_const_idx/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
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 data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[4\] == 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 i is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
11+
^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$
1012
^VERIFICATION FAILED$
1113
--
1214
--

‎regression/contracts/invar_havoc_static_array/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,10 @@ void main()
99
data[5] = 0;
1010

1111
for(unsigned i = 0; i < SIZE; i++)
12+
// clang-format off
13+
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
1214
__CPROVER_loop_invariant(i <= SIZE)
15+
// clang-format on
1316
{
1417
data[i] = 1;
1518
}

‎regression/contracts/invar_havoc_static_array/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
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 data\[5\] == 0: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[5\] == 1: 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 i is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
11+
^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
1012
^VERIFICATION FAILED$
1113
--
1214
--

‎regression/contracts/invar_havoc_static_array_const_idx/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
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 data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[4\] == 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 i is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
11+
^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$
1012
^VERIFICATION FAILED$
1113
--
1214
--

‎regression/contracts/invar_havoc_static_multi-dim_array/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +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 __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$
9-
^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.assertion\.\d+\] .* assertion __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$
9+
^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
1010
^VERIFICATION FAILED$
1111
--
1212
--

‎regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +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$
8-
^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 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 data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
9+
^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
10+
^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
1011
^VERIFICATION FAILED$
1112
--
1213
--

‎regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ void main()
1111
data[4][5][6] = 0;
1212

1313
for(unsigned i = 0; i < SIZE; i++)
14-
__CPROVER_loop_invariant(i <= SIZE)
14+
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
15+
__CPROVER_loop_invariant(i <= SIZE)
1516
{
1617
data[4][i][6] = 1;
1718
}

‎regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/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
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 data\[1\]\[2\]\[3\] == 0: FAILURE$
9-
^\[main.assertion.2\] .* assertion data\[4\]\[5\]\[6\] == 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 i is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
11+
^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
1012
^VERIFICATION FAILED$
1113
--
1214
--

‎regression/contracts/invar_loop-entry_check/test.desc

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,24 @@ main.c
33
--apply-loop-contracts _ --pointer-primitive-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 \*x1 == z1: SUCCESS$
9-
^\[main.3\] .* Check loop invariant before entry: SUCCESS$
10-
^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
11-
^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
12-
^\[main.5\] .* Check loop invariant before entry: SUCCESS$
13-
^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
14-
^\[main.assertion.3\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
8+
^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
9+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
10+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
11+
^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
12+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
13+
^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
14+
^\[main\.\d+\] .* Check that y1 is assignable: SUCCESS$
15+
^\[main\.\d+\] line 18 Check that \*x1 is assignable: SUCCESS$
16+
^\[main\.\d+\] line 19 Check that \*x1 is assignable: SUCCESS$
17+
^\[main\.\d+\] .* Check that y2 is assignable: SUCCESS$
18+
^\[main\.\d+\] line 30 Check that x2 is assignable: SUCCESS$
19+
^\[main\.\d+\] line 31 Check that x2 is assignable: SUCCESS$
20+
^\[main\.\d+\] .* Check that y3 is assignable: SUCCESS$
21+
^\[main\.\d+\] .* Check that s0\.n is assignable: SUCCESS$
22+
^\[main\.\d+\] .* Check that s2->n is assignable: SUCCESS$
23+
^\[main\.assertion\.\d+\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
1524
^VERIFICATION SUCCESSFUL$
1625
--
1726
--

‎regression/contracts/invar_loop-entry_fail/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|6)$
55
^SIGNAL=0$
6-
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
7-
^\[main.2\] .* Check that loop invariant is preserved: FAILURE$
6+
^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main\.\d+\] .* Check that loop invariant is preserved: FAILURE$
8+
^\[main\.\d+\] line 11 Check that y is assignable: SUCCESS$
9+
^\[main\.\d+\] line 12 Check that x is assignable: SUCCESS$
10+
^\[main\.\d+\] line 13 Check that x is assignable: SUCCESS$
811
^VERIFICATION FAILED$
912
--
1013
--

‎regression/contracts/invar_loop_constant_fail/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
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: SUCCESS$
9-
^\[main.assertion.2\] .* assertion s == 1: 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 s is assignable: SUCCESS$
9+
^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
11+
^\[main\.assertion\.\d+\] .* assertion s == 1: FAILURE$
1012
^VERIFICATION FAILED$
1113
--
1214
This test is expected to fail because it modifies a variable within a loop,

‎regression/contracts/invar_loop_constant_no_modify/test.desc

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,11 @@ 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$
9-
^\[main.assertion.2\] .* assertion s == 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: SUCCESS$
10+
^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$
1011
^VERIFICATION SUCCESSFUL$
1112
--
1213
This test checks that variables that are not modified within the loop

0 commit comments

Comments
 (0)