prusti-dev
prusti-dev copied to clipboard
Error with `extern crate prusti_contracts`
The following code fails with a error about snapshot equality not being a pure function, but only when using extern crate prusti_contracts; at the beginning of the file.
Without the first line, there are no errors:
extern crate prusti_contracts; // <== Removing this line removes the error
use prusti_contracts::*;
#[extern_spec(std::mem)]
#[ensures(snap(dest) === src)] // <== Error here
#[ensures(result === old(snap(dest)))]
fn replace<T>(dest: &mut T, src: T) -> T;
fn test() {
let mut a = 10;
std::mem::replace(&mut a, 5); // (No error if `replace` is never used)
}
[Prusti: invalid specification] use of impure function "uncategorized_problems::prusti_fn_not_pure::prusti_contracts::snapshot_equality" in pure code is not allowed