debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	bug fixes in Duplicate.cs and parsing of invariant attributes	qadeer	2013-12-22
\| \| \| \|	other bug fixes in QED stuff
*	regenerated after updating Parser.frame	qadeer	2013-12-16
\|
*	added syntax for par call and ParCallCmd	qadeer	2013-12-16
\|
*	Removed the remaining pure collections.	wuestholz	2013-07-23
\|
*	Fixed the Coco/R grammar and regenerated the parser.	wuestholz	2013-07-22
\|
*	All ...Seq classes now gone	Ally Donaldson	2013-07-22
\|
*	ExprSeq: farewell	Ally Donaldson	2013-07-22
\|
*	StringSeq: farewell	Ally Donaldson	2013-07-22
\|
*	CmdSeq: farewell	Ally Donaldson	2013-07-22
\|
*	Started to remove ...Seq classes	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring: PureCollections.Sequence not used anymore.	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Refactoring of TypeVariableSeq	Ally Donaldson	2013-07-22
\|
*	Refactoring of VariableSeq and TypeSeq	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	added parallel calls	Unknown	2013-03-01
\|
*	removed call forall and * args to calls	Unknown	2013-02-23
\|
*	Refactored code that generates an axiom for a function, and changed the ↵	Rustan Leino	2013-01-17
\| \| \| \|	pretty printing to always reflect when a function body is inlined
*	Allow attributes on procedure formals, function formals, and bound variables	Unknown	2013-01-07
\|
*	Removed old comments about "BASEMOVE" and other constructor calls, where the ↵	Unknown	2013-01-07
\| \| \| \|	conversion from Spec# into C# moved a constructor call
*	Boogie: added type 'real' with overloaded arithmetic operations plus real ↵	boehmes	2012-09-27
\| \| \| \| \| \| \| \| \|	division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
*	Boogie: new syntax for integer division and modulus: use div and mod instead ↵	boehmes	2012-09-27
\| \| \| \|	of / and %
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
*	Dafny and Boogie: get rid of 'static' fields in parser	Rustan Leino	2012-08-21
\|
*	added attributes to loop invariants	qadeer	2012-03-23
\|
*	make the call to ProcessDataTypeConstructors in the right place	qadeer	2012-03-11
\|
*	Boogie: map the given filename stdin.bpl to standard input	Unknown	2012-03-09
\|
*	made delegate a datatype	qadeer	2011-12-30
\| \| \| \|	added a DatatypeConstructor class
*	Make set iteration order deterministic	Michal Moskal	2011-12-07
\| \| \| \|	Make the set class generic
*	changed the semantics of requires and ensures for inlined procedures	qadeer	2011-11-17
\|
*	Added "free call" statements that don't check the precondition in the caller.	wuestholz	2011-09-14
\|
*	Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵	wuestholz	2011-07-15
\| \| \| \|	some trailing whitespace.
*	Boogie: white-space formating	Rustan Leino	2011-06-05
\|
*	close the file stream opened by the parser	Unknown	2011-05-19
\|
*	Boogie: Eliminated a couple of warnings by removing unused variable ↵	wuestholz	2011-01-21
\| \| \| \|	declarations from the Boogie Coco/R grammar.
*	Factored out the ParserHelper class into a separate project and updated the ↵	wuestholz	2010-12-02
\| \| \| \| \| \|	files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
*	Updated parser.cs files to pick up the new .frame improvements from ↵	rustanleino	2010-10-26
\| \| \| \|	boogiepartners
*	Boogie:	rustanleino	2010-10-26
\| \| \| \| \| \| \| \| \|	* Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners. * It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs. Dafny: * Ditto for its Parser.cs/Scanner.cs. * Added ability to provide a custom Errors handler for scanner/parser. * Added Test/dafny1/Cubes.dfy
*	Boogie:	rustanleino	2010-09-23
\| \| \| \| \| \|	* Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
*	Changed the interface of Parse so that it can consume a program from a Stream	akashlal	2010-09-03
\|
*	Boogie: Committing changed source files	tabarbe	2010-08-20
\|
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20