Cannot annotate a const generic function with a contract #3667
Description
This issue was reported in model-checking/verify-rust-std#143.
I tried this code:
#[kani::requires(true)]
const fn bar<T>(_v: T)
where T: Sized
{
}using the following command line invocation:
kani s.rs -Zfunction-contracts
with Kani version: 1fe80f9
$ kani s.rs -Zfunction-contracts
Kani Rust Verifier 0.56.0 (standalone)
error[E0493]: destructor of `T` cannot be evaluated at compile-time
--> s.rs:2:17
|
1 | #[kani::requires(true)]
| - value is dropped here
2 | const fn bar<T>(_v: T)
| ^^ the destructor for this type cannot be evaluated in constant functions
error: aborting due to 1 previous error
For more information about this error, try `rustc --explain E0493`.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101