Clean-up message_handler of parse_options_baset

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -58,8 +58,11 @@ Author: Daniel Kroening, [email protected]
 #include <goto-analyzer/unreachable_instructions.h>
 
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
+  : parse_options_baset(
+      JANALYZER_OPTIONS,
+      argc,
+      argv,
+      std::string("JANALYZER ") + CBMC_VERSION)
 {
 }
 
@@ -368,8 +371,7 @@ int janalyzer_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
-  goto_model =
-    initialize_goto_model(cmdline.args, log.get_message_handler(), options);
+  goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -387,10 +389,7 @@ int janalyzer_parse_optionst::doit()
     cmdline.isset("list-goto-functions"))
   {
     show_goto_functions(
-      goto_model,
-      log.get_message_handler(),
-      get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -406,15 +405,14 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
 
     if(cmdline.isset("show-taint"))
     {
-      taint_analysis(
-        goto_model, taint_file, log.get_message_handler(), true, "");
+      taint_analysis(goto_model, taint_file, ui_message_handler, true, "");
       return CPROVER_EXIT_SUCCESS;
     }
     else
     {
       std::string json_file = cmdline.get_value("json");
       bool result = taint_analysis(
-        goto_model, taint_file, log.get_message_handler(), false, json_file);
+        goto_model, taint_file, ui_message_handler, false, json_file);
       return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
     }
   }
@@ -519,7 +517,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, log.get_message_handler(), get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -570,12 +568,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
     else if(options.get_bool_option("verify"))
     {
       result = static_verifier(
-        goto_model, *analyzer, options, log.get_message_handler(), out);
+        goto_model, *analyzer, options, ui_message_handler, out);
     }
     else if(options.get_bool_option("simplify"))
     {
       result = static_simplifier(
-        goto_model, *analyzer, options, log.get_message_handler(), out);
+        goto_model, *analyzer, options, ui_message_handler, out);
     }
     else if(options.get_bool_option("unreachable-instructions"))
     {
@@ -616,18 +614,18 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
-      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      ui_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, log.get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, ui_message_handler);
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);
-    remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
+    remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
 
     // do partial inlining
     log.status() << "Partial Inlining" << messaget::eom;

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -159,7 +159,6 @@ class janalyzer_parse_optionst : public parse_options_baset
   janalyzer_parse_optionst(int argc, const char **argv);
 
 protected:
-  ui_message_handlert ui_message_handler;
   goto_modelt goto_model;
 
   void register_languages();
@@ -171,11 +170,6 @@ class janalyzer_parse_optionst : public parse_options_baset
   virtual int perform_analysis(const optionst &options);
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
-
-  ui_message_handlert::uit get_ui()
-  {
-    return ui_message_handler.get_ui();
-  }
 };
 
 #endif // CPROVER_JANALYZER_JANALYZER_PARSE_OPTIONS_H

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -75,8 +75,11 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/simple_method_stubbing.h>
 
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JBMC_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
+  : parse_options_baset(
+      JBMC_OPTIONS,
+      argc,
+      argv,
+      std::string("JBMC ") + CBMC_VERSION)
 {
 }
 
@@ -88,8 +91,7 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
       JBMC_OPTIONS + extra_options,
       argc,
       argv,
-      ui_message_handler),
-    ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
+      std::string("JBMC ") + CBMC_VERSION)
 {
 }
 
@@ -134,7 +136,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_SUCCESS);
   }
 
-  parse_path_strategy_options(cmdline, options, log.get_message_handler());
+  parse_path_strategy_options(cmdline, options, ui_message_handler);
 
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
@@ -421,9 +423,7 @@ int jbmc_parse_optionst::doit()
   }
 
   messaget::eval_verbosity(
-    cmdline.get_value("verbosity"),
-    messaget::M_STATISTICS,
-    log.get_message_handler());
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // command line options
@@ -498,7 +498,7 @@ int jbmc_parse_optionst::doit()
     }
 
     language->set_language_options(options);
-    language->set_message_handler(log.get_message_handler());
+    language->set_message_handler(ui_message_handler);
 
     log.status() << "Parsing " << filename << messaget::eom;
 
