We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
--cover assume
1 parent b7a0c20 commit 93d9ce8Copy full SHA for 93d9ce8
regression/cbmc-cover/assume_assert1/assume_assert.c
@@ -0,0 +1,9 @@
1
+#include <assert.h>
2
+
3
+int main()
4
+{
5
+ int x;
6
+ __CPROVER_assume(x > 0);
7
+ __CPROVER_assume(x < 0);
8
+ assert(0 == 1);
9
+}
regression/cbmc-cover/assume_assert1/test.desc
@@ -0,0 +1,11 @@
+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\(x > 0\): SATISFIED$
+^\[main.coverage.2\] file assume_assert.c line \d function main assert\(false\) after assume\(x > 0\): SATISFIED$
+^\[main.coverage.3\] file assume_assert.c line \d function main assert\(false\) before assume\(x < 0\): SATISFIED$
+^\[main.coverage.4\] file assume_assert.c line \d function main assert\(false\) after assume\(x < 0\): FAILED$
10
+--
11
+^warning: ignoring
0 commit comments