Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | * | Merge | Nadia Polikarpova | 2012-09-21 | |
| | | | | |\ | | |_|_|_|/ | |/| | | | | ||||
| * | | | | | Fixed a bug with empty big blocks. | Unknown | 2012-09-21 | |
| | | | | | | ||||
| * | | | | | Merge | Unknown | 2012-09-21 | |
| |\| | | | | ||||
| * | | | | | Added support for invariants about shared state. | Unknown | 2012-09-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reworked implementation of barriers. Started on support for barrier invariants. | |||
| | * | | | | Merge | Unknown | 2012-09-21 | |
| | |\| | | | ||||
| | * | | | | Added linked list Chalice example | Unknown | 2012-09-21 | |
| | | | | | | ||||
| | | * | | | Chalice: Update release script to adapt to new scala version. | stefanheule | 2012-09-21 | |
| | | | | | | ||||
| | | * | | | Merge | stefanheule | 2012-09-20 | |
| | | |\ \ \ | ||||
| | | * | | | | Chalice: New regression tests for fixed workitems 10189 and 10208. | stefanheule | 2012-09-20 | |
| | | | | | | | ||||
| | | * | | | | Chalice: New regression test case from workitem 10221. | stefanheule | 2012-09-20 | |
| | |/ / / / | ||||
| | | | | * | Merge | Nadia Polikarpova | 2012-09-20 | |
| | | | | |\ | | | | |_|/ | | | |/| | | ||||
| | | | | * | Allow a single != in a calc | Nadia Polikarpova | 2012-09-20 | |
| | | | | | | ||||
| | | * | | | Merge | Unknown | 2012-09-19 | |
| | | |\ \ \ | | | |/ / / | | |/| | | | ||||
| | | * | | | Boogie: improved parser makefile | Unknown | 2012-09-19 | |
| | | | | | | ||||
| | | | | * | Not reusing RelOp parser in CalcOp to avoid the conflict between !in and ! | Nadia Polikarpova | 2012-09-19 | |
| | | | | | | ||||
| | | | | * | Well-formedness check for calc lines | Nadia Polikarpova | 2012-09-19 | |
| | | | | | | ||||
| | | | | * | Allow multiple calc/block statements in a hint. Removed the empty calc test ↵ | Nadia Polikarpova | 2012-09-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | from dafny2/Calculations, as it actually belongs in dafny0. | |||
| | * | | | | Chalice: Fix bug of computing the function height. | stefanheule | 2012-09-19 | |
| | | | | | | ||||
| | * | | | | Merge | stefanheule | 2012-09-19 | |
| | |\ \ \ \ | | |/ / / / | |/| | | | | ||||
| | | | | * | Made verification error message more explicit | Nadia Polikarpova | 2012-09-19 | |
| | | | | | | ||||
| | | | | * | Allow empty calc statements | Nadia Polikarpova | 2012-09-19 | |
| | |_|_|/ | |/| | | | ||||
| * | | | | When uniformity analysis is disabled, no procedures (even the kernel entry | Unknown | 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 ↵ | stefanheule | 2012-09-19 | |
| | | | | | | | | | | | | | | | | | | | | triggers to make them more permissive (and for instance fix a recent test failure). | |||
| * | | | | Merge | Unknown | 2012-09-18 | |
| |\ \ \ \ | ||||
| * | | | | | Uniformity analysis. Patch by Peter Collingbourne. | Unknown | 2012-09-18 | |
| | | | | | | ||||
| | | * | | | Chalice: Added a test case (general-tests/triggers) to test the ↵ | Unknown | 2012-09-18 | |
| | | | | | | | | | | | | | | | | | | | | | | | | trigger-generation feature | |||
| | | * | | | Chalice: Updated linkedlist.chalice to include quantified specification, but ↵ | Unknown | 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 ↵ | Unknown | 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 ↵ | wuestholz | 2012-09-18 | |
| | | |/ / | | |/| | | | | | | | | | | | | Z3 4.1. | |||
| | | * | | Chalice: modified trigger generation for quantifiers to include the use of ↵ | Unknown | 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 | Unknown | 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!) | Unknown | 2012-09-17 | |
| | | | | | ||||
| | | * | | Automatic Merge | Unknown | 2012-09-17 | |
| | | |\ \ | ||||
| | | * | | | Chalice: modified Tr() to only generate a real list of statements when it's ↵ | Unknown | 2012-09-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | going to be used (otherwise Nil is passed). | |||
| | * | | | | Merge | Nadia Polikarpova | 2012-09-17 | |
| | |\ \ \ \ | | |/ / / / | |/| | | | | ||||
| | * | | | | Allow custom operators on a line | Nadia Polikarpova | 2012-09-17 | |
| | | | | | | ||||
| * | | | | | During dualisation, | Unknown | 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) | Nadia Polikarpova | 2012-09-16 | |
| | | | | | ||||
| | * | | | Allowing calc as hint (without braces) | Nadia Polikarpova | 2012-09-16 | |
| | | | | | ||||
| | * | | | Renamed terms into lines (according to the proposal), fixed some contracts | Nadia Polikarpova | 2012-09-16 | |
| | | | | | ||||
| | * | | | Added the new keyword (calc) to Util | Nadia Polikarpova | 2012-09-16 | |
| | | | | | ||||
| * | | | | Added creation of source variable pre- and post- conditions. | Egor Kyshtymov | 2012-09-16 | |
|/ / / / | | | | | | | | | | | | | | | | | Changed style of error messages. Cleaned up error reporting code. | |||
| * | | | Error reporting for calculation steps | Nadia Polikarpova | 2012-09-14 | |
| | | | | ||||
| * | | | Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵ | Nadia Polikarpova | 2012-09-14 | |
| | | | | | | | | | | | | | | | | t<i> op t<i + 1>), generated during resolution; first version of the translation | |||
| | | * | Chalice: Make the triggers for functions so it depends on all dependend ↵ | stefanheule | 2012-09-14 | |
| | | | | | | | | | | | | | | | | predicate triggers (avoiding matching loops). | |||
| * | | | Merge | Nadia Polikarpova | 2012-09-14 | |
| |\ \ \ | |/ / / |/| | | | ||||
| * | | | Pretty-print calc statements | Nadia Polikarpova | 2012-09-14 | |
| | | | | ||||
| | | * | Chalice: Extend one test case with more complete specification. | stefanheule | 2012-09-13 | |
| | | | | ||||
| | | * | Chalice: Allow the postcondition axiom to be used when checking function ↵ | stefanheule | 2012-09-13 | |
| | | | | | | | | | | | | | | | | specifications in certain well-defined cases. | |||
| * | | | Resolve and clone calc statements; fixed a small grammar bug | Nadia Polikarpova | 2012-09-13 | |
| | | | |