Skip to content

Fix/redirect exception handler output 2 #3951

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 5 commits into from
Closed

Fix/redirect exception handler output 2 #3951

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
8dcf94c
Add a messaget parameter to parse_option_baset to format errors
Jan 25, 2019
a8d64c3
Reformatting that clang-format wants.
Jan 25, 2019
f79bc90
Correct the expected strings for the JSON-UI tests
Jan 24, 2019
a0645f3
Enable the JSON UI tests for CBMC
Jan 24, 2019
6663119
Remove the patchy exception handling in Java tools and use default
Jan 25, 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
90 changes: 7 additions & 83 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ Author: Daniel Kroening, [email protected]
#include <goto-analyzer/unreachable_instructions.h>

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),
Copy link
Collaborator

Choose a reason for hiding this comment

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

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Can do...

ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
{
}
Expand Down Expand Up @@ -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;
Expand All @@ -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
Expand Down Expand Up @@ -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"))
{
Expand Down Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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);

Expand Down
116 changes: 7 additions & 109 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,8 @@ Author: Daniel Kroening, [email protected]
#include <java_bytecode/simple_method_stubbing.h>

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)
{
}
Expand All @@ -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)
{
}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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;
}
Expand All @@ -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());
Expand Down Expand Up @@ -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
}

Expand All @@ -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(
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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;
}

Expand Down
4 changes: 1 addition & 3 deletions jbmc/src/jbmc/jbmc_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,9 +84,7 @@ class optionst;
"(symex-driven-lazy-loading)"
// clang-format on

class jbmc_parse_optionst:
public parse_options_baset,
public messaget
class jbmc_parse_optionst : public messaget, public parse_options_baset
{
public:
virtual int doit() override;
Expand Down
Loading