Fix/redirect exception handler output 2 #3951
Conversation
martin-cs
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
| : parse_options_baset(JANALYZER_OPTIONS, argc, argv), | ||
| messaget(ui_message_handler), | ||
| : messaget(ui_message_handler), | ||
| parse_options_baset(JANALYZER_OPTIONS, argc, argv, *this), |
There was a problem hiding this comment.
Here and everywhere else: what about only passing the message handler, not the full messaget? I think that would reduce the amount of churn in this commit, and would still achieve the same effect.
| // 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. |
There was a problem hiding this comment.
Would all that actually be pretty safe if we were using the message_handlert instead of the messaget? There arguably still is a risk that the message handler is not properly configured just yet and output would not end up formatted as desired, but it should be safe.
There was a problem hiding this comment.
The message_handlert won't be because it is a member variable. This is an issue with the current "inherit from messaget" approach.
src/util/parse_options.cpp
Outdated
| @@ -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\n"; | |||
There was a problem hiding this comment.
I believe that needs a << messaget::eom
|
@peterschrammel, any chance to get #3683 reviewed and approved? @martin-cs can surely fix things here, but that should just make the problem go away I think. |
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.
These should check that exception messages are output wrapped in JSON rather than just dumped on std::cerr.
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.
martin-cs
force-pushed
the
fix/redirect-exception-handler-output-2
branch
from
3e83f00 to
6663119
Compare
|
Third time lucky maybe : #3952 ? |
This is #3921 redone to use messaget as suggested by @tautschnig plus the corresponding updates to the Java tools as #3897 . It fixes and enables the tests in #3902 . This should reduce the risk of output, especially exceptions, winding up on std::cerr when using JSON or XML output.