Conversation
| }) => if b { | ||
| conjunct |
There was a problem hiding this comment.
@vakaras If we inline a dummy trigger function body (with the body true) and also simplify, this would change semantics of quantifiers. Do you know in what order the inlining is performed?
There was a problem hiding this comment.
Yes, this can be a problem. For this and other reasons, it is better to use domain functions as triggers (with an axiom that says its value is always true).
prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs
Outdated
Show resolved
Hide resolved
|
|
||
| use prusti_contracts::*; | ||
|
|
||
| // ignore-test: prusti-constract functions used outside specification check not yet implemented |
There was a problem hiding this comment.
I'm not sure about "not yet" here: we don't want to implement something like this. Many specification functions don't make sense in executable code, and branching on time_credits or receipts is also such an example. I would remove this test.
There was a problem hiding this comment.
As they don't make sense in executable code why don't we report them when we find them?
There was a problem hiding this comment.
Because nobody has implemented that feature yet...
prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs
Outdated
Show resolved
Hide resolved
|
|
||
| use prusti_contracts::*; | ||
|
|
||
| // ignore-test: prusti-constract functions used outside specification check not yet implemented |
| fn safe_array_cmp<T: Eq>(a: &[T], b: &[T]) -> bool { | ||
| let mut i = 0; | ||
| let mut res = true; | ||
| while i < a.len() { |
There was a problem hiding this comment.
Why don't we need to put time_credits in the invariant?
There was a problem hiding this comment.
Prusti didn't complain so I thought I didn't have to and the loop.rs tests were passing without so I thought that it was okay but playing a bit with the generated Viper code showed me that it doesn't 😅
|
|
||
| use prusti_contracts::*; | ||
|
|
||
| // This test checks that setting the time reasoning option to false ignores timing constrains |
There was a problem hiding this comment.
As written in another comment, I don't think this should be the behaviour. This test also isn't even fully testing what the comment says: there is no timing specification to "ignore", only the default zero permissions.
Pialex99
force-pushed
the
time-reasoning
branch
from
36dcd2b to
c033436
Compare
Implications are brocken with time credits and receipts contraints as they are impure but Prusti translate them into ors which viper doesn't accept. Simplifying those expression solve this issue as they are changed back to an implication.
Pialex99
force-pushed
the
time-reasoning
branch
from
51798e1 to
31c8871
Compare
|
Superseded by #1408. |
3 participants
Add time reasoning functionality.