Loop contracts: a write missing from loop_modifies is accepted at -Zmir-opt-level=2 (the kani_loop_modifies binding is optimized out) #5053

I tried this code:

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]

#[kani::proof]
fn opt2_modifies_ignored() {
    let mut i: u32 = 0;
    let mut hidden: u32 = 0;
    #[kani::loop_invariant(i <= 5)]
    #[kani::loop_modifies(&i)]
    while i < 5 {
        hidden = i;
        i = i + 1;
    }
    assert!(i == 5);
    std::hint::black_box(hidden);
}

using the following command line invocation:

RUSTFLAGS=-Zmir-opt-level=2 kani file.rs -Z loop-contracts

with Kani version: main (reproduces at -Zmir-opt-level 2 and above)

I expected to see this happen: verification fails. hidden is written inside the loop but is not in #[kani::loop_modifies(&i)], so the write is outside the declared modifies set. At -Zmir-opt-level=1 this is what happens: the harness fails Check that hidden is assignable.

Instead, this happened: at -Zmir-opt-level=2 and above, the harness reports VERIFICATION SUCCESSFUL. The write to hidden, absent from loop_modifies, is silently admitted.

Likely cause: nothing reads the kani_loop_modifies binding, so MIR optimizations at level 2 and above remove it. With the binding gone, CBMC infers the write set from the loop body instead of enforcing the declared clause. The #[inline(never)] keep-alive that #4946 added for the loop_decreases measure binding fixes it in a local test; the same keep-alive on the loop_modifies binding should force it to survive optimization.

Reported by @feliperodri while reviewing #4957.