Skip to content

Commit 3f6f0ca

Browse files
author
Thomas Kiley
committed
Add tests for when the program verifies
In this case, the status is inconclusive until completion, at which point success will be reported by CBMC overall.
1 parent 0e6cfbf commit 3f6f0ca

File tree

2 files changed

+24
-0
lines changed

2 files changed

+24
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
for(int i = 0; i < 10; ++i)
4+
{
5+
assert(i != 10);
6+
}
7+
return 0;
8+
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--incremental-loop main.0
4+
activate-multi-line-match
5+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
6+
Incremental status: INCONCLUSIVE\nCurrent unwinding: 10
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
^VERIFICATION SUCCESSFUL$
10+
--
11+
^warning: ignoring
12+
Incremental status: SUCCESS
13+
--
14+
Check that for valid asserts, the incremental status is inconclusive
15+
as it is only after the incrementer has been stopped we conclude is
16+
verified.

0 commit comments

Comments
 (0)