diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-17 12:16:17 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-17 12:16:17 -0800 |
commit | 248b977790b429ebfd22481462193e3e35c57ce2 (patch) | |
tree | 9a59a408d113d6a3347f013c2492291769406e82 /src/expr/node.h | |
parent | 4538f5fe95758f2507c191ab39175491f24e6f67 (diff) |
Removes yet more throw specifiers. Updating the documentation as needed. (#1518)
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index fd3d20afa..92f905c8b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -228,7 +228,10 @@ class NodeTemplate { */ void assignNodeValue(expr::NodeValue* ev); - inline void assertTNodeNotExpired() const throw(AssertionException) { + // May throw an AssertionException if the Node is not live, i.e. the ref count + // is not positive. + inline void assertTNodeNotExpired() const + { if(!ref_count) { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } @@ -525,8 +528,7 @@ public: * @param check whether we should check the type as we compute it * (default: false) */ - TypeNode getType(bool check = false) const - throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); + TypeNode getType(bool check = false) const; /** * Substitution of Nodes. @@ -1271,7 +1273,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { template <bool ref_count> TypeNode NodeTemplate<ref_count>::getType(bool check) const - throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException) { +{ Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); |