debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice: Two new test-cases for recently fixed problems.	stefanheule	2012-10-01
\|
*	Chalice: Activate the test-case tests/permission-model/scaling.chalice that ↵	stefanheule	2012-09-30
\| \| \| \|	was previously disabled due to performance problems.
*	Chalice: Add a test-case for a recently fixed issue.	stefanheule	2012-09-28
\|
*	Merge	stefanheule	2012-09-24
\|\
* \|	Chalice: New regression test-case.	stefanheule	2012-09-24
\| \|
* \|	Chalice: Add new regression test case.	stefanheule	2012-09-24
\| \|
\| *	added output for a test case	Unknown	2012-09-24
\| \|
\| *	Merge	Unknown	2012-09-21
\| \|\ \| \|/ \|/\|
\| *	Added linked list Chalice example	Unknown	2012-09-21
\| \|
* \|	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
\|/
*	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: Extend one test case with more complete specification.	stefanheule	2012-09-13
\|
*	Chalice: Update reference file for a test (a recent improvement makes the ↵	stefanheule	2012-09-13
\| \| \| \|	verifier more complete). Also remove an old comment from that test.
*	Chalice: Test case for permissions in function postconditions.	stefanheule	2012-09-12
\|
*	Chalice: Also add time information for reg_test, reg_test_all and runalltests.	stefanheule	2012-09-11
\|
*	Chalice: Update reference output for all test-cases due to recent change in ↵	stefanheule	2012-09-11
\| \| \| \|	the output.
*	Chalice: Adapt test scripts to not output timing information.	stefanheule	2012-09-11
\|
*	Chalice: implemented the final cases of the "inside" feature for predicates. ↵	Unknown	2012-09-08
\| \| \| \| \| \|	At the same time, exhaling an unfolding expression now generates corresponding secondary permission information (this can in principle be useful; with fractional permissions it need not be the case that just because we exhale (part of) a predicate, we don't have any left. Also added a test case to test the new non-aliasing knowledge the "inside" encoding provides in various situations.
*	Chalice: added list segment example	Unknown	2012-09-03
\|
*	Intermediate version of implementation with two masks per predicate. #m_calc ↵	Unknown	2012-08-09
\| \| \| \| \| \|	mask starts out as ZeroPMask and is added to during translation. #m mask starts out havoced, and is assumed to be equal to #m_calc as late as possible. This idea doesn't seem to work out, since the assumes generated come too late in the code for some of the asserts (which depend on framing information) to work. However, given the changes I made to funciton framing recently, I'm wondering if the havoced masks are even necessary any more. Next: try removing them and just using #m_calc for everything..
*	Added variant of list reverse example (see ↵	Unknown	2012-07-26
\| \| \| \|	tests/examples/list-reverse.chalice) with extra unfold/fold pairs (this used to break an intermediate version of the functions encoding).
*	Automatic merge.	stefanheule	2012-06-07
\|\
\| *	Chalice: Add regression test for unfolding expressions in predicates.	stefanheule	2012-06-03
\| \|
\| *	Chalice: Add regression test case for disallowed 'waitlevel' in predicates.	stefanheule	2012-06-03
\| \|
\| *	Chalice: Move list-revers.chalice test case to examples, and remove failing ↵	stefanheule	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 ↵	Unknown	2012-05-21
\| \| \| \| \| \| \| \|	unfold/fold pairs which currently confuse the encoding.
* \|	Chalice: Fix reference output of modified test (line number change).	stefanheule	2012-05-20
\| \|
* \|	Automatic merge.	stefanheule	2012-05-18
\|\\|
* \|	Chalice: Remove precondition that was previously necessary, but not any more.	stefanheule	2012-05-18
\| \|
* \|	Chalice: Update test reference output to account for an improvement in Chalice.	stefanheule	2012-05-17
\| \|
\| *	Merge	Christian Klauser	2012-03-27
\| \|\ \| \|/ \|/\|
\| *	Update test script shortcuts to work in Powershell (which supplies an ↵	Christian Klauser	2012-03-27
\| \| \| \| \| \| \| \|	absolute path as %0 instead of just the scripts name)
* \|	Chalice: Fix resolver bug, and add a test case for it.	stefanheule	2012-03-13
\| \|
* \|	Chalice: New test case to cover internally found bug (already fixed by ↵	stefanheule	2012-03-13
\| \| \| \| \| \| \| \|	changeset 30e940802059deb4d1e600c3c1fbcda5e39128eb).
* \|	Chalice: Adapt test and reference output to recent changes (previously ↵	stefanheule	2012-03-13
\| \| \| \| \| \| \| \|	failing test now verifies; i.e. Chalice is less incomplete).
* \|	Chalice: Disable refinement tests.	stefanheule	2012-03-13
\| \|
* \|	Chalice: two new test cases to test the predicates.	stefanheule	2012-03-12
\| \|
* \|	Chalice: two new tests to check the predicate fix.	stefanheule	2012-03-12
\| \|
* \|	Chalice: Fix counter.chalice test-case.	stefanheule	2012-03-08
\| \|
* \|	Semi-automatic merge.	stefanheule	2012-02-25
\|\\|
* \|	Chalice: add missing reference files for two tests.	stefanheule	2012-02-25
\| \|
* \|	Chalice: update test case to correctly reflect current Chalice state.	stefanheule	2012-02-25
\| \|
* \|	Chalice: New test case for predicates.	stefanheule	2012-02-25
\| \|
* \|	Chalice: New regression test case.	stefanheule	2012-02-25
\| \|
* \|	Chalice: Test scripts for predicate tests.	stefanheule	2012-02-25
\| \|
* \|	Chalice: Include predicate tests in runalltests.bat.	stefanheule	2012-02-25
\| \|
* \|	Chalice: Test case for negative permission in the secondary mask.	stefanheule	2012-02-25
\| \|
* \|	Chalice: Add testcase for mutually recursive predicates (failed before the ↵	stefanheule	2012-02-25
\| \| \| \| \| \| \| \|	last commit).