Support loop modifies in loop contracts

[qinheping]

Requested feature: Allowing users to specify loop modifies instead of inferring them. Link to relevant documentation (Rust reference, Nomicon, RFC): #3167

Test case:

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

#[kani::proof]
fn simple_while_loop_with_old_harness() {
    let mut x: u8 = kani::any_where(|i| *i >= 2);
    let mut y: u8 = x;

    #[kani::loop_invariant(x >= 2 && y <= old(y)]
    #[kani::loop_modifies(x)]
    while x > 2 {
        x = x - 1;
    }

    assert!(x == 2);
}

[qinheping]

This feature will unblock https://github.com/model-checking/verify-rust-std/pull/131, https://github.com/model-checking/verify-rust-std/pull/130, and https://github.com/model-checking/verify-rust-std/pull/129.