debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
\| *	fixed emitter for CallCmd to include async	Unknown	2013-03-09
\| \|
* \|	Refactored MatchCandidate	allydonaldson	2013-03-08
\| \|
* \|	Merge	allydonaldson	2013-03-08
\|\ \
* \| \|	MatchCandidate modified to match candidates by variable name, rather than by ↵	allydonaldson	2013-03-08
\| \| \| \| \| \| \| \| \| \| \| \|	variable identity. ApplyAssignment method added, which takes a program (not necessarily the same program on which Houdini was invoked, but a program that has the same candidate set), and applies the Houdini assignment to the program.
\| \| *	Merge	Unknown	2013-03-07
\| \| \|\ \| \| \|/ \| \|/\|
\| \| *	updated the model parsing (probably caused by some change in Z3's output)	Unknown	2013-03-07
\| \| \|
\| \| *	added support for linear sets without useArrayTheory (but there is some ↵	Unknown	2013-03-07
\| \| \| \| \| \| \| \| \| \| \| \|	incompletness)
\| * \|	Fix LeastCommonAncestor method in Graph module	Nathan Chong	2013-03-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Solves a problem with Uniformity Analysis in GPUVerify. "The least common ancestor of two nodes u and v in a rooted tree T is a node w that is an ancestor of both u and v and that has the greatest depth in T" (CLR). This is needed when computing the control dependence relation of a CFG. In this case, we need the least common ancestor of a pair of nodes in the dominator tree so we can reuse the 'intersect' function given by Cooper et al in "A Simple, Fast Dominance Algorithm." The old code picked the ancestor of both u and v that has the least depth in T. This caused uniformity analysis, in GPUVerify, to be imprecise (adding blocks as non-uniform when they were infact uniform).
\| \| *	Merge	Unknown	2013-03-06
\| \| \|\ \| \|_\|/ \|/\| \|
\| \| *	in the process of adding support for linear sets without /useArrayTheory	Unknown	2013-03-06
\| \|/
\| *	removing GPUVerify and Dafny.sln	Unknown	2013-03-05
\| \|
\| *	Merge	Rustan Leino	2013-03-05
\| \|\
\| * \|	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \| \| \| \| \| \| \| \| \|	Codeplex repositories.
\| \| *	fixed datatype bug reported by Chris	Unknown	2013-03-05
\| \|/ \| \| \| \| \| \|	fixed function body referring to globals bug
* \|	Merge	allydonaldson	2013-03-05
\|\\|
\| *	fixed a bug in og	Unknown	2013-03-04
\| \|
\| *	fixed bugs in both parallel calls and linear stuff (reported by Chris)	Unknown	2013-03-03
\| \| \| \| \| \| \| \|	also added improved error reporting suggested by Chris
\| *	bug in OG for parallel call	Unknown	2013-03-02
\| \|
\| *	added parallel calls	Unknown	2013-03-01
\| \|
* \|	Merge	allydonaldson	2013-03-01
\|\\|
* \|	Fixed bug with predication, and fixed small problem with model generation ↵	allydonaldson	2013-03-01
\| \| \| \| \| \| \| \|	related to casting
\| *	removed call forall and * args to calls	Unknown	2013-02-23
\| \|
\| *	CR/LF line ending delta	Rustan Leino	2013-02-19
\| \|
\| *	Merge	Rustan Leino	2013-02-19
\| \|\
\| * \|	Fixed some type bugs in the interval domain.	Rustan Leino	2013-02-19
\| \| \|
\| \| *	AbstractHoudini: more details for computing a tighter predicate cover	Unknown	2013-02-15
\| \| \|
\| \| *	fixed bugs in typechecking of linear sets	Unknown	2013-02-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	added regressions to linear sets removed the need to supply the builtin map operations manually
\| \| *	fixed another bug reported by ChrisHaw	Unknown	2013-02-12
\| \| \| \| \| \| \| \| \| \| \| \|	Added an answer file
\| \| *	Further bug fixes in OG	Unknown	2013-02-05
\| \| \| \| \| \| \| \| \| \| \| \|	Added another sample
\| \| *	fixed bug in OG	Unknown	2013-02-01
\| \| \| \| \| \| \| \| \| \| \| \|	added another OG sample illustrating rely-guarantee encoding
\| \| *	handling old() in stable assertions	Unknown	2013-01-30
\| \| \| \| \| \| \| \| \| \| \| \|	bug fix in linear
\| \| *	Merge	Unknown	2013-01-29
\| \| \|\
\| \| * \|	made a whole bunch of changes to linear and og stuff	Unknown	2013-01-29
\| \| \| \|
\| \| \| *	Parse integers returned by Z3 into BigNum	akashlal	2013-01-29
\| \| \|/
\| \| *	bug fix reported by Chris	Unknown	2013-01-28
\| \| \|
\| \| *	added owicki-gries and linear-set to boogiedriver	Unknown	2013-01-25
\| \| \| \| \| \| \| \| \| \| \| \|	cleaned up the async type checking
\| \| *	first check in of Owicki-Gries and linear sets	Unknown	2013-01-24
\| \| \|
\| \| *	Output to Boogie\Binaries even in the Release version	Unknown	2013-01-25
\| \|/
\| *	Let Boogie clients determine their own version string	Rustan Leino	2013-01-23
\| \|
\| *	Refactored code that generates an axiom for a function, and changed the ↵	Rustan Leino	2013-01-17
\| \| \| \| \| \| \| \|	pretty printing to always reflect when a function body is inlined
\| *	Timeout in AbstractHoudini	akashlal	2013-01-16
\| \|
\| *	Allow attributes on procedure formals, function formals, and bound variables	Unknown	2013-01-07
\| \|
\| *	Some code clean-up	Unknown	2013-01-07
\| \|
\| *	Removed old comments about "BASEMOVE" and other constructor calls, where the ↵	Unknown	2013-01-07
\| \| \| \| \| \| \| \|	conversion from Spec# into C# moved a constructor call
\| *	bug fix for interaction between inlining and loops	Unknown	2013-01-04
\| \|
\| *	bug fix in model printing	Unknown	2013-01-04
\| \|
\| *	Use the new ProverInterface's Evaluate method in stratified inlinig	Unknown	2013-01-03
\| \| \| \| \| \| \| \|	(guarded by the flag /useProverEvaluate)
\| *	bug fix	Unknown	2012-12-28
\| \|
\| *	extended Evaluate to handle more types	Unknown	2012-12-28
\| \|
\| *	Some more changes to AbsHoudini	akashlal	2012-12-28
\| \|