@@ -747,7 +747,7 @@ void jbmc_parse_optionst::process_goto_function(
     goto_function,
     symbol_table,
     *class_hierarchy,
-    log.get_message_handler());
+    ui_message_handler);
   // Java virtual functions -> explicit dispatch tables:
   remove_virtual_functions(function);
 
@@ -851,7 +851,6 @@ bool jbmc_parse_optionst::show_loaded_functions(
     show_goto_functions(
       ns,
       ui_message_handler,
-      ui_message_handler.get_ui(),
       goto_model.get_goto_functions(),
       cmdline.isset("list-goto-functions"));
     return true;
@@ -860,11 +859,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
   if(cmdline.isset("show-properties"))
   {
     namespacet ns(goto_model.get_symbol_table());
-    show_properties(
-      ns,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      goto_model.get_goto_functions());
+    show_properties(ns, ui_message_handler, goto_model.get_goto_functions());
     return true;
   }
 
@@ -887,8 +882,7 @@ bool jbmc_parse_optionst::process_goto_functions(
     return false;
 
   // remove catch and throw
-  remove_exceptions(
-    goto_model, *class_hierarchy.get(), log.get_message_handler());
+  remove_exceptions(goto_model, *class_hierarchy.get(), ui_message_handler);
 
   // instrument library preconditions
   instrument_preconditions(goto_model);
@@ -910,7 +904,7 @@ bool jbmc_parse_optionst::process_goto_functions(
   {
     // Entry point will have been set before and function pointers removed
     log.status() << "Removing unused functions" << messaget::eom;
-    remove_unused_functions(goto_model, log.get_message_handler());
+    remove_unused_functions(goto_model, ui_message_handler);
   }
 
   // remove skips such that trivial GOTOs are deleted

jbmc/src/jbmc/jbmc_parse_options.h

@@ -117,7 +117,6 @@ class jbmc_parse_optionst : public parse_options_baset
     bool body_available);
 
 protected:
-  ui_message_handlert ui_message_handler;
   java_object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -62,8 +62,11 @@ Author: Peter Schrammel
 #include <goto-diff/unified_diff.h>
 
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
-  : parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler),
-    ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION)
+  : parse_options_baset(
+      JDIFF_OPTIONS,
+      argc,
+      argv,
+      std::string("JDIFF ") + CBMC_VERSION)
 {
 }
 
@@ -224,15 +227,9 @@ int jdiff_parse_optionst::doit()
     cmdline.isset("list-goto-functions"))
   {
     show_goto_functions(
-      goto_model1,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
     show_goto_functions(
-      goto_model2,
-      log.get_message_handler(),
-      ui_message_handler.get_ui(),
-      cmdline.isset("list-goto-functions"));
+      goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -277,18 +274,18 @@ bool jdiff_parse_optionst::process_goto_program(
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
-      log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));
+      ui_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, log.get_message_handler());
+    remove_exceptions_using_instanceof(goto_model, ui_message_handler);
 
     // Java instanceof -> clsid comparison:
     class_hierarchyt class_hierarchy(goto_model.symbol_table);
-    remove_instanceof(goto_model, class_hierarchy, log.get_message_handler());
+    remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
 
     mm_io(goto_model);
 
@@ -321,10 +318,9 @@ bool jdiff_parse_optionst::process_goto_program(
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
-      const auto cover_config = get_cover_config(
-        options, goto_model.symbol_table, log.get_message_handler());
-      if(instrument_cover_goals(
-           cover_config, goto_model, log.get_message_handler()))
+      const auto cover_config =
+        get_cover_config(options, goto_model.symbol_table, ui_message_handler);
+      if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
         return true;
     }
 

jbmc/src/jdiff/jdiff_parse_options.h

@@ -49,7 +49,6 @@ class jdiff_parse_optionst : public parse_options_baset
   jdiff_parse_optionst(int argc, const char **argv);
 
 protected:
-  ui_message_handlert ui_message_handler;
   void register_languages();
 
   void get_command_line_options(optionst &options);