debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Changed all lambda-expression rewriting to be done as a pre-processing step ↵	Rustan Leino	2014-02-28
\| \| \| \| \| \|	before real verification. Fixed treatment of lambda-expression attributes.
*	Fixed bug in handling of break statements	Rustan Leino	2014-02-10
\|
*	bug fixes in Duplicate.cs and parsing of invariant attributes	qadeer	2013-12-22
\| \| \| \|	other bug fixes in QED stuff
*	added syntax for par call and ParCallCmd	qadeer	2013-12-16
\|
*	Stratified inlining: inject free requires as assumes at call site	akashlal	2013-10-25
\|
*	cleaned up the OG code	qadeer	2013-08-07
\| \| \| \|	enabled it to be always on
*	ExprSeq: farewell	Ally Donaldson	2013-07-22
\|
*	BlockSeq: farewell	Ally Donaldson	2013-07-22
\|
*	StringSeq: farewell	Ally Donaldson	2013-07-22
\|
*	CmdSeq: farewell	Ally Donaldson	2013-07-22
\|
*	Started to remove ...Seq classes	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring: PureCollections.Sequence not used anymore.	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Changed Has method of PureSequence to Contains to make refactoring easier.	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	Large refactoring of Hashtable to Dictionary.	Ally Donaldson	2013-07-22
\|
*	In the typecheck method of HavocCmd, added calls to typecheck the havoced vars	Unknown	2013-05-04
\|
*	Print "\n" after a YieldCmd	akashlal	2013-05-03
\|
*	Added another constructor to CallCmd	akashlal	2013-03-11
\|
*	fixed emitter for CallCmd to include async	Unknown	2013-03-09
\|
*	added parallel calls	Unknown	2013-03-01
\|
*	removed call forall and * args to calls	Unknown	2013-02-23
\|
*	added owicki-gries and linear-set to boogiedriver	Unknown	2013-01-25
\| \| \| \|	cleaned up the async type checking
*	Removed old comments about "BASEMOVE" and other constructor calls, where the ↵	Unknown	2013-01-07
\| \| \| \|	conversion from Spec# into C# moved a constructor call
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
*	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