debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"	Dan Rosén	2014-06-24
\| \| \| \| \| \|	When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off.
*	Fixed crash in resolver	Rustan Leino	2014-06-19
\|
*	Removed old test infrastructure files except for	Dan Liew	2014-05-28
\| \| \| \| \| \| \| \| \|	./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
*	Fix lit test suite when running Boogie under a path that contains	Dan Liew	2014-05-27
\| \| \| \|	spaces.
*	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