kani contracts cause false-positives for unused mut lint on the gcd example

[pnkfelix]

I tried this code, which was reduced from the recent blog post

#[kani::ensures(a % result == 0 && b % result == 0 && result != 0)]
fn gcd(mut a: u64, mut b: u64) -> u64 {
    (&mut a, &mut b);
    0
}

using the following command line invocation:

cargo kani  -Zfunction-contracts

with Kani version: Kani Rust Verifier 0.45.0 (cargo plugin)

I expected to see this happen: Kani runs with no incorrect lint warnings from Rust.

Instead, this happened: Kani prints this:

warning: variable does not need to be mutable
 --> src/main.rs:2:8
  |
2 | ...cd(mut a: u...
  |       ----^
  |       |
  |       help: remove this `mut`
  |
  = note: `#[warn(unused_mut)]` on by default

warning: variable does not need to be mutable
 --> src/main.rs:2:20
  |
2 | ...4, mut b: u...
  |       ----^
  |       |
  |       help: remove this `mut`

warning: 2 warnings emitted

The advice from these warnings is not correct; the mut modifiers on the bindings need to be there, due to the way the function bodies are written. (And if you follow the given advice, you do get hard errors about needing to put the mut's back.)

My advice: Just turn off the unused_mut linting in tool invocation done by the proc-macro, if you can.