summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* MergeGravatar allydonaldson2013-05-27
|\
* | Staged Houdini can now take a path to a file of ignored variablesGravatar allydonaldson2013-05-27
| |
| * MergeGravatar akashlal2013-05-27
| |\
| | * AbsHoudini: Added support for quantifiersGravatar akashlal2013-05-27
| | |
| * | Changed the 'CounterexampleComparer' to take traces into account.Gravatar wuestholz2013-05-26
| | |
| * | Changed the 'CounterexampleComparer' to take error messages of assertions ↵Gravatar wuestholz2013-05-24
| |/ | | | | | | into account.
| * fixed bug in reporting the number of typechecking errorsGravatar Unknown2013-05-22
|/ | | | updated answer file
* MergeGravatar allydonaldson2013-05-22
|\
* | Fixed bug in staged Houdini.Gravatar allydonaldson2013-05-22
| |
| * deleted some commented codeGravatar Unknown2013-05-20
| |
| * further bug fixes in og; global copies of global variables are now thread localGravatar Unknown2013-05-19
| |
| * MergeGravatar Unknown2013-05-18
| |\ | |/ |/|
| * reworked the linear and og implementation based on available variables theoryGravatar Unknown2013-05-18
| |
* | Adapted Houdini algorithm to take staging into accountGravatar allydonaldson2013-05-18
|/
* AbsHoudini: Tolerate some assertion failing. Updated regression baseline.Gravatar akashlal2013-05-10
|
* new files for fixedpoint engine backendGravatar Unknown2013-05-07
|
* merging changes for fixedpoint engine backendGravatar Ken McMillan2013-05-07
|\
* | Adding fixedpoint engine backendGravatar Ken McMillan2013-05-07
| |
| * havocs and updates to globals added only if they are non-nullGravatar Unknown2013-05-06
| |
| * MergeGravatar Unknown2013-05-06
| |\
| * | fixed bug (reported by Akash) in treatment of linear parameters to callsGravatar Unknown2013-05-06
| | |
| | * AbsHoudini: Each function can specify its own abstract domain. Also addedGravatar akashlal2013-05-05
| |/ | | | | | | typechecking
| * In the typecheck method of HavocCmd, added calls to typecheck the havoced varsGravatar Unknown2013-05-04
| |
| * MergeGravatar Unknown2013-05-04
| |\
| * | fixed bug reported by AkashGravatar Unknown2013-05-04
|/ /
| * Print "\n" after a YieldCmdGravatar akashlal2013-05-03
| |
| * Some code refactoringGravatar akashlal2013-05-03
|/
* MergeGravatar allydonaldson2013-04-30
|\
* | Staged HoudiniGravatar allydonaldson2013-04-30
| |
| * Added a little bit of virtual-ness to the Inliner class. This is so that I canGravatar akashlal2013-04-28
| | | | | | | | subclass it to implement my own inlining policy.
| * AbsHoudini: Bug fixGravatar akashlal2013-04-28
| |
| * AbsHoudini: Added support for /errorLimit:n, n > 1Gravatar akashlal2013-04-25
| |
| * AbsHoudini: Added predicate-abstraction domain and some examples.Gravatar akashlal2013-04-25
| |
| * AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,Gravatar akashlal2013-04-25
| | | | | | | | few bug fixes, hack to support missing prover declarations.
| * added free ensures to each procedure to compensate for havocing of allocatorGravatar Unknown2013-04-19
| |
| * Made OG-Desugared parsable as a Boogie program.Gravatar akashlal2013-04-19
| |
| * MergeGravatar akashlal2013-04-19
| |\
| | * AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute,Gravatar akashlal2013-04-19
| | | | | | | | | | | | intervals domain
| * | Fix mod-set traversal to do visit code inside code expressions.Gravatar Rustan Leino2013-04-18
| |/
| * AbsHoudini: Added support for /inlineDepth, and fixed the regression testsGravatar akashlal2013-04-18
| | | | | | | | (all pass)
| * Nice clean re-implementation of AbstractHoudini. And testsGravatar akashlal2013-04-18
| |
| * refactored og and fixed latest bug reported by chrisGravatar Unknown2013-03-20
| |
| * the allocator corresponding to every linear variableGravatar Unknown2013-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 transformGravatar Unknown2013-03-13
| |
| * added mod set checking to the linear type checkerGravatar Unknown2013-03-13
| |
| * fixed bugs in linear and ogGravatar Unknown2013-03-11
| | | | | | | | added triggers to the axioms for linear set desugaring
| * fixed bug in model printingGravatar Unknown2013-03-11
| | | | | | | | reverted a previous erroneous fix I had made in model parsing
| * Added another constructor to CallCmdGravatar akashlal2013-03-11
| |
| * Minor changes to AbstractHoudiniGravatar akashlal2013-03-10
| |
| * MergeGravatar Unknown2013-03-09
| |\ | |/ |/|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 09:54:53 +0000