diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-02 11:40:48 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-04-02 11:40:48 -0700 |
commit | 2d40d7ade3c66ba10a1f20ae5ab014aed8e2df01 (patch) | |
tree | 504b340eea82c28e1ee18cacb06a5a015c195bd9 /src/expr/node.cpp | |
parent | cd41d9de391ea93736182e944c10b697d863c6a6 (diff) |
Do not call toString() on malformed node when throwing TypeCheckingExceptionPrivate. (#1733)
While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when
trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children
rather than calling toString() on the malformed node.
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 110925f41..b41014f9c 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -31,9 +31,20 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, : Exception(message), d_node(new Node(node)) { #ifdef CVC4_DEBUG + std::stringstream ss; LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); if(current != NULL){ - current->setContents(toString().c_str()); + // Since this node is malformed, we cannot use toString(). + // Instead, we print the kind and the children. + ss << "node kind: " << node.getKind() << ". children: "; + int i = 0; + for (const TNode& child : node) + { + ss << "child[" << i << "]: " << child << ". "; + i++; + } + string ssstring = ss.str(); + current->setContents(ssstring.c_str()); } #endif /* CVC4_DEBUG */ } |