-
Notifications
You must be signed in to change notification settings - Fork 274
Refactor assigns clause implementation #6334
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.
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
Conversation
e6678b5
to
2859f9f
Compare
Marked
|
Fixed this by removing dead variables from freely assignable set all together (although the implementation is still incorrect and, as discussed offline, @feliperodri would make a separate PR to fix that properly). But, what's concerning here is that EDIT: The remaining CI issues with Windows tests seem completely unrelated. |
I realize I'm late here and that the coding practices for this code base are established ... but I would want to see more comments in the code. While particularly valuable for a new comer like myself, a header comment per method stating what it does, and maybe also per method argument/result, would help a great deal. I imagine one day being able to run doxygen on the code and learning something useful from it. |
Codecov Report
@@ Coverage Diff @@
## develop #6334 +/- ##
===========================================
- Coverage 75.89% 75.89% -0.01%
===========================================
Files 1515 1515
Lines 163972 163969 -3
===========================================
- Hits 124444 124440 -4
- Misses 39528 39529 +1
Continue to review full report at Codecov.
|
b50690e
to
e414eb0
Compare
+ usused fields (e.g., `function_id`, `init_block`) are removed, + redundant functions (e.g. `pointer_for`) are removed, + const references are used throughout consistently + targets are tracked in an `unordered_set` as opposed to `vector` + introduced a "normalize" method for extracting base object of arrays + API renamed for clarity
e414eb0
to
d41ff8b
Compare
Will push a few more things before final review & merge, so marked as |
39a3440
to
00ebb97
Compare
7204528
to
b74afd5
Compare
assigns_clauset was calling `compatible_expression` (not `alias_expression`) on each target, and was thus only comparing the object IDs (not offsets and sizes). We fix this by removing `compatible_expression` entirely and calling `alias_expression` for each from assigns_clauset.
b74afd5
to
e1e7235
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for all the subsequent clean up and fixes!
I was planning to merge these changes as part of #6249, but given the volume of changes, I thought it would be best to create a separate PR.
Main changes are:
function_id
,init_block
) are removed,pointer_for
) are removed,unordered_set
as opposed tovector
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/