debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	GPUVerify: merge ElementEncodingRaceInstrumenter into RaceInstrumenter	Peter Collingbourne	2012-06-22
\|
*	Boogie build succeeded	CodeplexBot	2012-06-23
\|
*	Dafny: now, equality-support determination and checking feels ripe; so, ↵	Rustan Leino	2012-06-22
\| \| \| \| \| \|	codatatypes would then be sound Dafny: added special case to allow equality comparison against parameter-less datatype values
*	Merge	Unknown	2012-06-22
\|\
* \|	Dafny: mark code for equality-support determination tentative	Unknown	2012-06-22
\| \|
* \|	Dafny: equality-support test cases. This is just a snapshot--some things ↵	Unknown	2012-06-22
\| \| \| \| \| \| \| \|	still to be fixed up.
* \|	Dafny: added contracts to IRewriter methods	Unknown	2012-06-22
\| \|
* \|	Dafny: allow "assume ..." as a refining statement (provided it replaces an ↵	Unknown	2012-06-22
\| \| \| \| \| \| \| \|	"assume E")
* \|	Dafny: deal with equality-support issues in refinements	Unknown	2012-06-22
\| \| \| \| \| \| \| \|	Dafny: a small amount of refactoring and bug fixes
\| *	GPUVerify: implement generic stride constraint generation	Peter Collingbourne	2012-06-22
\| \|
\| *	GPUVerify: make VarDefAnalysis capable of analysing non-constants	Peter Collingbourne	2012-06-22
\| \|
\| *	Dafny: Fixed bug in CompilerizeName.	chmaria	2012-06-22
\| \|
\| *	Dafny: fixed two contracts	Rustan Leino	2012-06-22
\| \|
* \|	Dafny: Since it's no longer true that all types support equality at run-time ↵	Unknown	2012-06-21
\| \| \| \| \| \| \| \|	(in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
\| *	GPUVerify: construct BV_AND and BV_SUB using MakeBVFunctionCall	Peter Collingbourne	2012-06-21
\| \|
\| *	GPUVerify: replace MayBe{ThreadConfigurationVariable,Gid}Analyser with ↵	Peter Collingbourne	2012-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	simple functions based on VariableDefinitionAnalysis This also unbreaks the stride race instrumentation for various subtle reasons.
\| *	Boogie build succeeded, 1 test(s) failed	CodeplexBot	2012-06-21
\|/
*	Chalice: Fix bug in PrettyPrinter reported by danieljost ↵	stefanheule	2012-06-20
\| \| \| \|	(http://boogie.codeplex.com/workitem/10224).
*	GPUVerify: make BuildNamedDefVisitor and SubstDualisedDefVisitor Duplicators	Peter Collingbourne	2012-06-20
\|
*	merge with Peter's changes	qadeer	2012-06-20
\| \| \| \|	moved the try-catch for IrreducibleLoopException upstream
*	Merge	qadeer	2012-06-20
\|\
\| *	GPUVerify: fix constant offset invariant generation for the case where no ↵	Peter Collingbourne	2012-06-20
\| \| \| \| \| \| \| \|	constants are found
\| *	Block predicator: handle StateCmd	Peter Collingbourne	2012-06-20
\| \|
* \|	a bug fix	qadeer	2012-06-19
\| \|
* \|	another edit for predication	qadeer	2012-06-19
\| \|
* \|	Merge	qadeer	2012-06-19
\|\\|
* \|	integrating predication	qadeer	2012-06-19
\| \|
\| *	Merge	Unknown	2012-06-19
\| \|\ \| \|/ \|/\|
\| *	Dafny: improved refinement features; added staged version of the proof of ↵	Unknown	2012-06-19
\| \| \| \| \| \| \| \|	the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible)
* \|	Merge	qadeer	2012-06-18
\|\ \
\| * \|	Backed out changeset: 7c8e7338652b	qadeer	2012-06-18
\| \| \|
* \| \|	Fix line endings	Peter Collingbourne	2012-06-18
\| \| \|
* \| \|	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.
\| * \|	Merge	qadeer	2012-06-17
\|/\| \|
\| * \|	an experiment trying to get predication into Boogie	qadeer	2012-06-17
\| \| \|
* \| \|	Dafny: fixed parsing bug.	Jason Koenig	2012-06-15
\| \| \|
* \| \|	GPUVerify: implement is-a-constant analysis	Peter Collingbourne	2012-06-15
\|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size.
* \|	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: when dualising assume and assert statements, emit two statements ↵	Peter Collingbourne	2012-06-15
\|/ \| \| \|	instead of a conjunction
*	Merge	Unknown	2012-06-14
\|\
* \|	Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵	Unknown	2012-06-14
\| \| \| \| \| \| \| \|	for special characters in identifiers
* \|	Merge	Unknown	2012-06-14
\|\ \
* \| \|	Dafny: fixed a couple of compiler bugs	Unknown	2012-06-14
\| \| \|
* \| \|	Dafny: cleaned up test scripts a little	Unknown	2012-06-14
\| \| \|
\| \| *	Inter-thread race checking implementation done.	Unknown	2012-06-14
\| \| \|
\| \| *	Fix for structured regions.	Unknown	2012-06-14
\| \| \|
\| \| *	Progress on inter-group race checking	Unknown	2012-06-14
\| \| \|
\| \| *	Merge	Unknown	2012-06-14
\| \| \|\ \| \| \|/ \| \|/\|
\| \| *	Started work on inter-group race checking.	Unknown	2012-06-14
\| \| \|