Merge pull request #946 from tautschnig/coverage-fixes

Coverage report fixes

Author: Daniel Kroening

regression/cbmc/coverage_report1/main.c

@@ -0,0 +1,23 @@
+int main(int argc, char* argv[])
+{
+  if(argc>2)
+  {
+    argc=1;
+  }
+  else
+  {
+    argc=2;
+  }
+
+  switch(argc)
+  {
+    case 0:
+      argc=3;
+      break;
+    case 1:
+      argc=2;
+      break;
+  }
+
+  return 0;
+}

regression/cbmc/coverage_report1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--symex-coverage-report -
+<line branch="false" hits="1" number="12"/>
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/cbmc/symex_bmc.cpp

@@ -65,6 +65,7 @@ void symex_bmct::symex_step(
   }
 
   const goto_programt::const_targett cur_pc=state.source.pc;
+  const guardt cur_guard=state.guard;
 
   if(!state.guard.is_false() &&
      state.source.pc->is_assume() &&
@@ -84,16 +85,23 @@ void symex_bmct::symex_step(
   goto_symext::symex_step(goto_functions, state);
 
   if(record_coverage &&
-     // is the instruction being executed
-     !state.guard.is_false() &&
      // avoid an invalid iterator in state.source.pc
      (!cur_pc->is_end_function() ||
-      cur_pc->function!=goto_functions.entry_point()) &&
-     // ignore transition to next instruction when goto points elsewhere
-     (!cur_pc->is_goto() ||
-      cur_pc->get_target()==state.source.pc ||
-      !cur_pc->guard.is_true()))
-    symex_coverage.covered(cur_pc, state.source.pc);
+      cur_pc->function!=goto_functions.entry_point()))
+  {
+    // forward goto will effectively be covered via phi function,
+    // which does not invoke symex_step; as symex_step is called
+    // before merge_gotos, also state.guard will be false (we have
+    // taken an impossible transition); thus we synthesize a
+    // transition from the goto instruction to its target to make
+    // sure the goto is considered covered
+    if(cur_pc->is_goto() &&
+       cur_pc->get_target()!=state.source.pc &&
+       cur_pc->guard.is_true())
+      symex_coverage.covered(cur_pc, cur_pc->get_target());
+    else if(!state.guard.is_false())
+      symex_coverage.covered(cur_pc, state.source.pc);
+  }
 }
 
 /*******************************************************************\

src/cbmc/symex_coverage.cpp

@@ -131,6 +131,29 @@ static std::string rate(
 
 /*******************************************************************\
 
+Function: rate_detailed
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static std::string rate_detailed(
+  std::size_t covered,
+  std::size_t total,
+  bool per_cent=false)
+{
+  std::ostringstream oss;
+  oss << rate(covered, total, per_cent)
+      << " (" << covered << '/' << total << ')';
+  return oss.str();
+}
+
+/*******************************************************************\
+
 Function: goto_program_coverage_recordt::goto_program_coverage_recordt
 
   Inputs:
@@ -187,7 +210,7 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
                     from_type(ns, gf_it->first, sig_type));
 
   xml.set_attribute("line-rate",
-                    rate(lines_covered, lines_total));
+                    rate_detailed(lines_covered, lines_total));
   xml.set_attribute("branch-rate",
                     rate(branches_covered, branches_total));
 
@@ -219,10 +242,9 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
         condition.set_attribute("coverage", rate(taken, 2, true));
       }
 
-      std::ostringstream oss;
-      oss << rate(total_taken, number*2, true)
-          << " (" << total_taken << '/' << number*2 << ')';
-      line.set_attribute("condition-coverage", oss.str());
+      line.set_attribute(
+        "condition-coverage",
+        rate_detailed(total_taken, number*2, true));
     }
   }
 }
@@ -292,7 +314,8 @@ void goto_program_coverage_recordt::compute_coverage_lines(
         if(entry.first->second.hits==0)
           ++lines_covered;
 
-        entry.first->second.hits+=cov.second.num_executions;
+        if(cov.second.num_executions>entry.first->second.hits)
+          entry.first->second.hits=cov.second.num_executions;
 
         if(is_branch)
         {