Memory predicate tests and one-argument form [depends-on: #2644] #2706
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
added 5 commits
July 30, 2018 14:54
This change exposes is_lvalue for use outside of goto-programs/builtin_functions.cpp.
The --expand-pointer-predicates pass resolves pointer predicates
(util/pointer_predicates.{cpp, h}) which have side effects and
so require expanding into multiple instructions.
Currently, the only such predicate that needs to be expanded is
__CPROVER_points_to_valid_memory (name subject to change).
The __CPROVER_points_to_valid_memory predicates takes two parameters,
a pointer and a size. Semantically,
__CPROVER_points_to_valid_memory(p, size) should be true if and only
if p points to a memory object which is valid to read/write for at
least size bytes past p. When used in assertions, this will be checked
in a similar manner to how --pointer-check checks validity of a
dereference. When used in assumptions, this predicate creates (if none
exists already) an object for p to refer to, using
local_bitvector_analysis to make that determination, and then makes
assumptions (again corresponding to the assertions made by
--pointer-check) about that object.
This commit adds support for a one-argument form of __CPROVER_points_to_valid_memory, taking only a pointer, with no size. If ptr has type T*, then __CPROVER_points_to_valid_memory(ptr) is equivalent to __CPROVER_points_to_valid_memory(ptr, sizeof(T)).
qaphla
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
Closed
tautschnig
changed the title
|
Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work. |
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.
This adds two commits on top of #2644. The first commit slightly extends the functionality by adding a one-argument form (which infers the size from the type), while the second commit adds tests. The first three commits are just those from #2644 (which in turn takes two from #2635).
I expect there to be a lot of discussion on #2644 and likely many changes before anything gets merged in so it's likely that this should get mostly ignored until that point. However, the test cases in here may be useful for informing whatever functionality eventually comes from the discussion on #2644.