diff options
author | Dan Liew <delcypher@gmail.com> | 2014-04-24 12:12:22 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2014-04-24 12:12:22 +0100 |
commit | 292e8cc794f01df94ca02279f5833d7a460a62f9 (patch) | |
tree | 80400e7fa9b69edd1ecdb3600ca88244f533c389 /lib/Expr/Updates.cpp | |
parent | 7f44b9346356c91f633c6de6939c33a45756ae7e (diff) | |
parent | 2795655e567c3cdbfe3d4815edd83b4f4cdbb542 (diff) | |
download | klee-292e8cc794f01df94ca02279f5833d7a460a62f9.tar.gz |
Merge pull request #112 from hpalikareva/domain-range-extra
Removing a few more hard-coded values for domains and ranges of Array ob...
Diffstat (limited to 'lib/Expr/Updates.cpp')
-rw-r--r-- | lib/Expr/Updates.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 14fd8308..bf7049ba 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -22,8 +22,12 @@ UpdateNode::UpdateNode(const UpdateNode *_next, next(_next), index(_index), value(_value) { + // FIXME: What we need to check here instead is that _value is of the same width + // as the range of the array that the update node is part of. + /* assert(_value->getWidth() == Expr::Int8 && "Update value should be 8-bit wide."); + */ computeHash(); if (next) { ++next->refCount; @@ -84,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; |