Can't verify contracts for a method defined inside more than one impl block #3773
Description
I tried this code:
struct NonZero<T>(T);
impl NonZero<u32> {
#[kani::requires(true)]
fn unchecked_mul(self, x: u32) {}
}
impl NonZero<i32> {
#[kani::requires(true)]
fn unchecked_mul(self, x: i32) {}
}
#[kani::proof_for_contract(NonZero::unchecked_mul)]
fn verify_unchecked_mul() {
let x: NonZero<i32> = NonZero(-1);
x.unchecked_mul(-2);
}using the following command line invocation:
cargo kani -Z function-contracts
with Kani version: 0.56
I expected to see this happen: verification success
Instead, this happened: explanation
error: The function specified in the `proof_for_contract` attribute, `NonZero::unchecked_mul`, was not found.
Make sure the function is reachable from the harness.
--> src/lib.rs:63:1
|
63 | #[kani::proof_for_contract(NonZero::unchecked_mul)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)
error: could not compile `playground` (lib) due to 1 previous error; 2 warnings emitted
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.