File: skip_first_unwind.desc

package info (click to toggle)
cbmc 5.12-5
  • links: PTS
  • area: main
  • in suites: bullseye
  • size: 92,512 kB
  • sloc: cpp: 301,761; ansic: 51,699; java: 27,534; python: 5,113; yacc: 4,756; makefile: 3,184; lex: 2,749; sh: 1,347; perl: 555; xml: 404; pascal: 203; ada: 36
file content (13 lines) | stat: -rw-r--r-- 474 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
 
CORE
main.c
--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
--
This test "correctly" succeeds because the second iteration of the loop is
unreachable due to the assumption which is violated after the first iteration.
This behaviour is intended and documented, i.e. using ignore-before-unwind
assumes that we know that iterations before unwind-min are correct.