Skip to content

Commit 252b50d

Browse files
committed
Add second test case that features assume statement hidden behind
branch.
1 parent 1df78f4 commit 252b50d

File tree

2 files changed

+29
-0
lines changed

2 files changed

+29
-0
lines changed
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
int a;
6+
7+
if(a > 0)
8+
{
9+
assert(a > 0);
10+
}
11+
else if(a < 0)
12+
{
13+
__CPROVER_assume(a >= 0);
14+
assert(a < 0);
15+
}
16+
else
17+
{
18+
assert(a == 0);
19+
}
20+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
assume_assert.c
3+
--cover assume
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.1\] file assume_assert.c line 10 function main assert\(false\) before assume\(a >= 0\): SATISFIED$
7+
^\[main.2\] file assume_assert.c line 10 function main assert\(false\) after assume\(a >= 0\): FAILED$
8+
--
9+
^warning: ignoring

0 commit comments

Comments
 (0)