From 8dcf94c44b01e3ef1d66ce3270b86e5e5fcbbf0b Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 25 Jan 2019 17:24:38 +0000 Subject: [PATCH 1/5] Add a messaget parameter to parse_option_baset to format errors Getting parse_option_baset to use the same messaget object 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; messaget should be constructed before parse_option_baset so this patch swaps the order of inheritance and thus construction. However as the message_handlert is a local variable, it's not actually safe to use messaget during construction. A comment explaining this problem is given and the issue is no worse than it already was. --- .../src/janalyzer/janalyzer_parse_options.cpp | 4 +-- jbmc/src/janalyzer/janalyzer_parse_options.h | 2 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 8 ++--- jbmc/src/jbmc/jbmc_parse_options.h | 4 +-- jbmc/src/jdiff/jdiff_parse_options.cpp | 8 ++--- jbmc/src/jdiff/jdiff_parse_options.h | 2 +- src/cbmc/cbmc_parse_options.cpp | 8 ++--- src/cbmc/cbmc_parse_options.h | 4 +-- .../goto_analyzer_parse_options.cpp | 4 +-- .../goto_analyzer_parse_options.h | 4 +-- src/goto-diff/goto_diff_parse_options.cpp | 8 ++--- src/goto-diff/goto_diff_parse_options.h | 4 +-- .../goto_instrument_parse_options.h | 6 ++-- src/util/parse_options.cpp | 36 +++++++++++++------ src/util/parse_options.h | 8 ++++- 15 files changed, 65 insertions(+), 45 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 90fc5790998..a1d77118dad 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -58,8 +58,8 @@ 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), - messaget(ui_message_handler), + : messaget(ui_message_handler), + parse_options_baset(JANALYZER_OPTIONS, argc, argv, *this), ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION) { } diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index cd3ac664ae2..69a947f2cb9 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -150,7 +150,7 @@ class optionst; JAVA_BYTECODE_LANGUAGE_OPTIONS // clang-format on -class janalyzer_parse_optionst : public parse_options_baset, public messaget +class janalyzer_parse_optionst : public messaget, public parse_options_baset { public: virtual int doit() override; diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 4ab56be7ee1..c355f71b4d2 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -70,8 +70,8 @@ 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), - messaget(ui_message_handler), + : messaget(ui_message_handler), + parse_options_baset(JBMC_OPTIONS, argc, argv, *this), ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION) { } @@ -80,8 +80,8 @@ ::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), - messaget(ui_message_handler), + : messaget(ui_message_handler), + parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv, *this), ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION) { } diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 5e9b39f5f68..1f408320f4d 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -85,8 +85,8 @@ class optionst; // clang-format on class jbmc_parse_optionst: - public parse_options_baset, - public messaget + public messaget, + public parse_options_baset { public: virtual int doit() override; diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 683a8d1f7c7..bedae2f0cfe 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -63,8 +63,8 @@ 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), - jdiff_languagest(cmdline, ui_message_handler, &options), + : jdiff_languagest(cmdline, ui_message_handler, &options), + parse_options_baset(JDIFF_OPTIONS, argc, argv, *this), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler, &options) { @@ -74,8 +74,8 @@ ::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), - jdiff_languagest(cmdline, ui_message_handler, &options), + : jdiff_languagest(cmdline, ui_message_handler, &options), + parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv, *this), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler, &options) { diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index e56f44633ee..41f4ddf6c58 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -42,7 +42,7 @@ class goto_modelt; "(compact-output)" // clang-format on -class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest +class jdiff_parse_optionst : public jdiff_languagest, public parse_options_baset { public: virtual int doit(); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b1407a5d71e..5c6dd02eeb6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -71,9 +71,9 @@ 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), + : messaget(ui_message_handler), + parse_options_baset(CBMC_OPTIONS, argc, argv, *this), xml_interfacet(cmdline), - messaget(ui_message_handler), ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) { } @@ -82,9 +82,9 @@ ::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), + : messaget(ui_message_handler), + parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv, *this), xml_interfacet(cmdline), - messaget(ui_message_handler), ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION) { } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 1b26e83ab7e..d1fb605c0d7 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -84,9 +84,9 @@ class optionst; // clang-format on class cbmc_parse_optionst: + public messaget, public parse_options_baset, - public xml_interfacet, - public messaget + public xml_interfacet { public: virtual int doit() override; diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index a54e6f8b0a5..28a61c75abc 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -67,8 +67,8 @@ 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), - messaget(ui_message_handler), + : messaget(ui_message_handler), + parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv, *this), ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION) { } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 02cbaa59ce6..9517a8be598 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -154,8 +154,8 @@ class optionst; // clang-format on class goto_analyzer_parse_optionst: - public parse_options_baset, - public messaget + public messaget, + public parse_options_baset { public: virtual int doit() override; diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 5342c761ce0..f0d88c54070 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -61,8 +61,8 @@ 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), - goto_diff_languagest(cmdline, ui_message_handler), + : goto_diff_languagest(cmdline, ui_message_handler), + parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, *this), ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) { @@ -72,8 +72,8 @@ ::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), - goto_diff_languagest(cmdline, ui_message_handler), + : goto_diff_languagest(cmdline, ui_message_handler), + parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv, *this), ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), languages2(cmdline, ui_message_handler) { diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index e7822385f8d..0937037c656 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -42,8 +42,8 @@ class optionst; // clang-format on class goto_diff_parse_optionst: - public parse_options_baset, - public goto_diff_languagest + public goto_diff_languagest, + public parse_options_baset { public: virtual int doit(); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 7e70a1ff1d7..46cc97eb4c5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -112,16 +112,16 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format on class goto_instrument_parse_optionst: - public parse_options_baset, - public messaget + public messaget, + public parse_options_baset { public: virtual int doit(); virtual void help(); goto_instrument_parse_optionst(int argc, const char **argv): - parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv), messaget(ui_message_handler), + parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv, *this), ui_message_handler(cmdline, "goto-instrument"), function_pointer_removal_done(false), partial_inlining_done(false), diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 1b556f85c3f..289eaf8d630 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -22,13 +22,27 @@ Author: Daniel Kroening, kroening@kroening.com #include "cmdline.h" #include "exception_utils.h" #include "exit_codes.h" +#include "message.h" #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, messaget &l) + : log(l) { std::string optstring=std::string("?h(help)")+_optstring; parse_result=cmdline.parse(argc, argv, optstring.c_str()); + + // DO NOT USE l 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 messaget object has a reference to a + // an uninitialised object. Using it here will likely cause a + // hard to debug failure somewhere in the messaget code. } void parse_options_baset::help() @@ -37,7 +51,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 +60,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 +91,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..58ceb2640fd 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -14,11 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "cmdline.h" +// Forwards declare messaget so we can use references to it +class messaget; + 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, messaget &l); cmdlinet cmdline; @@ -30,6 +33,9 @@ class parse_options_baset virtual int main(); virtual ~parse_options_baset() { } +protected: + messaget &log; + private: void unknown_option_msg(); bool parse_result; From a8d64c358c6e23745d53e59f4e4115dfefb93daa Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 25 Jan 2019 17:31:39 +0000 Subject: [PATCH 2/5] Reformatting that clang-format wants. --- jbmc/src/jbmc/jbmc_parse_options.h | 4 +--- src/cbmc/cbmc_parse_options.h | 7 +++---- src/goto-diff/goto_diff_parse_options.h | 5 ++--- .../goto_instrument_parse_options.h | 19 +++++++++---------- src/util/parse_options.cpp | 5 ++++- src/util/parse_options.h | 5 ++++- 6 files changed, 23 insertions(+), 22 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 1f408320f4d..3d5493a128f 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -84,9 +84,7 @@ class optionst; "(symex-driven-lazy-loading)" // clang-format on -class jbmc_parse_optionst: - public messaget, - public parse_options_baset +class jbmc_parse_optionst : public messaget, public parse_options_baset { public: virtual int doit() override; diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index d1fb605c0d7..5ba0c3205bb 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -83,10 +83,9 @@ class optionst; "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) // clang-format on -class cbmc_parse_optionst: - public messaget, - public parse_options_baset, - public xml_interfacet +class cbmc_parse_optionst : public messaget, + public parse_options_baset, + public xml_interfacet { public: virtual int doit() override; diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 0937037c656..1fb0beca8ce 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -41,9 +41,8 @@ class optionst; "(compact-output)" // clang-format on -class goto_diff_parse_optionst: - public goto_diff_languagest, - public parse_options_baset +class goto_diff_parse_optionst : public goto_diff_languagest, + public parse_options_baset { public: virtual int doit(); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 46cc97eb4c5..c1dfee56281 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -111,21 +111,20 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format on -class goto_instrument_parse_optionst: - public messaget, - public parse_options_baset +class goto_instrument_parse_optionst : public messaget, + public parse_options_baset { public: virtual int doit(); virtual void help(); - goto_instrument_parse_optionst(int argc, const char **argv): - messaget(ui_message_handler), - parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv, *this), - 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) + : messaget(ui_message_handler), + parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv, *this), + 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 289eaf8d630..041ac3e6426 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -26,7 +26,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, messaget &l) + const std::string &_optstring, + int argc, + const char **argv, + messaget &l) : log(l) { std::string optstring=std::string("?h(help)")+_optstring; diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 58ceb2640fd..b1700a41890 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -21,7 +21,10 @@ class parse_options_baset { public: parse_options_baset( - const std::string &optstring, int argc, const char **argv, messaget &l); + const std::string &optstring, + int argc, + const char **argv, + messaget &l); cmdlinet cmdline; From f79bc90bb08e3d90cf61ad6b83ca4baec60f28db 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 a0645f322c011d9a265e398d8eb9bc5d8bfa7961 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 6663119b3d723e333d034b1deb4bdeee5f1be3bf 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 a1d77118dad..d41ce83d7b0 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 69a947f2cb9..d0ce84724ed 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 messaget, public parse_options_baset 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 c355f71b4d2..03472a92767 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -425,22 +425,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 @@ -636,28 +621,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; } @@ -672,7 +637,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()); @@ -738,29 +702,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 } @@ -776,7 +717,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( @@ -861,24 +801,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( @@ -933,7 +855,6 @@ bool jbmc_parse_optionst::process_goto_functions( goto_modelt &goto_model, const optionst &options) { - try { status() << "Running GOTO functions transformation passes" << eom; @@ -1021,29 +942,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 bedae2f0cfe..526ccedbefd 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -342,7 +342,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; @@ -407,31 +406,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; }