Open nishanthkarthik opened 2 weeks ago
extern crate prusti_contracts; use prusti_contracts::*; fn external<'a>(t: &'a mut u32, r: &'a mut u32) -> &'a mut u32 { if *t == *r { t } else { r } } fn main() { let mut x = 1u32; let mut y = 1u32; let r: &mut u32 = external(&mut x, &mut y); *r += 0; // error x += *r - *r; }
Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:20:57 UTC