debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Move block predicator to VCGeneration	Peter Collingbourne	2012-06-18
\|
*	GPUVerify: block predicator: add a mode which disables procedure predicates	Peter Collingbourne	2012-06-18
\| \| \| \| \|	This mode also conditionalises if statements to avoid problems with recursion.
*	GPUVerify: revert ac36537a0eb8, as this is in fact a candidate invariant ↵	Peter Collingbourne	2012-06-15
\| \| \| \| \| \|	(e.g. consider a loop within a conditional) Pointed out by Ally.
*	GPUVerify: the non-uniform loop invariant is not a candidate invariant	Peter Collingbourne	2012-06-12
\| \| \| \|	Thanks to Ally for pointing this out.
*	GPUVerify: emit non-uniform loop candidate invariant	Peter Collingbourne	2012-06-11
\|
*	GPUVerify: emit "uniform loop" candidate invariant	Peter Collingbourne	2012-06-11
\|
*	GPUVerify: fix line endings	Peter Collingbourne	2012-06-08
\|
*	GPUVerify: block predicator: use the name '_P' for the procedure predicate ↵	Peter Collingbourne	2012-06-07
\| \| \| \|	for consistency with the structured predicator
*	GPUVerify: emit assumes for backedges	Peter Collingbourne	2012-06-07
\| \| \| \| \| \|	Specifically, have the predicator emit backedge assumes with a :backedge attribute, and have the dualiser recognise such assumes and create an OR expression instead of an AND expression.
*	GPUVerify: use Concat instead of PureCollections.Sequence.operator+	Peter Collingbourne	2012-05-31
\|
*	GPUVerify: use a Formal for procedure predicates	Peter Collingbourne	2012-05-31
\|
*	GPUVerify: implement assume stealing in block predicator	Peter Collingbourne	2012-05-30
\|
*	GPUVerify: add block predicator	Peter Collingbourne	2012-05-25