Loop contracts in closures and coroutines

[qinheping]

Requested feature: Currently loop contracts implementation in #3151 doesn't support loop contracts in closures and coroutines. We want to allow loop contracts be correctly applied in closures and coroutines.
Use case:
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167

Test case:

fn main() {
let mut x: u8 = 11;

let mut res = ||->u8 {    
    #[kani::loop_invariant(x >= 2)]
    while x > 2 {
        x = x - 1;
    }
    x
};

    assert!(res() == 2);
}