diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-02-22 19:10:39 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-02-22 19:24:11 +0000 |
commit | 4d57a5a829124106a4ef81e5131a50d1e7caed7f (patch) | |
tree | 5504d3d5d3f93d991582cdd3d1213ec783f6fd8f /include | |
parent | f76b6c5fe0ce8920ee6edb13802f857dae49e785 (diff) | |
download | klee-4d57a5a829124106a4ef81e5131a50d1e7caed7f.tar.gz |
Move Array constructor out of ``Expr.h`` and into ``Expr.cpp``.
The implementation of the constructor calls a method on a ``ConstantExpr`` which means the type must be complete (i.e. a forward declaration of ``ConstantExpr`` is insufficient) which creates an unnecessary ordering Dependency in ``Expr.h``.
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/Expr.h | 19 |
1 files changed, 3 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(); } |