diff options
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Expr.h | 6 | ||||
-rw-r--r-- | include/klee/util/Assignment.h | 7 | ||||
-rw-r--r-- | include/klee/util/ExprRangeEvaluator.h | 2 |
3 files changed, 8 insertions, 7 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index ee3c3253..240c6220 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -675,15 +675,15 @@ public: static ref<Expr> create(const UpdateList &updates, ref<Expr> i); - Width getWidth() const { return updates.root->getRange(); } + Width getWidth() const { return updates.root ? updates.root->getRange() : Expr::Int8; } Kind getKind() const { return Read; } unsigned getNumKids() const { return numKids; } - ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } + ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } int compareContents(const Expr &b) const; - virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(updates, kids[0]); } diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 838d03bd..63df4b65 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -67,15 +67,16 @@ namespace klee { inline ref<Expr> Assignment::evaluate(const Array *array, unsigned index) const { + assert(array); bindings_ty::const_iterator it = bindings.find(array); if (it!=bindings.end() && index<it->second.size()) { - return ConstantExpr::alloc(it->second[index], Expr::Int8); + return ConstantExpr::alloc(it->second[index], array->getRange()); } else { if (allowFreeValues) { return ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array->getDomain())); } else { - return ConstantExpr::alloc(0, Expr::Int8); + return ConstantExpr::alloc(0, array->getRange()); } } } diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h index 34b85520..fea30b5b 100644 --- a/include/klee/util/ExprRangeEvaluator.h +++ b/include/klee/util/ExprRangeEvaluator.h @@ -102,7 +102,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) { const ReadExpr *re = cast<ReadExpr>(e); T index = evaluate(re->index); - assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read"); + assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read"); return evalRead(re->updates, index); } |