debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \|	Codeplex repositories.
*	Chalice: Update reference output for all test-cases due to recent change in ↵	stefanheule	2012-09-11
\| \| \| \|	the output.
*	Chalice: Only show the "first" smoke warning, as once the prover is able to ↵	stefanheule	2011-07-21
\| \| \| \| \| \| \|	show false, all follwoing attempts will always succeed. However, smoke warnings on different paths through a method are still all reported. Also, the places where to insert "assert false" are chosen more carefully (essentially always all statements that inhale something). Update test reference outputs accordingly.
*	Chalice: Use "/smoke" for the test suite by default to ensure test quality. ↵	stefanheule	2011-07-20
\| \| \| \|	Update all reference outputs accordingly.
*	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