Support for old(..) expressions in loop invariants

[fpoli]

The following program makes Prusti raise an internal error, because currently old(..) expressions are only allowed in postconditions.

use prusti_contracts::*;

#[ensures(a % result == 0)]
#[ensures(b % result == 0)]
fn euklid(a: u32, b: u32) -> u32 {
    let mut c = 0;
    if a == 0 {
        if b == 0 {
            return 1;
        } else {
            return b;
        }
    } else {
        let mut a = a;
        let mut b = b;
        while b != 0 {
            body_invariant!(a % c == 0 && b % c == 0 && old(a) % a == 0 && old(b) % b == 0);
            c = a % b;
            a = b;
            b = c;
        }
        return a;
    }
}

fn main() {}

The suggested workaround is to store a copy of the arguments in local variables at the beginning of the function: let old_a = a; etc.