Clean and document symex-dereference #4097
Merged
Conversation
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
smowton
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel and
tautschnig
as code owners
peterschrammel
approved these changes
Feb 5, 2019
tautschnig
approved these changes
Feb 5, 2019
| @@ -50,19 +50,14 @@ class value_set_dereferencet | |||
|
|
|||
| virtual ~value_set_dereferencet() { } | |||
|
|
|||
| enum class modet { READ, WRITE }; | |||
|
|
|||
| /// Dereference the given pointer-expression. Any errors are | |||
| /// reported to the callback method given in the constructor. | |||
| /// \param pointer: A pointer-typed expression, to | |||
| /// be dereferenced. | |||
| /// \param guard: A guard, which is assumed to hold when dereferencing. | |||
| /// \param mode: Indicates whether the dereferencing is a load or store | |||
| // (unused). | |||
There was a problem hiding this comment.
Documentation needs to be cleaned up as well.
| /// | ||
| /// \param expr: expression to get or create a failed symbol for | ||
| /// \param [out] symbol: failed symbol result | ||
| /// \return true if we populated \p symbol | ||
| bool symex_dereference_statet::get_or_create_failed_symbol( |
There was a problem hiding this comment.
Not sure whether in this PR or in a separate one, but could we please change the return value to optionalt<symbolt>? The "Boolean return value + out-parameter" combination is just too error-prone and nowadays we have better options.
There was a problem hiding this comment.
Pushed an extra commit to just use symbolt *, since that's what the existing code was expecting
smowton
force-pushed
the
smowton/admin/clean-and-document-symex-deref
branch
2 times, most recently
from
28e12ee to
3ab2c1f
Compare
|
This now needs a rebase (because I just merged the codet API PR) - sorry for the extra work! |
has_failed_symbol is renamed to get_or_create_failed_symbol to emphasise that that method really *may* have side-effects.
This is only used to access its namespace in a const context.
Both implementations currently disregard whether they're looking at an LHS or RHS expression.
This was propagated between dereference_rec and address_arithmetic without ever changing, before finally passing into value_set_dereferencet::dereference as a const reference.
smowton
force-pushed
the
smowton/admin/clean-and-document-symex-deref
branch
from
3ab2c1f to
577e3d9
Compare
smowton
force-pushed
the
smowton/admin/clean-and-document-symex-deref
branch
from
577e3d9 to
90b597b
Compare
It's already implicit in a bare pointer (rather than a reference) that it could be null, so let's just use that to express whether we have an answer or not.
smowton
force-pushed
the
smowton/admin/clean-and-document-symex-deref
branch
from
90b597b to
115cb7e
Compare
allredj
reviewed
Feb 12, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 115cb7e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100604500
5 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Review commit-by-commit. As you can see there were various bits of goto-symex where I pulled the threads to confirm what they did, and found the threads didn't go anywhere.