diff options
author | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-23 20:20:33 +0100 |
---|---|---|
committer | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-24 12:05:01 +0100 |
commit | 2795655e567c3cdbfe3d4815edd83b4f4cdbb542 (patch) | |
tree | 80400e7fa9b69edd1ecdb3600ca88244f533c389 /lib/Expr | |
parent | aa8cc67c0d8c16388ebe670757327a81f774d0ee (diff) | |
download | klee-2795655e567c3cdbfe3d4815edd83b4f4cdbb542.tar.gz |
Asserting that update lists have non-NULL roots within ReadExpr objects (update
lists can have NULL roots, e.g. in MemoryObject instances with concrete contents, where root is allocated lazily only when the updates are required). Also checking whether array updates are typed correctly in UpdateList::extend() rather than in the constructor of UpdateNode (only for update lists with non-NULL roots).
Diffstat (limited to 'lib/Expr')
-rw-r--r-- | lib/Expr/Updates.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 107cf9d4..bf7049ba 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -88,6 +88,12 @@ UpdateList &UpdateList::operator=(const UpdateList &b) { } void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) { + + if (root) { + assert(root->getDomain() == index->getWidth()); + assert(root->getRange() == value->getWidth()); + } + if (head) --head->refCount; head = new UpdateNode(head, index, value); ++head->refCount; |