Span of type error in contracts could be narrowed #3009
Description
I was having a go at transcribing the example from the recent blog post, and I encountered a sub-optimal diagnostic issue.
Test case:
#[kani::ensures(a % result && b % result == 0 && result != 0)]
fn gcd(a: u64, b: u64) -> u64 {
0
}The above currently generates the following from Kani:
error[E0308]: mismatched types
--> src/main.rs:1:1
|
1 | #[kani::ensures(a % result && b % result == 0 && result != 0)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `u64`
|
= note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)
error[E0308]: mismatched types
--> src/main.rs:1:1
|
1 | #[kani::ensures(a % result && b % result == 0 && result != 0)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `u64`
|
= note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)
error: aborting due to 2 previous errors
(I'm not sure why it prints two copies of the error message.)
I had a hard time seeing what was wrong, since the highlighted span was overly broad.
If you were to encode the contract as an assertion at the end of the method body and then invoke rustc, it produces a more precise diagnostic message:
error[E0308]: mismatched types
--> src/main.rs:13:13
|
13 | ...t!(a % result &&...
| ^^^^^^^^^^ expected `bool`, found `u64`
error: aborting due to 1 previous error
You can see how this more immediately reveals the source of the problem.