debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	A small fix in variable definition analysis.	Unknown	2012-08-29
\|
*	Added generation of invariants to restrict source location to sensible values.	Egor Kyshtymov	2012-08-28
\| \| \| \| \|	Refactored Make...Variable() and FindOrCreate...Variable() functions to take a variable name as a parameter rather than the variable itself.
*	Dafny: fixed contract bug in resolver	Rustan Leino	2012-08-27
\|
*	Added group information to race error reporting.	Egor Kyshtymov	2012-08-22
\|
*	Extra debugging output for Houdini	Unknown	2012-08-21
\|
*	Dafny and Boogie: get rid of 'static' fields in parser	Rustan Leino	2012-08-21
\|
*	Fixed problem where SOURCE variables were not being generated.	Unknown	2012-08-20
\|
*	Added functionality for race error reporting.	Egor Kyshtymov	2012-08-20
\|
*	DafnyExtension: simplified display of type names and field names	Unknown	2012-08-17
\|
*	DafnyExtension: various improvements	Unknown	2012-08-16
\|
*	Fixed bug where source location attributes are not being attached to a CHECK	Unknown	2012-08-16
\| \| \| \|	call, and refactored code to avoid the duplication which caused this error.
*	DafnyExtension: fixed more missing cases for hover texts	Unknown	2012-08-15
\|
*	Dafny: fixed some bugs in the newly added DafnyExtension code	Unknown	2012-08-15
\|
*	Dafny: added Statement.SubExpressions getter	Unknown	2012-08-15
\| \| \| \|	DafnyExtension: added hover text for identifiers
*	Merge	Unknown	2012-08-14
\|\
* \|	Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵	Unknown	2012-08-14
\| \| \| \| \| \| \| \|	crashing after certain deletes)
\| *	Added GPUVerifyBoogieDriver project.	Unknown	2012-08-14
\| \| \| \| \| \| \| \|	Contributed by Egor Kyshtymov.
\| *	Separated race checking into logging and checking calls. This simplifies	Unknown	2012-08-14
\| \| \| \| \| \| \| \|	error reporting.
\| *	Removed some dud code for handling nested maps, which we no longer support.	Unknown	2012-08-13
\| \|
\| *	Some more code cleanup related to removal of the "divided" option.	Unknown	2012-08-13
\| \|
\| *	Removed code related to "divided" option.	Unknown	2012-08-13
\|/
*	Merge	Unknown	2012-08-13
\|\
* \|	Barrier divergence checking now achieved via precondition.	Unknown	2012-08-13
\| \| \| \| \| \| \| \| \| \| \| \|	Race checking assertions contain tags to identify them. Attributes are passed correctly through the dualisation process.
\| *	Dafny: internal renaming	Unknown	2012-08-10
\| \|
\| *	Dafny: added heuristics for finding witnesses in assign-such-that checking	Unknown	2012-08-10
\| \|
\| *	DafnyExtension: hide execution-trace output, show split-expr related error ↵	Rustan Leino	2012-08-10
\| \| \| \| \| \| \| \|	locations, set a 10-second timeout
\| *	Dafny: fixed parser crash	Unknown	2012-08-09
\|/
*	Merge	Unknown	2012-08-09
\|\
* \|	Unstructured and smart predication are now default options for GPUVerify.	Unknown	2012-08-09
\| \| \| \| \| \| \| \| \| \| \| \|	The executable produced by building the project is now GPUVerifyVCGen. Refactored the way "other" functions are handled to make this more easily extensible.
\| *	DafnyExtension: improvements	Rustan Leino	2012-08-08
\| \|
\| *	Merge	Unknown	2012-08-08
\| \|\
\| * \|	Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and ↵	Unknown	2012-08-08
\| \| \| \| \| \| \| \| \| \| \| \|	visually indicates a non-verified buffer
* \| \|	Merge	Unknown	2012-08-07
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	Revised candidate invariant generation for barrier divergence checking.	Unknown	2012-08-07
\| \| \|
\| * \|	Houdini: recognise candidates of the form (p => (q => (... => (e => phi)))) ↵	Peter Collingbourne	2012-08-07
\|/ / \| \| \| \| \| \|	where e existential
* \|	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
\| \|
* \|	Dafny: corrected comment	Jason Koenig	2012-08-03
\| \|
* \|	Core: attach :partition to assumes generated from structured ifs and whiles	Peter Collingbourne	2012-08-03
\|/
*	Dafny: fixed bug in reverifying allowing old locals to be modified.	Jason Koenig	2012-08-01
\|
*	Dafny: reverify if the refining method modifies the heap.	Jason Koenig	2012-08-01
\|
*	Dafny: fixed bug where expressions were not replaced.	Jason Koenig	2012-08-01
\|
*	Dafny: support opening modules into the local scope	Jason Koenig	2012-07-30
\|
*	Dafny: removed allocated keyword, changed module import syntax. "opened" ↵	Jason Koenig	2012-07-30
\| \| \| \|	keyword is parsed but ignored.
*	GPUVerify: add an option which controls whether to use smart predication	Peter Collingbourne	2012-07-30
\|
*	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.
*	Graph: make DomRelation and DominatorMap public	Peter Collingbourne	2012-07-11
\|
*	BoogieDriver: correctly display time taken by prover if >60 seconds	Peter Collingbourne	2012-07-30
\|
*	Dafny: removed allocated, changed semantics of fresh	Jason Koenig	2012-07-29
\| \| \| \| \|	-allocated(x) removed, as really only useful in old(...) -old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).