Skip to content

Fix/redirect exception handler output #3921

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 4 commits into from
Closed

Fix/redirect exception handler output #3921

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9157fab
Add a callback so that error messages can be formatted
Jan 24, 2019
4f4fc7e
Use the callback in applications to reroute to message
Jan 24, 2019
744b43d
Correct the expected strings for the JSON-UI tests
Jan 24, 2019
9816337
Enable the JSON UI tests for CBMC
Jan 24, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions regression/cbmc/json-ui/no_entry.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
KNOWNBUG
CORE
no_entry.c
--json-ui
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$
4 changes: 2 additions & 2 deletions regression/cbmc/json-ui/syntax_error.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
KNOWNBUG
CORE
syntax_error.c
--json-ui
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$
6 changes: 6 additions & 0 deletions src/cbmc/cbmc_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 6 additions & 0 deletions src/goto-analyzer/goto_analyzer_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 6 additions & 0 deletions src/goto-diff/goto_diff_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 6 additions & 0 deletions src/goto-instrument/goto_instrument_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
27 changes: 17 additions & 10 deletions src/util/parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is passing a message handler to parse_options_baset not an option, so that this would be something like log.error() << "Usage error!\n" << messaget::eom;

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Various programs inherit from both messaget and parse_option_baset. If you would prefer things like program_parse_options::program_parse_options : messaget(), parse_option_baset(*this) { ... then I can do it that way.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Even though I strongly disagree with the inheritance done elsewhere, as far as parse_options_baset is concerned that's what I was thinking, yes. So I'd add a message_handlert &message_handler; member to parse_options_baset and then, on demand, create a messaget log(message_handler);. That way we can get away with a forward declaration of class message_handlert in parse_options.h, don't actually create unnecessary objects that we should not need under normal circumstances, and still do the output in the way desired and controlled by the caller.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good. I'll have a go and will open a new PR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, I thought the difference should be fairly small?

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()
Expand Down Expand Up @@ -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;
}
}
Expand Down
3 changes: 3 additions & 0 deletions src/util/parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down