We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 93d9ce8 commit 5f0bb03Copy full SHA for 5f0bb03
regression/cbmc-cover/assume_assert2/assume_assert.c
@@ -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
+}
regression/cbmc-cover/assume_assert2/test.desc
@@ -0,0 +1,9 @@
+CORE
+assume_assert.c
+--cover assume
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file assume_assert.c line \d+ function main assert\(false\) before assume\(a >= 0\): SATISFIED$
+^\[main.coverage.2\] file assume_assert.c line \d+ function main assert\(false\) after assume\(a >= 0\): FAILED$
+--
+^warning: ignoring
0 commit comments