diff options
author | Daniel Schemmel <daniel.schemmel@comsys.rwth-aachen.de> | 2019-06-20 22:31:23 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-07-23 20:06:47 +0100 |
commit | df33de1a47eaff1b191d22f482af5d26162e6aa9 (patch) | |
tree | db3f07ae551fcd2bd755d89ff59e485830839190 /lib/Solver | |
parent | f36dc9c60c41c2bcf7bc968d1deb782cb986cb2e (diff) | |
download | klee-df33de1a47eaff1b191d22f482af5d26162e6aa9.tar.gz |
Refactor ConstraintManager to more modern coding standards
Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 12 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 26 |
2 files changed, 20 insertions, 18 deletions
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index be46621b..a6ca93ac 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -53,15 +53,15 @@ private: return constraints==b.constraints && *query.get()==*b.query.get(); } }; - + struct CacheEntryHash { unsigned operator()(const CacheEntry &ce) const { unsigned result = ce.query->hash(); - - for (ConstraintManager::constraint_iterator it = ce.constraints.begin(); - it != ce.constraints.end(); ++it) - result ^= (*it)->hash(); - + + for (auto const &constraint : ce.constraints) { + result ^= constraint->hash(); + } + return result; } }; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 19a0d745..447e5575 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -441,12 +441,13 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) { // Helper function used only for assertions to make sure point created // during computeInitialValues is in fact correct. The ``retMap`` is used // in the case ``objects`` doesn't contain all the assignments needed. -bool assertCreatedPointEvaluatesToTrue(const Query &query, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - std::map<const Array*, std::vector<unsigned char> > &retMap){ - // _allowFreeValues is set to true so that if there are missing bytes in the assigment - // we will end up with a non ConstantExpr after evaluating the assignment and fail +bool assertCreatedPointEvaluatesToTrue( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char>> &values, + std::map<const Array *, std::vector<unsigned char>> &retMap) { + // _allowFreeValues is set to true so that if there are missing bytes in the + // assigment we will end up with a non ConstantExpr after evaluating the + // assignment and fail Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); // Add any additional bindings. @@ -456,19 +457,20 @@ bool assertCreatedPointEvaluatesToTrue(const Query &query, if (retMap.size() > 0) assign.bindings.insert(retMap.begin(), retMap.end()); - for(ConstraintManager::constraint_iterator it = query.constraints.begin(); - it != query.constraints.end(); ++it){ - ref<Expr> ret = assign.evaluate(*it); + for (auto const &constraint : query.constraints) { + ref<Expr> ret = assign.evaluate(constraint); - assert(isa<ConstantExpr>(ret) && "assignment evaluation did not result in constant"); + assert(isa<ConstantExpr>(ret) && + "assignment evaluation did not result in constant"); ref<ConstantExpr> evaluatedConstraint = dyn_cast<ConstantExpr>(ret); - if(evaluatedConstraint->isFalse()){ + if (evaluatedConstraint->isFalse()) { return false; } } ref<Expr> neg = Expr::createIsZero(query.expr); ref<Expr> q = assign.evaluate(neg); - assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); + assert(isa<ConstantExpr>(q) && + "assignment evaluation did not result in constant"); return cast<ConstantExpr>(q)->isTrue(); } |