janalyzer_parse_options is not a message

In addition this class already inherits a messaget object of type messaget.

Author: romainbrenguier

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -59,7 +59,6 @@ Author: Daniel Kroening, [email protected]
 
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler),
-    messaget(ui_message_handler),
     ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
 {
 }
@@ -260,7 +259,7 @@ void janalyzer_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);
       }
     }
@@ -343,21 +342,21 @@ int janalyzer_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() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8
+  log.status() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8
            << "-bit " << config.this_architecture() << " "
-           << config.this_operating_system() << eom;
+           << config.this_operating_system() << messaget::eom;
 
   register_languages();
 
   if(cmdline.args.size() > 1)
   {
-    error() << "Only one .class, .jar or .gbf file should be directly "
+    log.error() << "Only one .class, .jar or .gbf file should be directly "
       "specified on the command-line. To force loading another another class "
       "use '--java-load-class somepackage.SomeClass' or "
       "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along "
@@ -367,7 +366,7 @@ int janalyzer_parse_optionst::doit()
   }
 
   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;
@@ -386,7 +385,7 @@ int janalyzer_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;
@@ -404,14 +403,14 @@ int janalyzer_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);
+        goto_model, taint_file, log.get_message_handler(), false, json_file);
       return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
     }
   }
@@ -432,7 +431,7 @@ int janalyzer_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;
       }
 
@@ -457,7 +456,7 @@ int janalyzer_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;
       }
 
@@ -482,7 +481,7 @@ int janalyzer_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;
       }
 
@@ -513,7 +512,7 @@ int janalyzer_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;
   }
 
@@ -532,28 +531,28 @@ int janalyzer_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"
+      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;
     if(options.get_bool_option("show"))
     {
@@ -563,12 +562,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
     else if(options.get_bool_option("verify"))
     {
       result = static_verifier(
-        goto_model, *analyzer, options, get_message_handler(), out);
+        goto_model, *analyzer, options, log.get_message_handler(), out);
     }
     else if(options.get_bool_option("simplify"))
     {
       result = static_simplifier(
-        goto_model, *analyzer, options, get_message_handler(), out);
+        goto_model, *analyzer, options, log.get_message_handler(), out);
     }
     else if(options.get_bool_option("unreachable-instructions"))
     {
@@ -587,7 +586,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
     }
     else
     {
-      error() << "Unhandled task" << eom;
+      log.error() << "Unhandled task" << messaget::eom;
       return CPROVER_EXIT_INTERNAL_ERROR;
     }
 
@@ -596,7 +595,7 @@ int janalyzer_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;
 }
 
@@ -605,23 +604,23 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
   try
   {
     // 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());
 
     // 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
@@ -630,7 +629,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     remove_complex(goto_model);
 
     // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
+    log.status() << "Generic Property Instrumentation" << messaget::eom;
     goto_check(options, goto_model);
 
     // recalculate numbers, etc.
@@ -642,13 +641,13 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 
   catch(const char *e)
   {
-    error() << e << eom;
+    log.error() << e << messaget::eom;
     return true;
   }
 
   catch(const std::string &e)
   {
-    error() << e << eom;
+    log.error() << e << messaget::eom;
     return true;
   }
 
@@ -659,7 +658,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 
   catch(const std::bad_alloc &)
   {
-    error() << "Out of memory" << eom;
+    log.error() << "Out of memory" << messaget::eom;
     return true;
   }
 

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -150,7 +150,7 @@ class optionst;
   JAVA_BYTECODE_LANGUAGE_OPTIONS
 // clang-format on
 
-class janalyzer_parse_optionst : public parse_options_baset, public messaget
+class janalyzer_parse_optionst : public parse_options_baset
 {
 public:
   virtual int doit() override;