debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	new files for fixedpoint engine backend	Unknown	2013-05-07
\|
*	merging changes for fixedpoint engine backend	Ken McMillan	2013-05-07
\|\
* \|	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\| \|
\| *	havocs and updates to globals added only if they are non-null	Unknown	2013-05-06
\| \|
\| *	Merge	Unknown	2013-05-06
\| \|\
\| * \|	fixed bug (reported by Akash) in treatment of linear parameters to calls	Unknown	2013-05-06
\| \| \|
\| \| *	AbsHoudini: Each function can specify its own abstract domain. Also added	akashlal	2013-05-05
\| \|/ \| \| \| \| \| \|	typechecking
\| *	In the typecheck method of HavocCmd, added calls to typecheck the havoced vars	Unknown	2013-05-04
\| \|
\| *	Merge	Unknown	2013-05-04
\| \|\
\| * \|	fixed bug reported by Akash	Unknown	2013-05-04
\| \| \|
\| \| *	Print "\n" after a YieldCmd	akashlal	2013-05-03
\| \| \|
\| \| *	Some code refactoring	akashlal	2013-05-03
\| \|/
\| *	add another test file	Unknown	2013-04-30
\|/
*	Merge	allydonaldson	2013-04-30
\|\
* \|	Staged Houdini	allydonaldson	2013-04-30
\| \|
\| *	Added a little bit of virtual-ness to the Inliner class. This is so that I can	akashlal	2013-04-28
\| \| \| \| \| \| \| \|	subclass it to implement my own inlining policy.
\| *	AbsHoudini: Bug fix	akashlal	2013-04-28
\| \|
\| *	AbsHoudini: Added support for /errorLimit:n, n > 1	akashlal	2013-04-25
\| \|
\| *	AbsHoudini: Added predicate-abstraction domain and some examples.	akashlal	2013-04-25
\| \|
\| *	AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,	akashlal	2013-04-25
\| \| \| \| \| \| \| \|	few bug fixes, hack to support missing prover declarations.
\| *	added free ensures to each procedure to compensate for havocing of allocator	Unknown	2013-04-19
\| \|
\| *	Test case for OG --> Houdini	akashlal	2013-04-19
\| \|
\| *	Made OG-Desugared parsable as a Boogie program.	akashlal	2013-04-19
\| \|
\| *	Added a test case	akashlal	2013-04-19
\| \|
\| *	Merge	akashlal	2013-04-19
\| \|\
\| \| *	AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute,	akashlal	2013-04-19
\| \| \| \| \| \| \| \| \| \| \| \|	intervals domain
\| * \|	Fix mod-set traversal to do visit code inside code expressions.	Rustan Leino	2013-04-18
\| \|/
\| *	AbsHoudini: Added support for /inlineDepth, and fixed the regression tests	akashlal	2013-04-18
\| \| \| \| \| \| \| \|	(all pass)
\| *	Nice clean re-implementation of AbstractHoudini. And tests	akashlal	2013-04-18
\| \|
\| *	refactored og and fixed latest bug reported by chris	Unknown	2013-03-20
\| \|
\| *	the allocator corresponding to every linear variable	Unknown	2013-03-13
\| \| \| \| \| \| \| \| \| \|	in the modset of a procedure is now put into the modset itself (in addition to the allocators for the output parameters)
\| *	Added explicit mod set analysis calls to OG transform and linear transform	Unknown	2013-03-13
\| \|
\| *	added mod set checking to the linear type checker	Unknown	2013-03-13
\| \|
\| *	fixed bugs in linear and og	Unknown	2013-03-11
\| \| \| \| \| \| \| \|	added triggers to the axioms for linear set desugaring
\| *	fixed bug in model printing	Unknown	2013-03-11
\| \| \| \| \| \| \| \|	reverted a previous erroneous fix I had made in model parsing
\| *	Added another constructor to CallCmd	akashlal	2013-03-11
\| \|
\| *	Minor changes to AbstractHoudini	akashlal	2013-03-10
\| \|
\| *	Merge	Unknown	2013-03-09
\| \|\ \| \|/ \|/\|
\| *	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
\| \|/
\| *	removed Test\GPUVerify	Unknown	2013-03-06
\| \|
\| *	removing GPUVerify and Dafny.sln	Unknown	2013-03-05
\| \|