| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
|
| | |
|
| |
|
|
| |
to speedup houdini refutation of candidates
|
| |
|
|
| |
exhibit exit-free cycles
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
| | |
|
| |
|
|
| |
conversion from Spec# into C# moved a constructor call
|
| |
|
|
|
|
|
|
|
| |
- moved doomed and predication code into separate projects;
for doomed there is a static dependency from BoogieDriver
but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
|
| | |
|
| | |
|
| |
|
|
| |
implementation's CFG in Graphviz format
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
|
| |
|
|
|
|
| |
dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
|
| | |
|
| |
|
|
| |
nesting order
|
| |
|
|
| |
doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
|
| | |
|
| |
|
Dan Liew
Ally Donaldson
Pantazis Deligiannis
Nathan Chong
Unknown
Unknown
Unknown
Peter Collingbourne
qadeer
Unknown