Make dirtyt traverse operands of OTHER instructions #7106
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
remi-delmas-3000
requested review from
tautschnig,
feliperodri,
SaswatPadhi,
martin-cs,
peterschrammel and
chris-ryder
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #7106 +/- ##
===========================================
- Coverage 77.87% 77.87% -0.01%
===========================================
Files 1576 1576
Lines 181588 181587 -1
===========================================
- Hits 141413 141412 -1
Misses 40175 40175
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. |
remi-delmas-3000
changed the title
remi-delmas-3000
force-pushed
the
fix-dirtyt
branch
from
8eb5e4a to
e6fc280
Compare
martin-cs
approved these changes
Sep 7, 2022
|
|
||
| void dirtyt::search_other(const goto_programt::instructiont &instruction) | ||
| { | ||
| INVARIANT(instruction.is_other(), "instruction type must be OTHER"); |
There was a problem hiding this comment.
Pedantry but I would PRECONDITION this because it is the caller's responsibility rather than a property of the algorithm.
| } | ||
|
|
||
| void dirtyt::find_dirty(const exprt &expr) | ||
| { | ||
| if(expr.id()==ID_address_of) | ||
| if(expr.id() == ID_address_of) |
There was a problem hiding this comment.
Don't change it on this PR but in general it is good to have refactoring in a separate commit to make reviewing and bisecting for regressions easier.
tautschnig
approved these changes
Sep 7, 2022
There was a problem hiding this comment.
Thank you for fixing dirtyt for everyone. (And I'm with @martin-cs in that whitespace changes shouldn't be folded into the same commit.)
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.
Addresses #7072