debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	bug fix for interaction between inlining and loops	Unknown	2013-01-04
\|
*	fixed bug in the inlineDepth option for houdini	qadeer	2011-11-23
\| \| \| \|	small clean up in the inlining implementation
*	added the option /inlineDepth:n. This option defaults to -1. If the user ↵	qadeer	2011-11-13
\| \| \| \| \| \|	provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute.
*	Boogie: Get rid of {:inline} attributes on axioms	Michal Moskal	2011-10-27
\|
*	Remove a testcase for bvInt (feature to be killed soon)	MichalMoskal	2011-02-18
\|
*	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
*	Fixed the implementation of inlining to deal with inlining depth properly.	qadeer	2010-01-30
\|
*	Fixed problem where nullary function with definition had caused a crash.	rustanleino	2009-08-07
\|
*	Initial set of files.	mikebarnett	2009-07-15