diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Expr.h | 16 |
1 files changed, 10 insertions, 6 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; } |