Define coverage blocks so as to be terminated by all assumptions

regression/cbmc-cover/location-assume/end.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void main()
+{
+  int i;
+  int *p = &i;
+  int j;
+  __CPROVER_assume(j == 1 / (*p));
+}

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.

regression/cbmc-cover/location-assume/middle.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int i;
+  int j;
+  j = i;
+  __CPROVER_assume(0);
+  j = i + 2;
+  return 0;
+}

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.

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