-
Notifications
You must be signed in to change notification settings - Fork 277
bv_pointert cleanup #6830
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
bv_pointert cleanup #6830
Conversation
kroening
commented
Apr 26, 2022
- Each commit message has a non-empty body, explaining why the change was made.
- n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
This commit moves three methods that have (relatively) large bodies from the header file into the .cpp file.
There is no need for a pointer-aware bv_width class, as pointers are bitvector types (including a width) since 2016.
This removes various obvious declarators from method declarations in bv_pointerst.
Codecov Report
@@ Coverage Diff @@
## develop #6830 +/- ##
===========================================
+ Coverage 77.01% 77.02% +0.01%
===========================================
Files 1594 1594
Lines 184954 184991 +37
===========================================
+ Hits 142438 142490 +52
+ Misses 42516 42501 -15
Continue to review full report at Codecov.
|
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.
I'm happy with the first and third commit, but the middle one part reverts work that I previously did. Having a clean revert would be more helpful.
@@ -68,58 +68,33 @@ void bv_endianness_mapt::build_big_endian(const typet &src) | |||
endianness_mapt | |||
bv_pointerst::endianness_map(const typet &type, bool little_endian) const | |||
{ | |||
return bv_endianness_mapt{type, little_endian, ns, bv_pointers_width}; | |||
return bv_endianness_mapt{type, little_endian, ns, bv_width}; |
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.
That second commit is a part-revert of 5cf2b07. If we go for removing the capability that the commit was trying to add we should ponder a clean revert instead.
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.
We absolutely want to keep the parts of that commit that pass the pointer type around!
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.
Approving with the caveat that I may propose to revert the middle commit at a future date.