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

@@ -1190,18 +1190,15 @@ void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_programt &goto_program,
   coverage_criteriont criterion,
-  message_handlert &message_handler,
-  bool function_only)
+  message_handlert &message_handler)
 {
   coverage_goalst goals; // empty already covered goals
   instrument_cover_goals(
     symbol_table,
     goto_program,
     criterion,
     message_handler,
-    goals,
-    function_only,
-    false);
+    goals);
 }
 
 /// Call a goto_program trivial unless it has: * Any declarations * At least 2
@@ -1235,14 +1232,8 @@ void instrument_cover_goals(
   goto_programt &goto_program,
   coverage_criteriont criterion,
   message_handlert &message_handler,
-  coverage_goalst &goals,
-  bool function_only,
-  bool ignore_trivial)
+  coverage_goalst &goals)
 {
-  // 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())
@@ -1259,19 +1250,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);
@@ -1282,7 +1265,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);
@@ -1324,8 +1307,7 @@ void instrument_cover_goals(
           // check whether the current goal already exists
           if(!goals.is_existing_goal(source_location) &&
              !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;
@@ -1348,8 +1330,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
@@ -1367,7 +1348,7 @@ void instrument_cover_goals(
         t->function=i_it->function;
       }
 
-      if(i_it->is_goto() && !i_it->guard.is_true() && cover_curr_function &&
+      if(i_it->is_goto() && !i_it->guard.is_true() &&
          !i_it->source_location.is_built_in())
       {
         std::string b=
@@ -1406,7 +1387,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);
 
@@ -1448,7 +1429,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);
 
@@ -1494,7 +1475,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);
@@ -1594,7 +1575,6 @@ void instrument_cover_goals(
   coverage_criteriont criterion,
   message_handlert &message_handler,
   coverage_goalst &goals,
-  bool function_only,
   bool ignore_trivial,
   const std::string &cover_include_pattern)
 {
@@ -1604,6 +1584,10 @@ void instrument_cover_goals(
 
   Forall_goto_functions(f_it, goto_functions)
   {
+    // exclude trivial coverage goals of a goto program
+    if(ignore_trivial && program_is_trivial(f_it->second.body))
+      return;
+
     if(f_it->first==goto_functions.entry_point() ||
        f_it->first==(CPROVER_PREFIX "initialize") ||
        f_it->second.is_hidden() ||
@@ -1619,18 +1603,15 @@ void instrument_cover_goals(
       f_it->second.body,
       criterion,
       message_handler,
-      goals,
-      function_only,
-      ignore_trivial);
+      goals);
   }
 }
 
 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)
 {
   // empty set of existing goals
   coverage_goalst goals;
@@ -1640,7 +1621,6 @@ void instrument_cover_goals(
     criterion,
     message_handler,
     goals,
-    function_only,
     false,
     "");
 }
@@ -1714,6 +1694,16 @@ 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, "\\$&");
+  }
+
   // check existing test goals
   coverage_goalst existing_goals;
   if(cmdline.isset("existing-coverage"))
@@ -1744,9 +1734,8 @@ bool instrument_cover_goals(
       criterion,
       message_handler,
       existing_goals,
-      cmdline.isset("cover-function-only"),
       cmdline.isset("no-trivial-tests"),
-      cmdline.get_value("cover-include-pattern"));
+      cover_include_pattern);
   }
 
   // check whether all existing goals match with instrumented goals

src/goto-instrument/cover.h

@@ -49,34 +49,29 @@ 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,
   coverage_goalst &,
-  bool function_only=false,
   bool ignore_trivial=false,
-  const std::string &cover_inclue_pattern="");
+  const std::string &cover_include_pattern="");
 
 void instrument_cover_goals(
   const symbol_tablet &,
   goto_programt &,
   coverage_criteriont,
   message_handlert &message_handler,
-  coverage_goalst &goals,
-  bool function_only=false,
-  bool ignore_trivial=false);
+  coverage_goalst &goals);
 
 bool instrument_cover_goals(
   const cmdlinet &,