debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Converted test0/Arrays1.bpl test to OutputCheck style test.	Dan Liew	2014-05-12
\|
*	Remove old python testing scripts	Dan Liew	2014-05-11
\|
*	Enabled most of the name resolution lit tests. They don't all pass	Dan Liew	2014-05-05
\| \| \| \|	yet due to a bug in -useBaseNameForFileName.
*	disabled quantifier merging, except when no triggers are provided (as ↵	Unknown	2014-03-03
\| \| \| \|	discussed with Rustan)
*	cleaned up the OG code	qadeer	2013-08-07
\| \| \| \|	enabled it to be always on
*	added python scripts (work in unix and windows) for testing Z3 and CVC4 to ↵	Pantazis Deligiannis	2013-07-07
\| \| \| \|	many of the test suite dirs
*	removed call forall and * args to calls	Unknown	2013-02-23
\|
*	Allow attributes on procedure formals, function formals, and bound variables	Unknown	2013-01-07
\|
*	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 %
*	Boogie: Simplified (and liberalized) parsing of string literals as attribute ↵	Unknown	2012-03-12
\| \| \| \|	parameters
*	Boogie: added features to help with modular verification. In particular, ↵	Rustan Leino	2011-05-13
\| \| \| \|	define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.
*	Changed label checking for goto targets in StmtList so that they can be any ↵	qadeer	2011-04-21
\| \| \| \|	label in the current implementation.
*	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
*	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.
*	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.
*	Removed Output files. These are created on a local machine when the tests ↵	rustanleino	2009-08-07
\| \| \| \|	are run.
*	Initial set of files.	mikebarnett	2009-07-15