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

CBMC upgrade to 6.0.1 failed #3287

Closed
github-actions bot opened this issue Jun 24, 2024 · 0 comments
Closed

CBMC upgrade to 6.0.1 failed #3287

github-actions bot opened this issue Jun 24, 2024 · 0 comments

Comments

@github-actions
Copy link
Contributor

Updating CBMC from 5.95.1 to 6.0.1 failed.
The failed automated run can be found here.
@tautschnig tautschnig mentioned this issue Jun 24, 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
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@tautschnig