debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merging complete. Everything looks good crosses fingers	Checkmate50	2016-06-06
\|
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	bug fixes in Duplicate.cs and parsing of invariant attributes	qadeer	2013-12-22
\| \| \| \|	other bug fixes in QED stuff
*	added syntax for par call and ParCallCmd	qadeer	2013-12-16
\|
*	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: PureCollections.Sequence not used anymore.	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	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
\|
*	Boogie: Simplified (and liberalized) parsing of string literals as attribute ↵	Unknown	2012-03-12
\| \| \| \|	parameters
*	updated Boogie strings so that they can refer to \" (and more)	qadeer	2012-03-12
\| \| \| \|	fixed BCT :value
*	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
\|
*	Fix atg file and add comment about Set/Variable/	Michal Moskal	2011-12-07
\|
*	commented calls to GC.Collect()	qadeer	2011-11-18
\|
*	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.
*	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: Added boolean code expressions (sans well-formedness checks on the ↵	rustanleino	2010-08-10
\| \| \| \|	input).
*	Boogie: Added an additional parameter 'defines' to the method ↵	wuestholz	2010-07-06
\| \| \| \|	'BoogiePL.Parser.Parse'.
*	Updated the frame files to work with the latest Coco/R. This entails not ↵	mikebarnett	2010-06-22
\| \| \| \| \| \|	having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files.
*	added attributes to CallForallCmd as well	qadeer	2010-03-07
\|
*	added the ability to annotate calls with attributes	qadeer	2010-03-06
\|
*	Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda ↵	MichalMoskal	2010-02-19
\| \| \| \|	expressions; they might not yet fully work for polymorphic maps.
*	Implement if-then-else expression.	MichalMoskal	2010-02-18
\|
*	Allow ":" in addition to "returns" in function definitions. Make the ↵	MichalMoskal	2009-12-17
\| \| \| \| \| \| \| \|	pretty-printer use ":" not "returns". Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions. Consequently foo(int,y:bool) is no longer allowed. Update the testsuite to match that.
*	Fixed problem where nullary function with definition had caused a crash.	rustanleino	2009-08-07
\|
*	Initial set of files.	mikebarnett	2009-07-15