diff options
| -rw-r--r-- | include/klee/Expr.h | 19 | ||||
| -rw-r--r-- | lib/Expr/Expr.cpp | 18 |
2 files changed, 21 insertions, 16 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 731aa446..2f24ffa4 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -636,22 +636,9 @@ private: /// not parse correctly since two arrays with the same name cannot be /// distinguished once printed. Array(const std::string &_name, uint64_t _size, - const ref<ConstantExpr> *constantValuesBegin = 0, - const ref<ConstantExpr> *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) - : name(_name), size(_size), domain(_domain), range(_range), - constantValues(constantValuesBegin, constantValuesEnd) { - - assert((isSymbolicArray() || constantValues.size() == size) && - "Invalid size for constant array!"); - computeHash(); -#ifndef NDEBUG - for (const ref<ConstantExpr> *it = constantValuesBegin; - it != constantValuesEnd; ++it) - assert((*it)->getWidth() == getRange() && - "Invalid initial constant value!"); -#endif //NDEBUG - } + const ref<ConstantExpr> *constantValuesBegin = 0, + const ref<ConstantExpr> *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8); public: bool isSymbolicArray() const { return constantValues.empty(); } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 2c64aff4..ccd757af 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -483,6 +483,24 @@ ref<Expr> NotOptimizedExpr::create(ref<Expr> src) { extern "C" void vc_DeleteExpr(void*); +Array::Array(const std::string &_name, uint64_t _size, + const ref<ConstantExpr> *constantValuesBegin, + const ref<ConstantExpr> *constantValuesEnd, Expr::Width _domain, + Expr::Width _range) + : name(_name), size(_size), domain(_domain), range(_range), + constantValues(constantValuesBegin, constantValuesEnd) { + + assert((isSymbolicArray() || constantValues.size() == size) && + "Invalid size for constant array!"); + computeHash(); +#ifndef NDEBUG + for (const ref<ConstantExpr> *it = constantValuesBegin; + it != constantValuesEnd; ++it) + assert((*it)->getWidth() == getRange() && + "Invalid initial constant value!"); +#endif // NDEBUG +} + Array::~Array() { } |