flux
flux copied to clipboard
Failing to assume invariants on field when unfolding a struct
Why is the following program considered not safe ?
struct A {
val: u32,
}
impl A {
fn f(&mut self) -> () {
if self.val == 0 {
return;
}
let a = self.val - 1;
}
}
but the following is considered safe ?
fn f(val: u32) -> () {
if val == 0 {
return;
}
let a = val - 1;
}