Missing modifies clause triggers very confusing error

[celinval]

I tried this code:

#[kani::ensures(*val == 0)]
pub fn reset(val: &mut u8) {
    assign_default(val)
}

pub fn assign_default<T: Default>(dst: &mut T) {
    *dst = T::default();
}

#[kani::proof_for_contract(reset)]
fn check_reset() {
    let mut v = kani::any();
    reset(&mut v);
}

using the following command line invocation:

kani reset.rs

with Kani version:

I expected to see this happen: A message indicating that I tried to write to val which wasn't marked as modifiable.

Instead, this happened: I got the following error:

Failed Checks: Check that *dst is assignable
 File: "reset.rs", line 7, in assign_default::<u8>

I don't know how much we can improve this message here, but here are a few suggestions:

1. Rename assignable to modifiable (since in Kani we have a modifies clause).
2. Add a tip that maybe the contract is missing a modifies clause.
3. Ideally, we should print the name of the argument / static variable being assigned here instead of the local name.