From 279d7ae9b69f3f410fae125e605a6332ada7b916 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 25 Jan 2019 17:24:38 +0000 Subject: [PATCH 1/5] Add a message_handlert parameter to parse_option_baset Getting parse_option_baset to use the same message_handlert as the rest of the application should mean that error message, especially those from default exception handlers will be formatted correctly. So, if you use --json-ui then the exception messages will be in JSON rather than just dumped on std::cerr. There is an issue with object constructors; as the message_handlert is a local variable in most programs, it is not initialised when it is passed as a reference. A comment explaining this problem is given and the issue is no worse than it already was. --- .../src/janalyzer/janalyzer_parse_options.cpp | 2 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 +-- jbmc/src/jdiff/jdiff_parse_options.cpp | 4 +-- src/cbmc/cbmc_parse_options.cpp | 4 +-- .../goto_analyzer_parse_options.cpp | 2 +- src/goto-diff/goto_diff_parse_options.cpp | 4 +-- .../goto_instrument_parse_options.h | 2 +- src/util/parse_options.cpp | 35 +++++++++++++------ src/util/parse_options.h | 6 +++- 9 files changed, 40 insertions(+), 23 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 90fc5790998..1ea58d745f9 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -58,7 +58,7 @@ 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), + : parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION) { diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 4ab56be7ee1..79c3826a4f2 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -70,7 +70,7 @@ 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), + : parse_options_baset(JBMC_OPTIONS, argc, argv, ui_message_handler), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION) { @@ -80,7 +80,7 @@ ::jbmc_parse_optionst::jbmc_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv), + : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv, ui_message_handler), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION) { diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 683a8d1f7c7..fcdb83e68c4 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -63,7 +63,7 @@ Author: Peter Schrammel // TODO: do not use language_uit for this; requires a refactoring of // initialize_goto_model to support parsing specific command line files jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv) - : parse_options_baset(JDIFF_OPTIONS, argc, argv), + : parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler), jdiff_languagest(cmdline, ui_message_handler, &options), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler, &options) @@ -74,7 +74,7 @@ ::jdiff_parse_optionst::jdiff_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv), + : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv, ui_message_handler), jdiff_languagest(cmdline, ui_message_handler, &options), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler, &options) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b1407a5d71e..f86a57aa3bc 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -71,7 +71,7 @@ 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), + : parse_options_baset(CBMC_OPTIONS, argc, argv, ui_message_handler), xml_interfacet(cmdline), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) @@ -82,7 +82,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv), + : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv, ui_message_handler), xml_interfacet(cmdline), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index a54e6f8b0a5..84825f590c4 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -67,7 +67,7 @@ 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), + : 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) { diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 5342c761ce0..ab6bdc9620c 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -61,7 +61,7 @@ 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), + : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, ui_message_handler), goto_diff_languagest(cmdline, ui_message_handler), ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) @@ -72,7 +72,7 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv), + : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv, ui_message_handler), goto_diff_languagest(cmdline, ui_message_handler), ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 7e70a1ff1d7..9bf7af8674e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -120,7 +120,7 @@ class goto_instrument_parse_optionst: virtual void help(); goto_instrument_parse_optionst(int argc, const char **argv): - parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv), + parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv, ui_message_handler), messaget(ui_message_handler), ui_message_handler(cmdline, "goto-instrument"), function_pointer_removal_done(false), diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 1b556f85c3f..9a1c81fea46 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -25,10 +25,23 @@ Author: Daniel Kroening, kroening@kroening.com #include "signal_catcher.h" parse_options_baset::parse_options_baset( - const std::string &_optstring, int argc, const char **argv) + const std::string &_optstring, int argc, const char **argv, message_handlert &mh) + : log(mh) { std::string optstring=std::string("?h(help)")+_optstring; parse_result=cmdline.parse(argc, argv, optstring.c_str()); + + // 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() @@ -37,7 +50,7 @@ void parse_options_baset::help() void parse_options_baset::usage_error() { - std::cerr << "Usage error!\n\n"; + log.error() << "Usage error!\n" << messaget::eom; help(); } @@ -46,7 +59,7 @@ void parse_options_baset::usage_error() void parse_options_baset::unknown_option_msg() { if(!cmdline.unknown_arg.empty()) - std::cerr << "Unknown option: " << cmdline.unknown_arg << "\n"; + log.error() << "Unknown option: " << cmdline.unknown_arg << messaget::eom; } int parse_options_baset::main() @@ -77,43 +90,43 @@ int parse_options_baset::main() // CPROVER style exceptions in order of decreasing happiness catch(const invalid_command_line_argument_exceptiont &e) { - std::cerr << e.what() << '\n'; + log.error() << e.what() << messaget::eom; return CPROVER_EXIT_USAGE_ERROR; } catch(const cprover_exception_baset &e) { - std::cerr << e.what() << '\n'; + log.error() << e.what() << messaget::eom; return CPROVER_EXIT_EXCEPTION; } catch(const std::string &e) { - std::cerr << "C++ string exception : " << e << '\n'; + log.error() << "C++ string exception : " << e << messaget::eom; return CPROVER_EXIT_EXCEPTION; } catch(const char *e) { - std::cerr << "C string exception : " << e << '\n'; + log.error() << "C string exception : " << e << messaget::eom; return CPROVER_EXIT_EXCEPTION; } catch(int e) { - std::cerr << "Numeric exception : " << e << '\n'; + log.error() << "Numeric exception : " << e << messaget::eom; return CPROVER_EXIT_EXCEPTION; } // C++ style exceptions catch(const std::bad_alloc &) { - std::cerr << "Out of memory" << '\n'; + log.error() << "Out of memory" << messaget::eom; return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; } catch(const std::exception &e) { - std::cerr << e.what() << '\n'; + log.error() << e.what() << messaget::eom; return CPROVER_EXIT_EXCEPTION; } catch(...) { - std::cerr << "Unknown exception type!" << '\n'; + log.error() << "Unknown exception type!" << messaget::eom; return CPROVER_EXIT_EXCEPTION; } } diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 304657c6879..ca9ba213a45 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -13,12 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "cmdline.h" +#include "message.h" class parse_options_baset { public: parse_options_baset( - const std::string &optstring, int argc, const char **argv); + const std::string &optstring, int argc, const char **argv, message_handlert &mh); cmdlinet cmdline; @@ -30,6 +31,9 @@ class parse_options_baset virtual int main(); virtual ~parse_options_baset() { } +protected: + messaget log; + private: void unknown_option_msg(); bool parse_result; From b9f5585e434c386fa6bbb960361638a3cc8ad8c3 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 25 Jan 2019 20:00:32 +0000 Subject: [PATCH 2/5] An offering of whitespace to the clang-format gods This is just the reformattings required by the previous commit. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 6 +++++- jbmc/src/jdiff/jdiff_parse_options.cpp | 6 +++++- src/cbmc/cbmc_parse_options.cpp | 6 +++++- src/goto-diff/goto_diff_parse_options.cpp | 6 +++++- .../goto_instrument_parse_options.h | 18 +++++++++++------- src/util/parse_options.cpp | 5 ++++- src/util/parse_options.h | 5 ++++- 7 files changed, 39 insertions(+), 13 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 79c3826a4f2..c63ab8bc219 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -80,7 +80,11 @@ ::jbmc_parse_optionst::jbmc_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv, ui_message_handler), + : parse_options_baset( + JBMC_OPTIONS + extra_options, + argc, + argv, + ui_message_handler), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION) { diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index fcdb83e68c4..1b5c824e8dd 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -74,7 +74,11 @@ ::jdiff_parse_optionst::jdiff_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv, ui_message_handler), + : parse_options_baset( + JDIFF_OPTIONS + extra_options, + argc, + argv, + ui_message_handler), jdiff_languagest(cmdline, ui_message_handler, &options), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler, &options) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index f86a57aa3bc..20060bbeeda 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -82,7 +82,11 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv, ui_message_handler), + : parse_options_baset( + CBMC_OPTIONS + extra_options, + argc, + argv, + ui_message_handler), xml_interfacet(cmdline), messaget(ui_message_handler), ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index ab6bdc9620c..c86b1199b1f 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -72,7 +72,11 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst( int argc, const char **argv, const std::string &extra_options) - : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv, ui_message_handler), + : parse_options_baset( + GOTO_DIFF_OPTIONS + extra_options, + argc, + argv, + ui_message_handler), goto_diff_languagest(cmdline, ui_message_handler), ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 9bf7af8674e..3c26973c8c1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -119,13 +119,17 @@ class goto_instrument_parse_optionst: virtual int doit(); virtual void help(); - goto_instrument_parse_optionst(int argc, const char **argv): - parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv, ui_message_handler), - messaget(ui_message_handler), - ui_message_handler(cmdline, "goto-instrument"), - function_pointer_removal_done(false), - partial_inlining_done(false), - remove_returns_done(false) + goto_instrument_parse_optionst(int argc, const char **argv) + : parse_options_baset( + GOTO_INSTRUMENT_OPTIONS, + argc, + argv, + ui_message_handler), + messaget(ui_message_handler), + ui_message_handler(cmdline, "goto-instrument"), + function_pointer_removal_done(false), + partial_inlining_done(false), + remove_returns_done(false) { } diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 9a1c81fea46..67d04c6b697 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -25,7 +25,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "signal_catcher.h" parse_options_baset::parse_options_baset( - const std::string &_optstring, int argc, const char **argv, message_handlert &mh) + const std::string &_optstring, + int argc, + const char **argv, + message_handlert &mh) : log(mh) { std::string optstring=std::string("?h(help)")+_optstring; diff --git a/src/util/parse_options.h b/src/util/parse_options.h index ca9ba213a45..fa0671bb382 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -19,7 +19,10 @@ class parse_options_baset { public: parse_options_baset( - const std::string &optstring, int argc, const char **argv, message_handlert &mh); + const std::string &optstring, + int argc, + const char **argv, + message_handlert &mh); cmdlinet cmdline; From df79fd0fe9081cc1e4b84191def0fad09c743d68 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 24 Jan 2019 16:57:39 +0000 Subject: [PATCH 3/5] Correct the expected strings for the JSON-UI tests --- regression/cbmc/json-ui/no_entry.desc | 2 +- regression/cbmc/json-ui/syntax_error.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/json-ui/no_entry.desc b/regression/cbmc/json-ui/no_entry.desc index 949d5e73631..ca617d7ff74 100644 --- a/regression/cbmc/json-ui/no_entry.desc +++ b/regression/cbmc/json-ui/no_entry.desc @@ -4,7 +4,7 @@ no_entry.c activate-multi-line-match ^EXIT=6$ ^SIGNAL=0$ -"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR", +"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR" -- ^warning: ignoring ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/json-ui/syntax_error.desc b/regression/cbmc/json-ui/syntax_error.desc index 7c35f907dfb..a4827340f13 100644 --- a/regression/cbmc/json-ui/syntax_error.desc +++ b/regression/cbmc/json-ui/syntax_error.desc @@ -4,7 +4,7 @@ syntax_error.c activate-multi-line-match ^EXIT=6$ ^SIGNAL=0$ -"messageText": "syntax error before .*",[\n ]*"messageType": "ERROR",[\n ]*"sourceLocation": {[\n ]*"file": "syntax_error.c",[\n ]*"function": "main",[\n ]*"line": "4", +"messageText": "syntax error before .*",[\n ]*"messageType": "ERROR",[\n ]*"sourceLocation": \{[\n ]*"file": "syntax_error.c",[\n ]*"function": "main",[\n ]*"line": "4", -- ^warning: ignoring ^VERIFICATION SUCCESSFUL$ From 185e5b77ff2657b0ae056d5cd225366a5b61368d Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 24 Jan 2019 16:58:36 +0000 Subject: [PATCH 4/5] Enable the JSON UI tests for CBMC These should check that exception messages are output wrapped in JSON rather than just dumped on std::cerr. --- regression/cbmc/json-ui/no_entry.desc | 2 +- regression/cbmc/json-ui/syntax_error.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/json-ui/no_entry.desc b/regression/cbmc/json-ui/no_entry.desc index ca617d7ff74..ea376532787 100644 --- a/regression/cbmc/json-ui/no_entry.desc +++ b/regression/cbmc/json-ui/no_entry.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE no_entry.c --json-ui activate-multi-line-match diff --git a/regression/cbmc/json-ui/syntax_error.desc b/regression/cbmc/json-ui/syntax_error.desc index a4827340f13..b7c3530a7bc 100644 --- a/regression/cbmc/json-ui/syntax_error.desc +++ b/regression/cbmc/json-ui/syntax_error.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE syntax_error.c --json-ui activate-multi-line-match From a959df97b77268ff8aba62e91ece60a718ee49f8 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 25 Jan 2019 18:00:58 +0000 Subject: [PATCH 5/5] Remove the patchy exception handling in Java tools and use default This is a copy of an earlier patch to the CBMC tools which replaced patchy and inconsistent exception handling in each tool with the comprehensive set of catch handlers in parse_options_baset. --- .../src/janalyzer/janalyzer_parse_options.cpp | 86 +------------- jbmc/src/janalyzer/janalyzer_parse_options.h | 1 - jbmc/src/jbmc/jbmc_parse_options.cpp | 108 +----------------- jbmc/src/jdiff/jdiff_parse_options.cpp | 26 ----- 4 files changed, 8 insertions(+), 213 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 1ea58d745f9..2397065c41b 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -355,29 +355,8 @@ int janalyzer_parse_optionst::doit() register_languages(); - try - { - goto_model = - initialize_goto_model(cmdline.args, get_message_handler(), options); - } - - catch(const char *e) - { - error() << e << eom; - return CPROVER_EXIT_EXCEPTION; - } - - catch(const std::string &e) - { - error() << e << eom; - return CPROVER_EXIT_EXCEPTION; - } - - catch(int e) - { - error() << "Numeric exception: " << e << eom; - return CPROVER_EXIT_EXCEPTION; - } + goto_model = + initialize_goto_model(cmdline.args, get_message_handler(), options); if(process_goto_program(options)) return CPROVER_EXIT_INTERNAL_ERROR; @@ -402,34 +381,7 @@ int janalyzer_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } - try - { - return perform_analysis(options); - } - - catch(const char *e) - { - error() << e << eom; - return CPROVER_EXIT_EXCEPTION; - } - - catch(const std::string &e) - { - error() << e << eom; - return CPROVER_EXIT_EXCEPTION; - } - - catch(int e) - { - error() << "Numeric exception: " << e << eom; - return CPROVER_EXIT_EXCEPTION; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << eom; - return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; - } + return perform_analysis(options); } /// Depending on the command line mode, run one of the analysis tasks @@ -554,8 +506,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) return CPROVER_EXIT_SUCCESS; } - if(set_properties()) - return CPROVER_EXIT_SET_PROPERTIES_FAILED; + if(cmdline.isset("property")) + ::set_properties(goto_model, cmdline.get_values("property")); if(options.get_bool_option("general-analysis")) { @@ -637,34 +589,6 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) return CPROVER_EXIT_USAGE_ERROR; } -bool janalyzer_parse_optionst::set_properties() -{ - try - { - if(cmdline.isset("property")) - ::set_properties(goto_model, cmdline.get_values("property")); - } - - catch(const char *e) - { - error() << e << eom; - return true; - } - - catch(const std::string &e) - { - error() << e << eom; - return true; - } - - catch(int) - { - return true; - } - - return false; -} - bool janalyzer_parse_optionst::process_goto_program(const optionst &options) { try diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index cd3ac664ae2..42b48315c53 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -167,7 +167,6 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget virtual void get_command_line_options(optionst &options); virtual bool process_goto_program(const optionst &options); - bool set_properties(); virtual int perform_analysis(const optionst &options); diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index c63ab8bc219..b34bd30acb8 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -429,22 +429,7 @@ int jbmc_parse_optionst::doit() // optionst options; - try - { - get_command_line_options(options); - } - - catch(const char *error_msg) - { - error() << error_msg << eom; - return 6; // should contemplate EX_SOFTWARE from sysexits.h - } - - catch(const std::string &error_msg) - { - error() << error_msg << eom; - return 6; // should contemplate EX_SOFTWARE from sysexits.h - } + get_command_line_options(options); // // Print a banner @@ -640,28 +625,8 @@ int jbmc_parse_optionst::doit() bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model) { - try - { - if(cmdline.isset("property")) - ::set_properties(goto_model, cmdline.get_values("property")); - } - - catch(const char *e) - { - error() << e << eom; - return true; - } - - catch(const std::string &e) - { - error() << e << eom; - return true; - } - - catch(int) - { - return true; - } + if(cmdline.isset("property")) + ::set_properties(goto_model, cmdline.get_values("property")); return false; } @@ -676,7 +641,6 @@ int jbmc_parse_optionst::get_goto_program( return 6; } - try { lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object( *this, options, get_message_handler()); @@ -742,29 +706,6 @@ int jbmc_parse_optionst::get_goto_program( status() << config.object_bits_info() << eom; } - catch(const char *e) - { - error() << e << eom; - return 6; - } - - catch(const std::string &e) - { - error() << e << eom; - return 6; - } - - catch(int) - { - return 6; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << eom; - return 6; - } - return -1; // no error, continue } @@ -780,7 +721,6 @@ void jbmc_parse_optionst::process_goto_function( bool using_symex_driven_loading = options.get_bool_option("symex-driven-lazy-loading"); - try { // Removal of RTTI inspection: remove_instanceof( @@ -865,24 +805,6 @@ void jbmc_parse_optionst::process_goto_function( // update the function member in each instruction function.update_instructions_function(); } - - catch(const char *e) - { - error() << e << eom; - throw; - } - - catch(const std::string &e) - { - error() << e << eom; - throw; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << eom; - throw; - } } bool jbmc_parse_optionst::show_loaded_functions( @@ -937,7 +859,6 @@ bool jbmc_parse_optionst::process_goto_functions( goto_modelt &goto_model, const optionst &options) { - try { status() << "Running GOTO functions transformation passes" << eom; @@ -1025,29 +946,6 @@ bool jbmc_parse_optionst::process_goto_functions( remove_skip(goto_model); } - catch(const char *e) - { - error() << e << eom; - return true; - } - - catch(const std::string &e) - { - error() << e << eom; - return true; - } - - catch(int) - { - return true; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << eom; - return true; - } - return false; } diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 1b5c824e8dd..438586677c8 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -346,7 +346,6 @@ bool jdiff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) { - try { // remove function pointers status() << "Removing function pointers and virtual functions" << eom; @@ -411,31 +410,6 @@ bool jdiff_parse_optionst::process_goto_program( goto_model.goto_functions.update(); } - catch(const char *e) - { - error() << e << eom; - return true; - } - - catch(const std::string &e) - { - error() << e << eom; - return true; - } - - catch(int e) - { - error() << "Numeric exception: " << e << eom; - return true; - } - - catch(const std::bad_alloc &) - { - error() << "Out of memory" << eom; - exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); - return true; - } - return false; }