Skip to content

Commit 320da32

Browse files
author
Thomas Kiley
committed
Add tests verifying the incremental status is output
1 parent 03ab5c7 commit 320da32

File tree

3 files changed

+8
-0
lines changed

3 files changed

+8
-0
lines changed

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,6 @@ main.c
55
^SIGNAL=0$
66
"messageText": "VERIFICATION FAILED"
77
"currentUnwinding": 1
8+
"incrementalStatus": "INCONCLUSIVE"
89
--
910
^warning: ignoring

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,6 @@ main.c
66
<text>VERIFICATION FAILED</text>
77
<current-unwinding>1</current-unwinding>
88
<refinement-iteration>1</refinement-iteration>
9+
<incremental-status>INCONCLUSIVE</incremental-status>
910
--
1011
^warning: ignoring
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,15 @@
11
CORE
22
main.c
33
--incremental-loop main.0 --unwind-min 5 --unwind-max 10
4+
activate-multi-line-match
45
Current unwinding: 1
6+
Incremental status: INCONCLUSIVE
7+
Current unwinding: 5\nUnwinding .*\nIncremental status: INCONCLUSIVE
8+
Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE
59
^EXIT=10$
610
^SIGNAL=0$
711
^VERIFICATION FAILED$
812
--
913
^warning: ignoring
14+
--
15+
The multi-line match is added to verify that an incremental status is printed immediately after each unwinding

0 commit comments

Comments
 (0)