Fix basic block coverage with unsatisfiable ASSUME statements

Insert coverage assertions at the end of basic blocks instead of the
beginning to ensure blocks are only marked as covered when all
instructions, including ASSUME statements, can be executed.

Fixes: #826

Author: tautschnig

regression/cbmc-cover/block-assume-coverage/main.c

@@ -0,0 +1,33 @@
+// Test for issue #826: Basic blocks incorrectly considered covered
+// with unsatisfiable ASSUME statements
+//
+// This test demonstrates that basic blocks should only be marked as
+// covered when ALL instructions in the block can execute, including
+// ASSUME statements.
+//
+// Before the fix: Block 3 would be incorrectly marked as SATISFIED
+//   because the coverage assertion was at the beginning of the block.
+// After the fix: Block 3 is correctly marked as FAILED because the
+//   ASSUME statement is unsatisfiable (x >= 0 when x < 0).
+
+int main()
+{
+  int x;
+
+  // Block with satisfiable ASSUME - should be covered
+  if(x > 0)
+  {
+    __CPROVER_assume(x > 0);
+    return 1;
+  }
+
+  // Block with unsatisfiable ASSUME - should NOT be covered
+  if(x < 0)
+  {
+    __CPROVER_assume(x >= 0);
+    return 2;
+  }
+
+  // Block with no ASSUME - should be covered
+  return 0;
+}

regression/cbmc-cover/block-assume-coverage/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+block 1 \(lines main.c:main:\d+\): SATISFIED
+block 2 \(lines main.c:main:\d+\): SATISFIED
+block 3 \(lines main.c:main:\d+\): FAILED
+block 4 \(lines main.c:main:\d+\): SATISFIED
+--

src/goto-instrument/cover_basic_blocks.cpp

@@ -63,6 +63,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
       else
       {
         block_infos.emplace_back();
+        // representative_inst will be updated to the last instruction
         block_infos.back().representative_inst = it;
         block_infos.back().source_location = source_locationt::nil();
         current_block = block_infos.size() - 1;
@@ -77,15 +78,18 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
 
     add_block_lines(block_info, *it);
 
-    // set representative program location to instrument
+    // Update representative instruction to always be the last instruction
+    block_info.representative_inst = it;
+
+    // set source location for reporting (from first instruction with valid
+    // location)
     if(
       !it->source_location().is_nil() &&
       !it->source_location().get_file().empty() &&
       !it->source_location().get_line().empty() &&
       !it->source_location().is_built_in() &&
       block_info.source_location.is_nil())
     {
-      block_info.representative_inst = it; // update
       block_info.source_location = it->source_location();
     }
 

src/goto-instrument/cover_basic_blocks.h

@@ -74,7 +74,7 @@ class cover_basic_blockst final : public cover_blocks_baset
 
   /// \param block_nr: a block number
   /// \return the instruction selected for
-  ///   instrumentation representative of the given block
+  ///   instrumentation representative of the given block (last instruction)
   std::optional<goto_programt::const_targett>
   instruction_of(std::size_t block_nr) const override;
 
@@ -109,7 +109,7 @@ class cover_basic_blockst final : public cover_blocks_baset
 
   struct block_infot
   {
-    /// the program location to instrument for this block
+    /// the program location to instrument for this block (last instruction)
     std::optional<goto_programt::const_targett> representative_inst;
 
     /// the source location representative for this block

src/goto-instrument/cover_instrument_location.cpp

@@ -25,8 +25,13 @@ void cover_location_instrumentert::instrument(
     i_it->turn_into_skip();
 
   const std::size_t block_nr = basic_blocks.block_of(i_it);
+
+  // The representative instruction is the last instruction in the block,
+  // ensuring all instructions (including any ASSUME statements) can be
+  // executed.
   const auto representative_instruction = basic_blocks.instruction_of(block_nr);
-  // we only instrument the selected instruction
+
+  // we only instrument the selected instruction (last in block)
   if(representative_instruction && *representative_instruction == i_it)
   {
     const std::string b = std::to_string(block_nr + 1); // start with 1