-
Notifications
You must be signed in to change notification settings - Fork 106
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Failing (trivial) assertion in presence of a quantifier over a slice #962
Comments
A small addendum, it seems this is because the assertions do not (always?) seem to trigger the quantifier. The quantifier being (at the Viper level):
while the array accesses in the Viper method are expressed as:
In order to verify the original example, it needs to properly trigger the quantifier at least once, so that this Viper function is called at least once, after which Silicon knows to connect
An example of a program that does verify: use prusti_contracts::*;
fn main() {}
#[requires(forall(|i: usize|
(0 <= i && i < slice.len()) ==> (slice[i] == i),
triggers=[(slice[i],)]
))]
#[requires(slice[0] == slice[0])] // dummy statement
pub fn test(slice: &mut [usize]) {
if slice.len() == 3 {
debug_assert!(slice[0] == 0);
debug_assert!(slice[1] == 1);
debug_assert!(slice[2] == 2);
}
} Although it is still interesting why it can verify the first 2 assertions in the original example but not the 3rd, I would expect all three assertions to fail due to the quantifier not triggering :D Also, for the working example there is no pre-condition that describes the length of Existing Github issues related to this one are #796 and #877. |
The following Rust program:
Fails verification with the error:
The weird part is that the first 2 assertions are verified okay, but then Prusti misses out on the third assertion (which should hold).
The text was updated successfully, but these errors were encountered: