diff options
| author | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-24 15:32:34 +0100 |
|---|---|---|
| committer | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-24 15:32:34 +0100 |
| commit | b058af7f05be473e31a82fa1cdacf675eea784da (patch) | |
| tree | deac2388bba38541741efc6ef171418286442061 /lib/Solver | |
| parent | 9dd4766a3f58070501ed6498e6aa42c14776cc0f (diff) | |
| download | klee-b058af7f05be473e31a82fa1cdacf675eea784da.tar.gz | |
Fixed creation of arrays with variable domains and ranges in STPBuilder and MetaSMTBuilder.
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 12 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 3 |
2 files changed, 8 insertions, 7 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 2b084ac7..deb12e77 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -187,7 +187,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArr if (!hashed) { - array_expr = evaluate(_solver, buildArray(8, 32)); + array_expr = evaluate(_solver, buildArray(root->getDomain(), root->getRange())); if (root->isConstantArray()) { for (unsigned i = 0, e = root->size; i != e; ++i) { @@ -603,7 +603,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu // ExprPPrinter::printSingleExpr(std::cerr, e); // std::cerr << "\n"; - switch (e->getKind()) { + switch (e->getKind()) { case Expr::Constant: { @@ -614,7 +614,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu // Coerce to bool if necessary. if (coe_width == 1) { - res = (coe->isTrue()) ? getTrue() : getFalse(); + res = (coe->isTrue()) ? getTrue() : getFalse(); } else if (coe_width <= 32) { res = bvConst32(coe_width, coe->getZExtValue(32)); @@ -624,7 +624,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu } else { ref<ConstantExpr> tmp = coe; - res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); + res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); while (tmp->getWidth() > 64) { tmp = tmp->Extract(64, tmp->getWidth() - 64); unsigned min_width = std::min(64U, tmp->getWidth()); @@ -658,9 +658,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu case Expr::Read: { ReadExpr *re = cast<ReadExpr>(e); - assert(re); + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); // FixMe call method of Array - *width_out = 8; res = evaluate(_solver, metaSMT::logic::Array::select( getArrayForUpdate(re->updates.root, re->updates.head), diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index ebc096df..e4a21f74 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -553,7 +553,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { case Expr::Read: { ReadExpr *re = cast<ReadExpr>(e); - *width_out = 8; + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); return vc_readExpr(vc, getArrayForUpdate(re->updates.root, re->updates.head), construct(re->index, 0)); |