Skip to content

Commit 0e6cfbf

Browse files
author
Thomas Kiley
committed
Adapt tests for printing
We now print after all solving, and the last thing before the next increment, therefore the printing checks are easier to check immediately precedes the next unwinding, rather than checking appears after the increment we are talking about.
1 parent fdbbf7e commit 0e6cfbf

File tree

4 files changed

+10
-10
lines changed

4 files changed

+10
-10
lines changed
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
CORE
22
main.c
33
--incremental-loop main.0 --unwind-max 15
4+
activate-multi-line-match
45
^EXIT=0$
56
^SIGNAL=0$
67
^VERIFICATION SUCCESSFUL$
8+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 15
79
--
810
^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ main.c
44
activate-multi-line-match
55
Current unwinding: 1
66
Incremental status: INCONCLUSIVE
7-
Current unwinding: 5\nUnwinding .*\nIncremental status: INCONCLUSIVE
8-
Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE
7+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
8+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 7
99
^EXIT=10$
1010
^SIGNAL=0$
1111
^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,9 @@ CORE
22
test.c
33
--incremental-loop main.0 --no-propagation
44
activate-multi-line-match
5-
Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE
6-
Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE
7-
Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE
8-
Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE
5+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
6+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
7+
Incremental status: FAILURE\nCurrent unwinding: 7
98
^EXIT=10$
109
^SIGNAL=0$
1110
^VERIFICATION FAILED$

regression/cbmc-incr-oneloop/multiple-asserts/test.desc

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,9 @@ CORE
22
test.c
33
--incremental-loop main.0
44
activate-multi-line-match
5-
Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE
6-
Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE
7-
Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE
8-
Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE
5+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
6+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
7+
Incremental status: FAILURE\nCurrent unwinding: 7
98
^EXIT=10$
109
^SIGNAL=0$
1110
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)