Cannot verify a constant function with contracts #3254
Description
I tried this code:
#[kani::requires(true)]
#[inline]
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 dummy.rs
with Kani version:
I expected to see this happen: verification succeed
Instead, this happened: Kani failed to compile