Skip to content

Commit

Permalink
Add tests of the affect of assumptions on coverage blocks
Browse files Browse the repository at this point in the history
  • Loading branch information
thomasspriggs committed Oct 10, 2023
1 parent f7d9e49 commit f6b4cbf
Show file tree
Hide file tree
Showing 4 changed files with 52 additions and 0 deletions.
9 changes: 9 additions & 0 deletions regression/cbmc-cover/location-assume/end.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#include <assert.h>

void main()
{
int i;
int *p = &i;
int j;
__CPROVER_assume(j == 1 / (*p));
}
17 changes: 17 additions & 0 deletions regression/cbmc-cover/location-assume/end.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
CORE
end.c
--pointer-check --div-by-zero-check --cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file end.c line 5 function main block 1 \(lines end\.c:main:5-8\): SATISFIED$
^\[main.coverage.2\] file end.c line 8 function main block 2 \(lines end\.c:main:8\): SATISFIED$
^\[main.coverage.3\] file end.c line 8 function main block 3 \(lines end\.c:main:8\): SATISFIED$
^\[main.coverage.4\] file end.c line 8 function main block 4 \(lines end\.c:main:8\): SATISFIED$
^\[main.coverage.5\] file end.c line 9 function main block 5 \(lines end\.c:main:9\): SATISFIED$
^\*\* 5 of 5 covered \(100.0%\)
--
^warning: ignoring
--
Test that in the case where multiple assertions are added on the same line of
code due to the addition of instrumentation checks, these do not result in
further splitting blocks.
11 changes: 11 additions & 0 deletions regression/cbmc-cover/location-assume/middle.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#include <assert.h>

int main()
{
int i;
int j;
j = i;
__CPROVER_assume(0);
j = i + 2;
return 0;
}
15 changes: 15 additions & 0 deletions regression/cbmc-cover/location-assume/middle.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
CORE
middle.c
--cover location
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file middle.c line 5 function main block 1 \(lines middle\.c:main:5-8\): SATISFIED$
^\[main.coverage.2\] file middle.c line 9 function main block 2 \(lines middle\.c:main:9-11\): FAILED$
^\*\* 1 of 2 covered \(50.0%\)
--
^warning: ignoring
--
This test confirms that assumptions in the middle of what would otherwise be a
single blocks without control flow will cause the code to be split into 2
coverage blocks. This is required as an unsatisfiable assumption can result in
the following statements being unreachable.

0 comments on commit f6b4cbf

Please sign in to comment.