Add additional exception classes and introduce base exception#2996
Merged
tautschnig merged 1 commit intodiffblue:developfrom Sep 19, 2018
Merged
Conversation
hannes-steffenhagen-diffblue
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
hannes-steffenhagen-diffblue
force-pushed
the
feature-new_exception_types
branch
from
1a86de4 to
d44183a
Compare
This adds a number of new exception classes that are meant to be used to replace unstructured throws in other parts of the code. The exception types have been selected according to what we already determined we are going to need. Further, this has a slight fix in the format for invalid_user_input_exceptiont (it did previously not add a separator between the reason and the suggestion on how to fix the error). This also adds a cprover_exception_baset which is mean to avoid unnecessary overhead when adding new exception types - without it, all driver programs would have to updated to explicitly catch the new exception type whenever we introduce one. Also removes some dead code parse_options_baset (there was a final return that cannot be reached because all ancestor statements are returns).
hannes-steffenhagen-diffblue
force-pushed
the
feature-new_exception_types
branch
from
d44183a to
fb1be5d
Compare
| catch(const invalid_user_input_exceptiont &e) | ||
| { | ||
| std::cerr << e.what() << "\n"; | ||
| return CPROVER_EXIT_USAGE_ERROR; |
Contributor
Author
There was a problem hiding this comment.
I'm not sure whether or not we can merge this into the below case because this returns a different error code than the other exceptions.
Contributor
There was a problem hiding this comment.
Looks reasonable to be left as is, as it is in line with the previous code, which had a semantic distinction for the case when a user was passing a wrong argument (which afaik, is also important for automated tools or scripts using cbmc).
peterschrammel
approved these changes
Sep 19, 2018
tautschnig
approved these changes
Sep 19, 2018
allredj
reviewed
Sep 19, 2018
Contributor
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: fb1be5d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85327320
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is part of the error handling cleanup work we are doing at the moment. It unifies the several exception types we introduced during that work into a single commit and addresses some requests for changes common to all of them at the same time.
This adds a number of new exception classes that are meant to be used to replace
unstructured throws in other parts of the code. The exception types have been
selected according to what we already determined we are going to need.
Further, this has a slight fix in the format for invalid_user_input_exceptiont
(it did previously not add a separator between the reason and the suggestion on
how to fix the error).
This also adds a cprover_exception_baset which is mean to avoid unnecessary
overhead when adding new exception types - without it, all driver programs would
have to updated to explicitly catch the new exception type whenever we introduce
one.
Also removes some dead code parse_options_baset (there was a final return that
cannot be reached because all ancestor statements are returns).