Open vfukala opened 1 year ago
A minimized example. This program verifies (with default flags) despite the prusti_assert!(false);
:
use prusti_contracts::*;
struct List {
sz: usize
}
impl List {
#[trusted]
#[ensures(result.sz == 0)]
fn new() -> List { unreachable!() }
#[trusted]
#[requires(self.sz == 0)]
#[ensures(self.sz == 1)]
#[ensures(old(0 - self.sz) == 0)]
fn add_to_empty(&mut self) { unreachable!() }
}
fn main() {
let mut l = List::new();
l.add_to_empty();
prusti_assert!(false);
}
If any of the following conditions holds, the program (correctly) doesn't verify:
CHECK_OVERFLOWS=false
#[ensures(self.sz == 1)]
(line 14)#[ensures(old(0 - self.sz) == 0)]
(line 15)0 - self.sz
on line 15 to any of: 0
, self.sz
, or self.sz - 0
Nice catch! It seems that overflow conditions of old expressions are encoded without an old(..)
around them. That is, the postcondition old(0 - self.sz) == 0
is being encoded as self.sz == 0 && old(0 - self.sz) == 0
but it should be old(self.sz == 0) && old(0 - self.sz) == 0
.
prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs
still passes even whenprusti_assert!(false);
is added to line 115.The entire test case then looks like this:
This does not happen (the test case doesn't pass) when the
prusti_assert!(false);
is added before the threeassert!(get...
right above.(equivalently:) The test case doesn't pass if instead,
prusti_refute!(false);
is added to line 115.