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 /lib/Expr | |
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 'lib/Expr')
-rw-r--r-- | lib/Expr/Expr.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
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() { } |