Define coverage blocks so as to be terminated by assumptions

If a coverage block has an assumption in the middle then then an
assertion at the end of the block could be reported as covered but
actually be unreachable due to the preceding the assumption. Therefore
coverage blocks should be terminated by assumptions in order to ensure
than coverage reporting is accurate.

Author: thomasspriggs

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

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
 --

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

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

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$

regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -1,9 +1,15 @@
 CORE paths-lifo-expected-failure new-smt-backend
 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$

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
   }