prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Error with `extern crate prusti_contracts`

Open Patrick-6 opened this issue 2 years ago • 0 comments

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

Patrick-6 avatar Mar 08 '23 09:03 Patrick-6