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.
The following program makes Prusti raise an internal error, because currently
old(..)
expressions are only allowed in postconditions.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.