diff --git a/regression/cbmc-cover/location2/main.c b/regression/cbmc-cover/location2/main.c new file mode 100644 index 00000000000..188033a34b9 --- /dev/null +++ b/regression/cbmc-cover/location2/main.c @@ -0,0 +1,11 @@ +#include + +#define BUFLEN 100 + +static void *(*const volatile memset_func)(void *, int, size_t) = memset; + +int main() +{ + char buffer[BUFLEN]; + memset_func(&buffer, 0, BUFLEN); +} diff --git a/regression/cbmc-cover/location2/test.desc b/regression/cbmc-cover/location2/test.desc new file mode 100644 index 00000000000..747ff0c5800 --- /dev/null +++ b/regression/cbmc-cover/location2/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 9 function main block 1 \(lines main.c:main:9,10\): SATISFIED$ +^\[main.coverage.2\] file main.c line 11 function main block 2 \(lines main.c:main:11\): SATISFIED$ +^\*\* 2 of 2 covered \(100.0%\) +-- +^warning: ignoring +main.c::5 +-- +Expressions outside a function should not end up listed as part of source code +blocks. diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index ce94e4b1f13..a5548af84e3 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -163,8 +163,11 @@ void cover_basic_blockst::add_block_lines( } }; add_location(instruction.source_location()); - instruction.get_code().visit_pre( - [&](const exprt &expr) { add_location(expr.source_location()); }); + instruction.get_code().visit_pre([&](const exprt &expr) { + const auto &location = expr.source_location(); + if(!location.get_function().empty()) + add_location(location); + }); } cover_basic_blocks_javat::cover_basic_blocks_javat(