debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Uniformity analysis. Patch by Peter Collingbourne.	Unknown	2012-09-18
\|
*	Added functionality for race error reporting.	Egor Kyshtymov	2012-08-20
\|
*	Smart block predicator: track parents, and use to emit the invariant that if ↵	Peter Collingbourne	2012-08-06
\| \| \| \|	a loop is enabled then so is its parent
*	Smart block predicator: move *Map from parameters to fields	Peter Collingbourne	2012-08-06
\|
*	Smart block predicator: drop the unused createCandidateInvariants parameter	Peter Collingbourne	2012-08-06
\|
*	VCGeneration: implement smart predication	Peter Collingbourne	2012-07-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This predication algorithm is intended to reduce the complexity of predicated verification conditions by reducing the amount of predicated state and using only boolean algebra, as opposed to the previous algorithm which also uses integers. It assigns a unique predicate to every superblock, which is defined per Agrawal [1] except that superblocks are further partitioned such that either no element of the same superblock may be contained within a natural loop or each element of the superblock has the same innermost natural loop head. Predicates are assigned at the element of the superblock which dominates all others, and are reset to false at a loop head and at the start of a procedure in order to ensure correct execution for future iterations. When exiting a loop, all predicates corresponding to heads of exited loops are reset to false. The algorithm requires that every successor at every divergence point in the CFG contains assumes marked with an attribute (called ':partition') which a frontend uses to certify to the predicator that for each block, if each successor of that block contains an assume statement marked with :partition, exactly one of those assume statement's predicates will hold. The frontend we use for GPUVerify generates such attributes, and as such the new predicator is only used there, and the old predicator has been retained for Corral etc. [1] Hiralal Agrawal. Dominators, super blocks, and program coverage. In POPL '94, p25-34.
*	VCGen: add MergeBlocksIntoPredecessors function	Peter Collingbourne	2012-07-09
\|
*	Made error trace generation (without labels) more general for stratified	Unknown	2012-07-04
\| \| \| \|	inlining
*	Worked on cross-thread annotations.	Unknown	2012-07-03
\|
*	Added support for non-predicated assertions	Unknown	2012-07-02
\|
*	Started adding support for annotation intrinsics for unstructured programs.	Unknown	2012-07-02
\|
*	Merge	Unknown	2012-06-25
\|\
* \	Merge	Unknown	2012-06-21
\|\ \
\| \| *	merge with Peter's changes	qadeer	2012-06-20
\| \| \| \| \| \| \| \| \| \| \| \|	moved the try-catch for IrreducibleLoopException upstream
\| \| *	Merge	qadeer	2012-06-20
\| \| \|\ \| \| \|/ \| \|/\|
\| * \|	Block predicator: handle StateCmd	Peter Collingbourne	2012-06-20
\| \| \|
\| \| *	a bug fix	qadeer	2012-06-19
\| \| \|
\| \| *	another edit for predication	qadeer	2012-06-19
\| \| \|
\| \| *	integrating predication	qadeer	2012-06-19
\| \|/
\| *	Merge	qadeer	2012-06-18
\| \|\ \| \|/ \|/\|
\| *	Fix line endings	Peter Collingbourne	2012-06-18
\| \|
\| *	Move block predicator to VCGeneration	Peter Collingbourne	2012-06-18
\|/
*	deleted an unused class	qadeer	2012-06-12
\|
*	refactoring in SI	qadeer	2012-06-12
\|
*	Merge	qadeer	2012-06-10
\|\
* \|	1. changed new SI implemnetation so that it performs substitution for call sites	qadeer	2012-06-10
\| \| \| \| \| \| \| \|	2. changed the block expression to be the negation of the disjunction of all outgoing edges
\| *	Dafny/Boogie/BVD: made Dafny plug-in for BVD work again	Rustan Leino	2012-06-08
\|/
*	final (hopefully) fix to new SI	qadeer	2012-06-07
\|
*	testing a fix in SI	qadeer	2012-06-07
\| \| \| \| \|	also changing back the output path in BoogieDriver also disabling z3api for now since it does not build
*	Merging again	Ken McMillan	2012-06-07
\|\
\| *	Trying to merge with recent changes, failing.	Ken McMillan	2012-06-05
\| \|\
\| \| *	Some changes to support expanded use of z3api.	Ken McMillan	2012-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after).
* \| \|	Bug fix with mvInfo during VCGen	akashlal	2012-06-06
\| \| \|
* \| \|	update to SI	qadeer	2012-06-04
\|/ /
* \|	moved class Macro to Absy	qadeer	2012-06-04
\| \| \| \| \| \| \| \| \| \|	cleanup up DefineMacro Changed SI to use macros for reach info
* \|	added FindLeastToVerify to StratfiedVCGenBase as an abstract method	qadeer	2012-05-30
\| \|
* \|	moved a couple of overrides from StratifiedVCGen to StratifiedVCGenBase	qadeer	2012-05-30
\| \|
* \|	added support for recordProcCallSites to new SI	qadeer	2012-05-30
\| \|
* \|	extra recursion bound	akashlal	2012-05-30
\| \|
* \|	further refactoring of SI;	qadeer	2012-05-29
\| \| \| \| \| \| \| \|	removed the program argument to call to VerifyImplementation in Dafny
* \|	Removed program argument from VerifyImplementation. It is redundant since ↵	qadeer	2012-05-29
\| \| \| \| \| \| \| \| \| \| \| \|	the constructor of ConditionGeneration takes a program reference and stashes it in a field.
* \|	further refactoring	qadeer	2012-05-28
\| \|
* \|	more refactoring	qadeer	2012-05-28
\| \|
* \|	Merge	qadeer	2012-05-28
\|\ \
* \| \|	removed call site simplification from the old SI flow	qadeer	2012-05-28
\| \| \|
\| * \|	No need for extra attributes in ExtractLoops	akashlal	2012-05-28
\| \| \|
\| * \|	updating FindLeastToVerify to the new flow	akashlal	2012-05-28
\|/ /
* \|	Better interface for adding skipped calls, and	akashlal	2012-05-26
\| \| \| \| \| \| \| \|	adding extra recursion bound to some procedures.
* \|	new stratified inlining (initial prototype)	qadeer	2012-05-25
\| \|
* \|	more refactoring in stratified inlining	qadeer	2012-05-24
\| \|