Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | 2012-09-24 | |
|\ | |||
* | | Fixed issue with uniformity analysis and block merging. Uniformity analysis | 2012-09-24 | |
| | | | | | | | | now enabled by default. | ||
| * | Merge | 2012-09-24 | |
| |\ | |||
| * | | Chalice: New regression test-case. | 2012-09-24 | |
| | | | |||
| * | | Chalice: Fix type-checker incompleteness. | 2012-09-24 | |
| | | | |||
| * | | Chalice: Add new regression test case. | 2012-09-24 | |
| | | | |||
| * | | Chalice: Improve code to generate triggers for framing axiom. | 2012-09-24 | |
| | | | |||
| * | | Chalice: Fix triggers for framing axiom of known-folded locations. | 2012-09-24 | |
| | | | |||
| | * | Merge | 2012-09-24 | |
| |/| |/| | | |||
| | * | Added detailed trace functionality. | 2012-09-24 | |
| | | | | | | | | | | | | | | | Improved error reporting. Tidied up code. | ||
* | | | Merge | 2012-09-24 | |
|\ \ \ | |||
* | | | | Support for barrier invariants. | 2012-09-24 | |
| | | | | |||
| * | | | Merge | 2012-09-24 | |
| |\ \ \ | |||
| * | | | | added output for a test case | 2012-09-24 | |
| | | | | | |||
| | * | | | DafnyExtension: adding some missing keywords (for imports) | 2012-09-21 | |
| |/ / / |/| | | | |||
| | * | | Chalice: Fix soundness issue about when it is sound to keep knowledge about ↵ | 2012-09-21 | |
| | | | | | | | | | | | | | | | | predicate permission masks. | ||
| | * | | Chalice: Alternative approach to frame known-folded locations; use ↵ | 2012-09-21 | |
| | | | | | | | | | | | | | | | | quantification instead of explicit enumeration of locations. | ||
* | | | | Fixed a bug with empty big blocks. | 2012-09-21 | |
| | | | | |||
* | | | | Merge | 2012-09-21 | |
|\| | | | |||
* | | | | Added support for invariants about shared state. | 2012-09-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | Reworked implementation of barriers. Started on support for barrier invariants. | ||
| * | | | Merge | 2012-09-21 | |
| |\| | | |||
| * | | | Added linked list Chalice example | 2012-09-21 | |
| | | | | |||
| | * | | Chalice: Update release script to adapt to new scala version. | 2012-09-21 | |
| | | | | |||
| | * | | Merge | 2012-09-20 | |
| | |\ \ | |||
| | * | | | Chalice: New regression tests for fixed workitems 10189 and 10208. | 2012-09-20 | |
| | | | | | |||
| | * | | | Chalice: New regression test case from workitem 10221. | 2012-09-20 | |
| |/ / / | |||
| | * | | Merge | 2012-09-19 | |
| | |\ \ | | |/ / | |/| | | |||
| | * | | Boogie: improved parser makefile | 2012-09-19 | |
| | | | | |||
| * | | | Chalice: Fix bug of computing the function height. | 2012-09-19 | |
| | | | | |||
| * | | | Merge | 2012-09-19 | |
| |\ \ \ | |/ / / |/| | | | |||
* | | | | When uniformity analysis is disabled, no procedures (even the kernel entry | 2012-09-19 | |
| | | | | | | | | | | | | | | | | | | | | point) will be regarded as uniform. This simplification avoids various edge cases. | ||
| * | | | Chalice: Use the framing function instead of the limited function in ↵ | 2012-09-19 | |
| | | | | | | | | | | | | | | | | triggers to make them more permissive (and for instance fix a recent test failure). | ||
* | | | | Merge | 2012-09-18 | |
|\ \ \ \ | |||
* | | | | | Uniformity analysis. Patch by Peter Collingbourne. | 2012-09-18 | |
| | | | | | |||
| | * | | | Chalice: Added a test case (general-tests/triggers) to test the ↵ | 2012-09-18 | |
| | | | | | | | | | | | | | | | | | | | | trigger-generation feature | ||
| | * | | | Chalice: Updated linkedlist.chalice to include quantified specification, but ↵ | 2012-09-18 | |
| | | | | | | | | | | | | | | | | | | | | now the test does not pass.. this is a problem with triggering the framing axiom, if the way the function is mentioned in a state is under a quantifier... but it's about to be fixed :) | ||
| | * | | | Chalice: Updated trigger generation to duplicate the entire quantifier in ↵ | 2012-09-18 | |
| | | | | | | | | | | | | | | | | | | | | cases where different numbers of extra boolean variables are needed to generate different trigger sets. In this case, the resulting quantified assertions are conjoined together in the result. | ||
| * | | | | Dafny: Updated a test that would take a long time (almost 2h) to verify with ↵ | 2012-09-18 | |
| | |/ / | |/| | | | | | | | | | | Z3 4.1. | ||
| | * | | Chalice: modified trigger generation for quantifiers to include the use of ↵ | 2012-09-18 | |
| | | | | | | | | | | | | | | | | additional boolean variables to replace any sub-expressions that would be problematic in a candidate trigger (logical operators and comparison operators are forbidden). These extra variables are used in the triggers but not in the bnody of the quantifier. However, they need to be quantified over as well, and this creates a problem if different trigger sets employ different sets of extra variables. For the moment, the implementation groups all of the trigger sets by the sets of extra variables they use, and only outputs the first (in practice, often the only) such group. Hopefully this will be improved on soon. | ||
* | | | | Dualisation modified so that global arrays are not dualised, and group-shared | 2012-09-18 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | arrays are turned into 2D maps with first index type bool. Thread 1 always indexes into "true", while threads 2 indexes into "samegroup" (a formula which is true iff threads 1 and 2 are in the same group). Thus if the threads are in different groups they operate on different shared arrays, but if they are in the same group they operate on the same shared array. This paves the way for implementing support for barrier invariants. | ||
| * | | | Dafny: some test cases for "calc" (very cool!) | 2012-09-17 | |
| | | | | |||
| | * | | Automatic Merge | 2012-09-17 | |
| | |\ \ | |||
| | * | | | Chalice: modified Tr() to only generate a real list of statements when it's ↵ | 2012-09-17 | |
| | | | | | | | | | | | | | | | | | | | | going to be used (otherwise Nil is passed). | ||
| * | | | | Merge | 2012-09-17 | |
| |\ \ \ \ | |/ / / / |/| | | | | |||
| * | | | | Allow custom operators on a line | 2012-09-17 | |
| | | | | | |||
* | | | | | During dualisation, | 2012-09-17 | |
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | x := y; now becomes x$1 := y$1; x$2 := y$2; instead of x$1, x$2 := y$1, y$2; This is to make way for further changes. | ||
| * | | | Allow several calculation operators (for the whole calculation) | 2012-09-16 | |
| | | | | |||
| * | | | Allowing calc as hint (without braces) | 2012-09-16 | |
| | | | | |||
| * | | | Renamed terms into lines (according to the proposal), fixed some contracts | 2012-09-16 | |
| | | | | |||
| * | | | Added the new keyword (calc) to Util | 2012-09-16 | |
| | | | |