diff options
author | Martin Nowack <martin_nowack@tu-dresden.de> | 2017-10-29 22:02:32 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-02-18 12:49:41 +0000 |
commit | 51183b4370eb2a081c440b6ff32acc4e5f50890e (patch) | |
tree | b2e56a9c2bdf2d4a471672fd43af02f7eb033d09 /lib/Core | |
parent | faf2494ac3a5dec057384fd413e0c2a024a5347b (diff) | |
download | klee-51183b4370eb2a081c440b6ff32acc4e5f50890e.tar.gz |
Fix generation of expressions from constant sequential data
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/ExecutorUtil.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 53f4c5b8..4f51ecb6 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -58,9 +58,11 @@ namespace klee { return ConstantExpr::create(0, getWidthForLLVMType(c->getType())); } else if (const ConstantDataSequential *cds = dyn_cast<ConstantDataSequential>(c)) { + // Handle a vector or array: first element has the smallest address, + // the last element the highest std::vector<ref<Expr> > kids; - for (unsigned i = 0, e = cds->getNumElements(); i != e; ++i) { - ref<Expr> kid = evalConstant(cds->getElementAsConstant(i), ki); + for (unsigned i = cds->getNumElements(); i != 0; --i) { + ref<Expr> kid = evalConstant(cds->getElementAsConstant(i - 1), ki); kids.push_back(kid); } ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data()); |