Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | deleted some commented code | 2013-05-20 | ||
| | | | ||||
| * | | further bug fixes in og; global copies of global variables are now thread local | 2013-05-19 | ||
| | | | ||||
| * | | Merge | 2013-05-18 | ||
| |\ \ | |/ / |/| | | ||||
| * | | reworked the linear and og implementation based on available variables theory | 2013-05-18 | ||
| | | | ||||
* | | | Adapted Houdini algorithm to take staging into account | 2013-05-18 | ||
|/ / | ||||
* / | AbsHoudini: Tolerate some assertion failing. Updated regression baseline. | 2013-05-10 | ||
|/ | ||||
* | new files for fixedpoint engine backend | 2013-05-07 | ||
| | ||||
* | merging changes for fixedpoint engine backend | 2013-05-07 | ||
|\ | ||||
* | | Adding fixedpoint engine backend | 2013-05-07 | ||
| | | ||||
| * | havocs and updates to globals added only if they are non-null | 2013-05-06 | ||
| | | ||||
| * | Merge | 2013-05-06 | ||
| |\ | ||||
| * | | fixed bug (reported by Akash) in treatment of linear parameters to calls | 2013-05-06 | ||
| | | | ||||
| | * | AbsHoudini: Each function can specify its own abstract domain. Also added | 2013-05-05 | ||
| |/ | | | | | | | typechecking | |||
| * | In the typecheck method of HavocCmd, added calls to typecheck the havoced vars | 2013-05-04 | ||
| | | ||||
| * | Merge | 2013-05-04 | ||
| |\ | ||||
| * | | fixed bug reported by Akash | 2013-05-04 | ||
| | | | ||||
| | * | Print "\n" after a YieldCmd | 2013-05-03 | ||
| | | | ||||
| | * | Some code refactoring | 2013-05-03 | ||
| |/ | ||||
| * | add another test file | 2013-04-30 | ||
|/ | ||||
* | Merge | 2013-04-30 | ||
|\ | ||||
* | | Staged Houdini | 2013-04-30 | ||
| | | ||||
| * | Added a little bit of virtual-ness to the Inliner class. This is so that I can | 2013-04-28 | ||
| | | | | | | | | subclass it to implement my own inlining policy. | |||
| * | AbsHoudini: Bug fix | 2013-04-28 | ||
| | | ||||
| * | AbsHoudini: Added support for /errorLimit:n, n > 1 | 2013-04-25 | ||
| | | ||||
| * | AbsHoudini: Added predicate-abstraction domain and some examples. | 2013-04-25 | ||
| | | ||||
| * | AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini, | 2013-04-25 | ||
| | | | | | | | | few bug fixes, hack to support missing prover declarations. | |||
| * | added free ensures to each procedure to compensate for havocing of allocator | 2013-04-19 | ||
| | | ||||
| * | Test case for OG --> Houdini | 2013-04-19 | ||
| | | ||||
| * | Made OG-Desugared parsable as a Boogie program. | 2013-04-19 | ||
| | | ||||
| * | Added a test case | 2013-04-19 | ||
| | | ||||
| * | Merge | 2013-04-19 | ||
| |\ | ||||
| | * | AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute, | 2013-04-19 | ||
| | | | | | | | | | | | | intervals domain | |||
| * | | Fix mod-set traversal to do visit code inside code expressions. | 2013-04-18 | ||
| |/ | ||||
| * | AbsHoudini: Added support for /inlineDepth, and fixed the regression tests | 2013-04-18 | ||
| | | | | | | | | (all pass) | |||
| * | Nice clean re-implementation of AbstractHoudini. And tests | 2013-04-18 | ||
| | | ||||
| * | refactored og and fixed latest bug reported by chris | 2013-03-20 | ||
| | | ||||
| * | the allocator corresponding to every linear variable | 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 | 2013-03-13 | ||
| | | ||||
| * | added mod set checking to the linear type checker | 2013-03-13 | ||
| | | ||||
| * | fixed bugs in linear and og | 2013-03-11 | ||
| | | | | | | | | added triggers to the axioms for linear set desugaring | |||
| * | fixed bug in model printing | 2013-03-11 | ||
| | | | | | | | | reverted a previous erroneous fix I had made in model parsing | |||
| * | Added another constructor to CallCmd | 2013-03-11 | ||
| | | ||||
| * | Minor changes to AbstractHoudini | 2013-03-10 | ||
| | | ||||
| * | Merge | 2013-03-09 | ||
| |\ | |/ |/| | ||||
| * | fixed emitter for CallCmd to include async | 2013-03-09 | ||
| | | ||||
* | | Refactored MatchCandidate | 2013-03-08 | ||
| | | ||||
* | | Merge | 2013-03-08 | ||
|\ \ | ||||
* | | | MatchCandidate modified to match candidates by variable name, rather than by ↵ | 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 | 2013-03-07 | ||
| | |\ | | |/ | |/| | ||||
| | * | updated the model parsing (probably caused by some change in Z3's output) | 2013-03-07 | ||
| | | |