diff options
author | Tim King <taking@google.com> | 2017-07-14 15:18:23 -0700 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2017-07-18 11:41:10 -0700 |
commit | 0f3b77bbd30be2388558000085d910d82e81d989 (patch) | |
tree | 073cf7d8b6a8ceddaca28aeba510df85af7fdf50 /src/context/context.cpp | |
parent | 53a226a753e509e028c386072c87d94c0a1316be (diff) |
Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap garbage.
Diffstat (limited to 'src/context/context.cpp')
-rw-r--r-- | src/context/context.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/context/context.cpp b/src/context/context.cpp index 2b781b95c..66d6a6542 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -296,6 +296,10 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) : d_pScope->addToChain(this); } +void ContextObj::enqueueToGarbageCollect() { + Assert(d_pScope != NULL); + d_pScope->enqueueToGarbageCollect(this); +} ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) { if(preNotify) { @@ -354,6 +358,29 @@ std::ostream& operator<<(std::ostream& out, return out << " --> NULL"; } +Scope::~Scope() { + // Call restore() method on each ContextObj object in the list. + // Note that it is the responsibility of restore() to return the + // next item in the list. + while (d_pContextObjList != NULL) { + d_pContextObjList = d_pContextObjList->restoreAndContinue(); + } + + if (d_garbage) { + while (!d_garbage->empty()) { + ContextObj* obj = d_garbage->back(); + d_garbage->pop_back(); + obj->deleteSelf(); + } + } +} + +void Scope::enqueueToGarbageCollect(ContextObj* obj) { + if (!d_garbage) { + d_garbage.reset(new std::vector<ContextObj*>); + } + d_garbage->push_back(obj); +} } /* CVC4::context namespace */ } /* CVC4 namespace */ |