debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: Added CC translation of postconditions.	chmaria	2012-06-18
\|
*	Dafny: Added tests.	chmaria	2012-06-12
\|
*	Dafny: Added compiler tests.	chmaria	2012-06-11
\|
*	Dafny: Added infrastructure for compiler tests.	chmaria	2012-06-05
\|
*	Dafny: Added runtime checking tests.	chmaria	2012-06-05
\|
*	Dafny: Fix in the CC rewriter options.	chmaria	2012-06-05
\|
*	Dafny: Added CC translation of preconditions.	chmaria	2012-06-05
\|
*	Dafny: Added CC translation of assumptions.	chmaria	2012-06-05
\|
*	Dafny: Added CC translation of assertions.	chmaria	2012-06-04
\|
*	Dafny: Added infrastructure for runtime checking.	chmaria	2012-06-04
\|
*	Merge with default	Unknown	2012-06-01
\|\
* \|	1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵	Unknown	2012-06-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.
* \|	Dafny: Created a branch for runtime checking.	chmaria	2012-06-01
\| \|
\| *	GPUVerify: use Concat instead of PureCollections.Sequence.operator+	Peter Collingbourne	2012-05-31
\| \|
\| *	GPUVerify: resolve barrier implementation in unstructured mode	Peter Collingbourne	2012-05-31
\| \| \| \| \| \| \| \| \| \|	Resolution of goto labels is required for the graph builder to work.
\| *	GPUVerify: use a Formal for procedure predicates	Peter Collingbourne	2012-05-31
\|/
*	Merge	Unknown	2012-05-31
\|\
* \|	Dafny: Added map comprehensions and updated display syntax	Unknown	2012-05-31
\| \|
\| *	GPUVerify: teach analyses, dualiser and race instrumenter about assigns with ↵	Peter Collingbourne	2012-05-31
\| \| \| \| \| \| \| \|	multiple LHSs
\| *	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
\| \|
\| *	Merge	qadeer	2012-05-30
\| \|\
\| * \|	added support for recordProcCallSites to new SI	qadeer	2012-05-30
\| \| \|
\| \| *	GPUVerify: implement assume stealing in block predicator	Peter Collingbourne	2012-05-30
\| \|/
\| *	GPUVerify: disable barrier divergence check in unstructured mode for now	Peter Collingbourne	2012-05-30
\| \|
\| *	GPUVerify: have shared state abstraction, race instrumenter reuse blocks	Peter Collingbourne	2012-05-30
\| \| \| \| \| \| \| \| \| \|	Since we do not update transfer commands, they would otherwise refer to old blocks.
\| *	GPUVerify: factor shared state abstraction for unstructured blocks	Peter Collingbourne	2012-05-29
\| \|
\| *	Boogie build succeeded	CodeplexBot	2012-05-30
\| \|
\| *	extra recursion bound	akashlal	2012-05-30
\| \|
\| *	Merge	qadeer	2012-05-29
\| \|\ \| \|/ \|/\|
\| *	further refactoring of SI;	qadeer	2012-05-29
\| \| \| \| \| \| \| \|	removed the program argument to call to VerifyImplementation in Dafny
* \|	Merge	Unknown	2012-05-29
\|\ \
* \| \|	Dafny: fixed regression tests	Unknown	2012-05-29
\| \| \|
* \| \|	Dafny: Added maps to regression tests.	Unknown	2012-05-29
\| \| \|
\| \| *	Merge	qadeer	2012-05-29
\| \| \|\ \| \| \|/ \| \|/\|
* \| \|	Dafny: fixed minor map related issues	Unknown	2012-05-29
\| \| \|
\| \| *	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.
\| * \|	GPUVerify: factor the race instrumenter to handle unstructured blocks	Peter Collingbourne	2012-05-29
\| \| \|
\| * \|	GPUVerify: mark new work-item constants as non-unique	Peter Collingbourne	2012-05-29
\| \| \|
* \| \|	Dafny: Added compilation of finite maps	Unknown	2012-05-25
\| \| \|
\| * \|	GPUVerify: in unstructured mode, disable uniformity analysis and return ↵	Peter Collingbourne	2012-05-25
\| \| \| \| \| \| \| \| \| \| \| \|	conservative results
\| * \|	GPUVerify: implement a set of BV operation constructors which insert a ↵	Peter Collingbourne	2012-05-25
\| \|/ \| \| \| \| \| \|	function declaration if missing
\| *	Merge	qadeer	2012-05-28
\| \|\
\| * \|	further refactoring	qadeer	2012-05-28
\| \| \|
\| \| *	Boogie build succeeded	CodeplexBot	2012-05-29
\| \|/
\| *	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
\| \|/