jdiff_parse_options is not a message

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

Author: romainbrenguier

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -63,7 +63,6 @@ Author: Peter Schrammel
 
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler),
-    messaget(ui_message_handler),
     ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION)
 {
 }
@@ -186,19 +185,19 @@ int jdiff_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() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
-           << "-bit " << config.this_architecture() << " "
-           << config.this_operating_system() << eom;
+  log.status() << "JDIFF 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;
   }
 
@@ -226,12 +225,12 @@ int jdiff_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;
@@ -275,20 +274,21 @@ bool jdiff_parse_optionst::process_goto_program(
 {
   {
     // 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"));
 
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
 
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions_using_instanceof(goto_model, get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, log.get_message_handler());
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);
-    remove_instanceof(goto_model, class_hierarchy, get_message_handler());
+    remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
 
     mm_io(goto_model);
 
@@ -302,7 +302,7 @@ bool jdiff_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
@@ -322,9 +322,9 @@ bool jdiff_parse_optionst::process_goto_program(
     if(cmdline.isset("cover"))
     {
       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;
     }
 

jbmc/src/jdiff/jdiff_parse_options.h

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