File tree Expand file tree Collapse file tree 3 files changed +33
-0
lines changed
regression/cbmc/xml-interface1 Expand file tree Collapse file tree 3 files changed +33
-0
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+
3
+ void foo (int x )
4
+ {
5
+ for (int i = 0 ; i < 5 ; ++ i )
6
+ {
7
+ if (x )
8
+ assert (0 );
9
+ assert (0 );
10
+ }
11
+ assert (0 );
12
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ --xml-interface
3
+ < test.xml
4
+ ^EXIT=10$
5
+ ^SIGNAL=0$
6
+ Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
7
+ <result property="foo\.assertion\.3" status="SUCCESS"/>
8
+ <result property="foo\.assertion\.1" status="FAILURE">
9
+ <goto_trace>
10
+ VERIFICATION FAILED
11
+ --
12
+ <result property="foo\.assertion\.2" status=
Original file line number Diff line number Diff line change
1
+ <options >
2
+ <valueOption actual =" main.c" />
3
+ <valueOption name =" function" actual =" foo" />
4
+ <valueOption name =" unwind" actual =" 3" />
5
+ <valueOption name =" property" actual =" foo.assertion.1" />
6
+ <valueOption name =" property" actual =" foo.assertion.3" />
7
+ <flagOption name =" trace" actual =" on" />
8
+ <flagOption name =" show-properties" actual =" off" />
9
+ </options >
You can’t perform that action at this time.
0 commit comments