klee
|
#include <ExprVisitor.h>
Classes | |
class | Action |
Public Member Functions | |
ref< Expr > | visit (const ref< Expr > &e) |
Protected Member Functions | |
ExprVisitor (bool _recursive=false) | |
virtual | ~ExprVisitor () |
virtual Action | visitExpr (const Expr &) |
virtual Action | visitExprPost (const Expr &) |
virtual Action | visitNotOptimized (const NotOptimizedExpr &) |
virtual Action | visitRead (const ReadExpr &) |
virtual Action | visitSelect (const SelectExpr &) |
virtual Action | visitConcat (const ConcatExpr &) |
virtual Action | visitExtract (const ExtractExpr &) |
virtual Action | visitZExt (const ZExtExpr &) |
virtual Action | visitSExt (const SExtExpr &) |
virtual Action | visitAdd (const AddExpr &) |
virtual Action | visitSub (const SubExpr &) |
virtual Action | visitMul (const MulExpr &) |
virtual Action | visitUDiv (const UDivExpr &) |
virtual Action | visitSDiv (const SDivExpr &) |
virtual Action | visitURem (const URemExpr &) |
virtual Action | visitSRem (const SRemExpr &) |
virtual Action | visitNot (const NotExpr &) |
virtual Action | visitAnd (const AndExpr &) |
virtual Action | visitOr (const OrExpr &) |
virtual Action | visitXor (const XorExpr &) |
virtual Action | visitShl (const ShlExpr &) |
virtual Action | visitLShr (const LShrExpr &) |
virtual Action | visitAShr (const AShrExpr &) |
virtual Action | visitEq (const EqExpr &) |
virtual Action | visitNe (const NeExpr &) |
virtual Action | visitUlt (const UltExpr &) |
virtual Action | visitUle (const UleExpr &) |
virtual Action | visitUgt (const UgtExpr &) |
virtual Action | visitUge (const UgeExpr &) |
virtual Action | visitSlt (const SltExpr &) |
virtual Action | visitSle (const SleExpr &) |
virtual Action | visitSgt (const SgtExpr &) |
virtual Action | visitSge (const SgeExpr &) |
Private Types | |
typedef ExprHashMap< ref< Expr > > | visited_ty |
Private Member Functions | |
ref< Expr > | visitActual (const ref< Expr > &e) |
Private Attributes | |
visited_ty | visited |
bool | recursive |
Definition at line 16 of file ExprVisitor.h.
|
private |
Definition at line 84 of file ExprVisitor.h.
|
inlineexplicitprotected |
Definition at line 45 of file ExprVisitor.h.
|
inlineprotectedvirtual |
Definition at line 46 of file ExprVisitor.h.
Definition at line 26 of file ExprVisitor.cpp.
References visitActual(), and visited.
Referenced by klee::ExprOptimizer::computeIndexes(), klee::ExprEvaluator::evalRead(), klee::Assignment::evaluate(), CexData::evaluateExact(), CexData::evaluatePossible(), klee::findSymbolicObjects(), klee::ExprOptimizer::getSelectOptExpr(), klee::ExprOptimizer::optimizeExpr(), klee::ExprEvaluator::protectedDivOperation(), klee::ExprRewriter::rewrite(), klee::ConstraintManager::rewriteConstraints(), klee::Assignment::satisfies(), klee::ConstraintManager::simplifyExpr(), visitActual(), klee::ConstantArrayExprVisitor::visitConcat(), klee::ConstantArrayExprVisitor::visitRead(), klee::ExprEvaluator::visitRead(), klee::ConstantArrayFinder::visitRead(), and klee::SymbolicObjectFinder::visitRead().
Definition at line 42 of file ExprVisitor.cpp.
References klee::Expr::Add, klee::Expr::And, klee::ExprVisitor::Action::argument, klee::Expr::AShr, klee::ExprVisitor::Action::ChangeTo, klee::Expr::Concat, klee::Expr::Constant, klee::ExprVisitor::Action::DoChildren, klee::Expr::Eq, klee::Expr::Extract, klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getKind(), klee::Expr::getNumKids(), klee::ExprVisitor::Action::kind, klee::Expr::LShr, klee::Expr::Mul, klee::Expr::Ne, klee::Expr::Not, klee::Expr::NotOptimized, klee::Expr::Or, klee::Expr::Read, klee::Expr::rebuild(), recursive, klee::Expr::SDiv, klee::Expr::Select, klee::Expr::SExt, klee::Expr::Sge, klee::Expr::Sgt, klee::Expr::Shl, klee::ExprVisitor::Action::SkipChildren, klee::Expr::Sle, klee::Expr::Slt, klee::Expr::SRem, klee::Expr::Sub, klee::Expr::UDiv, klee::Expr::Uge, klee::Expr::Ugt, klee::Expr::Ule, klee::Expr::Ult, klee::Expr::URem, visit(), visitAdd(), visitAnd(), visitAShr(), visitConcat(), visitEq(), visitExpr(), visitExprPost(), visitExtract(), visitLShr(), visitMul(), visitNe(), visitNot(), visitNotOptimized(), visitOr(), visitRead(), visitSDiv(), visitSelect(), visitSExt(), visitSge(), visitSgt(), visitShl(), visitSle(), visitSlt(), visitSRem(), visitSub(), visitUDiv(), visitUge(), visitUgt(), visitUle(), visitUlt(), visitURem(), visitXor(), visitZExt(), klee::Expr::Xor, and klee::Expr::ZExt.
Referenced by visit().
|
protectedvirtual |
Definition at line 165 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 197 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 217 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::ConstantArrayExprVisitor, klee::IndexTransformationExprVisitor, klee::ArrayReadExprVisitor, and klee::ArrayValueOptReplaceVisitor.
Definition at line 149 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 221 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::ExprEvaluator, and ExprReplaceVisitor.
Definition at line 129 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::ExprEvaluator, ExprReplaceVisitor, and ExprReplaceVisitor2.
Definition at line 133 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::skipChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 153 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 213 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::IndexTransformationExprVisitor.
Definition at line 173 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 225 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 193 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 137 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::IndexCompatibilityExprVisitor.
Definition at line 201 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::ConstantArrayExprVisitor, klee::IndexCompatibilityExprVisitor, klee::ArrayReadExprVisitor, klee::ExprEvaluator, klee::ConstantArrayFinder, klee::SymbolicObjectFinder, and klee::ArrayValueOptReplaceVisitor.
Definition at line 141 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::ExprEvaluator.
Definition at line 181 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 145 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 161 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 257 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 253 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 209 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 249 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 245 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::IndexCompatibilityExprVisitor, and klee::ExprEvaluator.
Definition at line 189 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 169 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::ExprEvaluator.
Definition at line 177 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 241 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 237 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 233 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 229 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Reimplemented in klee::IndexCompatibilityExprVisitor, and klee::ExprEvaluator.
Definition at line 185 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 205 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
protectedvirtual |
Definition at line 157 of file ExprVisitor.cpp.
References klee::ExprVisitor::Action::doChildren().
Referenced by visitActual().
|
private |
Definition at line 86 of file ExprVisitor.h.
Referenced by visitActual().
|
private |
Definition at line 85 of file ExprVisitor.h.
Referenced by visit().