Merge pull request #6981 from tautschnig/bugfixes/6978-source-loc

Location coverage reporting should ignore globals

Author: tautschnig

regression/cbmc-cover/location2/main.c

@@ -0,0 +1,11 @@
+#include <string.h>
+
+#define BUFLEN 100
+
+static void *(*const volatile memset_func)(void *, int, size_t) = memset;
+
+int main()
+{
+  char buffer[BUFLEN];
+  memset_func(&buffer, 0, BUFLEN);
+}

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.

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(