-
Notifications
You must be signed in to change notification settings - Fork 12.8k
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.
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
Add drop intrinsic trait #3061
Labels
Milestone
Comments
Closed
Done. |
bors
pushed a commit
to rust-lang-ci/rust
that referenced
this issue
May 15, 2021
Fix help message for edition config option
RalfJung
pushed a commit
to RalfJung/rust
that referenced
this issue
Sep 25, 2023
Automatic sync from rustc
celinval
pushed a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
This commit adds a new `Dead` goto-instruction that gets codegened whenever Kani sees a MIR `StatementDead` statement. This new goto instruction corresponds to the CBMC [code_deadt]( https://diffblue.github.io/cbmc/classcode__deadt.html) statement that marks the point where a local variable goes out of scope. This new instruction is needed to detect invalid accesses of dead local variables. The commit also codegens a CBMC `Decl` instruction upon seeing a MIR StatementLive. This ensures that variables that go out of scope at the end of a loop are not falsely marked as having a dead dereference when they are accessed on the next loop iteration. Resolves rust-lang#3061. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
celinval
pushed a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
This is a follow-up on rust-lang#3063 that adds a test with multiple crates to make sure this scenario is correctly handled and that Kani reports the bug. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This will be the way to create types with destructors.
The text was updated successfully, but these errors were encountered: