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