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

Changes from 1 commit
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
40 changes: 39 additions & 1 deletion src/util/parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,16 +71,54 @@ int parse_options_baset::main()

return doit();
}

// CPROVER style exceptions in order of decreasing happiness
catch(const invalid_command_line_argument_exceptiont &e)
{
std::cerr << e.what() << "\n";
std::cerr << e.what() << '\n';
return CPROVER_EXIT_USAGE_ERROR;
}
catch(incorrect_goto_program_exceptiont &e)
{
std::cerr << e.what() << '\n';
return CPROVER_EXIT_EXCEPTION;
}
Copy link
Collaborator

Choose a reason for hiding this comment

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

Is this case actually needed? Shouldn't the cprover_exception_baset below catch all of them?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I don't think so but it was an explicit case in the code I removed so I thought that it had been separated out for a reason and that reason should be preserved.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Fair enough, but then you might add an extra commit that removes it? You've got a catch-all at the very end anyway.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've added a commit that does this. Please merge if you are happy with this.

Copy link
Contributor

Choose a reason for hiding this comment

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

@martin-cs Historical note: When it was created there originally wasn't a base class, so we had separate handlers for each exception. A base class was added by vote. Also, we weren't entirely sure if all kinds of exceptions used the same exit code. Both of these situations were eventually remedied, so I don't think it's necessary anymore. This probably slipped past us when the situation changed.

catch(const cprover_exception_baset &e)
{
std::cerr << e.what() << '\n';
return CPROVER_EXIT_EXCEPTION;
}
catch(const std::string &e)
{
std::cerr << "C++ string exception : " << e << '\n';
return CPROVER_EXIT_EXCEPTION;
}
catch(const char *e)
{
std::cerr << "C string exception : " << e << '\n';
return CPROVER_EXIT_EXCEPTION;
}
catch(int e)
{
std::cerr << "Numeric exception : " << e << '\n';
return CPROVER_EXIT_EXCEPTION;
}
// C++ style exceptions
catch(const std::bad_alloc &)
{
std::cerr << "Out of memory" << '\n';
return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
}
catch(const std::exception &e)
{
std::cerr << e.what() << '\n';
return CPROVER_EXIT_EXCEPTION;
}
catch(...)
{
std::cerr << "Unknown exception type!" << '\n';
return CPROVER_EXIT_EXCEPTION;
}
}

std::string
Expand Down