CBMC: Remove uses of object_whole and same_object#1390
Merged
Conversation
hanno-becker
force-pushed
the
no_object_whole
branch
from
b2e80ec to
29e071d
Compare
hanno-becker
force-pushed
the
no_object_whole
branch
2 times, most recently
from
460ce09 to
c977b3c
Compare
hanno-becker
changed the title
Contributor
Author
|
@mkannwischer If you're happy with it, let's merge it directly as part of #1379 |
mkannwischer
approved these changes
Dec 15, 2025
In preparation for the introduction of workspace structures at the higher-level APIs, this commit removes all uses of the CBMC footprint predicate `object_whole` and instead uses the more fine-grained `memory_slice`. For `mlk_poly_getnoise_eta1122_4x`, we also remove the sole use of `same_object` in the code base, and remove its definition from cbmc.h. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
hanno-becker
force-pushed
the
no_object_whole
branch
from
c977b3c to
8949cc8
Compare
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
In preparation for the introduction of workspace structures
at the higher-level APIs, this commit removes all uses of
the CBMC footprint predicate
object_wholeand instead usesthe more fine-grained
memory_slice.For
mlk_poly_getnoise_eta1122_4x, we also remove the soleuse of
same_objectin the code base, and remove its definitionfrom cbmc.h.