You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
Resolvesrust-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.
This will be the way to create types with destructors.
The text was updated successfully, but these errors were encountered: