goto_diff_parse_options is not a message

In addition the class already inherits a log field of type messaget.

Author: romainbrenguier

src/goto-diff/goto_diff_parse_options.cpp

@@ -65,7 +65,6 @@ Author: Peter Schrammel
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, ui_message_handler),
-    messaget(ui_message_handler),
     ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION)
 {
 }
@@ -201,8 +200,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   if(options.get_bool_option("partial-loops") &&
      options.get_bool_option("unwinding-assertions"))
   {
-    error() << "--partial-loops and --unwinding-assertions"
-            << " must not be given together" << eom;
+    log.error() << "--partial-loops and --unwinding-assertions"
+                << " must not be given together" << messaget::eom;
     exit(1);
   }
 
@@ -224,19 +223,19 @@ int goto_diff_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-DIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
-           << "-bit " << config.this_architecture() << " "
-           << config.this_operating_system() << eom;
+  log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
+               << sizeof(void *) * 8 << "-bit " << config.this_architecture()
+               << " " << config.this_operating_system() << messaget::eom;
 
   if(cmdline.args.size()!=2)
   {
-    error() << "Please provide two programs to compare" << eom;
+    log.error() << "Please provide two programs to compare" << messaget::eom;
     return CPROVER_EXIT_INCORRECT_TASK;
   }
 
@@ -264,12 +263,12 @@ int goto_diff_parse_optionst::doit()
   {
     show_goto_functions(
       goto_model1,
-      get_message_handler(),
+      log.get_message_handler(),
       ui_message_handler.get_ui(),
       cmdline.isset("list-goto-functions"));
     show_goto_functions(
       goto_model2,
-      get_message_handler(),
+      log.get_message_handler(),
       ui_message_handler.get_ui(),
       cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
@@ -321,16 +320,18 @@ bool goto_diff_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, get_message_handler(), cprover_cpp_library_factory);
+      goto_model, log.get_message_handler(), cprover_cpp_library_factory);
     link_to_library(
-      goto_model, get_message_handler(), cprover_c_library_factory);
+      goto_model, log.get_message_handler(), cprover_c_library_factory);
 
     // remove function pointers
-    status() << "Removal of function pointers and virtual functions" << eom;
+    log.status() << "Removal of 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"));
 
     mm_io(goto_model);
 
@@ -344,7 +345,7 @@ bool goto_diff_parse_optionst::process_goto_program(
     rewrite_union(goto_model);
 
     // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
+    log.status() << "Generic Property Instrumentation" << messaget::eom;
     goto_check(options, goto_model);
 
     // checks don't know about adjusted float expressions
@@ -364,9 +365,9 @@ bool goto_diff_parse_optionst::process_goto_program(
       remove_skip(goto_model);
 
       const auto cover_config = get_cover_config(
-        options, goto_model.symbol_table, get_message_handler());
+        options, goto_model.symbol_table, log.get_message_handler());
       if(instrument_cover_goals(
-           cover_config, goto_model, get_message_handler()))
+           cover_config, goto_model, log.get_message_handler()))
         return true;
     }
 

src/goto-diff/goto_diff_parse_options.h

@@ -39,7 +39,7 @@ class optionst;
   "(compact-output)"
 // clang-format on
 
-class goto_diff_parse_optionst : public parse_options_baset, public messaget
+class goto_diff_parse_optionst : public parse_options_baset
 {
 public:
   virtual int doit();