Skip to content

Commit e99e11d

Browse files
committed
Retracing test simple goto
This adds one test file for the new --retrace feature.
1 parent 5719ed9 commit e99e11d

File tree

4 files changed

+36
-0
lines changed

4 files changed

+36
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
simple_goto.c
3+
--function foo --retrace 00
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
simple_goto.c
3+
--function foo --retrace 01
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
simple_goto.c
3+
--function foo --retrace 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
4+
void foo(bool arg1, bool arg2)
5+
{
6+
bool v1 = false;
7+
bool v2 = false;
8+
if(arg1)
9+
goto l1;
10+
v1 = true;
11+
l1:
12+
if(arg2)
13+
goto l2;
14+
v2 = true;
15+
l2:
16+
assert(v1);
17+
assert(v2);
18+
}

0 commit comments

Comments
 (0)