[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.