diff --git a/regression/cbmc-cover/location-assume/end.c b/regression/cbmc-cover/location-assume/end.c new file mode 100644 index 00000000000..0429196a1a1 --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.c @@ -0,0 +1,9 @@ +#include + +void main() +{ + int i; + int *p = &i; + int j; + __CPROVER_assume(j == 1 / (*p)); +} diff --git a/regression/cbmc-cover/location-assume/end.desc b/regression/cbmc-cover/location-assume/end.desc new file mode 100644 index 00000000000..b89e0ead3be --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.desc @@ -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. diff --git a/regression/cbmc-cover/location-assume/middle.c b/regression/cbmc-cover/location-assume/middle.c new file mode 100644 index 00000000000..64da9f6a25d --- /dev/null +++ b/regression/cbmc-cover/location-assume/middle.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + int i; + int j; + j = i; + __CPROVER_assume(0); + j = i + 2; + return 0; +} diff --git a/regression/cbmc-cover/location-assume/middle.desc b/regression/cbmc-cover/location-assume/middle.desc new file mode 100644 index 00000000000..650c62b33b1 --- /dev/null +++ b/regression/cbmc-cover/location-assume/middle.desc @@ -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. diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc index bac822b042c..6cc5084011f 100644 --- a/regression/cbmc-cover/location12/test.desc +++ b/regression/cbmc-cover/location12/test.desc @@ -7,7 +7,8 @@ main.c ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$ ^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$ -^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$ -^\*\* 4 of 5 covered \(80.0%\) +^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: FAILED$ +^\[foo.coverage.4\] file main.c line 5 function foo block 4.*: SATISFIED$ +^\*\* 4 of 6 covered \(66.7%\) -- ^warning: ignoring diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc index b48161384c3..90cf7a9f26d 100644 --- a/regression/cbmc-cover/location15/test.desc +++ b/regression/cbmc-cover/location15/test.desc @@ -6,7 +6,8 @@ main.c ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$ ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$ -^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 14 function main block 4.*: FAILED$ +^\[main.coverage.5\] file main.c line 16 function main block 5.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$ ^\*\* 3 of \d+ covered -- diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc index 74d7080448c..40e65248f26 100644 --- a/regression/cbmc-cover/location16/test.desc +++ b/regression/cbmc-cover/location16/test.desc @@ -9,7 +9,8 @@ main.c ^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$ ^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$ ^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$ -^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$ -^\*\* 4 of 7 covered \(57.1%\) +^\[func.coverage.5\] file main.c line 14 function func block 5.*: FAILED$ +^\[func.coverage.6\] file main.c line 15 function func block 6.*: SATISFIED$ +^\*\* 4 of 8 covered \(50.0%\) -- ^warning: ignoring diff --git a/regression/cbmc-cover/location2/test.desc b/regression/cbmc-cover/location2/test.desc index 747ff0c5800..817de5431b9 100644 --- a/regression/cbmc-cover/location2/test.desc +++ b/regression/cbmc-cover/location2/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main.coverage.1\] file main.c line 9 function main block 1 \(lines main.c:main:9,10\): SATISFIED$ -^\[main.coverage.2\] file main.c line 11 function main block 2 \(lines main.c:main:11\): SATISFIED$ -^\*\* 2 of 2 covered \(100.0%\) +^\[main.coverage.3\] file main.c line 11 function main block 3 \(lines main.c:main:11\): SATISFIED$ +^\*\* 3 of 3 covered \(100.0%\) -- ^warning: ignoring main.c::5 diff --git a/regression/cbmc-cover/simple_assert/test.desc b/regression/cbmc-cover/simple_assert/test.desc index d3fac6c4c46..dfdc0dee6f9 100644 --- a/regression/cbmc-cover/simple_assert/test.desc +++ b/regression/cbmc-cover/simple_assert/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$ -(1 of 1|3 of 3) covered \(100\.0%\)$ +(1 of 1|2 of 2|3 of 3) covered \(100\.0%\)$ -- ^warning: ignoring ^CONVERSION ERROR$ diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 0544dcdb715..1d0b8b404bc 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,9 +1,15 @@ CORE paths-lifo-expected-failure test.c --cover location --pointer-check --malloc-may-fail --malloc-fail-null -\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED -\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED -\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED +\[main\.coverage\.10\] file test\.c line \d+ function main block 10 \(lines test\.c:main:17,18\): SATISFIED +\[main\.coverage\.9\] file test\.c line \d+ function main block 9 \(lines test\.c:main:15\): FAILED +\[main\.coverage\.8\] file test\.c line \d+ function main block 8 \(lines test\.c:main:12,14\): SATISFIED +\[main\.coverage\.7\] file test\.c line \d+ function main block 7 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.6\] file test\.c line \d+ function main block 6 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12\): SATISFIED \[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 81ff18b6b11..466dddfe813 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -73,10 +73,11 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) } next_is_target = -#if 0 - // Disabled for being too messy +#if 1 + // Previously disabled for being too messy. it->is_goto() || it->is_function_call() || it->is_assume(); #else + // Disabled for being misleading. it->is_goto() || it->is_function_call(); #endif }