From: Clark Barrett Date: Tue, 23 Mar 2010 21:30:27 +0000 (+0000) Subject: Documented that ContextObj::destroy() only restores back to context level 0. X-Git-Tag: cvc5-1.0.0~9173 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=876993722316c92f6d24525e22c89c215ac90521;p=cvc5.git Documented that ContextObj::destroy() only restores back to context level 0. If there is more cleanup to do, it has to be done by the destructor. --- diff --git a/src/context/context.h b/src/context/context.h index 87e4e5fa1..455169a62 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -273,10 +273,14 @@ public: * ContextMemoryManager (see item 2 above). * 4. In the subclass implementation, any time the state is about to be * changed, first call makeCurrent(). - * 5. In the subclass implementation, the destructor should call destroy(). - * Unfortunately, the destroy() functionality cannot be in the ContextObj - * destructor since it needs to call the subclass-specific restore() method - * in order to properly clean up saved copies. + * 5. In the subclass implementation, the destructor should call destroy(), + * which repeatedly calls restore() until the object is restored to context + * level 0. Note, however, that if there is additional cleanup required at + * level 0, destroy() does not do this. It has to be implemented in the + * destructor of the subclass. The reason the destroy() functionality + * cannot be in the ContextObj destructor is that it needs to call the + * subclass-specific restore() method in order to properly clean up saved + * copies. */ class ContextObj { /** @@ -358,9 +362,10 @@ protected: /** * Should be called from sub-class destructor: calls restore until restored - * to initial version. Also removes object from all Scope lists. Note that - * this doesn't actually free the memory allocated by the ContextMemoryManager - * for this object. This isn't done until the corresponding Scope is popped. + * to initial version (version at context level 0). Also removes object from + * all Scope lists. Note that this doesn't actually free the memory + * allocated by the ContextMemoryManager for this object. This isn't done + * until the corresponding Scope is popped. */ void destroy() throw(AssertionException);