Skip to content

Commit 011937c

Browse files
peterschrammelgiulio-garbi
authored andcommitted
Add test for --nondet-static-matching
1 parent 308e950 commit 011937c

File tree

2 files changed

+29
-0
lines changed

2 files changed

+29
-0
lines changed
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
3+
int do_nondet_init1;
4+
int init1;
5+
6+
int main(int argc, char **argv)
7+
{
8+
static int do_nondet_init2;
9+
static int init2;
10+
11+
assert(do_nondet_init1 == 0);
12+
assert(init1 == 0);
13+
assert(do_nondet_init2 == 0);
14+
assert(init2 == 0);
15+
16+
return 0;
17+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--nondet-static-matching '.*\.c:.*nondet.*'
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
assertion do_nondet_init1 == 0: FAILURE
8+
assertion init1 == 0: SUCCESS
9+
assertion do_nondet_init2 == 0: FAILURE
10+
assertion init2 == 0: SUCCESS
11+
--
12+
--

0 commit comments

Comments
 (0)