From 9157fab38025247c82661122ffa79457b8efd543 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 24 Jan 2019 16:55:32 +0000 Subject: [PATCH 1/4] Add a callback so that error messages can be formatted This allows a class that inherits from parse_options_baset to override the standard direction for error messages from exception handlers so that they can be correctly formatted in JSON, XML, etc. --- src/util/parse_options.cpp | 27 +++++++++++++++++---------- src/util/parse_options.h | 3 +++ 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 5c1db010b2e..5f941ba180b 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -35,16 +35,23 @@ void parse_options_baset::help() void parse_options_baset::usage_error() { - std::cerr << "Usage error!\n\n"; + error_message("Usage error!\n"); help(); } +/// This can be overloaded so that error messages are valid XML / JSON. +void parse_options_baset::error_message(const std::string &err) +{ + std::cerr << err << '\n'; + return; +} + /// Print an error message mentioning the option that was not recognized when /// parsing the command line. void parse_options_baset::unknown_option_msg() { if(!cmdline.unknown_arg.empty()) - std::cerr << "Unknown option: " << cmdline.unknown_arg << "\n"; + error_message("Unknown option: " + cmdline.unknown_arg + "\n"); } int parse_options_baset::main() @@ -75,43 +82,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'; + error_message(e.what()); return CPROVER_EXIT_USAGE_ERROR; } catch(const cprover_exception_baset &e) { - std::cerr << e.what() << '\n'; + error_message(e.what()); return CPROVER_EXIT_EXCEPTION; } catch(const std::string &e) { - std::cerr << "C++ string exception : " << e << '\n'; + error_message("C++ string exception : " + e); return CPROVER_EXIT_EXCEPTION; } catch(const char *e) { - std::cerr << "C string exception : " << e << '\n'; + error_message(std::string("C string exception : ") + e); return CPROVER_EXIT_EXCEPTION; } catch(int e) { - std::cerr << "Numeric exception : " << e << '\n'; + error_message("Numeric exception : " + std::to_string(e)); return CPROVER_EXIT_EXCEPTION; } // C++ style exceptions catch(const std::bad_alloc &) { - std::cerr << "Out of memory" << '\n'; + error_message("Out of memory"); return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; } catch(const std::exception &e) { - std::cerr << e.what() << '\n'; + error_message(e.what()); return CPROVER_EXIT_EXCEPTION; } catch(...) { - std::cerr << "Unknown exception type!" << '\n'; + error_message("Unknown exception type!"); return CPROVER_EXIT_EXCEPTION; } } diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 6b2b982fd51..46c70ba631c 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -30,6 +30,9 @@ class parse_options_baset virtual int main(); virtual ~parse_options_baset() { } +protected: + virtual void error_message(const std::string &err); + private: void unknown_option_msg(); bool parse_result; From 4f4fc7eff9443a036bc7d5e61e48c6c2a733350d Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 24 Jan 2019 16:57:07 +0000 Subject: [PATCH 2/4] Use the callback in applications to reroute to message This means that exceptions, invariant failures, etc. will be given in the appropriate format. --- src/cbmc/cbmc_parse_options.h | 6 ++++++ src/goto-analyzer/goto_analyzer_parse_options.h | 6 ++++++ src/goto-diff/goto_diff_parse_options.h | 6 ++++++ src/goto-instrument/goto_instrument_parse_options.h | 6 ++++++ 4 files changed, 24 insertions(+) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 1b26e83ab7e..9689a9b6aca 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -121,6 +121,12 @@ class cbmc_parse_optionst: void get_command_line_options(optionst &); void preprocessing(const optionst &); bool set_properties(); + + virtual void error_message(const std::string &err) override + { + error() << err << eom; + return; + } }; #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 02cbaa59ce6..9c3b46aa65b 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -181,6 +181,12 @@ class goto_analyzer_parse_optionst: { return ui_message_handler.get_ui(); } + + virtual void error_message(const std::string &err) override + { + error() << err << eom; + return; + } }; #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index e7822385f8d..7830d45ba4c 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -71,6 +71,12 @@ class goto_diff_parse_optionst: goto_modelt &goto_model); void preprocessing(); + + virtual void error_message(const std::string &err) override + { + error() << err << eom; + return; + } }; #endif // CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 7e70a1ff1d7..f8248c96d10 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -151,6 +151,12 @@ class goto_instrument_parse_optionst: { return ui_message_handler.get_ui(); } + + virtual void error_message(const std::string &err) override + { + error() << err << eom; + return; + } }; #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H From 744b43df7275469ba5e4eed13234e6b7e63926ac Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 24 Jan 2019 16:57:39 +0000 Subject: [PATCH 3/4] 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 98163370de9a74c0d5a3fd9ccffc61647128b7a8 Mon Sep 17 00:00:00 2001 From: martin Date: Thu, 24 Jan 2019 16:58:36 +0000 Subject: [PATCH 4/4] 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