debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Made 2 invariants of class 'CommandLineOptions' robust by:	wuestholz	2015-01-09
\| \| \| \| \| \| \|	- making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr)
*	Lets have a setter for TopLevelDeclarations as well	akashlal	2014-09-25
\|
*	Did more refactoring and addressed several todos.	wuestholz	2014-09-23
\|
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	Did some refactoring.	wuestholz	2014-09-23
\|
*	minor fix to abshoudini's handling of quantifiers	akashlal	2014-09-20
\|
*	a bug fix in Houdini (also AbsHoudini)	qadeer	2014-09-19
\|
*	InlineAssume attribute for ensures clauses; if present, the ensures ↵	qadeer	2014-09-18
\| \| \| \|	condition is assumed while inlining.
*	fixed a bug in inlining	qadeer	2014-09-17
\| \| \| \|	changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
*	Fix nasty bug introduced by commit 61a94f409975.	Dan Liew	2014-07-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
*	OnModel now carries the result of the prover call	akashlal	2014-06-28
\|
*	Minor fix to abshoudini	akashlal	2014-04-16
\|
*	(Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵	Rustan Leino	2014-02-24
\| \| \| \| \| \|	of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
*	Recursive walking of Exprs doesn't play nice when the depth of the AST is high.	akashlal	2014-01-07
\| \| \| \| \|	Reduce depth of AST whenever possible (e.g., use a binary tree instead of a linear list of terms)
*	binary tree of ANDs saves stack space	akashlal	2013-11-29
\|
*	AbsHoudini: Support timeout, MakeTop, InlineFunctions	akashlal	2013-11-02
\|
*	ExprSeq: 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 towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵	Ally Donaldson	2013-07-22
\| \| \| \|	plain Hashtable.
*	Did some refactoring in the execution engine and worked on the parallelization.	wuestholz	2013-07-01
\|
*	AbsHoudini: Bug fix, with bv constants.	akashlal	2013-06-19
\|
*	AbsHoudini: Bug fix	akashlal	2013-06-19
\|
*	AbsHoudini: Few more abstract domains	akashlal	2013-06-16
\|
*	AbsHoudini: added an implication domain	akashlal	2013-06-15
\|
*	AbsHoudini: Added support for quantifiers	akashlal	2013-05-27
\|
*	AbsHoudini: Tolerate some assertion failing. Updated regression baseline.	akashlal	2013-05-10
\|
*	AbsHoudini: Each function can specify its own abstract domain. Also added	akashlal	2013-05-05
\| \| \| \|	typechecking
*	Some code refactoring	akashlal	2013-05-03
\|
*	AbsHoudini: Bug fix	akashlal	2013-04-28
\|
*	AbsHoudini: Added support for /errorLimit:n, n > 1	akashlal	2013-04-25
\|
*	AbsHoudini: Added predicate-abstraction domain and some examples.	akashlal	2013-04-25
\|
*	AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,	akashlal	2013-04-25
\| \| \| \|	few bug fixes, hack to support missing prover declarations.
*	AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute,	akashlal	2013-04-19
\| \| \| \|	intervals domain
*	AbsHoudini: Added support for /inlineDepth, and fixed the regression tests	akashlal	2013-04-18
\| \| \| \|	(all pass)
*	Nice clean re-implementation of AbstractHoudini. And tests	akashlal	2013-04-18
\|
*	Minor changes to AbstractHoudini	akashlal	2013-03-10
\|
*	AbstractHoudini: more details for computing a tighter predicate cover	Unknown	2013-02-15
\|
*	Timeout in AbstractHoudini	akashlal	2013-01-16
\|
*	Some more changes to AbsHoudini	akashlal	2012-12-28
\|
*	AbstractHoudini optimization: replace summary predicate with Boolean variables	Unknown	2012-12-21
\| \| \| \|	(just like stratified inlining)
*	AbstractHoudini: more fixes, for self-recursion	akashlal	2012-12-16
\| \| \| \|	and Bilateral at the same time.
*	AbstractHoudini: bug fixes	akashlal	2012-12-16
\|
*	AbstractHoudini: support for generating a witness	Unknown	2012-12-15
\|
*	First implementation of ExplainHoudini	Unknown	2012-12-12
\|
*	More stuff for abstract houdini; updated test case	Unknown	2012-12-10
\|
*	Bug fix for abstract-houdini	Unknown	2012-12-07
\|
*	Allow richer spec for abs-houdini	Unknown	2012-12-03
\|