Skip to content

Commit 2f78caf

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

File tree

4 files changed

+33
-0
lines changed

4 files changed

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

0 commit comments

Comments
 (0)