debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	qadeer	2013-12-02
\|\
* \|	added the QED build configuration	qadeer	2013-12-02
\| \|
\| *	Patch by Nathan Chong: iterative version of remove empty blocks algorithm. ↵	Ally Donaldson	2013-12-02
\|/ \| \| \|	This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems.
*	Fixedpoint VC catch up with recent changes	Ken McMillan	2013-11-11
\|
*	Merge duality changes to mainline	Ken McMillan	2013-11-09
\|\
\| *	handling timeouts for fixedpoint engines	Ken McMillan	2013-11-09
\| \|
* \|	code cleanup	akashlal	2013-11-02
\| \|
* \|	And a test case	akashlal	2013-10-21
\| \|
* \|	Bug fix in stratified inlining (triggered by {:inline} functions)	akashlal	2013-10-21
\| \|
* \|	Merge	Pantazis Deligiannis	2013-10-09
\|\ \
* \| \|	small refactoring	Pantazis Deligiannis	2013-10-02
\| \| \|
* \| \|	support for disabling loop entry invariant assertion checking	Pantazis Deligiannis	2013-10-01
\| \| \|
* \| \|	changes to support a configured errorLimit	Pantazis Deligiannis	2013-09-30
\| \| \|
* \| \|	more changes towards parallelisation of Houdini	Pantazis Deligiannis	2013-09-29
\| \| \|
\| * \|	refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of ↵	qadeer	2013-09-09
\| \| \| \| \| \| \| \| \| \| \| \|	GenerateVC
\| * \|	fixed bug introduced by the last checkin in letvciterative	qadeer	2013-09-08
\| \| \| \| \| \| \| \| \| \| \| \|	added /vc:i to all tests in stratifiedinline
\| * \|	fixed the problem with codexprs	qadeer	2013-09-07
\| \| \| \| \| \| \| \| \| \| \| \|	now positive/negative context is detected and appropriate translation is done
\| * \|	When a codeexpr is used at the top-level in an assume statement, we use the ↵	qadeer	2013-09-04
\| \| \| \| \| \| \| \| \| \| \| \|	alternative existential semantics.
\| * \|	Factored out the closure for codeexpr conversion so that it can be reused.	qadeer	2013-09-04
\| \| \| \| \| \| \| \| \| \| \| \|	Enabled it in stratified inlining.
\| * \|	Applied Chris Hawblitzel's changes to deal with {:expand}	qadeer	2013-08-23
\| \| \| \| \| \| \| \| \| \| \| \|	Erased {:yields} in the resulting sequential program in OwickiGriesTransform
* \| \|	Merge	Pantazis Deligiannis	2013-08-20
\|\\| \|
* \| \|	new option for reversing the topological order - this could potentially help ↵	Pantazis Deligiannis	2013-08-19
\| \| \| \| \| \| \| \| \| \| \| \|	to speedup houdini refutation of candidates
* \| \|	new option to disable checking for loop maintained invariants - this leads ↵	Pantazis Deligiannis	2013-08-15
\| \| \| \| \| \| \| \| \| \| \| \|	to an underapproximation that helps to speedup houdini refutation of candidates
\| * \|	Fixed a contract.	wuestholz	2013-08-09
\| \| \|
\| * \|	Fixed several build errors in the 'Checked' configuration.	wuestholz	2013-08-05
\|/ /
* \|	Removed the remaining pure collections.	wuestholz	2013-07-23
\| \|
* \|	Resolved some issues with data races.	wuestholz	2013-07-23
\| \|
* \|	Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵	wuestholz	2013-07-22
\| \| \| \| \| \| \| \|	code (as opposed to contracts).
* \|	All ...Seq classes now gone	Ally Donaldson	2013-07-22
\| \|
* \|	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
\| \|
* \|	Merge	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
\| \| \|
\| * \|	Fixed an issue with parallelization.	wuestholz	2013-07-22
\|/ /
* \|	Merge	Ally Donaldson	2013-07-22
\|\ \
* \| \|	Changed Has method of PureSequence to Contains to make refactoring easier.	Ally Donaldson	2013-07-22
\| \| \|
\| * \|	merge	Pantazis Deligiannis	2013-07-22
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	Fixed bugs arising from differences between hashtables and dictionaries	Ally Donaldson	2013-07-22
\| \| \|
* \| \|	Large refactoring of Hashtable to Dictionary.	Ally Donaldson	2013-07-22
\| \| \|
* \| \|	Merge	allydonaldson	2013-07-22
\|\ \ \
\| * \| \|	Fixed what looks like a type-related bug in the manipulation of ↵	allydonaldson	2013-07-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	newGotoCmdOrigins: this Hashtable is commented as having type TransferCmd -> ReturnCmd, but it was being used here as if the key type was Block.
* \| \| \|	Refactored variable2sequenceNumber to use Dictionary	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.
\| * \|	merge	Pantazis Deligiannis	2013-07-19
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	Populate a model only once.	Rustan Leino	2013-07-18
\| \| \|
\| * \|	Merge	Pantazis Deligiannis	2013-07-15
\|/\| \|