Skip to content

Commit c09dc87

Browse files
Petr BauchPetr Bauch
authored andcommitted
Add regression test to check the new user option
1 parent 2d2c18e commit c09dc87

File tree

2 files changed

+20
-0
lines changed

2 files changed

+20
-0
lines changed
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int x = 1;
2+
3+
int main()
4+
{
5+
assert(x == 1); //unreachable, hence success
6+
assert(x == 2);
7+
assert(x == 3);
8+
9+
return 0;
10+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-line 6 --havoc-variables x
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion x == 2: FAILURE
8+
\[main.assertion.3\] line [0-9]+ assertion x == 3: FAILURE
9+
--
10+
^warning: ignoring

0 commit comments

Comments
 (0)