diff options
| -rw-r--r-- | include/klee/Expr.h | 16 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 |
2 files changed, 11 insertions, 7 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index f893c6cc..ee3c3253 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -587,7 +587,9 @@ public: /// a symbolic array. If non-empty, this size of this array is equivalent to /// the array size. const std::vector< ref<ConstantExpr> > constantValues; - + + Expr::Width domain, range; + public: /// Array - Construct a new array object. /// @@ -598,9 +600,11 @@ public: /// distinguished once printed. Array(const std::string &_name, uint64_t _size, const ref<ConstantExpr> *constantValuesBegin = 0, - const ref<ConstantExpr> *constantValuesEnd = 0) + const ref<ConstantExpr> *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) : name(_name), size(_size), - constantValues(constantValuesBegin, constantValuesEnd) { + constantValues(constantValuesBegin, constantValuesEnd), + domain(_domain), range(_range) { assert((isSymbolicArray() || constantValues.size() == size) && "Invalid size for constant array!"); computeHash(); @@ -616,8 +620,8 @@ public: bool isSymbolicArray() const { return constantValues.empty(); } bool isConstantArray() const { return !isSymbolicArray(); } - Expr::Width getDomain() const { return Expr::Int32; } - Expr::Width getRange() const { return Expr::Int8; } + Expr::Width getDomain() const { return domain; } + Expr::Width getRange() const { return range; } unsigned computeHash(); unsigned hash() const { return hashValue; } @@ -671,7 +675,7 @@ public: static ref<Expr> create(const UpdateList &updates, ref<Expr> i); - Width getWidth() const { return Expr::Int8; } + Width getWidth() const { return updates.root->getRange(); } Kind getKind() const { return Read; } unsigned getNumKids() const { return numKids; } diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index ad0df3c2..ebc096df 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -439,7 +439,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width memmove(buf + space, buf, addrlen); // moving the address part to the end memcpy(buf, root->name.c_str(), space); // filling out the name part - array_expr = buildArray(buf, 32, 8); + array_expr = buildArray(buf, root->getDomain(), root->getRange()); if (root->isConstantArray()) { // FIXME: Flush the concrete values into STP. Ideally we would do this |