debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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.
*	Boogie: Added resolution and type checking for attributes on "call" and ↵	rustanleino	2010-03-09
\| \| \| \|	"call forall". Fixed printing of these attributes to print all attributes.
*	added support for printing attributes on calls via Emit	qadeer	2010-03-08
\|
*	added attributes to CallForallCmd as well	qadeer	2010-03-07
\|
*	added the ability to annotate calls with attributes	qadeer	2010-03-06
\|
*	Boogie:	rustanleino	2010-02-20
\| \| \| \| \| \| \| \| \| \| \|	* Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case) * Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads. * Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized * Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1 Boogie refactoring: * Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand * Cleaned up some parsing of command-line options
*	added an option /doModSetAnalysis specially for Zvonimir	qadeer	2010-02-20
\| \| \| \|	changed liveVarsBefore from Boogie.Set to Generics.Set
*	* Added "deprecated" comment in help message about /interprocInfer switch. ↵	rustanleino	2010-02-18
\| \| \| \| \| \| \|	The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
*	(no commit message)	qadeer	2010-02-12
\|
*	Z3 parameters to help it bail out of fruitless searches faster	mkawa	2009-12-05
\| \| \| \| \|	print _all_ the attributes of an assert this time add simpletypes to the visitor
*	print attributes in AssertCmd.Emit	mkawa	2009-12-02
\|
*	Added resolution and translation of algebraic datatypes and (in function ↵	rustanleino	2009-11-20
\| \| \| \| \| \|	bodies) match expressions. Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
*	Initial set of files.	mikebarnett	2009-07-15