Merge pull request #7494 from tautschnig/bugfixes/7473-recursion

Fix symex coverage reporting of recursive calls

Author: tautschnig

regression/cbmc/coverage_report2/main.c

@@ -0,0 +1,14 @@
+int factorial(int n)
+{
+  if(n == 0)
+  {
+    return 1;
+  }
+  return n * factorial(n - 1);
+}
+
+int main(void)
+{
+  int result = factorial(5);
+  return 0;
+}

regression/cbmc/coverage_report2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--symex-coverage-report - --unwind 1
+<line branch="true" condition-coverage="50% \(1/2\)" hits="2" number="3">
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Invariant check failed

regression/validate-trace-xml-schema/check.py

@@ -50,6 +50,7 @@
     # produces intermingled XML on the command line
     ['coverage_report1', 'test.desc'],
     ['coverage_report1', 'paths.desc'],
+    ['coverage_report2', 'test.desc'],
     ['graphml_witness1', 'test.desc'],
     ['switch8', 'program-only.desc'],
     ['Failing_Assert1', 'dimacs.desc'],

src/goto-checker/symex_coverage.cpp

@@ -236,15 +236,12 @@ void goto_program_coverage_recordt::compute_coverage_lines(
     symex_coveraget::coveraget::const_iterator c_entry = coverage.find(it);
     if(c_entry != coverage.end())
     {
-      if(!(c_entry->second.size() == 1 || is_branch))
-      {
-        std::cerr << it->location_number << '\n';
-        for(const auto &cov : c_entry->second)
-          std::cerr << cov.second.succ->location_number << '\n';
-      }
-      DATA_INVARIANT(
-        c_entry->second.size() == 1 || is_branch,
-        "instructions other than branch instructions have exactly 1 successor");
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        c_entry->second.size() == 1 || is_branch || it->is_function_call(),
+        "instructions other than branch instructions or function calls have "
+        "exactly 1 successor",
+        "found at goto program instruction number " +
+          std::to_string(it->location_number));
 
       for(const auto &cov : c_entry->second)
       {