| Commit message (Expand) | 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 |
| |/ |
|
| * | 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 |
|/ |
|
* | 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 |
| * | 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 |
| * | added free ensures to each procedure to compensate for havocing of allocator | Unknown | 2013-04-19 |
| * | Made OG-Desugared parsable as a Boogie program. | akashlal | 2013-04-19 |
| * | Merge | akashlal | 2013-04-19 |
| |\ |
|
| | * | AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute, | akashlal | 2013-04-19 |
| * | | 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 |
| * | 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 |
| * | 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 |
| * | fixed bug in model printing | Unknown | 2013-03-11 |
| * | 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 |
| | * | 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 incom... | Unknown | 2013-03-07 |
| * | | Fix LeastCommonAncestor method in Graph module | Nathan Chong | 2013-03-07 |
| | * | 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 Codepl... | Rustan Leino | 2013-03-05 |
| | * | fixed datatype bug reported by Chris | Unknown | 2013-03-05 |
| |/ |
|
* | | Merge | allydonaldson | 2013-03-05 |
|\| |
|