get_cover_config is now called separately from instrument_cover_goals

Author: Vojtech Forejt

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -321,7 +321,12 @@ bool jdiff_parse_optionst::process_goto_program(
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
+      const auto cover_config = get_cover_config(
+        options, goto_model.symbol_table, get_message_handler());
+      if(!cover_config)
+        return true;
+      if(instrument_cover_goals(
+           options, *cover_config, goto_model, get_message_handler()))
         return true;
     }
 

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -127,9 +127,15 @@ SCENARIO(
       {
         optionst options;
         options.set_option("cover", "location");
-        REQUIRE_FALSE(
-          instrument_cover_goals(
-            options, new_table, new_goto_functions, null_message_handler));
+        const auto cover_config =
+          get_cover_config(options, new_table, null_message_handler);
+        REQUIRE(cover_config);
+        REQUIRE_FALSE(instrument_cover_goals(
+          options,
+          *cover_config,
+          new_table,
+          new_goto_functions,
+          null_message_handler));
 
         auto function = new_goto_functions.function_map.find(function_name);
         REQUIRE(function != new_goto_functions.function_map.end());

src/cbmc/cbmc_parse_options.cpp

@@ -860,7 +860,12 @@ bool cbmc_parse_optionst::process_goto_program(
     // instrument cover goals
     if(options.is_set("cover"))
     {
-      if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
+      const auto cover_config = get_cover_config(
+        options, goto_model.symbol_table, log.get_message_handler());
+      if(!cover_config)
+        return true;
+      if(instrument_cover_goals(
+           options, *cover_config, goto_model, log.get_message_handler()))
         return true;
     }
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -363,7 +363,12 @@ bool goto_diff_parse_optionst::process_goto_program(
       // for coverage annotation:
       remove_skip(goto_model);
 
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
+      const auto cover_config = get_cover_config(
+        options, goto_model.symbol_table, get_message_handler());
+      if(!cover_config)
+        return true;
+      if(instrument_cover_goals(
+           options, *cover_config, goto_model, get_message_handler()))
         return true;
     }
 

src/goto-instrument/cover.cpp

@@ -329,11 +329,13 @@ void instrument_cover_goals(
 
 /// Instruments goto functions based on given command line options
 /// \param options: the options
+/// \param cover_config: configuration, produced using get_cover_config
 /// \param symbol_table: the symbol table
 /// \param goto_functions: the goto functions
 /// \param message_handler: a message handler
 bool instrument_cover_goals(
   const optionst &options,
+  const cover_configt &cover_config,
   const symbol_tablet &symbol_table,
   goto_functionst &goto_functions,
   message_handlert &message_handler)
@@ -342,13 +344,8 @@ bool instrument_cover_goals(
   msg.status() << "Rewriting existing assertions as assumptions"
                << messaget::eom;
 
-  std::unique_ptr<cover_configt> cover_config =
-    get_cover_config(options, symbol_table, message_handler);
-  if(!cover_config)
-    return true;
-
   if(
-    cover_config->traces_must_terminate &&
+    cover_config.traces_must_terminate &&
     !goto_functions.function_map.count(goto_functions.entry_point()))
   {
     msg.error() << "cover-traces-must-terminate: invalid entry point ["
@@ -359,29 +356,31 @@ bool instrument_cover_goals(
   Forall_goto_functions(f_it, goto_functions)
   {
     const symbolt function_symbol = symbol_table.lookup_ref(f_it->first);
-    cover_config->mode = function_symbol.mode;
     instrument_cover_goals(
-      *cover_config, function_symbol, f_it->second, message_handler);
+      cover_config, function_symbol, f_it->second, message_handler);
   }
   goto_functions.compute_location_numbers();
 
-  cover_config->function_filters.report_anomalies();
-  cover_config->goal_filters.report_anomalies();
+  cover_config.function_filters.report_anomalies();
+  cover_config.goal_filters.report_anomalies();
 
   return false;
 }
 
 /// Instruments a goto model based on given command line options
 /// \param options: the options
+/// \param cover_config: configuration, produced using get_cover_config
 /// \param goto_model: the goto model
 /// \param message_handler: a message handler
 bool instrument_cover_goals(
   const optionst &options,
+  const cover_configt &cover_config,
   goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   return instrument_cover_goals(
     options,
+    cover_config,
     goto_model.symbol_table,
     goto_model.goto_functions,
     message_handler);

src/goto-instrument/cover.h

@@ -14,7 +14,6 @@ Date: May 2016
 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_H
 #define CPROVER_GOTO_INSTRUMENT_COVER_H
 
-#include <goto-programs/goto_model.h>
 #include "cover_filter.h"
 #include "cover_instrument.h"
 
@@ -46,12 +45,14 @@ struct cover_configt
 
 void instrument_cover_goals(
   const symbol_tablet &,
+  const cover_configt &,
   goto_functionst &,
   coverage_criteriont,
   message_handlert &message_handler);
 
 void instrument_cover_goals(
   const symbol_tablet &,
+  const cover_configt &,
   goto_programt &,
   coverage_criteriont,
   message_handlert &message_handler);
@@ -68,12 +69,14 @@ void parse_cover_options(const cmdlinet &, optionst &);
 
 bool instrument_cover_goals(
   const optionst &,
+  const cover_configt &,
   const symbol_tablet &,
   goto_functionst &,
   message_handlert &);
 
 bool instrument_cover_goals(
   const optionst &,
+  const cover_configt &,
   goto_modelt &,
   message_handlert &);