Fix for arrays containing structs will null pointers #1009
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
Uninitialized entries in an array are set to zero (i.e. the struct contains zero and a null pointer). The output should still generate the possible valid if statements as it does with an array of function pointers containing null (as demonstrated in approx-const-fp-array-variable-const-fp-with-null).
thk123
force-pushed
the
bugfix/arrays-structs-null-pointers
branch
from
6a9f22c to
e7de7a6
Compare
added 4 commits
June 13, 2017 18:23
It is more logical that the functor operator takes the expression it is considering as it would allow the same object to be reused for multiple function pointer resolutions.
We now exclude the line that would catch if the function is replaced by all 9 possibilities.
We now allow finding a null pointer at any point in the removal process
(previously we were just excepting it in an array of pointers). This
fixes diffblue/cbmc-toyota#128
This slightly changes the behaviour in the event we can precisely
resolve a null pointer. Previously we would have replaced the function
pointer with a branch on all valid function pointers. Now we will
(providing --pointer-check is enabled) simply assert false.
This behaviour is more desirable - if we know a pointer is NULL then the
previous if statements that were generated would all be ignored anyway,
so this just reduces the size of the goto program with no impact on its
behaviour.
Pointers to not functions still cause a rejection, so tests that exibit
this have been modified to require this.
thk123
force-pushed
the
bugfix/arrays-structs-null-pointers
branch
from
e7de7a6 to
8ec1890
Compare
|
Requesting review from @danpoe @NlightNFotis @martin-cs |
NlightNFotis
approved these changes
Jun 14, 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.
We now allow finding a null pointer at any point in the removal process (previously we were just excepting it in an array of pointers). This fixes diffblue/cbmc-toyota#128
This slightly changes the behaviour in the event we can precisely resolve a null pointer. Previously we would have replaced the function pointer with a branch on all valid function pointers. Now we will (providing --pointer-check is enabled) simply assert false.
This behaviour is more desirable - if we know a pointer is NULL then the previous if statements that were generated would all be ignored anyway, so this just reduces the size of the goto program with no impact on its behaviour.
Pointers to not functions still cause a rejection, so tests that exhibit this have been modified to require this. I am not sure this is correct as I think it makes the behaviour a little inconsistent.
Between this PR and #1007 the PR #936 can be removed since the tests it adds are included in these PRs. Further - they are actually fixed!