diff --git a/regression/cbmc-cover/block-assume-coverage/main.c b/regression/cbmc-cover/block-assume-coverage/main.c new file mode 100644 index 00000000000..7cad1d01718 --- /dev/null +++ b/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; +} diff --git a/regression/cbmc-cover/block-assume-coverage/test.desc b/regression/cbmc-cover/block-assume-coverage/test.desc new file mode 100644 index 00000000000..2919af66342 --- /dev/null +++ b/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 +-- diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 23df805b4dc..396f4683992 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/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,7 +78,11 @@ 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() && @@ -85,7 +90,6 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) !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(); } diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 8c9bd2c2a89..d65b4da6536 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/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 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 representative_inst; /// the source location representative for this block diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp index 64b93dc1936..ca7af1f0674 100644 --- a/src/goto-instrument/cover_instrument_location.cpp +++ b/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