debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	- extended to example to use acknowledgements (but uses sending debit)	jansmans	2009-10-07
\|
*	- verified a program inpsired by "Copyless Message Passing" in Chalice	jansmans	2009-10-07
\| \| \| \|	(todo: we should really support sending debit over channel to allow sending with acknowledgements)
*	- where clauses are now properly type-checked	jansmans	2009-10-02
\| \| \| \|	- all credits must be consumed on entry to a loop by the invariant (to avoid getting the wrong maxlock)
*	Implemented -noDeadlockChecks mode. With this mode, it is possible to give ↵	rustanleino	2009-10-01
\| \| \| \|	some demos that use locks before explaining the global order on locks.
*	- made the output of the Chalice-to-C# translator slightly nicer	jansmans	2009-08-17
\|
*	- Chalice-to-C# compiler now supports channels	jansmans	2009-08-17
\|
*	* Implemented channels	rustanleino	2009-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- channel declarations - send and receive statements - bounds clause for new, to accommodate channels - Added ProdConsChannel.chalice test case - Resolve and Translate (but no Compile yet) - Added Credits to global state in encoding (this caused changes to lots of source lines) * Simplified meaning of maxlock==E * Various parser improvements * Added alternative syntax for eval statements * Some renamings in error messages (e.g., install -> reorder) * Added preliminary parsing for condition variables and their wait and signal operations * Added new keywords to Chalice emacs mode
*	Made Makefile DOS friendly.	rustanleino	2009-08-06
\|
*	Parse channels and condition variables.	rustanleino	2009-08-05
\|
*	Initial set of files.	mikebarnett	2009-07-15