summaryrefslogtreecommitdiff
path: root/Chalice/tests
Commit message (Expand)AuthorAge
* Chalice: Add regression test for unfolding expressions in predicates.Gravatar stefanheule2012-06-03
* Chalice: Add regression test case for disallowed 'waitlevel' in predicates.Gravatar stefanheule2012-06-03
* Chalice: Move list-revers.chalice test case to examples, and remove failing p...Gravatar stefanheule2012-05-24
* Chalice: Added list reversal example, along with variants with extra unfold/f...Gravatar Unknown2012-05-21
* MergeGravatar Christian Klauser2012-03-27
|\
* | Update test script shortcuts to work in Powershell (which supplies an absolut...Gravatar Christian Klauser2012-03-27
| * Chalice: Fix resolver bug, and add a test case for it.Gravatar stefanheule2012-03-13
| * Chalice: New test case to cover internally found bug (already fixed by change...Gravatar stefanheule2012-03-13
| * Chalice: Adapt test and reference output to recent changes (previously failin...Gravatar stefanheule2012-03-13
| * Chalice: Disable refinement tests.Gravatar stefanheule2012-03-13
| * Chalice: two new test cases to test the predicates.Gravatar stefanheule2012-03-12
| * Chalice: two new tests to check the predicate fix.Gravatar stefanheule2012-03-12
| * Chalice: Fix counter.chalice test-case.Gravatar stefanheule2012-03-08
| * Semi-automatic merge.Gravatar stefanheule2012-02-25
| |\ | |/ |/|
| * Chalice: add missing reference files for two tests.Gravatar stefanheule2012-02-25
| * Chalice: update test case to correctly reflect current Chalice state.Gravatar stefanheule2012-02-25
| * Chalice: New test case for predicates.Gravatar stefanheule2012-02-25
| * Chalice: New regression test case.Gravatar stefanheule2012-02-25
| * Chalice: Test scripts for predicate tests.Gravatar stefanheule2012-02-25
| * Chalice: Include predicate tests in runalltests.bat.Gravatar stefanheule2012-02-25
| * Chalice: Test case for negative permission in the secondary mask.Gravatar stefanheule2012-02-25
| * Chalice: Add testcase for mutually recursive predicates (failed before the la...Gravatar stefanheule2012-02-25
| * Chalice: update reference output of AssocitationList (to remove bogus fail)Gravatar stefanheule2012-02-25
| * Chalice: update reference output to new error messages.Gravatar stefanheule2012-02-25
* | Chalice: fix all refinement regression testsGravatar Kuat Yessenov2011-12-23
* | Chalice: partial fixes to the broken refinement extension regression tests.Gravatar Kuat Yessenov2011-12-21
* | Chalice: Added missing reference output for AVLTree examplesGravatar mschwerhoff2011-09-27
* | Added Uri Juhasz' AVL-treesGravatar Unknown2011-09-08
* | Chalice: Changed tests/runalltests.bat such that additional parameters can be...Gravatar mschwerhoff2011-08-15
|/
* Chalice: Add comment to a broken test-case.Gravatar stefanheule2011-08-04
* Chalice: Add regression tests for all fixed bugs and separate the tests in 'e...Gravatar stefanheule2011-08-03
* Chalice: only show warning about misleading smoke warnings if there are actua...Gravatar stefanheule2011-08-03
* Chalice: Check definedness of where-clause of channels (was missing before), ...Gravatar stefanheule2011-07-22
* Chalice: Improve smoke testing: look for preconditions of functions, predicat...Gravatar stefanheule2011-07-22
* Chalice: Only show the "first" smoke warning, as once the prover is able to s...Gravatar stefanheule2011-07-21
* Chalice: Use "/smoke" for the test suite by default to ensure test quality. U...Gravatar stefanheule2011-07-20
* Chalice: Fix all three copyless message passing programs. There were problems...Gravatar stefanheule2011-07-19
* Chalice: Fix batch file problem and update reference output.Gravatar stefanheule2011-07-19
* Chalice: Smoke testing to find unreachable code, preconditions that are equiv...Gravatar stefanheule2011-07-18
* Chalice: Also exhale correctly in two steps for multiple contracts (e.g. two ...Gravatar stefanheule2011-07-18
* Chalice: Fix a problem with permission expressions. Prevsiously, exhaling "ac...Gravatar stefanheule2011-07-18
* Chalice: New test script to execute all tests (in all folder) at once. Test s...Gravatar stefanheule2011-07-07
* Chalice: Error message of the valid-permission-check often included '<undefin...Gravatar stefanheule2011-07-07
* Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is d...Gravatar stefanheule2011-07-07
* Chalice: Four new interesting Chalice examples (added to test suite with the ...Gravatar stefanheule2011-07-05
* Chalice: Completely switch to new testing scripts (more flexible and fine-gra...Gravatar stefanheule2011-07-05
* Chalice: New permission model that provides more abstraction and more flexibi...Gravatar stefanheule2011-07-01