diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 17 | ||||
| -rw-r--r-- | lib/Solver/SMTLIBLoggingSolver.cpp | 23 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 |
3 files changed, 25 insertions, 17 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index b5c99907..6da1b492 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -284,7 +284,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShr if (shift == 0) { res = expr; } - else if (shift >= width - 1) { + else if (shift >= width) { res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width))); } else { @@ -499,6 +499,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShif bvLeftShift(expr, width, i, shiftBits), res)); } + + // If overshifting, shift to zero + res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), + res, + bvZero(width))); return(res); } @@ -521,6 +526,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShi res)); // ToDo Reconsider widht to provide to bvRightShift } + + // If overshifting, shift to zero + res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), + res, + bvZero(width))); return(res); } @@ -548,6 +558,11 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRig constructAShrByConstant(expr, width, i, signedBool, shiftBits), res)); } + + // If overshifting, shift to zero + res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), + res, + bvZero(width))); return(res); } diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index f64e11e0..2f3e97da 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -8,7 +8,7 @@ //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" -#include "klee/util/ExprSMTLIBLetPrinter.h" +#include "klee/util/ExprSMTLIBPrinter.h" using namespace klee; @@ -18,7 +18,7 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver { private: - ExprSMTLIBPrinter* printer; + ExprSMTLIBPrinter printer; virtual void printQuery(const Query& query, const Query* falseQuery = 0, @@ -26,36 +26,29 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver { if (0 == falseQuery) { - printer->setQuery(query); + printer.setQuery(query); } else { - printer->setQuery(*falseQuery); + printer.setQuery(*falseQuery); } if (0 != objects) { - printer->setArrayValuesToGet(*objects); + printer.setArrayValuesToGet(*objects); } - printer->generateOutput(); + printer.generateOutput(); } public: SMTLIBLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) - : QueryLoggingSolver(_solver, path, ";", queryTimeToLog), - printer() + : QueryLoggingSolver(_solver, path, ";", queryTimeToLog) { //Setup the printer - printer = createSMTLIBPrinter(); - printer->setOutput(logBuffer); - } - - ~SMTLIBLoggingSolver() - { - delete printer; + printer.setOutput(logBuffer); } }; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 34ce0ede..6d7dd8b7 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -283,7 +283,7 @@ ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr, if (shift==0) { return expr; - } else if (shift>=width-1) { + } else if (shift>=width) { return bvZero(width); // Overshift to zero } else { return vc_iteExpr(vc, |