Replace cover-function-only by cover-include-pattern

cover-function-only (instrumentating coverage goals in the
entry point function only) is now implemented with the help
of cover-include-pattern (regex matching of functions to
be instrumented). This is to avoid potential consistencies
due to providing two mechanisms for filtering functions.
cover-function-only has priority over the given
cover-include-pattern.

Author: peterschrammel

src/goto-instrument/cover.cpp

@@ -1055,22 +1055,6 @@ std::set<exprt> collect_decisions(const goto_programt::const_targett t)
   return std::set<exprt>();
 }
 
-void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  goto_programt &goto_program,
-  coverage_criteriont criterion,
-  message_handlert &message_handler,
-  bool function_only)
-{
-  instrument_cover_goals(
-    symbol_table,
-    goto_program,
-    criterion,
-    message_handler,
-    function_only,
-    false);
-}
-
 /// Call a goto_program trivial unless it has: * Any declarations * At least 2
 /// branches * At least 5 assignments
 /// \par parameters: Program `goto_program`
@@ -1101,14 +1085,8 @@ void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_programt &goto_program,
   coverage_criteriont criterion,
-  message_handlert &message_handler,
-  bool function_only,
-  bool ignore_trivial)
+  message_handlert &message_handler)
 {
-  // exclude trivial coverage goals of a goto program
-  if(ignore_trivial && program_is_trivial(goto_program))
-    return;
-
   // ignore if built-in library
   if(!goto_program.instructions.empty() &&
      goto_program.instructions.front().source_location.is_built_in())
@@ -1125,19 +1103,11 @@ void instrument_cover_goals(
 
   Forall_goto_program_instructions(i_it, goto_program)
   {
-    std::string curr_function=id2string(i_it->function);
-
-    // if the --cover-function-only flag is set, then we only add coverage
-    // instrumentation for the entry function
-    bool cover_curr_function=
-      !function_only ||
-      curr_function.find(config.main)!=std::string::npos;
-
     switch(criterion)
     {
     case coverage_criteriont::ASSERTION:
       // turn into 'assert(false)' to avoid simplification
-      if(i_it->is_assert() && cover_curr_function)
+      if(i_it->is_assert())
       {
         i_it->guard=false_exprt();
         i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
@@ -1148,7 +1118,7 @@ void instrument_cover_goals(
 
     case coverage_criteriont::COVER:
       // turn __CPROVER_cover(x) into 'assert(!x)'
-      if(i_it->is_function_call() && cover_curr_function)
+      if(i_it->is_function_call())
       {
         const code_function_callt &code_function_call=
           to_code_function_call(i_it->code);
@@ -1190,7 +1160,7 @@ void instrument_cover_goals(
           // check whether the current goal needs to be covered
           if(
             !source_location.get_file().empty() &&
-            !source_location.is_built_in() && cover_curr_function)
+            !source_location.is_built_in())
           {
             std::string comment="block "+b;
             const irep_idt function=i_it->function;
@@ -1213,8 +1183,7 @@ void instrument_cover_goals(
       if(i_it->is_assert())
         i_it->make_skip();
 
-      if(i_it==goto_program.instructions.begin() &&
-         cover_curr_function)
+      if(i_it == goto_program.instructions.begin())
       {
         // we want branch coverage to imply 'entry point of function'
         // coverage
@@ -1232,8 +1201,9 @@ void instrument_cover_goals(
         t->function=i_it->function;
       }
 
-      if(i_it->is_goto() && !i_it->guard.is_true() && cover_curr_function &&
-         !i_it->source_location.is_built_in())
+      if(
+        i_it->is_goto() && !i_it->guard.is_true() &&
+        !i_it->source_location.is_built_in())
       {
         std::string b=
           std::to_string(basic_blocks.block_of(i_it)+1); // start with 1
@@ -1271,7 +1241,7 @@ void instrument_cover_goals(
         i_it->make_skip();
 
       // Conditions are all atomic predicates in the programs.
-      if(cover_curr_function && !i_it->source_location.is_built_in())
+      if(!i_it->source_location.is_built_in())
       {
         const std::set<exprt> conditions=collect_conditions(i_it);
 
@@ -1313,7 +1283,7 @@ void instrument_cover_goals(
         i_it->make_skip();
 
       // Decisions are maximal Boolean combinations of conditions.
-      if(cover_curr_function && !i_it->source_location.is_built_in())
+      if(!i_it->source_location.is_built_in())
       {
         const std::set<exprt> decisions=collect_decisions(i_it);
 
@@ -1359,7 +1329,7 @@ void instrument_cover_goals(
       // 3. Each condition in a decision takes every possible outcome
       // 4. Each condition in a decision is shown to independently
       //    affect the outcome of the decision.
-      if(cover_curr_function && !i_it->source_location.is_built_in())
+      if(!i_it->source_location.is_built_in())
       {
         const std::set<exprt> conditions=collect_conditions(i_it);
         const std::set<exprt> decisions=collect_decisions(i_it);
@@ -1459,7 +1429,6 @@ void instrument_cover_goals(
   goto_functionst &goto_functions,
   coverage_criteriont criterion,
   message_handlert &message_handler,
-  bool function_only,
   bool ignore_trivial,
   const std::string &cover_include_pattern)
 {
@@ -1480,28 +1449,21 @@ void instrument_cover_goals(
       continue;
 
     instrument_cover_goals(
-      symbol_table,
-      f_it->second.body,
-      criterion,
-      message_handler,
-      function_only,
-      ignore_trivial);
+      symbol_table, f_it->second.body, criterion, message_handler);
   }
 }
 
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_functionst &goto_functions,
   coverage_criteriont criterion,
-  message_handlert &message_handler,
-  bool function_only)
+  message_handlert &message_handler)
 {
   instrument_cover_goals(
     symbol_table,
     goto_functions,
     criterion,
     message_handler,
-    function_only,
     false,
     "");
 }
@@ -1575,6 +1537,17 @@ bool instrument_cover_goals(
     }
   }
 
+  // cover entry point function only
+  std::string cover_include_pattern =
+    cmdline.get_value("cover-include-pattern");
+  if(cmdline.isset("cover-function-only"))
+  {
+    std::regex special_characters(
+      "\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|");
+    cover_include_pattern =
+      ".*" + std::regex_replace(config.main, special_characters, "\\$&") + ".*";
+  }
+
   msg.status() << "Instrumenting coverage goals" << messaget::eom;
 
   for(const auto &criterion : criteria)
@@ -1584,9 +1557,8 @@ bool instrument_cover_goals(
       goto_functions,
       criterion,
       message_handler,
-      cmdline.isset("cover-function-only"),
       cmdline.isset("no-trivial-tests"),
-      cmdline.get_value("cover-include-pattern"));
+      cover_include_pattern);
   }
 
   if(cmdline.isset("cover-traces-must-terminate"))

src/goto-instrument/cover.h

@@ -29,32 +29,21 @@ void instrument_cover_goals(
   const symbol_tablet &,
   goto_functionst &,
   coverage_criteriont,
-  message_handlert &message_handler,
-  bool function_only=false);
+  message_handlert &message_handler);
 
 void instrument_cover_goals(
   const symbol_tablet &,
   goto_programt &,
   coverage_criteriont,
-  message_handlert &message_handler,
-  bool function_only=false);
+  message_handlert &message_handler);
 
 void instrument_cover_goals(
   const symbol_tablet &,
   goto_functionst &,
   coverage_criteriont,
   message_handlert &message_handler,
-  bool function_only=false,
-  bool ignore_trivial=false,
-  const std::string &cover_inclue_pattern="");
-
-void instrument_cover_goals(
-  const symbol_tablet &,
-  goto_programt &,
-  coverage_criteriont,
-  message_handlert &message_handler,
-  bool function_only=false,
-  bool ignore_trivial=false);
+  bool ignore_trivial = false,
+  const std::string &cover_include_pattern = "");
 
 bool instrument_cover_goals(
   const cmdlinet &,