Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Chalice: Fix bug in PrettyPrinter reported by danieljost ↵ | stefanheule | 2012-06-20 |
| | | | | (http://boogie.codeplex.com/workitem/10224). | ||
* | Chalice: Remove IsGoodState as it is not needed and causes problems in ↵ | stefanheule | 2012-06-07 |
| | | | | certain cases. | ||
* | Chalice: Add regression test for unfolding expressions in predicates. | stefanheule | 2012-06-03 |
| | |||
* | Chalice: Allow unfolding expressions in predicates (this fixes workitem 10223). | stefanheule | 2012-06-03 |
| | |||
* | Chalice: Add regression test case for disallowed 'waitlevel' in predicates. | stefanheule | 2012-06-03 |
| | |||
* | Chalice: Disallow 'waitlevel' in predicates. | stefanheule | 2012-06-03 |
| | |||
* | Chalice: Move list-revers.chalice test case to examples, and remove failing ↵ | stefanheule | 2012-05-24 |
| | | | | parts of that test case (they are now reported as workitem 10221). Also, the assertion is now written as a postcondition. | ||
* | Chalice: Added list reversal example, along with variants with extra ↵ | Unknown | 2012-05-21 |
| | | | | unfold/fold pairs which currently confuse the encoding. | ||
* | Merge | Christian Klauser | 2012-03-27 |
|\ | |||
* | | Update test script shortcuts to work in Powershell (which supplies an ↵ | Christian Klauser | 2012-03-27 |
| | | | | | | | | absolute path as %0 instead of just the scripts name) | ||
| * | Chalice: Added /boogieOpt:noinfer to chalice.bat in order to run Boogie ↵ | mschwerhoff | 2012-03-26 |
| | | | | | | | | without the specification inference component, because the latter is currently causing trouble with one of the AVL-tree examples. | ||
| * | Chalice: Fix resolver bug, and add a test case for it. | stefanheule | 2012-03-13 |
| | | |||
| * | Chalice: New test case to cover internally found bug (already fixed by ↵ | stefanheule | 2012-03-13 |
| | | | | | | | | changeset 30e940802059deb4d1e600c3c1fbcda5e39128eb). | ||
| * | Chalice: Fix tracking of folded predicates under old(). | stefanheule | 2012-03-13 |
| | | |||
| * | Chalice: By default use the new stdin method to pass the Boogie program to ↵ | stefanheule | 2012-03-13 |
| | | | | | | | | Boogie. Command line options /print and /print:<file> can be used to inspect the Boogie file. | ||
| * | Chalice: Do not print empty conditionals. | stefanheule | 2012-03-13 |
| | | |||
| * | Chalice: Adapt test and reference output to recent changes (previously ↵ | stefanheule | 2012-03-13 |
| | | | | | | | | failing test now verifies; i.e. Chalice is less incomplete). | ||
| * | Chalice: Make sure secondary permissions stay positive. | stefanheule | 2012-03-13 |
| | | |||
| * | Chalice: Disable refinement tests. | stefanheule | 2012-03-13 |
| | | |||
| * | Chalice: Fix problem introduced by backing out changeset 622fb6995ea4 ↵ | stefanheule | 2012-03-13 |
| | | | | | | | | (namely, track folded predicates for unfoldings correctly) | ||
| * | Backed out changeset: 622fb6995ea4 | stefanheule | 2012-03-13 |
| | | |||
| * | Chalice: two new test cases to test the predicates. | stefanheule | 2012-03-12 |
| | | |||
| * | Chalice: two new tests to check the predicate fix. | stefanheule | 2012-03-12 |
| | | |||
| * | Chalice: Fix treatment of 'unfolding' w.r.t. secondary permissions. | stefanheule | 2012-03-11 |
| | | |||
| * | Chalice: Simpler approach to tracking secondary permissions. | stefanheule | 2012-03-11 |
| | | |||
| * | Chalice: Command line option /noBplFile that directly passes the ↵ | stefanheule | 2012-03-10 |
| | | | | | | | | intermediate program to Boogie. | ||
| * | Chalice: Temporarily mark refinment extension as unsupported. | stefanheule | 2012-03-09 |
| | | |||
| * | Chalice: Catch errors during type-checking and parsing, just like for the ↵ | stefanheule | 2012-03-09 |
| | | | | | | | | translation process. | ||
| * | Automatic merge. | stefanheule | 2012-03-09 |
| |\ | |||
| * | | Chalice: Fix counter.chalice test-case. | stefanheule | 2012-03-08 |
| | | | |||
| * | | Chalice: Remove artifact from old model of handling permissions and havocing. | stefanheule | 2012-03-08 |
| | | | |||
| * | | Chalice: Add additional assumption about "held" field for "holds(o)" ↵ | stefanheule | 2012-03-08 |
| | | | | | | | | | | | | construction. | ||
| * | | Chalice: Fix problem with "held" ghost field, which is managed without ↵ | stefanheule | 2012-03-08 |
| | | | | | | | | | | | | permissions and its value should be preserved across heap havocs. | ||
| | * | Chalice: Modified permission scaling when rd-acquiring/releasing monitors such | mschwerhoff | 2012-03-07 |
| |/ |/| | | | | | | | | | | | | | 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). | ||
| * | Chalice: Fix chalice.bat to work with paths that contain spaces. | stefanheule | 2012-02-27 |
| | | |||
| * | Chalice: (change indendation of source file) | Unknown | 2012-02-27 |
| | | |||
| * | Chalice: Fix problem with calculating the dependencies of functions. | Unknown | 2012-02-27 |
| | | |||
| * | Chalice: Fix chalice.bat. | Unknown | 2012-02-27 |
| | | |||
| * | Chalice: fix error introduced by the previous merge. | stefanheule | 2012-02-25 |
| | | |||
| * | Semi-automatic merge. | stefanheule | 2012-02-25 |
| |\ | |/ |/| | |||
| * | Chalice: add missing reference files for two tests. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: update test case to correctly reflect current Chalice state. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: New test case for predicates. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: New regression test case. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: Handle unfolding in function preconditions. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: Disable "flags" for the auxiliary information of predicates. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: Recurse only one level for "unfold" when updating the secondary mask. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: Test scripts for predicate tests. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: Include predicate tests in runalltests.bat. | stefanheule | 2012-02-25 |
| | | |||
| * | Chalice: Add flag to only consider the predicate in the auxiliarly ↵ | stefanheule | 2012-02-25 |
| | | | | | | | | information once. |