debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice: added list segment example	Unknown	2012-09-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.
*	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)
\| *	Semi-automatic merge.	stefanheule	2012-02-25
\| \|\ \| \|/ \|/\|
\| *	Chalice: update reference output of AssocitationList (to remove bogus fail)	stefanheule	2012-02-25
\| \|
* \|	Chalice: Added missing reference output for AVLTree examples	mschwerhoff	2011-09-27
\| \|
* \|	Added Uri Juhasz' AVL-trees	Unknown	2011-09-08
\|/
*	Chalice: Add comment to a broken test-case.	stefanheule	2011-08-04
\|
*	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: only show warning about misleading smoke warnings if there are ↵	stefanheule	2011-08-03
\| \| \| \|	actually smoke warnings.
*	Chalice: Check definedness of where-clause of channels (was missing before), ↵	stefanheule	2011-07-22
\| \| \| \|	and smoke test for 'false' where clauses. Due to the missing definedness check, a mistake in the specification of CopyLessMessagePassing-with-ack2.chalice was not detected (and has been fixed now).
*	Chalice: Improve smoke testing: look for preconditions of functions, ↵	stefanheule	2011-07-22
\| \| \| \|	predicates and monitor invariants that are equivalent to false, and add a command line option "/smokeAll" to insert 'assert false' after every Chalice statement.
*	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: Fix all three copyless message passing programs. There were ↵	stefanheule	2011-07-19
\| \| \| \|	problems in the specification (all three programs) and the program itself ("..with-ack2"). Furthermore, if only two types of messages can be sent, a boolean flag is now used instead of an integer (to simplify the specifications).
*	Chalice: Fix batch file problem and update reference output.	stefanheule	2011-07-19
\|
*	Chalice: Smoke testing to find unreachable code, preconditions that are ↵	stefanheule	2011-07-18
\| \| \| \|	equivalent to false and assumptions that introduce contradictions. Can be used with the command line switch "-smoke".
*	Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is ↵	stefanheule	2011-07-07
\| \| \| \|	demonstrated in a new test case.
*	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