From 4268bee456c9d93756cc43b25e92a7d3c2419715 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 16 Apr 2019 07:39:28 +0100 Subject: [PATCH 1/7] Remove redundant get_ui() method ui_message_handler.get_ui() already does the same thing, and is more explicit. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 5 +++-- jbmc/src/janalyzer/janalyzer_parse_options.h | 5 ----- src/goto-analyzer/goto_analyzer_parse_options.cpp | 5 +++-- src/goto-analyzer/goto_analyzer_parse_options.h | 5 ----- src/goto-instrument/goto_instrument_parse_options.cpp | 9 +++++---- src/goto-instrument/goto_instrument_parse_options.h | 5 ----- 6 files changed, 11 insertions(+), 23 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 77dd822eac5..04578e70ade 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -389,7 +389,7 @@ int janalyzer_parse_optionst::doit() show_goto_functions( goto_model, log.get_message_handler(), - get_ui(), + ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } @@ -519,7 +519,8 @@ 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, log.get_message_handler(), ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index 3140a94f72a..f2ffed0966d 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -171,11 +171,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 diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 0bda5470a06..ae371b7e005 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -424,7 +424,7 @@ int goto_analyzer_parse_optionst::doit() show_goto_functions( goto_model, log.get_message_handler(), - get_ui(), + ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } @@ -553,7 +553,8 @@ int goto_analyzer_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, log.get_message_handler(), ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index ee063e657e4..47affefd3af 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -174,11 +174,6 @@ class goto_analyzer_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_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a16a95021cc..003af398843 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -268,7 +268,7 @@ int goto_instrument_parse_optionst::doit() namespacet ns(goto_model.symbol_table); value_set_analysist value_set_analysis(ns); value_set_analysis(goto_model.goto_functions); - show_value_sets(get_ui(), goto_model, value_set_analysis); + show_value_sets(ui_message_handler.get_ui(), goto_model, value_set_analysis); return CPROVER_EXIT_SUCCESS; } @@ -564,7 +564,8 @@ int goto_instrument_parse_optionst::doit() cmdline.isset("show-properties")) { const namespacet ns(goto_model.symbol_table); - show_properties(goto_model, log.get_message_handler(), get_ui()); + show_properties( + goto_model, log.get_message_handler(), ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -584,7 +585,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_model); + show_loop_ids(ui_message_handler.get_ui(), goto_model); return CPROVER_EXIT_SUCCESS; } @@ -637,7 +638,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-locations")) { - show_locations(get_ui(), goto_model); + show_locations(ui_message_handler.get_ui(), goto_model); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index e5b0b6c9e4c..e3e5da49dcd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -147,11 +147,6 @@ class goto_instrument_parse_optionst : public parse_options_baset bool remove_returns_done; goto_modelt goto_model; - - ui_message_handlert::uit get_ui() - { - return ui_message_handler.get_ui(); - } }; #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H From 436274f911cf0dc10cd85f834574e25d20198f36 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Apr 2019 07:30:31 +0100 Subject: [PATCH 2/7] Make parse_options_baset the owner of message_handler The message handler field was owned by the classes inheriting from parse_options_baset which lead to strange patterns where the handler reference was initialized using a reference to a field which was not constructed yet. This is cleaner and avoid some reference duplications. --- .../src/janalyzer/janalyzer_parse_options.cpp | 7 +- jbmc/src/janalyzer/janalyzer_parse_options.h | 1 - jbmc/src/jbmc/jbmc_parse_options.cpp | 10 ++- jbmc/src/jbmc/jbmc_parse_options.h | 1 - jbmc/src/jdiff/jdiff_parse_options.cpp | 7 +- jbmc/src/jdiff/jdiff_parse_options.h | 1 - src/cbmc/cbmc_parse_options.cpp | 14 ++-- src/cbmc/cbmc_parse_options.h | 1 - .../goto_analyzer_parse_options.cpp | 7 +- .../goto_analyzer_parse_options.h | 1 - src/goto-diff/goto_diff_parse_options.cpp | 7 +- src/goto-diff/goto_diff_parse_options.h | 1 - src/goto-harness/goto_harness_main.cpp | 3 +- .../goto_harness_parse_options.cpp | 6 +- src/goto-harness/goto_harness_parse_options.h | 2 - .../goto_instrument_parse_options.cpp | 73 ++++++++----------- .../goto_instrument_parse_options.h | 4 +- src/util/parse_options.cpp | 11 ++- src/util/parse_options.h | 8 +- 19 files changed, 82 insertions(+), 83 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 04578e70ade..c19309983ed 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -58,8 +58,11 @@ Author: Daniel Kroening, kroening@kroening.com #include 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) { } diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index f2ffed0966d..dc9af92502f 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/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(); diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 61dc2bef46f..34ffd0ac76c 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -75,8 +75,11 @@ Author: Daniel Kroening, kroening@kroening.com #include 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) { } diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index b2685cab415..2fa213baf1a 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/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; diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 61e13fe60a9..9e7a71b026f 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -62,8 +62,11 @@ Author: Peter Schrammel #include 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) { } diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index fcb144b43b0..c5d4fe736f4 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/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); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2558212b9b0..ca4c268c316 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -83,9 +83,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "xml_interface.h" cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv) - : parse_options_baset(CBMC_OPTIONS, argc, argv, ui_message_handler), - xml_interfacet(cmdline), - ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) + : parse_options_baset( + CBMC_OPTIONS, + argc, + argv, + std::string("CBMC ") + CBMC_VERSION), + xml_interfacet(cmdline) { } @@ -97,9 +100,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( CBMC_OPTIONS + extra_options, argc, argv, - ui_message_handler), - xml_interfacet(cmdline), - ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) + std::string("CBMC ") + CBMC_VERSION), + xml_interfacet(cmdline) { } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index bc9ef50440c..0d8d8f2fea5 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -111,7 +111,6 @@ class cbmc_parse_optionst : public parse_options_baset, public xml_interfacet protected: goto_modelt goto_model; - ui_message_handlert ui_message_handler; void register_languages(); void get_command_line_options(optionst &); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index ae371b7e005..c154c4d56e5 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -69,8 +69,11 @@ Author: Daniel Kroening, kroening@kroening.com goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( int argc, const char **argv) - : parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv, ui_message_handler), - ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION) + : parse_options_baset( + GOTO_ANALYSER_OPTIONS, + argc, + argv, + std::string("GOTO-ANALYZER ")) { } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 47affefd3af..3ef39630b76 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -162,7 +162,6 @@ class goto_analyzer_parse_optionst: public parse_options_baset goto_analyzer_parse_optionst(int argc, const char **argv); protected: - ui_message_handlert ui_message_handler; goto_modelt goto_model; virtual void register_languages(); diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index a85ed2c1c78..66cf0831cfe 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -64,8 +64,11 @@ Author: Peter Schrammel #include "change_impact.h" goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv) - : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, ui_message_handler), - ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION) + : parse_options_baset( + GOTO_DIFF_OPTIONS, + argc, + argv, + std::string("GOTO-DIFF ") + CBMC_VERSION) { } diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index a350d061bf5..e46977d2fac 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -48,7 +48,6 @@ class goto_diff_parse_optionst : public parse_options_baset goto_diff_parse_optionst(int argc, const char **argv); protected: - ui_message_handlert ui_message_handler; void register_languages(); void get_command_line_options(optionst &options); diff --git a/src/goto-harness/goto_harness_main.cpp b/src/goto-harness/goto_harness_main.cpp index 285970764df..7e9eb28fa5f 100644 --- a/src/goto-harness/goto_harness_main.cpp +++ b/src/goto-harness/goto_harness_main.cpp @@ -10,6 +10,5 @@ Author: Diffblue Ltd. int main(int argc, const char *argv[]) { - auto parse_options = goto_harness_parse_optionst(argc, argv); - return parse_options.main(); + return goto_harness_parse_optionst{argc, argv}.main(); } diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 4a55b659cf0..f671ec11673 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -126,8 +126,10 @@ void goto_harness_parse_optionst::help() goto_harness_parse_optionst::goto_harness_parse_optionst( int argc, const char *argv[]) - : parse_options_baset{GOTO_HARNESS_OPTIONS, argc, argv, ui_message_handler}, - ui_message_handler(cmdline, std::string("GOTO-HARNESS ") + CBMC_VERSION) + : parse_options_baset{GOTO_HARNESS_OPTIONS, + argc, + argv, + std::string("GOTO-HARNESS ") + CBMC_VERSION} { } diff --git a/src/goto-harness/goto_harness_parse_options.h b/src/goto-harness/goto_harness_parse_options.h index c611d75e70b..edcf045bff8 100644 --- a/src/goto-harness/goto_harness_parse_options.h +++ b/src/goto-harness/goto_harness_parse_options.h @@ -45,8 +45,6 @@ class goto_harness_parse_optionst : public parse_options_baset irep_idt harness_function_name; }; - ui_message_handlert ui_message_handler; - /// Handle command line arguments that are common to all /// harness generators. goto_harness_configt handle_common_options(); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 003af398843..b5bfdd78310 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -268,7 +268,8 @@ int goto_instrument_parse_optionst::doit() namespacet ns(goto_model.symbol_table); value_set_analysist value_set_analysis(ns); value_set_analysis(goto_model.goto_functions); - show_value_sets(ui_message_handler.get_ui(), goto_model, value_set_analysis); + show_value_sets( + ui_message_handler.get_ui(), goto_model, value_set_analysis); return CPROVER_EXIT_SUCCESS; } @@ -345,7 +346,7 @@ int goto_instrument_parse_optionst::doit() do_remove_returns(); parameter_assignments(goto_model); - remove_unused_functions(goto_model, log.get_message_handler()); + remove_unused_functions(goto_model, ui_message_handler); if(!cmdline.isset("inline")) { @@ -385,7 +386,7 @@ int goto_instrument_parse_optionst::doit() do_remove_returns(); parameter_assignments(goto_model); - remove_unused_functions(goto_model, log.get_message_handler()); + remove_unused_functions(goto_model, ui_message_handler); if(!cmdline.isset("inline")) { @@ -556,7 +557,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("interpreter")) { log.status() << "Starting interpreter" << messaget::eom; - interpreter(goto_model, log.get_message_handler()); + interpreter(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } @@ -565,7 +566,7 @@ int goto_instrument_parse_optionst::doit() { const namespacet ns(goto_model.symbol_table); show_properties( - goto_model, log.get_message_handler(), ui_message_handler.get_ui()); + goto_model, ui_message_handler, ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -617,7 +618,7 @@ int goto_instrument_parse_optionst::doit() { show_goto_functions( goto_model, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -761,7 +762,7 @@ int goto_instrument_parse_optionst::doit() namespacet ns(goto_model.symbol_table); log.status() << "Performing full inlining" << messaget::eom; - goto_inline(goto_model, log.get_message_handler()); + goto_inline(goto_model, ui_message_handler); log.status() << "Removing calls to functions without a body" << messaget::eom; @@ -771,10 +772,7 @@ int goto_instrument_parse_optionst::doit() log.status() << "Accelerating" << messaget::eom; guard_managert guard_manager; accelerate_functions( - goto_model, - log.get_message_handler(), - cmdline.isset("z3"), - guard_manager); + goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager); remove_skip(goto_model); } @@ -827,8 +825,7 @@ int goto_instrument_parse_optionst::doit() log.status() << "Writing GOTO program to `" << cmdline.args[1] << "'" << messaget::eom; - if(write_goto_binary( - cmdline.args[1], goto_model, log.get_message_handler())) + if(write_goto_binary(cmdline.args[1], goto_model, ui_message_handler)) return CPROVER_EXIT_CONVERSION_FAILED; else return CPROVER_EXIT_SUCCESS; @@ -858,7 +855,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( log.status() << "Function Pointer Removal" << messaget::eom; remove_function_pointers( - log.get_message_handler(), goto_model, cmdline.isset("pointer-check")); + ui_message_handler, goto_model, cmdline.isset("pointer-check")); log.status() << "Virtual function removal" << messaget::eom; remove_virtual_functions(goto_model); log.status() << "Cleaning inline assembler statements" << messaget::eom; @@ -879,7 +876,7 @@ void goto_instrument_parse_optionst::do_remove_const_function_pointers_only() log.status() << "Removing const function pointers only" << messaget::eom; remove_function_pointers( - log.get_message_handler(), + ui_message_handler, goto_model, cmdline.isset("pointer-check"), true); // abort if we can't resolve via const pointers @@ -917,7 +914,7 @@ void goto_instrument_parse_optionst::get_goto_program() config.set(cmdline); - auto result = read_goto_binary(cmdline.args[0], log.get_message_handler()); + auto result = read_goto_binary(cmdline.args[0], ui_message_handler); if(!result.has_value()) throw 0; @@ -974,9 +971,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() { log.status() << "Adding gotos to skip loops" << messaget::eom; if(skip_loops( - goto_model, - cmdline.get_value("skip-loops"), - log.get_message_handler())) + goto_model, cmdline.get_value("skip-loops"), ui_message_handler)) throw 0; } @@ -990,7 +985,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() log.status() << "Adding up to " << max_argc << " command line arguments" << messaget::eom; - if(model_argc_argv(goto_model, max_argc, log.get_message_handler())) + if(model_argc_argv(goto_model, max_argc, ui_message_handler)) throw 0; } @@ -999,7 +994,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() remove_functions( goto_model, cmdline.get_values("remove-function-body"), - log.get_message_handler()); + ui_message_handler); } // we add the library in some cases, as some analyses benefit @@ -1018,9 +1013,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom; link_to_library( - goto_model, log.get_message_handler(), cprover_cpp_library_factory); - link_to_library( - goto_model, log.get_message_handler(), cprover_c_library_factory); + goto_model, ui_message_handler, cprover_cpp_library_factory); + link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); } // now do full inlining, if requested @@ -1037,7 +1031,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() } log.status() << "Performing full inlining" << messaget::eom; - goto_inline(goto_model, log.get_message_handler(), true); + goto_inline(goto_model, ui_message_handler, true); } if(cmdline.isset("show-custom-bitvector-analysis") || @@ -1063,7 +1057,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() escape_analysis.instrument(goto_model); // inline added functions, they are often small - goto_partial_inline(goto_model, log.get_message_handler()); + goto_partial_inline(goto_model, ui_message_handler); // recalculate numbers, etc. goto_model.goto_functions.update(); @@ -1109,24 +1103,15 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(!cmdline.isset("log")) { goto_function_inline( - goto_model, - function, - ui_message_handler, - true, - caching); + goto_model, function, ui_message_handler, true, caching); } else { std::string filename=cmdline.get_value("log"); bool have_file=!filename.empty() && filename!="-"; - jsont result= - goto_function_inline_and_log( - goto_model, - function, - ui_message_handler, - true, - caching); + jsont result = goto_function_inline_and_log( + goto_model, function, ui_message_handler, true, caching); if(have_file) { @@ -1195,12 +1180,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.get_value("generate-function-body-options"), object_factory_parameters, goto_model.symbol_table, - log.get_message_handler()); + ui_message_handler); generate_function_bodies( std::regex(cmdline.get_value("generate-function-body")), *generate_implementation, goto_model, - log.get_message_handler()); + ui_message_handler); } // add generic checks, if needed @@ -1246,7 +1231,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_remove_returns(); log.status() << "String Abstraction" << messaget::eom; - string_abstraction(goto_model, log.get_message_handler()); + string_abstraction(goto_model, ui_message_handler); } // some analyses require function pointer removal and partial inlining @@ -1359,7 +1344,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.isset("render-cluster-function"), cmdline.isset("cav11"), cmdline.isset("hide-internals"), - log.get_message_handler(), + ui_message_handler, cmdline.isset("ignore-arrays")); } @@ -1508,7 +1493,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions, callercallee, goto_model.symbol_table, - log.get_message_handler())) + ui_message_handler)) throw 0; } @@ -1522,7 +1507,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() slice_global_inits(goto_model); log.status() << "Performing an aggressive slice" << messaget::eom; - aggressive_slicert aggressive_slicer(goto_model, log.get_message_handler()); + aggressive_slicert aggressive_slicer(goto_model, ui_message_handler); if(cmdline.isset("aggressive-slice-call-depth")) aggressive_slicer.call_depth = diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index e3e5da49dcd..ba46d872ed9 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -122,8 +122,7 @@ class goto_instrument_parse_optionst : public parse_options_baset GOTO_INSTRUMENT_OPTIONS, argc, argv, - ui_message_handler), - ui_message_handler(cmdline, "goto-instrument"), + "goto-instrument"), function_pointer_removal_done(false), partial_inlining_done(false), remove_returns_done(false) @@ -131,7 +130,6 @@ class goto_instrument_parse_optionst : public parse_options_baset } protected: - ui_message_handlert ui_message_handler; void register_languages(); void get_goto_program(); diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 67d04c6b697..f31d737905f 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -28,11 +28,14 @@ parse_options_baset::parse_options_baset( const std::string &_optstring, int argc, const char **argv, - message_handlert &mh) - : log(mh) + const std::string &program) + : parse_result(cmdline.parse( + argc, + argv, + (std::string("?h(help)") + _optstring).c_str())), + ui_message_handler(cmdline, program), + log(ui_message_handler) { - std::string optstring=std::string("?h(help)")+_optstring; - parse_result=cmdline.parse(argc, argv, optstring.c_str()); // DO NOT USE log HERE! // diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 54bac8c4bc8..6cfdbcf9ad9 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "cmdline.h" #include "message.h" +#include "ui_message.h" class parse_options_baset { @@ -22,7 +23,7 @@ class parse_options_baset const std::string &optstring, int argc, const char **argv, - message_handlert &mh); + const std::string &program); cmdlinet cmdline; @@ -34,12 +35,15 @@ class parse_options_baset virtual int main(); virtual ~parse_options_baset() { } +private: + bool parse_result; + protected: + ui_message_handlert ui_message_handler; messaget log; private: void unknown_option_msg(); - bool parse_result; }; std::string From 0d9f7517d2e072f3101083b0b94891875660e900 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Apr 2019 08:23:32 +0100 Subject: [PATCH 3/7] Remove comment made unecessary Now the log field gets initialized before parse_options_baset is constructed so there is no danger as described in the comment. --- src/util/parse_options.cpp | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index f31d737905f..c1bece29bab 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -36,18 +36,6 @@ parse_options_baset::parse_options_baset( ui_message_handler(cmdline, program), log(ui_message_handler) { - - // DO NOT USE log HERE! - // - // The usual pattern of use is that the application class inherits from - // messaget and parse_options_baset using a member variable of type - // message_handlert to construct the messaget part. - // - // C++'s rules of initialisation mean that the constructors for - // messaget and then parse_options_base run before those of message_handlert. - // This means that the message_handlert object is uninitialised. - // Using it here will likely cause a hard to debug failure somewhere in - // the messaget code. } void parse_options_baset::help() From edd2c654e20e751928979ab11fce3f516cb7529e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 16 Apr 2019 08:34:07 +0100 Subject: [PATCH 4/7] Replace log.get_message_handler() calls The calls will always return a reference to the field ui_message_handler which can be accessed directly instead. --- .../src/janalyzer/janalyzer_parse_options.cpp | 22 +++++++++---------- jbmc/src/jbmc/jbmc_parse_options.cpp | 17 ++++++-------- jbmc/src/jdiff/jdiff_parse_options.cpp | 17 +++++++------- src/cbmc/cbmc_parse_options.cpp | 8 +++---- .../goto_analyzer_parse_options.cpp | 20 ++++++++--------- src/goto-diff/goto_diff_parse_options.cpp | 18 +++++++-------- .../goto_harness_parse_options.cpp | 4 ++-- .../goto_instrument_parse_options.cpp | 3 +-- 8 files changed, 49 insertions(+), 60 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index c19309983ed..86ec50959c3 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -371,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; @@ -391,7 +390,7 @@ int janalyzer_parse_optionst::doit() { show_goto_functions( goto_model, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -409,15 +408,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; } } @@ -523,7 +521,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { show_properties( - goto_model, log.get_message_handler(), ui_message_handler.get_ui()); + goto_model, ui_message_handler, ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -574,12 +572,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")) { @@ -620,18 +618,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; diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 34ffd0ac76c..06e8627f054 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -136,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); @@ -423,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 @@ -500,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; @@ -749,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); @@ -864,7 +862,7 @@ bool jbmc_parse_optionst::show_loaded_functions( namespacet ns(goto_model.get_symbol_table()); show_properties( ns, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), goto_model.get_goto_functions()); return true; @@ -889,8 +887,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); @@ -912,7 +909,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 diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 9e7a71b026f..dd847f74db9 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -228,12 +228,12 @@ int jdiff_parse_optionst::doit() { show_goto_functions( goto_model1, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); show_goto_functions( goto_model2, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -280,18 +280,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); @@ -324,10 +324,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; } diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ca4c268c316..0e0a8195ce7 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -486,7 +486,7 @@ int cbmc_parse_optionst::doit() register_languages(); if(cmdline.isset("test-preprocessor")) - return test_c_preprocessor(log.get_message_handler()) + return test_c_preprocessor(ui_message_handler) ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED : CPROVER_EXIT_SUCCESS; @@ -532,7 +532,7 @@ int cbmc_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; @@ -556,7 +556,7 @@ int cbmc_parse_optionst::doit() cmdline.isset("show-properties")) // use this one { show_properties( - goto_model, log.get_message_handler(), ui_message_handler.get_ui()); + goto_model, ui_message_handler, ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -774,7 +774,7 @@ void cbmc_parse_optionst::preprocessing(const optionst &options) return; } - language->set_message_handler(log.get_message_handler()); + language->set_message_handler(ui_message_handler); if(language->preprocess(infile, filename, std::cout)) log.error() << "PREPROCESSING ERROR" << messaget::eom; diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index c154c4d56e5..67bdfc0f484 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -401,8 +401,7 @@ int goto_analyzer_parse_optionst::doit() register_languages(); - 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; @@ -426,7 +425,7 @@ int goto_analyzer_parse_optionst::doit() { show_goto_functions( goto_model, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -446,15 +445,14 @@ int goto_analyzer_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; } } @@ -557,7 +555,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { show_properties( - goto_model, log.get_message_handler(), ui_message_handler.get_ui()); + goto_model, ui_message_handler, ui_message_handler.get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -611,13 +609,13 @@ 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, log.get_message_handler()); + show_on_source(goto_model, *analyzer, ui_message_handler); return CPROVER_EXIT_SUCCESS; } 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")) { @@ -625,7 +623,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) output_stream.close(); output_stream.open(outfile, std::ios::binary); 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")) { @@ -685,7 +683,7 @@ bool goto_analyzer_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")); // do partial inlining log.status() << "Partial Inlining" << messaget::eom; diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 66cf0831cfe..8871a839c1e 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -266,12 +266,12 @@ int goto_diff_parse_optionst::doit() { show_goto_functions( goto_model1, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); show_goto_functions( goto_model2, - log.get_message_handler(), + ui_message_handler, ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -326,15 +326,14 @@ bool goto_diff_parse_optionst::process_goto_program( log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom; link_to_library( - goto_model, log.get_message_handler(), cprover_cpp_library_factory); - link_to_library( - goto_model, log.get_message_handler(), cprover_c_library_factory); + goto_model, ui_message_handler, cprover_cpp_library_factory); + link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); // remove function pointers log.status() << "Removal of 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")); mm_io(goto_model); @@ -367,10 +366,9 @@ bool goto_diff_parse_optionst::process_goto_program( // for coverage annotation: remove_skip(goto_model); - 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; } diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index f671ec11673..343e88e8402 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -55,7 +55,7 @@ int goto_harness_parse_optionst::doit() // Read goto binary into goto-model auto read_goto_binary_result = - read_goto_binary(got_harness_config.in_file, log.get_message_handler()); + read_goto_binary(got_harness_config.in_file, ui_message_handler); if(!read_goto_binary_result.has_value()) { throw deserialization_exceptiont{"failed to read goto program from file `" + @@ -89,7 +89,7 @@ int goto_harness_parse_optionst::doit() // Write end result to new goto-binary if(write_goto_binary( - got_harness_config.out_file, goto_model, log.get_message_handler())) + got_harness_config.out_file, goto_model, ui_message_handler)) { throw system_exceptiont{"failed to write goto program from file `" + got_harness_config.out_file + "'"}; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index b5bfdd78310..d17c3c82df1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -809,8 +809,7 @@ int goto_instrument_parse_optionst::doit() do_indirect_call_and_rtti_removal(); log.status() << "Removing unused functions" << messaget::eom; - remove_unused_functions( - goto_model.goto_functions, log.get_message_handler()); + remove_unused_functions(goto_model.goto_functions, ui_message_handler); } if(cmdline.isset("undefined-function-is-assume-false")) From 1d09894a7d7f024ae52759c2ccc828881bfcfd25 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 17 Apr 2019 09:07:30 +0100 Subject: [PATCH 5/7] Remove unecessary log argument in cbmc_parse_optionst The messaget can be constructed from the message_handler. --- src/cbmc/cbmc_parse_options.cpp | 8 ++++---- src/cbmc/cbmc_parse_options.h | 1 - unit/compound_block_locations.cpp | 2 +- unit/path_strategies.cpp | 2 +- 4 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 0e0a8195ce7..0673f9dc2e9 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -547,7 +547,7 @@ int cbmc_parse_optionst::doit() } int get_goto_program_ret = - get_goto_program(goto_model, options, cmdline, log, ui_message_handler); + get_goto_program(goto_model, options, cmdline, ui_message_handler); if(get_goto_program_ret!=-1) return get_goto_program_ret; @@ -692,12 +692,12 @@ int cbmc_parse_optionst::get_goto_program( goto_modelt &goto_model, const optionst &options, const cmdlinet &cmdline, - messaget &log, ui_message_handlert &ui_message_handler) { + messaget log{ui_message_handler}; if(cmdline.args.empty()) { - log.error() << "Please provide a program to verify" << log.eom; + log.error() << "Please provide a program to verify" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } @@ -739,7 +739,7 @@ int cbmc_parse_optionst::get_goto_program( return CPROVER_EXIT_SUCCESS; } - log.status() << config.object_bits_info() << log.eom; + log.status() << config.object_bits_info() << messaget::eom; } return -1; // no error, continue diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 0d8d8f2fea5..c5cae07c4c6 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -106,7 +106,6 @@ class cbmc_parse_optionst : public parse_options_baset, public xml_interfacet goto_modelt &, const optionst &, const cmdlinet &, - messaget &, ui_message_handlert &); protected: diff --git a/unit/compound_block_locations.cpp b/unit/compound_block_locations.cpp index 1365ab8e51e..e71679b04ba 100644 --- a/unit/compound_block_locations.cpp +++ b/unit/compound_block_locations.cpp @@ -289,7 +289,7 @@ void compound_block_locationst::check_compound_block_locations( goto_modelt gm; int ret; - ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh); + ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, mh); REQUIRE(ret == -1); const auto found = gm.goto_functions.function_map.find("main"); diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 6061077a615..6d8ddd0248c 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -398,7 +398,7 @@ void _check_with_strategy( goto_modelt goto_model; int ret; ret = cbmc_parse_optionst::get_goto_program( - goto_model, options, cmdline, log, ui_message_handler); + goto_model, options, cmdline, ui_message_handler); REQUIRE(ret == -1); symbol_tablet symex_symbol_table; From 747e13b33b3675bf2aeb2e3d9462c89c38b63953 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 17 Apr 2019 09:10:32 +0100 Subject: [PATCH 6/7] Show properties take a ui_message_handlert This is more precise on the type of message handler we are expecting and makes the ui argument redundant. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 3 +-- jbmc/src/jbmc/jbmc_parse_options.cpp | 6 +----- src/cbmc/cbmc_parse_options.cpp | 3 +-- .../goto_analyzer_parse_options.cpp | 3 +-- .../goto_instrument_parse_options.cpp | 3 +-- src/goto-programs/show_properties.cpp | 16 ++++++++-------- src/goto-programs/show_properties.h | 6 ++---- 7 files changed, 15 insertions(+), 25 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 86ec50959c3..cb91e5f9d10 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -520,8 +520,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { - show_properties( - goto_model, ui_message_handler, ui_message_handler.get_ui()); + show_properties(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 06e8627f054..84157b93cd1 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -860,11 +860,7 @@ bool jbmc_parse_optionst::show_loaded_functions( if(cmdline.isset("show-properties")) { namespacet ns(goto_model.get_symbol_table()); - show_properties( - ns, - ui_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; } diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 0673f9dc2e9..e9cba7090ce 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -555,8 +555,7 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("show-claims") || // will go away cmdline.isset("show-properties")) // use this one { - show_properties( - goto_model, ui_message_handler, ui_message_handler.get_ui()); + show_properties(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 67bdfc0f484..ce9485ed3b5 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -554,8 +554,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { - show_properties( - goto_model, ui_message_handler, ui_message_handler.get_ui()); + show_properties(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d17c3c82df1..a78407d34cd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -565,8 +565,7 @@ int goto_instrument_parse_optionst::doit() cmdline.isset("show-properties")) { const namespacet ns(goto_model.symbol_table); - show_properties( - goto_model, ui_message_handler, ui_message_handler.get_ui()); + show_properties(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index b7172871445..a8cf43df408 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -163,25 +163,25 @@ void show_properties_json( void show_properties( const namespacet &ns, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions) { + ui_message_handlert::uit ui = ui_message_handler.get_ui(); if(ui == ui_message_handlert::uit::JSON_UI) - show_properties_json(ns, message_handler, goto_functions); + show_properties_json(ns, ui_message_handler, goto_functions); else for(const auto &fct : goto_functions.function_map) - show_properties(ns, fct.first, message_handler, ui, fct.second.body); + show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body); } void show_properties( const goto_modelt &goto_model, - message_handlert &message_handler, - ui_message_handlert::uit ui) + ui_message_handlert &ui_message_handler) { + ui_message_handlert::uit ui = ui_message_handler.get_ui(); const namespacet ns(goto_model.symbol_table); if(ui == ui_message_handlert::uit::JSON_UI) - show_properties_json(ns, message_handler, goto_model.goto_functions); + show_properties_json(ns, ui_message_handler, goto_model.goto_functions); else - show_properties(ns, message_handler, ui, goto_model.goto_functions); + show_properties(ns, ui_message_handler, goto_model.goto_functions); } diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index ea8cc46e4a7..f444f8d3e77 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -32,13 +32,11 @@ class message_handlert; void show_properties( const goto_modelt &, - message_handlert &message_handler, - ui_message_handlert::uit ui); + ui_message_handlert &ui_message_handler); void show_properties( const namespacet &ns, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions); /// \brief Returns a source_locationt that corresponds From 262cc351dd74265dded3b6e4120962dc33e5fd76 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 17 Apr 2019 09:19:51 +0100 Subject: [PATCH 7/7] show_goto_functions takes a ui_message_handler This removes the need for passing a seperate ui argument. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 5 +---- jbmc/src/jbmc/jbmc_parse_options.cpp | 1 - jbmc/src/jdiff/jdiff_parse_options.cpp | 10 ++-------- src/cbmc/cbmc_parse_options.cpp | 1 - src/goto-analyzer/goto_analyzer_parse_options.cpp | 5 +---- src/goto-diff/goto_diff_parse_options.cpp | 10 ++-------- src/goto-instrument/goto_instrument_parse_options.cpp | 5 +---- src/goto-programs/show_goto_functions.cpp | 11 +++++------ src/goto-programs/show_goto_functions.h | 10 ++++------ 9 files changed, 16 insertions(+), 42 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index cb91e5f9d10..5e661a8a38b 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -389,10 +389,7 @@ int janalyzer_parse_optionst::doit() cmdline.isset("list-goto-functions")) { show_goto_functions( - goto_model, - ui_message_handler, - ui_message_handler.get_ui(), - cmdline.isset("list-goto-functions")); + goto_model, ui_message_handler, cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 84157b93cd1..bb00a58ea98 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -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; diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index dd847f74db9..627d324152d 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -227,15 +227,9 @@ int jdiff_parse_optionst::doit() cmdline.isset("list-goto-functions")) { show_goto_functions( - goto_model1, - ui_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, - ui_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; } diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e9cba7090ce..9f8a85d91a6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -733,7 +733,6 @@ int cbmc_parse_optionst::get_goto_program( show_goto_functions( goto_model, ui_message_handler, - ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index ce9485ed3b5..8b38b9188e6 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -424,10 +424,7 @@ int goto_analyzer_parse_optionst::doit() cmdline.isset("list-goto-functions")) { show_goto_functions( - goto_model, - ui_message_handler, - ui_message_handler.get_ui(), - cmdline.isset("list-goto-functions")); + goto_model, ui_message_handler, cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 8871a839c1e..2753ec1d1ba 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -265,15 +265,9 @@ int goto_diff_parse_optionst::doit() cmdline.isset("list-goto-functions")) { show_goto_functions( - goto_model1, - ui_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, - ui_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; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a78407d34cd..c21c8935dc6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -616,10 +616,7 @@ int goto_instrument_parse_optionst::doit() cmdline.isset("list-goto-functions")) { show_goto_functions( - goto_model, - ui_message_handler, - ui_message_handler.get_ui(), - cmdline.isset("list-goto-functions")); + goto_model, ui_message_handler, cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 087a57bcbfd..d1f5c2a1b60 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -25,12 +25,12 @@ Author: Peter Schrammel void show_goto_functions( const namespacet &ns, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only) { - messaget msg(message_handler); + ui_message_handlert::uit ui = ui_message_handler.get_ui(); + messaget msg(ui_message_handler); switch(ui) { case ui_message_handlert::uit::XML_UI: @@ -82,11 +82,10 @@ void show_goto_functions( void show_goto_functions( const goto_modelt &goto_model, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, bool list_only) { const namespacet ns(goto_model.symbol_table); show_goto_functions( - ns, message_handler, ui, goto_model.goto_functions, list_only); + ns, ui_message_handler, goto_model.goto_functions, list_only); } diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h index db1510db64b..aec8c352c76 100644 --- a/src/goto-programs/show_goto_functions.h +++ b/src/goto-programs/show_goto_functions.h @@ -30,15 +30,13 @@ class goto_functionst; void show_goto_functions( const namespacet &ns, - message_handlert &message_handler, - ui_message_handlert::uit ui, + ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, - bool list_only = false); + bool list_only); void show_goto_functions( const goto_modelt &, - message_handlert &message_handler, - ui_message_handlert::uit ui, - bool list_only = false); + ui_message_handlert &ui_message_handler, + bool list_only); #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H