Skip to content

Fix/simplify exception handling #3897

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

Merged
merged 8 commits into from
Jan 23, 2019
Merged

Fix/simplify exception handling #3897

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
da4cc61
Add default handling for the kinds of exceptions used in CPROVER
Jan 22, 2019
52ceb9b
Remove redundant try/catch blocks from goto-analyzer
Jan 22, 2019
338b155
Remove redundant try/catch blocks from cbmc
Jan 22, 2019
920acd8
Remove redundant try/catch blocks from goto-instrument
Jan 22, 2019
5c23e11
Remove some exception handling in goto-analyzer
Jan 22, 2019
461e8c7
Remove some exception handling in CBMC
Jan 22, 2019
5804cb0
Remove some exception handling in goto-diff
Jan 22, 2019
2212653
Remove redundant case in the exception handling in parse_options.cpp
Jan 23, 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
125 changes: 5 additions & 120 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,22 +433,7 @@ int cbmc_parse_optionst::doit()
//

optionst options;
try
{
get_command_line_options(options);
}

catch(const char *error_msg)
{
error() << error_msg << eom;
return CPROVER_EXIT_EXCEPTION;
}

catch(const std::string &error_msg)
{
error() << error_msg << eom;
return CPROVER_EXIT_EXCEPTION;
}
get_command_line_options(options);

eval_verbosity(
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
Expand Down Expand Up @@ -575,32 +560,11 @@ int cbmc_parse_optionst::doit()

bool cbmc_parse_optionst::set_properties()
{
try
{
if(cmdline.isset("claim")) // will go away
::set_properties(goto_model, cmdline.get_values("claim"));
if(cmdline.isset("claim")) // will go away
::set_properties(goto_model, cmdline.get_values("claim"));

if(cmdline.isset("property")) // use this one
::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 e)
{
error() << "Numeric exception : " << e << eom;
return true;
}
if(cmdline.isset("property")) // use this one
::set_properties(goto_model, cmdline.get_values("property"));

return false;
}
Expand All @@ -618,7 +582,6 @@ int cbmc_parse_optionst::get_goto_program(
return CPROVER_EXIT_INCORRECT_TASK;
}

try
{
goto_model =
initialize_goto_model(cmdline.args, ui_message_handler, options);
Expand Down Expand Up @@ -655,42 +618,11 @@ int cbmc_parse_optionst::get_goto_program(
log.status() << config.object_bits_info() << log.eom;
}

catch(incorrect_goto_program_exceptiont &e)
{
log.error() << e.what() << log.eom;
return CPROVER_EXIT_EXCEPTION;
}

catch(const char *e)
{
log.error() << e << log.eom;
return CPROVER_EXIT_EXCEPTION;
}

catch(const std::string &e)
{
log.error() << e << log.eom;
return CPROVER_EXIT_EXCEPTION;
}

catch(int e)
{
log.error() << "Numeric exception : " << e << log.eom;
return CPROVER_EXIT_EXCEPTION;
}

catch(const std::bad_alloc &)
{
log.error() << "Out of memory" << log.eom;
return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
}

return -1; // no error, continue
}

void cbmc_parse_optionst::preprocessing(const optionst &options)
{
try
{
if(cmdline.args.size()!=1)
{
Expand Down Expand Up @@ -722,35 +654,13 @@ void cbmc_parse_optionst::preprocessing(const optionst &options)
if(language->preprocess(infile, filename, std::cout))
error() << "PREPROCESSING ERROR" << eom;
}

catch(const char *e)
{
error() << e << eom;
}

catch(const std::string &e)
{
error() << e << eom;
}

catch(int e)
{
error() << "Numeric exception : " << e << eom;
}

catch(const std::bad_alloc &)
{
error() << "Out of memory" << eom;
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
}
}

bool cbmc_parse_optionst::process_goto_program(
goto_modelt &goto_model,
const optionst &options,
messaget &log)
{
try
{
// Remove inline assembler; this needs to happen before
// adding the library.
Expand Down Expand Up @@ -878,31 +788,6 @@ bool cbmc_parse_optionst::process_goto_program(
remove_skip(goto_model);
}

catch(const char *e)
{
log.error() << e << eom;
return true;
}

catch(const std::string &e)
{
log.error() << e << eom;
return true;
}

catch(int e)
{
log.error() << "Numeric exception : " << e << eom;
return true;
}

catch(const std::bad_alloc &)
{
log.error() << "Out of memory" << eom;
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
return true;
}

return false;
}

Expand Down
111 changes: 5 additions & 106 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -396,29 +396,8 @@ int goto_analyzer_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 Down Expand Up @@ -448,34 +427,7 @@ int goto_analyzer_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);
}


Expand Down Expand Up @@ -603,8 +555,8 @@ int goto_analyzer_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"));
Copy link
Contributor

Choose a reason for hiding this comment

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

What does this change mean?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

After removing the try block, set_properties only contained the two lines I've introduced and then return false so I inlined them.


if(options.get_bool_option("general-analysis"))
{
Expand Down Expand Up @@ -713,38 +665,9 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
return CPROVER_EXIT_USAGE_ERROR;
}

bool goto_analyzer_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 goto_analyzer_parse_optionst::process_goto_program(
const optionst &options)
{
try
{
#if 0
// Remove inline assembler; this needs to happen before
Expand Down Expand Up @@ -786,30 +709,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
// add loop ids
goto_model.goto_functions.compute_loop_numbers();
}

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
1 change: 0 additions & 1 deletion 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 @@ -172,7 +172,6 @@ class goto_analyzer_parse_optionst:
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
26 changes: 0 additions & 26 deletions src/goto-diff/goto_diff_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -386,7 +386,6 @@ bool goto_diff_parse_optionst::process_goto_program(
const optionst &options,
goto_modelt &goto_model)
{
try
{
// Remove inline assembler; this needs to happen before
// adding the library.
Expand Down Expand Up @@ -450,31 +449,6 @@ bool goto_diff_parse_optionst::process_goto_program(
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 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;
}

Expand Down
Loading