debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	removed some extraneous parameters	qadeer	2011-12-19
\|
*	Dafny: for a datatype with just one constructor, don't check (but do assume) ↵	Rustan Leino	2011-12-19
\| \| \| \|	that destructors are applied only to those values constructed by that one-and-only constructor
*	Dafny: compile to .exe only if there is a Main method; otherwise, compile to ↵	Rustan Leino	2011-12-19
\| \| \| \|	a .dll
*	fixed a completeness problem in houdini with inlining	qadeer	2011-12-18
\|
*	Fixed the Boogie build.	wuestholz	2011-12-16
\|
*	Merge	Unknown	2011-12-15
\|\
* \|	A few fixes to get GPUVerify working with OpenCL front-end.	Unknown	2011-12-15
\| \|
\| *	Dafny: Made sure that error locations refer to the Dafny program, even if ↵	wuestholz	2011-12-15
\| \| \| \| \| \| \| \|	the /print option is used.
\| *	Dafny: Added support for attributes on various specification constructs ↵	wuestholz	2011-12-07
\| \| \| \| \| \| \| \|	(assert, ensures, modifies, decreases, invariant).
\| *	Dafny: implemented thresholds for the new interval domain (/infer:j)	Rustan Leino	2011-12-12
\| \|
\| *	Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵	Rustan Leino	2011-12-12
\| \| \| \| \| \| \| \|	operator when negating <, <=, >=, or >
\| *	Merge	Rustan Leino	2011-12-10
\| \|\ \| \|/ \|/\|
\| *	Dafny: fix bug in translation of (the splitting of) if-then-else expressions ↵	Rustan Leino	2011-12-10
\| \| \| \| \| \| \| \|	(see bug report Issue 10214 on codeplex)
* \|	Merge	Unknown	2011-12-09
\|\ \
* \| \|	Some fixes to get GPUVerify close to working with OpenCL.	Unknown	2011-12-09
\| \| \|
\| * \|	Bring SourceView to front when double-clicking source line	stobies	2011-12-08
\| \|/
\| *	Dafny: corrected merge snafus	Rustan Leino	2011-12-07
\| \|
\| *	Dafny: reran Coco on merged Dafny.atg	Rustan Leino	2011-12-07
\| \|
\| *	Merge	Rustan Leino	2011-12-07
\| \|\
\| * \	Merge	Rustan Leino	2011-12-07
\| \|\ \
\| \| * \	Merge	Michal Moskal	2011-12-07
\| \| \|\ \ \| \|_\|/ / \|/\| \| \|
\| \| * \|	Fix atg file and add comment about Set/Variable/	Michal Moskal	2011-12-07
\| \| \| \|
\| \| * \|	Fix some bugs in the new Set	Michal Moskal	2011-12-07
\| \| \| \|
\| \| * \|	Make set iteration order deterministic	Michal Moskal	2011-12-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Make the set class generic
* \| \| \|	Merge	Unknown	2011-12-07
\|\ \ \ \
* \| \| \| \|	Changed names of builtins to make them generic.	Unknown	2011-12-07
\| \| \| \| \|
\| \| * \| \|	Merge	Rustan Leino	2011-12-07
\| \| \|\ \ \ \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable ↵	wuestholz	2011-12-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	wellformedness checks).
\| \| * \| \|	Dafny: fixed division in new interval domain	Rustan Leino	2011-12-07
\| \| \| \| \|
\| * \| \| \|	bug fix in houdini inlineDepth	qadeer	2011-12-06
\| \| \| \| \|
\| \| * \| \|	Merge	Rustan Leino	2011-12-06
\| \| \|\ \ \
\| * \| \ \ \	Merge	qadeer	2011-12-06
\| \|\ \ \ \ \ \| \| \| \|/ / / \| \| \|/\| \| \|
\| * \| \| \| \|	more logging	qadeer	2011-12-06
\| \| \| \| \| \|
\| \| * \| \| \|	Dafny: Made some minor changes to the grammar.	wuestholz	2011-12-06
\| \|/ / / /
\| \| * \| \|	Merge	Rustan Leino	2011-12-05
\| \| \|\ \ \ \| \| \|/ / / \| \|/\| \| \|
\| \| * \| \|	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}
\| * \| \| \|	further fixes to houdini	qadeer	2011-12-05
\| \| \| \| \|
\| * \| \| \|	Merge	qadeer	2011-12-05
\| \|\ \ \ \ \| \|/ / / / \|/\| \| \| \|
\| * \| \| \|	added more instrumentation to Houdini	qadeer	2011-12-05
\| \| \|/ / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	when vcgen fails, instead of stopping houdini, the failing vc is added to a list of blacklisted vcs fixed bug in the call graph generation when inlining is used
* / \| \|	Emit attribute on a requires	akashlal	2011-12-04
\|/ / /
* \| \|	VCC: Fixes for recent prelude changes	Michal Moskal	2011-12-02
\| \| \|
* \| \|	Boogie: Fixed a crash due to old expressions in lambda expressions that were ↵	wuestholz	2011-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	not replaced after lambda expansion. (reported by Florian Egli)
* \| \|	added a mechanism for supplying the list of input bpl files inside a .txt file	qadeer	2011-12-01
\|/ /
* \|	a bug fix in model parsing	qadeer	2011-11-30
\| \|
* \|	Merge	qadeer	2011-11-28
\|\ \
* \| \|	fixed a bug in model parsing	qadeer	2011-11-28
\| \| \|
\| * \|	Remove invariant that was just wrong	Michal Moskal	2011-11-28
\| \| \|
\| * \|	Merge	akashlal	2011-11-26
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Added option of turning off model generation in SI. Can be very expensive ↵	akashlal	2011-11-26
\| \| \| \| \| \| \| \| \| \| \| \|	sometimes.
* \| \|	Merge	qadeer	2011-11-24
\|\\| \|