debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice: Add regression tests for all fixed bugs and separate the tests in ↵	stefanheule	2011-08-03
\| \| \| \|	'examples' into "read" examples and general tests.
*	Chalice: Use "/smoke" for the test suite by default to ensure test quality. ↵	stefanheule	2011-07-20
\| \| \| \|	Update all reference outputs accordingly.
*	Chalice: New test script to execute all tests (in all folder) at once. Test ↵	stefanheule	2011-07-07
\| \| \| \|	scripts now set the errorlevel to the number of failed tests.
*	Chalice: Four new interesting Chalice examples (added to test suite with the ↵	stefanheule	2011-07-05
\| \| \| \|	correct reference output). The example FictionallyDisjointCells.chalice is due to Yannis Kassios. Small fix to test script.
*	Chalice: Completely switch to new testing scripts (more flexible and ↵	stefanheule	2011-07-05
\| \| \| \|	fine-grained testing) and remove old test.bat. New testing scripts are described in Chalice/tests/readme.txt.
*	Chalice: New permission model that provides more abstraction and more ↵	stefanheule	2011-07-01
	flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/). This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced: - Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed - Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases - Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.) Currently not working - but planned to be updated as well - are the following features: - Stepwise refinements - autoFold - read locks There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice. A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs) - workitem 10200: Issue with the axiom of framing functions - workitem 10197: The translation of old(waitlevel) resultet in Boogie error - workitem 10196: Quantification over empty sequences - workitem 10195: Contradiction when descending sequences are used - workitem 10192: Invalid translation of old-construct in certain cases - workitem 10190: Stack overflow when parsing large comment blocks - workitem 10147: Duplicated method parameters and return values are not detected