debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Core: attach :partition to assumes generated from structured ifs and whiles	Peter Collingbourne	2012-08-03
\|
*	Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).	Unknown	2012-04-04
\|
*	Emit of invariants now prints out the invariant attributes also	qadeer	2012-03-26
\|
*	Merge	Rustan Leino	2011-12-07
\|\
\| *	Make set iteration order deterministic	Michal Moskal	2011-12-07
\| \| \| \| \| \| \| \|	Make the set class generic
* \|	Boogie: Added new abstract interpretation harness, which uses native Boogie ↵	Rustan Leino	2011-12-05
\|/ \| \| \| \| \| \| \|	Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
*	Added lazy summary computation to stratified inlining (not finished yet)	akashlal	2011-11-20
\|
*	Added "free call" statements that don't check the precondition in the caller.	wuestholz	2011-09-14
\|
*	Fixed a bug with "don't care" return value on an async call	Unknown	2011-08-24
\|
*	more changes to bitvector analysis	qadeer	2011-08-09
\|
*	async call return value is either int or bv32	qadeer	2011-07-09
\|
*	early clearing of live variables and incarnation maps	qadeer	2011-06-24
\|
*	fixed a bug in ComputeAllLabels	qadeer	2011-04-27
\|
*	Changed label checking for goto targets in StmtList so that they can be any ↵	qadeer	2011-04-21
\| \| \| \|	label in the current implementation.
*	Made CallCmd.callee public for easy manipulation of un-resolved programs	akashlal	2011-03-21
\|
*	Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵	mikebarnett	2011-03-10
\| \| \| \| \| \|	dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
*	Changed the behavior of /doModSetAnalysis so that	qadeer	2010-12-15
\| \| \| \| \|	(1) Boogie errors due to modifies clause mismatch are suppressed (2) modset analysis is performed and modifies clauses of procedures with implementations are updated
*	Add ToString() overrides to help in debugging	MichalMoskal	2010-12-10
\|
*	stratified inlining: reuse call tree across queries	akashlal	2010-12-01
\|
*	Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln	qadeer	2010-12-01
\|
*	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
*	Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵	tabarbe	2010-08-26
\| \| \| \|	Core to jive with recent changes made to the cce class.
*	Boogie: Committing changed source files	tabarbe	2010-08-20
\|
*	Boogie: Renaming core sources in preparation for port commit	tabarbe	2010-08-20