flux
flux copied to clipboard
Catch-all patterns
#[flux::sig(fn(i32[@n]) -> bool[0 < n])]
fn is_positive(x: i32) -> bool {
match x {
..=0 => false,
1.. => true,
}
}
Flux is able to verify the function is_positive
matches its signature. But if I replace the 1..
in the second match arm with _
then is says the postcondition might not hold. It seems like Flux isn't able to deduce what reaching the second match arm means about x
.
I should note that I came up with the above example while trying to isolate the error I got with the following code. My apologies if I've conflated two different issues.
#[flux::refined_by(l: int)]
#[flux::invariant(l >= 0)]
pub enum List {
#[flux::variant(List[0])]
Nil,
#[flux::variant((i32, Box<List[@n]>) -> List[n+1])]
Cons(i32, Box<List>),
}
impl List {
#[flux::sig(fn(&List[@l]) -> usize[l])]
fn len_const_memory(&self) -> usize {
let mut result = 0;
let mut this: &Self = self;
while let Self::Cons(_, tail) = this {
result += 1;
this = tail;
}
result // error: postcondition might not hold
}
}