Support struct field accessing in loop contracts

[qinheping]

Requested feature: Support of using struct.field in loop contracts
Use case: #[kani::loop_invariant(h.x == 2)]
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167

Test case:

struct hole{
    x: u8
}

#[kani::proof]
fn simple_while_loop_harness() {
    let mut h: hole = hole{ x: kani::any_where(|i| *i >= 2)};
    #[kani::loop_invariant(h.x == 2)]
    while h.x > 2 {
        h.x = h.x - 1;
    }

    assert!(h.x == 2);
}