Merge pull request #4517 from romainbrenguier/clean-up/goto-analyzer-messaget

goto_analyzer_parse_optionst is not a messaget

Author: romainbrenguier

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -70,7 +70,6 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,
   const char **argv)
   : parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv, ui_message_handler),
-    messaget(ui_message_handler),
     ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION)
 {
 }
@@ -298,7 +297,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       if(!options.get_bool_option("domain set"))
       {
         // Default to constants as it is light-weight but useful
-        status() << "Domain not specified, defaulting to --constants" << eom;
+        log.status() << "Domain not specified, defaulting to --constants"
+                     << messaget::eom;
         options.set_option("constants", true);
       }
     }
@@ -386,20 +386,20 @@ int goto_analyzer_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity(
+  messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner
   //
-  status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
-           << sizeof(void *) * 8 << "-bit " << config.this_architecture() << " "
-           << config.this_operating_system() << eom;
+  log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
+               << sizeof(void *) * 8 << "-bit " << config.this_architecture()
+               << " " << config.this_operating_system() << messaget::eom;
 
   register_languages();
 
   goto_model =
-    initialize_goto_model(cmdline.args, get_message_handler(), options);
+    initialize_goto_model(cmdline.args, log.get_message_handler(), options);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -423,7 +423,7 @@ int goto_analyzer_parse_optionst::doit()
   {
     show_goto_functions(
       goto_model,
-      get_message_handler(),
+      log.get_message_handler(),
       get_ui(),
       cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
@@ -443,15 +443,15 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     if(cmdline.isset("show-taint"))
     {
-      taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
+      taint_analysis(
+        goto_model, taint_file, log.get_message_handler(), true, "");
       return CPROVER_EXIT_SUCCESS;
     }
     else
     {
       std::string json_file=cmdline.get_value("json");
-      bool result=
-        taint_analysis(
-          goto_model, taint_file, get_message_handler(), false, json_file);
+      bool result = taint_analysis(
+        goto_model, taint_file, log.get_message_handler(), false, json_file);
       return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
     }
   }
@@ -471,8 +471,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       std::ofstream ofs(json_file);
       if(!ofs)
       {
-        error() << "Failed to open json output `"
-                << json_file << "'" << eom;
+        log.error() << "Failed to open json output `" << json_file << "'"
+                    << messaget::eom;
         return CPROVER_EXIT_INTERNAL_ERROR;
       }
 
@@ -496,8 +496,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       std::ofstream ofs(json_file);
       if(!ofs)
       {
-        error() << "Failed to open json output `"
-                << json_file << "'" << eom;
+        log.error() << "Failed to open json output `" << json_file << "'"
+                    << messaget::eom;
         return CPROVER_EXIT_INTERNAL_ERROR;
       }
 
@@ -521,8 +521,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       std::ofstream ofs(json_file);
       if(!ofs)
       {
-        error() << "Failed to open json output `"
-                << json_file << "'" << eom;
+        log.error() << "Failed to open json output `" << json_file << "'"
+                    << messaget::eom;
         return CPROVER_EXIT_INTERNAL_ERROR;
       }
 
@@ -553,7 +553,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, get_message_handler(), get_ui());
+    show_properties(goto_model, log.get_message_handler(), get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -574,29 +574,29 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     if(!out)
     {
-      error() << "Failed to open output file `"
-              << outfile << "'" << eom;
+      log.error() << "Failed to open output file `" << outfile << "'"
+                  << messaget::eom;
       return CPROVER_EXIT_INTERNAL_ERROR;
     }
 
     // Build analyzer
-    status() << "Selecting abstract domain" << eom;
+    log.status() << "Selecting abstract domain" << messaget::eom;
     namespacet ns(goto_model.symbol_table);  // Must live as long as the domain.
     std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
 
     if(analyzer == nullptr)
     {
-      status() << "Task / Interpreter / Domain combination not supported"
-               << messaget::eom;
+      log.status() << "Task / Interpreter / Domain combination not supported"
+                   << messaget::eom;
       return CPROVER_EXIT_INTERNAL_ERROR;
     }
 
     // Run
-    status() << "Computing abstract states" << eom;
+    log.status() << "Computing abstract states" << messaget::eom;
     (*analyzer)(goto_model);
 
     // Perform the task
-    status() << "Performing task" << eom;
+    log.status() << "Performing task" << messaget::eom;
 
     bool result = true;
 
@@ -607,27 +607,21 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
     }
     else if(options.get_bool_option("show-on-source"))
     {
-      show_on_source(goto_model, *analyzer, get_message_handler());
+      show_on_source(goto_model, *analyzer, log.get_message_handler());
       return CPROVER_EXIT_SUCCESS;
     }
     else if(options.get_bool_option("verify"))
     {
-      result = static_verifier(goto_model,
-                               *analyzer,
-                               options,
-                               get_message_handler(),
-                               out);
+      result = static_verifier(
+        goto_model, *analyzer, options, log.get_message_handler(), out);
     }
     else if(options.get_bool_option("simplify"))
     {
       PRECONDITION(!outfile.empty() && outfile != "-");
       output_stream.close();
       output_stream.open(outfile, std::ios::binary);
-      result = static_simplifier(goto_model,
-                                 *analyzer,
-                                 options,
-                                 get_message_handler(),
-                                 out);
+      result = static_simplifier(
+        goto_model, *analyzer, options, log.get_message_handler(), out);
     }
     else if(options.get_bool_option("unreachable-instructions"))
     {
@@ -652,7 +646,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
     }
     else
     {
-      error() << "Unhandled task" << eom;
+      log.error() << "Unhandled task" << messaget::eom;
       return CPROVER_EXIT_INTERNAL_ERROR;
     }
 
@@ -662,8 +656,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
 
   // Final defensive error case
-  error() << "no analysis option given -- consider reading --help"
-          << eom;
+  log.error() << "no analysis option given -- consider reading --help"
+              << messaget::eom;
   return CPROVER_EXIT_USAGE_ERROR;
 }
 
@@ -677,19 +671,20 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
-    status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
+    log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom;
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
     #endif
 
     // remove function pointers
-    status() << "Removing function pointers and virtual functions" << eom;
+    log.status() << "Removing function pointers and virtual functions"
+                 << messaget::eom;
     remove_function_pointers(
-      get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
 
     // do partial inlining
-    status() << "Partial Inlining" << eom;
+    log.status() << "Partial Inlining" << messaget::eom;
     goto_partial_inline(goto_model, ui_message_handler);
 
     // remove returns, gcc vectors, complex
@@ -699,7 +694,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 
 #if 0
     // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
+    log.status() << "Generic Property Instrumentation" << messaget::eom;
     goto_check(options, goto_model);
 #else
     (void)options; // unused parameter

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -153,9 +153,7 @@ class optionst;
   OPT_VALIDATE \
 // clang-format on
 
-class goto_analyzer_parse_optionst:
-  public parse_options_baset,
-  public messaget
+class goto_analyzer_parse_optionst: public parse_options_baset
 {
 public:
   virtual int doit() override;