debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: fixed some test cases	Jason Koenig	2012-06-28
\|
*	Dafny: fixed bug with translation of class._System.object;	Jason Koenig	2012-06-28
\|
*	Dafny: Merge	Jason Koenig	2012-06-27
\|\
* \|	Dafny: fixed bug in which _module scope declarations were not verified.	Jason Koenig	2012-06-27
\| \|
* \|	Dafny: Fixed module bugs	Jason Koenig	2012-06-27
\| \|
\| *	GPUVerify: when building offset predicates, skip unsubstitutable offsets	Peter Collingbourne	2012-06-27
\| \| \| \| \| \| \| \|	Fixes Bugzilla bug #65.
\| *	GPUVerify: use original expression for undefined variables	Peter Collingbourne	2012-06-27
\| \| \| \| \| \| \| \|	Fixes Bugzilla bug #64.
* \|	Dafny: Implemented abstract modules	Jason Koenig	2012-06-26
\| \|
\| *	GPUVerify: implement generic reduced strength analysis for loop counters	Peter Collingbourne	2012-06-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	All counters which we are able to infer facts about now receive a candidate invariant _before_ predication, dualisation etc. This is probably a more natural place to insert such invariants, and means that they are also subject to predication etc. without us having to do anything. Also, kill the id plus constant analyses, which are no longer used.
\| *	GPUVerify: fix UnstructuredRegion.CmdsChildRegions	Peter Collingbourne	2012-06-26
\| \|
\| *	Model: sort variables by name	Peter Collingbourne	2012-06-26
\| \| \| \| \| \| \| \|	This makes the model file much easier to read.
\| *	Reinstated support for barrier flags.	Unknown	2012-06-27
\| \|
\| *	Undo bad merge.	afd	2012-06-27
\| \|
\| *	Merge	Unknown	2012-06-26
\| \|\
\| * \|	Added support for barrier flags.	Unknown	2012-06-26
\| \| \|
\| * \|	Merge	Unknown	2012-06-25
\| \|\ \
\| \| \| *	GPUVerify: factor all offset predicate handling code into a central location	Peter Collingbourne	2012-06-25
\| \| \| \|
\| \| \| *	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.
\| * \| \|	Merge	Unknown	2012-06-21
\| \|\ \ \
\| \| \| \| *	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	Jason Koenig	2012-06-19
\|\ \ \ \ \| \| \|_\|/ \| \|/\| \|
* \| \| \|	Dafny: disallow declare identifiers starting with underscore (_)	Jason Koenig	2012-06-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It is still possible to reference names containing an underscore, but it is not possible to make a variable, method, class, bound variable, type, or module name beginning with one.
* \| \| \|	Dafny: Added nested modules	Jason Koenig	2012-06-19
\| \| \| \|