Repository navigation
Cannot verify a constant function if crate has effect feature enabled #3258
Description
I tried this code:
#![feature(effects)]
#[kani::requires(kani::mem::can_dereference(arg))]
const unsafe fn dummy<T>(arg: *const T) -> T {
std::ptr::read(arg)
}
#[kani::proof_for_contract(dummy)]
fn check() {
unsafe { dummy(&kani::any::<u8>()) };
}using the following command line invocation:
kani -Z function-contracts -Z mem-predicates contract.rs
with Kani version:
I expected to see this happen: Verification should pass;
Instead, this happened: Compilation fails
error: mismatch in the number of generic parameters: original function/method `dummy` takes 2 generic parameters(s), stub `dummy_recursion_wrapper_8b0f77` takes 1
--> constant.rs:15:1
|
15 | #[kani::proof_for_contract(dummy)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)
Activity
celinval commentedon Jun 12, 2024
Note: For
effectsfeature, the compiler inserts an extra constant parameter named "host". More implementation details here:rust-lang/rust#113210
rust-lang/rust#118605
Fix contract of constant fn with effect feature (#3259)
Update toolchain to 10/25 (#3648)