diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 492c859c88d..0bda5470a06 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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 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 diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 02cbaa59ce6..ee063e657e4 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/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;