diff options
author | Tim King <taking@cs.nyu.edu> | 2010-03-23 19:41:49 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-03-23 19:41:49 +0000 |
commit | e11bce2790fa9e517e08ae5d3c477da651db3630 (patch) | |
tree | ffc4bb7cab3a6887c83fd3817c4cd79503d53a2c /src/expr/node_value.h | |
parent | 9576517676138a8ca2887a967f1b056662ef6754 (diff) |
Fixed some memory cleanup and destruction issues with ContextObj, ECData, CDList, and CDMap. Added the d_underTheShotgun field to NodeManager to keep track of which NodeValue is currently being deleted. If a Node or TNode has this node value, it can always be deleted. This avoids the need for introducing SoftNodes. Currently passes Debug and Production make check
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index cbe4e718a..9f1063715 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -141,6 +141,8 @@ private: /** Decrement ref counts of children */ inline void decrRefCounts(); + bool isBeingDeleted() const; + public: template <bool ref_count> @@ -266,6 +268,9 @@ inline void NodeValue::decrRefCounts() { } inline void NodeValue::inc() { + Assert(!isBeingDeleted(), + "NodeValue is currently being deleted " + "and increment is being called on it. Don't Do That!"); // FIXME multithreading if(EXPECT_TRUE( d_rc < MAX_RC )) { ++d_rc; @@ -301,6 +306,13 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { return d_children + d_nchildren; } + +inline bool NodeValue::isBeingDeleted() const +{ + return NodeManager::currentNM() != NULL && + NodeManager::currentNM()->isCurrentlyDeleting(this); +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ |