From fffc77e04e638a15fed4db22a8586f1fbb05b19a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 29 Jun 2022 11:15:48 +0000
Subject: [PATCH] Location coverage reporting should ignore globals

We iterate over instructions in non-built-in functions, and it is
therefore reasonable to expect that all source locations have functions
that they belong to. If symbols declared at global scope are part of
expressions then this shouldn't yield calling them out in location
coverage. (That's just where they were declared, it doesn't even
strictly imply their assignments were covered.)

Fixes: #6978
---
 regression/cbmc-cover/location2/main.c     | 11 +++++++++++
 regression/cbmc-cover/location2/test.desc  | 14 ++++++++++++++
 src/goto-instrument/cover_basic_blocks.cpp |  7 +++++--
 3 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc-cover/location2/main.c
 create mode 100644 regression/cbmc-cover/location2/test.desc

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 <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);
+}
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(