| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
parts of that test case (they are now reported as workitem 10221). Also, the assertion is now written as a postcondition.
|
|
|
|
| |
unfold/fold pairs which currently confuse the encoding.
|
|\ |
|
| |
| |
| |
| | |
absolute path as %0 instead of just the scripts name)
|
| |
| |
| |
| | |
without the specification inference component, because the latter is currently causing trouble with one of the AVL-tree examples.
|
| | |
|
| |
| |
| |
| | |
changeset 30e940802059deb4d1e600c3c1fbcda5e39128eb).
|
| | |
|
| |
| |
| |
| | |
Boogie. Command line options /print and /print:<file> can be used to inspect the Boogie file.
|
| | |
|
| |
| |
| |
| | |
failing test now verifies; i.e. Chalice is less incomplete).
|
| | |
|
| | |
|
| |
| |
| |
| | |
(namely, track folded predicates for unfoldings correctly)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
intermediate program to Boogie.
|
| | |
|
| |
| |
| |
| | |
translation process.
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
construction.
|
| | |
| | |
| | |
| | | |
permissions and its value should be preserved across heap havocs.
|
| |/
|/|
| |
| |
| |
| |
| |
| | |
that rd* permissions are preserved. Previously, rd-acquiring a rd*(f) from a
monitor invariant resulted in rd(f, 1), now it results in rd*(f).
Notice: Rd-scaling monitor invariants should eventually be solved in general,
currently all permissions (except rd*) are scaled down to rd(_, 1).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\
| |/
|/| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
information once.
|
| | |
|
| |
| |
| |
| | |
last commit).
|