Skip to content

Commit 978abb8

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

File tree

4 files changed

+34
-0
lines changed

4 files changed

+34
-0
lines changed
Lines changed: 6 additions & 0 deletions
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$
Lines changed: 6 additions & 0 deletions
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$
Lines changed: 6 additions & 0 deletions
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$
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <stdbool.h>
2+
#include <assert.h>
3+
4+
void foo(bool arg1, bool arg2)
5+
{
6+
bool v1 = false;
7+
bool v2 = false;
8+
if(arg1) goto l1;
9+
v1 = true;
10+
l1:
11+
if(arg2) goto l2;
12+
v2 = true;
13+
l2:
14+
assert(v1);
15+
assert(v2);
16+
}

0 commit comments

Comments
 (0)