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

Diff for: 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 for: 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 for: 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 for: 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 for: 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 for: regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -1,9 +1,10 @@
 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\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:17,18\): SATISFIED
+\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:15\): FAILED
+\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12,14\): 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 for: src/goto-instrument/cover_basic_blocks.cpp

@@ -29,15 +29,34 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
   return {};
 }
 
+static bool
+same_source_line(const source_locationt &a, const source_locationt &b)
+{
+  return a.get_file() == b.get_file() && a.get_line() == b.get_line();
+}
+
 cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
 {
   bool next_is_target = true;
+  const goto_programt::instructiont *preceding_assume = nullptr;
   std::size_t current_block = 0;
 
   forall_goto_program_instructions(it, goto_program)
   {
+    // For the purposes of coverage blocks, multiple consecutive assume
+    // instructions with the same source location are considered to be part of
+    // the same block. Assumptions should terminate a block, as subsequent
+    // instructions may be unreachable. However check instrumentation passes
+    // may insert multiple assertions in the same program location. Therefore
+    // these are combined for reasons of readability of the coverage output.
+    bool end_of_assume_group =
+      preceding_assume &&
+      !(it->is_assume() &&
+        same_source_line(
+          preceding_assume->source_location(), it->source_location()));
+
     // Is it a potential beginning of a block?
-    if(next_is_target || it->is_target())
+    if(next_is_target || it->is_target() || end_of_assume_group)
     {
       if(auto block_number = continuation_of_block(it, block_map))
       {
@@ -72,13 +91,8 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
       block_info.source_location = it->source_location();
     }
 
-    next_is_target =
-#if 0
-      // Disabled for being too messy
-      it->is_goto() || it->is_function_call() || it->is_assume();
-#else
-      it->is_goto() || it->is_function_call();
-#endif
+    next_is_target = it->is_goto() || it->is_function_call();
+    preceding_assume = it->is_assume() ? &*it : nullptr;
   }
 }