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

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,17 @@ 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,12 @@ 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