Support dereference in loop contracts #3866
Description
I tried this code:
#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]
#[kani::proof]
fn zero() {
const N: usize = 5;
let mut a: [i32; N] = kani::any();
let zeros = [0; N];
let s = &mut a;
let mut i = 0;
#[kani::loop_invariant(s[..i] == zeros[..i])]
while i < s.len() {
s[i] = 0;
i += 1;
}
assert!(a == zeros);
}using the following command line invocation:
kani zero.rs -Zloop-contracts
with Kani version: afd0469
I expected to see this happen: Verification successful
Instead, this happened:
$ kani zero.rs -Zloop-contracts
Kani Rust Verifier 0.58.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/kani_middle/transform/loop_contracts.rs:315:37:
internal error: entered unreachable code: The loop invariant support only reference of user variables. The provided invariants contain unsupported dereference. Please report github.com/model-checking/kani/issues/new?template=bug_report.md
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md
[Kani] no current codegen item.
[Kani] no current codegen location.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101