Skip to content

Commit ffcaea9

Browse files
committed
Block coverage reporting: do not use built-in locations
source_linest::insert will disregard any source locations that refer to built-ins. cover_basic_blockst, however, only checked that any source location used as basic-block representative had file and line information. This resulted in cover_basic_blockst believing it had found a representative source location when source_linest didn't quite agree. This change makes the example presented in #6536 (which originates from Rust/Kani) work. The issue wasn't reproducible with C examples. Fixes: #6536
1 parent b345e2a commit ffcaea9

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/goto-instrument/cover_basic_blocks.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
6565
!it->source_location().is_nil() &&
6666
!it->source_location().get_file().empty() &&
6767
!it->source_location().get_line().empty() &&
68+
!it->source_location().is_built_in() &&
6869
block_info.source_location.is_nil())
6970
{
7071
block_info.representative_inst = it; // update

0 commit comments

Comments
 (0)