File tree Expand file tree Collapse file tree 2 files changed +20
-0
lines changed
regression/cbmc-cover/assume_assert1 Expand file tree Collapse file tree 2 files changed +20
-0
lines changed Original file line number Diff line number Diff line change
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
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ assume_assert.c
3
+ --cover assume
4
+ ^EXIT=0$
5
+ ^SIGNAL=0$
6
+ ^\[main.coverage.1\] file assume_assert.c line \d function main assert\(false\) before assume\(x > 0\): SATISFIED$
7
+ ^\[main.coverage.2\] file assume_assert.c line \d function main assert\(false\) after assume\(x > 0\): SATISFIED$
8
+ ^\[main.coverage.3\] file assume_assert.c line \d function main assert\(false\) before assume\(x < 0\): SATISFIED$
9
+ ^\[main.coverage.4\] file assume_assert.c line \d function main assert\(false\) after assume\(x < 0\): FAILED$
10
+ --
11
+ ^warning: ignoring
You can’t perform that action at this time.
0 commit comments