Fix basic block coverage with unsatisfiable ASSUME statements

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