diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-04-01 14:08:43 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-07-01 15:52:40 +0100 |
commit | 8d89546353180aa51484c27be68ffb0bb10583cd (patch) | |
tree | 8e70beb9356431a5f847c761e3824219eea92b17 /lib/Expr | |
parent | fdfc73bb3217c3a9527e09075b52aecdf19de666 (diff) | |
download | klee-8d89546353180aa51484c27be68ffb0bb10583cd.tar.gz |
Clean-up and add documentation
Diffstat (limited to 'lib/Expr')
-rw-r--r-- | lib/Expr/Constraints.cpp | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 6b576435..2a4c2adb 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -9,10 +9,9 @@ #include "klee/Expr/Constraints.h" -#include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprVisitor.h" -#include "klee/Support/OptionCategories.h" #include "klee/Module/KModule.h" +#include "klee/Support/OptionCategories.h" #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" @@ -28,29 +27,28 @@ llvm::cl::opt<bool> RewriteEqualities( "constant is added (default=true)"), llvm::cl::init(true), llvm::cl::cat(SolvingCat)); -} +} // namespace class ExprReplaceVisitor : public ExprVisitor { private: ref<Expr> src, dst; public: - ExprReplaceVisitor(ref<Expr> _src, ref<Expr> _dst) : src(_src), dst(_dst) {} + ExprReplaceVisitor(const ref<Expr> &_src, const ref<Expr> &_dst) + : src(_src), dst(_dst) {} - Action visitExpr(const Expr &e) { - if (e == *src.get()) { + Action visitExpr(const Expr &e) override { + if (e == *src) { return Action::changeTo(dst); - } else { - return Action::doChildren(); } + return Action::doChildren(); } - Action visitExprPost(const Expr &e) { - if (e == *src.get()) { + Action visitExprPost(const Expr &e) override { + if (e == *src) { return Action::changeTo(dst); - } else { - return Action::doChildren(); } + return Action::doChildren(); } }; @@ -59,17 +57,16 @@ private: const std::map< ref<Expr>, ref<Expr> > &replacements; public: - ExprReplaceVisitor2(const std::map<ref<Expr>, ref<Expr>> &_replacements) + explicit ExprReplaceVisitor2( + const std::map<ref<Expr>, ref<Expr>> &_replacements) : ExprVisitor(true), replacements(_replacements) {} - Action visitExprPost(const Expr &e) { - std::map< ref<Expr>, ref<Expr> >::const_iterator it = - replacements.find(ref<Expr>(const_cast<Expr*>(&e))); + Action visitExprPost(const Expr &e) override { + auto it = replacements.find(ref<Expr>(const_cast<Expr *>(&e))); if (it!=replacements.end()) { return Action::changeTo(it->second); - } else { - return Action::doChildren(); } + return Action::doChildren(); } }; @@ -118,7 +115,7 @@ ref<Expr> ConstraintManager::simplifyExpr(const ConstraintSet &constraints, return ExprReplaceVisitor2(equalities).visit(e); } -void ConstraintManager::addConstraintInternal(ref<Expr> e) { +void ConstraintManager::addConstraintInternal(const ref<Expr> &e) { // rewrite any known equalities and split Ands into different conjuncts switch (e->getKind()) { @@ -158,9 +155,9 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) { } } -void ConstraintManager::addConstraint(ref<Expr> e) { - e = simplifyExpr(constraints, e); - addConstraintInternal(e); +void ConstraintManager::addConstraint(const ref<Expr> &e) { + ref<Expr> simplified = simplifyExpr(constraints, e); + addConstraintInternal(simplified); } ConstraintManager::ConstraintManager(ConstraintSet &_constraints) |