[kasimte]

Resolves #4984.

A const fn taking self by value can't carry a function contract when Self has a destructor. It fails to compile with error[E0493]: destructor ... cannot be evaluated at compile-time.

This is motivated by model-checking/verify-rust-std#669, which needs this fix to put a contract on Box::<MaybeUninit<T>>::assume_init (a const unsafe fn).

The fix moves the owned receiver into the generated replace closure. Its drop then happens inside the closure instead of the const fn's own scope, where E0493 fires. Kani already does this for a contract's other arguments. It couldn't for self, which is a keyword and can't be rebound.

Using a move rather than std::mem::forget(self) is deliberate. Calling forget would also clear E0493, but it would skip the destructor and silently change what replace mode does. The move keeps the destructor, which runs after the contract's clauses. Only replace mode changes; the other modes already consume self through the body.

Other tests cover a const fn owned-Drop receiver in both check and replace mode, and a violated-ensures case that still fails, confirming checking isn't weakened. A non-const receiver through stub_verified asserts that its destructor runs exactly once, with a kani::cover! against a vacuous pass. A #[modifies] clause on by-value self is contrived, so that replace arm is left untested.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[kasimte]

Rebased onto current main. CI on the new head is waiting on workflow approval.

This fixes the E0493 a contracted const fn throws when self is taken by value and its type has a destructor (#4984).

Happy to rebase again. Thanks.

[Copilot]

🟡 Changes recommended

The tail receiver binding changes destructor order relative to owned arguments, altering existing replacement-mode behavior.

1 open issue

• Preserve receiver drop order after argument locals · New

What changed in this PR

This PR addresses #4984 by moving owned receivers into generated contract replacement closures, allowing contracts on const methods whose receiver types have destructors.

Changes:

• Detects by-value receivers and adds a receiver move after replacement-mode contract clauses.
• Preserves the tail move when additional contract attributes expand the generated body.
• Adds successful check/replace regressions and a failing-postcondition test.

File	Description
tests/​kani/​FunctionContracts/​const_fn_owned_receiver.rs	Tests const owned receivers in check and replace modes.
tests/​expected/​function-contract/​const_fn_owned_receiver_fail.rs	Tests detection of a violated postcondition.
tests/​expected/​function-contract/​const_fn_owned_receiver_fail.expected	Records the expected verification failure.
library/​kani_macros/​src/​sysroot/​contracts/​replace.rs	Generates and repositions the receiver move.
library/​kani_macros/​src/​sysroot/​contracts/​mod.rs	Defines the internal receiver binding name.
library/​kani_macros/​src/​sysroot/​contracts/​check.rs	Adds owned-receiver detection.

_{Review effort: Balanced}

[kasimte]

Addressed the drop-order comment and merged current main. Awaiting CI workflow approval.

[kasimte]

@feliperodri When you get a chance, this one just needs the CI workflow approved to run. Would appreciate a look whenever convenient. Thanks!

[feliperodri]

Reviewed the fix and the tests. Built the PR, and I confirmed the bug and the fix:

• const_fn_owned_receiver fails on main with E0493 and passes with this PR.
• All 16 FunctionContracts Kani tests pass; replace_receiver_drop passes too.
• const_fn_owned_receiver_fail passes.
• tests/expected/function-contract/as-assertions/assert-postconditions.rs fails on main as well, so it isn't caused by this PR.

The split_replace pop is needed: expand_replace re-splits a body that already ends with the move. The move comes after all borrows of self, so preconditions, remembers, havocs and postconditions are unaffected.

Comments (none block merging):

1. Pre-existing, tracked in #5118: replace stubs drop the owned receiver even when the real body moves it out. For fn id(self) -> Owned { self }, the real function drops nothing, but the stub's drop counter reads 1. replace_receiver_drop pins "dropped exactly once", which only holds for bodies that drop self. Please mention this limitation in the PR description or the contracts docs.
2. replace_receiver_drop is a regression guard. It passes on main; the fail-before test is const_fn_owned_receiver. The description could say so.
3. The motivating case, Box::<MaybeUninit<T>>::assume_init (verify-rust-std#669), is not covered by a test in this PR. Please check it against that PR.
4. Typed self: Box<Self> receivers are not tested. A valid const fn with that receiver and a Drop type doesn't compile even without Kani, so I don't think a test is needed.