Skip to content

Commit 75cf803

Browse files
author
Thomas Kiley
committed
Update min-unwind tests for behaviour of different unwind values
It is agreed that if --unwind N can find an error, that unwind-min N should find the same error. That is, we start checking immediately after doing N unwinds, rather than after doing N increments of the incremental unwinding (i.e. unwind + solve)
1 parent 9795351 commit 75cf803

File tree

3 files changed

+25
-1
lines changed

3 files changed

+25
-1
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 0
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.\d+\] line \d+ property: FAILURE$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring
10+
--
11+
This test correctly fails because the first iteration of the loop violates the
12+
property.
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.\d+\] line \d+ property: FAILURE$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring
10+
--
11+
This test correctly fails because the first iteration of the loop violates the
12+
property.

regression/cbmc-incr-oneloop/ignore-before-unwind/skip_first_unwind.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1
3+
--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 2
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)