Merge pull request #5635 from thomasspriggs/tas/expression_coverage

Make location coverage reported include all lines of a multi-line statement

Author: thomasspriggs

regression/cbmc-cover/location-multiline-statement/dereference.h

@@ -0,0 +1,2 @@
+
+*

regression/cbmc-cover/location-multiline-statement/example.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+int foo(int x, int y)
+{
+  return x;
+}
+
+int main()
+{
+  int *ptr = malloc(sizeof(*ptr));
+
+  // clang-format off
+  foo(1,
+      *ptr);
+  // clang-format on
+
+  if(0)
+  {
+    *ptr = 0;
+  }
+
+  return 0;
+}

regression/cbmc-cover/location-multiline-statement/multi-file.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+
+int foo(int x, int y)
+{
+  return x;
+}
+
+int main()
+{
+  int *ptr = malloc(sizeof(*ptr));
+
+  // clang-format off
+  foo(
+    1,
+#include "dereference.h"
+    ptr);
+  // clang-format on
+
+  if(0)
+  {
+    *ptr = 0;
+  }
+
+  return 0;
+}

regression/cbmc-cover/location-multiline-statement/multi-file.desc

@@ -0,0 +1,11 @@
+CORE
+multi-file.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.2\] file multi-file.c line 10 function main block 2 \(lines [\w\- /\.\\:]*dereference.h:main:2; multi-file.c:main:10,13,14,16\): SATISFIED
+--
+^warning: ignoring
+--
+Test that the lines covered by location coverage in the output include all lines
+of a multi-line statement where some of the lines are in an included file.

regression/cbmc-cover/location-multiline-statement/test.desc

@@ -0,0 +1,11 @@
+CORE
+example.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.2\] file example.c line 10 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$
+--
+^warning: ignoring
+--
+Test that the lines covered by location coverage in the output include all lines
+of a multi-line statement.

src/goto-instrument/cover_basic_blocks.cpp

@@ -29,12 +29,12 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
   return {};
 }
 
-cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
+cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
 {
   bool next_is_target = true;
   std::size_t current_block = 0;
 
-  forall_goto_program_instructions(it, _goto_program)
+  forall_goto_program_instructions(it, goto_program)
   {
     // Is it a potential beginning of a block?
     if(next_is_target || it->is_target())
@@ -58,13 +58,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
 
     block_map[it] = current_block;
 
-    // update lines belonging to block
-    const irep_idt &line = it->source_location.get_line();
-    if(!line.empty())
-    {
-      block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
-      block_info.source_lines.insert(it->source_location);
-    }
+    add_block_lines(block_info, *it);
 
     // set representative program location to instrument
     if(
@@ -155,6 +149,23 @@ void cover_basic_blockst::output(std::ostream &out) const
         << '\n';
 }
 
+void cover_basic_blockst::add_block_lines(
+  cover_basic_blockst::block_infot &block,
+  const goto_programt::instructiont &instruction)
+{
+  const auto &add_location = [&](const source_locationt &location) {
+    const irep_idt &line = location.get_line();
+    if(!line.empty())
+    {
+      block.lines.insert(unsafe_string2unsigned(id2string(line)));
+      block.source_lines.insert(location);
+    }
+  };
+  add_location(instruction.source_location);
+  instruction.code.visit_pre(
+    [&](const exprt &expr) { add_location(expr.source_location()); });
+}
+
 void cover_basic_blockst::update_covered_lines(block_infot &block_info)
 {
   if(block_info.source_location.is_nil())

src/goto-instrument/cover_basic_blocks.h

@@ -63,7 +63,7 @@ class cover_blocks_baset
 class cover_basic_blockst final : public cover_blocks_baset
 {
 public:
-  explicit cover_basic_blockst(const goto_programt &_goto_program);
+  explicit cover_basic_blockst(const goto_programt &goto_program);
 
   /// \param t: a goto instruction
   /// \return the block number of the block
@@ -119,6 +119,11 @@ class cover_basic_blockst final : public cover_blocks_baset
   /// map block numbers to block information
   std::vector<block_infot> block_infos;
 
+  /// Adds the lines which \param instruction spans to \param block.
+  static void add_block_lines(
+    cover_basic_blockst::block_infot &block,
+    const goto_programt::instructiont &instruction);
+
   /// create list of covered lines as CSV string and set as property of source
   /// location of basic block, compress to ranges if applicable
   static void update_covered_lines(block_infot &block_info);