The `old` construct does not respect the function requirements

[celinval]

I tried this code:

#[kani::requires(val < i32::MAX)]
#[kani::ensures(|result| *result == old(val + 1))]
pub fn next(mut val: i32) -> i32 {
    val + 1
}

#[kani::proof_for_contract(next)]
pub fn check_next() {
    // Placing the restriction before calling makes the problem go away.
    // let _ = next(kani::any_where(|val: &i32| *val < i32::MAX));
    let _ = next(kani::any());
}

using the following command line invocation:

kani -Z function-contracts next.rs

with Kani version:

I expected to see this happen: Verification succeeded

Instead, this happened: Verification failed due to overflow:

Failed Checks: attempt to add with overflow
 File: "next.rs", line 2, in next_check_53aede

[artemagvanian]

Interestingly enough, the following code (with ensures and requires statements reordered) passes all checks:

#[kani::ensures(|result| *result == old(val + 1))]
#[kani::requires(val < i32::MAX)]
pub fn next(mut val: i32) -> i32 {
    val + 1
}

#[kani::proof_for_contract(next)]
pub fn check_next() {
    // Placing the restriction before calling makes the problem go away.
    // let _ = next(kani::any_where(|val: &i32| *val < i32::MAX));
    let _ = next(kani::any());
}

That might mean that we need to perform the old substitution before generating the requires clause.

[celinval]

Interesting. Unfortunately we cannot control the order that the attrbutes are processed. So we need to fix the attribute expansion.