Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Prepare for CBMC version 6 #2972

Closed
tautschnig opened this issue Jan 11, 2024 · 0 comments
Closed

Prepare for CBMC version 6 #2972

tautschnig opened this issue Jan 11, 2024 · 0 comments
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Comments

@tautschnig
Copy link
Member

We will need to make changes in Kani to support CBMC version 6 (see diffblue/cbmc#7743), once that's released. See also #2952 for what's already failing.

The following changes will be required:
@tautschnig tautschnig added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Jan 11, 2024
tautschnig added a commit to tautschnig/kani that referenced this issue Feb 6, 2024
@tautschnig
Update to CBMC version 6.0.0
da76cb3 
Updates to match changes to the GOTO binary format.

Resolves: model-checking#2972
@tautschnig tautschnig mentioned this issue Feb 6, 2024
Merged
tautschnig added a commit that referenced this issue Jul 31, 2024
@tautschnig
Update to CBMC version 6.1.1 (#2995)
e4078b4 
Updates to match changes to the GOTO binary format.

Resolves: #2952, #2972, #3287, #3391

This includes changes our handling of storage markers to be marking
is-alive only rather than treating StorageLive as creating a new object.
That is, object instances are now tied to their Mir-provided
declarations (which, at present, only appear once per function). To
still account for when Rust scopes deem an object to be alive, we use
StorageLive and StorageDead to update __CPROVER_dead_object. This
(global) variable is used by CBMC's pointer checks to track when a
pointer may not be safe to dereference for it could be pointing to an
object that no longer is in scope.

Resolves: #3099
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@tautschnig