Prusti reports an "impure function" error when using standard arithmetic operators (like + or *) on references inside specifications.
Reproduction
use prusti_contracts::*;
#[pure]
#[requires(a + b <= std::u32::MAX)] // Error: use of impure function "std::ops::Add::add"
fn sum_ref(a: u32, b: &u32) -> u32 {
a + *b
}
#[pure]
#[requires(a * b > 0)] // Error: use of impure function "std::ops::Mul::mul"
fn mul_refs(a: &i32, b: &i32) -> i32 {
a * b
}
fn main() {}
Actual Behavior
error: [Prusti: invalid specification] use of impure function "std::ops::Add::add" in pure code is not allowed
error: [Prusti: invalid specification] use of impure function "std::ops::Mul::mul" in pure code is not allowed
Expected Behavior
Arithmetic operations on primitive references should be treated as pure, just like operations on values.
Prusti reports an "impure function" error when using standard arithmetic operators (like
+or*) on references inside specifications.Reproduction
Actual Behavior
Expected Behavior
Arithmetic operations on primitive references should be treated as pure, just like operations on values.