Fix irrelevant loss of const throwing off the const analysis #1007
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
Though this example program appears to lose const-ness, since it is a primitive it is a copy so it is irrelevant.
|
Requesting reviews from: @NlightNFotis @martin-cs |
This was referenced Jun 13, 2017
added 2 commits
June 13, 2017 18:02
Previously the check for loss of const-correctness was to look at each
assignment and check whether in either the left/right hand sides of the
assignment or somewhere in the right hand side expression tree the
following condition was met:
Any type or any of its subtypes lost const-ness
This condition is now replaced by a more subtle condition:
if they are both pointers then:
there subtypes should not directly lose const-ness
if the subtype is a pointer, we recursively apply this check on the
subtypes
if they are not pointers:
we don't care about const-qualification loss at this level since it is
a copy
This fixes diffblue/cbmc-toyota#127 where an `const int` being assigned
to an
`int` would trigger disabling the function pointer removal.
Pulled out the private access class into a util file
Updating
New implementation of is_type_at_least_as_const_as only checks one
depth so we
don't need to pass in naked pointers. Updated the comment to reflect
methods new
purpose. Added unit tests to document exactly what the method is testing
Added tests to demonstrate the does_type_preserve_const_correctness
This is useful documentation of how it is different to the
is_type_at_least_as_const_as.
Added more examples of spurious const loss
thk123
force-pushed
the
bugfix/irrelevant-const-removal
branch
from
e56e15c to
fcd4e42
Compare
NlightNFotis
approved these changes
Jun 16, 2017
peterschrammel
approved these changes
Jun 25, 2017
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.
There is a bug in
does_remove_constanalysis where code like this:Would cause it to think the const-correctness had been lost (as detailed in diffblue/cbmc-toyota#127 🔒)
This fixes this by applying a more subtle condition when checking whether an assign statement actually violates const correctness:
Added unit tests to document exactly what the two methods do as the difference is quite subtle. The unit tests are a little difficult to read (and I'd ideally like to test
int**type assignments). I will come back to this later to structure them into a table format so can be easily verified by others that they are doing what they expect.