-
Notifications
You must be signed in to change notification settings - Fork 100
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
Issues with verifying the result is None #1427
Comments
(I can't test this atm, but) does it make a difference if you remove these two postconditions from the extern spec? #[ensures(!result <==> self.is_none())]
#[ensures(!result <==> self.is_some())] |
It does not seem to make any difference... I've commented both/either one of them out, and they crash. If I comment out both post-conditions for
then, Prusti does not crash, but then it wouldn't be very helpful since we can't verify
|
This bug happens for the same reason as #1391. The problem is that for enums which are only used in specifications (pre- and postconditions, assertions) of a function but not in its body, some functions and axioms are not generated in the viper domain of the snapshot type. In particular, some constructors and the discriminant axioms are missing. In this case, the injectivity axiom is still present and refers to a missing constructor:
We can work around this bug by explicitly mentioning the type in the function body, which causes everything in the snapshot domain to be generated: #[pure]
fn test(u: u32) -> Option<u32> {
return None
}
#[requires(test(10).is_none())]
fn main() {
let _: Option<u32> = None;
} |
Hi, There seems to be a similar bug with
Prusti crashes if the post-condition for
the explicit mentioning of the type makes Prusti crash, only if the fuction is marked as pure. |
Hi, calling a function that always returns None from the pre/post-condition/ prusti assertions, i.e.,
produces errors:
Error 1:
Error 2:
If
test(..)
returns an Option of type tuple (i.e.,Option<(u32, u32)>
), then it additionally produces:In this simple example, returning
Some
from a branch fixes the issueHowever, say we have a struct
struct S1(Option<usize>)
with the following two methodsPrusti crashes if we compile as shown above, but it wouldn't if
filter(..)
doesn't guarantee P1 (i.e., omit P2 entirely, or modify it such that#[ensures(u <= 4 ==> result.is_none())]
. This fails normallyu
forfilter
tousize
and output toOption<usize>
(to match the field type ofS1
). But in this case, P1 always gets verified (regardless of the strength / presence of post-condition forfilter
)The same issue is observed when we convert the post-condition to a Prusti assertion instead.
Most interestingly, if we try to verify that the result is some (i.e.,
#[ensures(self.filter(10).is_some())]
), then Prusti doesn't crash.As reference, I defined the external specifications as follows, although this doesn't seem to be the problem
The text was updated successfully, but these errors were encountered: