summaryrefslogtreecommitdiff
path: root/Chalice
Commit message (Expand)AuthorAge
* Chalice: Add a test-case for a recently fixed issue.Gravatar stefanheule2012-09-28
* Chalice: changed quantifier triggering to use #limited#trigger versions of fu...Gravatar Unknown2012-09-27
* MergeGravatar stefanheule2012-09-24
|\
* | Chalice: New regression test-case.Gravatar stefanheule2012-09-24
* | Chalice: Fix type-checker incompleteness.Gravatar stefanheule2012-09-24
* | Chalice: Add new regression test case.Gravatar stefanheule2012-09-24
* | Chalice: Improve code to generate triggers for framing axiom.Gravatar stefanheule2012-09-24
* | Chalice: Fix triggers for framing axiom of known-folded locations.Gravatar stefanheule2012-09-24
| * added output for a test caseGravatar Unknown2012-09-24
* | Chalice: Fix soundness issue about when it is sound to keep knowledge about p...Gravatar stefanheule2012-09-21
* | Chalice: Alternative approach to frame known-folded locations; use quantifica...Gravatar stefanheule2012-09-21
| * MergeGravatar Unknown2012-09-21
| |\ | |/ |/|
| * Added linked list Chalice exampleGravatar Unknown2012-09-21
* | Chalice: Update release script to adapt to new scala version.Gravatar stefanheule2012-09-21
* | Chalice: New regression tests for fixed workitems 10189 and 10208.Gravatar stefanheule2012-09-20
* | Chalice: New regression test case from workitem 10221.Gravatar stefanheule2012-09-20
|/
* Chalice: Fix bug of computing the function height.Gravatar stefanheule2012-09-19
* Chalice: Use the framing function instead of the limited function in triggers...Gravatar stefanheule2012-09-19
* Chalice: Added a test case (general-tests/triggers) to test the trigger-gener...Gravatar Unknown2012-09-18
* Chalice: Updated linkedlist.chalice to include quantified specification, but ...Gravatar Unknown2012-09-18
* Chalice: Updated trigger generation to duplicate the entire quantifier in cas...Gravatar Unknown2012-09-18
* Chalice: modified trigger generation for quantifiers to include the use of ad...Gravatar Unknown2012-09-18
* Automatic MergeGravatar Unknown2012-09-17
|\
* | Chalice: modified Tr() to only generate a real list of statements when it's g...Gravatar Unknown2012-09-17
| * Chalice: Make the triggers for functions so it depends on all dependend predi...Gravatar stefanheule2012-09-14
| * Chalice: Extend one test case with more complete specification.Gravatar stefanheule2012-09-13
| * Chalice: Allow the postcondition axiom to be used when checking function spec...Gravatar stefanheule2012-09-13
| * Chalice: Merge the two definitional axioms (was previously necessary to work ...Gravatar stefanheule2012-09-13
| * Chalice: Update reference file for a test (a recent improvement makes the ver...Gravatar stefanheule2012-09-13
| * Chalice: Remove CanAssumeFunctionDefs from framing axiom, as it is not needed...Gravatar stefanheule2012-09-13
| * Chalice: Use the height of functions to increase the expressiveness of the po...Gravatar stefanheule2012-09-13
| * Chalice: Remove debug output.Gravatar stefanheule2012-09-13
| * Chalice: Compute the 'height' for functions (based on the condensation of the...Gravatar stefanheule2012-09-13
|/
* Chalice: Test case for permissions in function postconditions.Gravatar stefanheule2012-09-12
* Chalice: Disallow accessibility predicates in function postconditions.Gravatar stefanheule2012-09-12
* Chalice: Switch to latest Scala release (there seems to be a compiler bug wit...Gravatar stefanheule2012-09-12
* Chalice: Also add time information for reg_test, reg_test_all and runalltests.Gravatar stefanheule2012-09-11
* Chalice: Update reference output for all test-cases due to recent change in t...Gravatar stefanheule2012-09-11
* Chalice: Adapt test scripts to not output timing information.Gravatar stefanheule2012-09-11
* Chalice: New command line parameter /time:<n> that allows to output timing in...Gravatar stefanheule2012-09-11
* Chalice: implemented automatic trigger-finding for quantifiers in user-suppli...Gravatar Unknown2012-09-11
* Chalice: added findFunctionAppsContaining(..) to Expression, which finds all ...Gravatar Unknown2012-09-08
* Chalice: implemented the final cases of the "inside" feature for predicates. ...Gravatar Unknown2012-09-08
* Chalice: implemented "inside" information for all cases which translate to st...Gravatar Unknown2012-09-06
* Chalice: added "inside" knowledge of predicate instance nesting to unfold sta...Gravatar Unknown2012-09-06
* Chalice: first part of implementation of tracking which predicate instances o...Gravatar Unknown2012-09-06
* Chalice: MergeGravatar Unknown2012-09-05
|\
* | Chalice: support for static functions. Functions declared "static" are axioma...Gravatar Unknown2012-09-05
| * Chalice: Remove accidental changes to chalice.bat.Gravatar stefanheule2012-09-05
|/
* Chalice: adopted triggering/axioms used for "recursive" functions for all fun...Gravatar Unknown2012-09-04