Support dereference in loop contracts

[zhassan-aws]

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