debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Chalice: Implemented -vs switch, for use when running Chalice from inside ↵	rustanleino	2010-01-15
\| \| \| \|	Visual Studio
*	Chalice: updated Prelude to match new Boogie parsing of function parameters; ↵	rustanleino	2010-01-06
\| \| \| \|	fixed minor bug in Chalice grammar
*	Applied patch 4316, which fixes an unsoundness in the axiomatization of ↵	rustanleino	2009-11-05
\| \| \| \|	sequences (for both Dafny and Chalice). This in turn fixes issue 5876.
*	- Sieve.chalice verifies + executes faster	jansmans	2009-10-20
\|
*	- the "-gen" option works only if the program verifies	jansmans	2009-10-16
\|
*	Implicitly declare as local variables undeclared variables occurring as ↵	rustanleino	2009-10-16
\| \| \| \|	LHS's of CALL and RECEIVE statements (as was already done for FORK statements).
*	Sieve of Eratosthenes, written in Chalice.	rustanleino	2009-10-15
\|
*	- fixed a positioning bug in Parser.scala	jansmans	2009-10-07
\| \| \| \|	- CopyLessMessagePassing-with-ack2.chalice verifies (i.e. separate channel for acknowledgements)
*	- 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