All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CexExactEvaluator Class Reference
Inheritance diagram for CexExactEvaluator:
Collaboration diagram for CexExactEvaluator:

Public Member Functions

 CexExactEvaluator (std::map< const Array *, CexObjectData * > &_objects)
- Public Member Functions inherited from klee::ExprEvaluator
 ExprEvaluator ()
- Public Member Functions inherited from klee::ExprVisitor
ref< Exprvisit (const ref< Expr > &e)

Public Attributes

std::map< const Array
*, CexObjectData * > & 

Protected Member Functions

ref< ExprgetInitialValue (const Array &array, unsigned index)
- Protected Member Functions inherited from klee::ExprEvaluator
Action evalRead (const UpdateList &ul, unsigned index)
Action visitRead (const ReadExpr &re)
Action visitExpr (const Expr &e)
Action protectedDivOperation (const BinaryExpr &e)
Action visitUDiv (const UDivExpr &e)
Action visitSDiv (const SDivExpr &e)
Action visitURem (const URemExpr &e)
Action visitSRem (const SRemExpr &e)
- Protected Member Functions inherited from klee::ExprVisitor
 ExprVisitor (bool _recursive=false)
virtual ~ExprVisitor ()
virtual Action visitExprPost (const Expr &)
virtual Action visitNotOptimized (const NotOptimizedExpr &)
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 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 &)

Detailed Description

Definition at line 383 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

CexExactEvaluator::CexExactEvaluator ( std::map< const Array *, CexObjectData * > &  _objects)

Definition at line 407 of file FastCexSolver.cpp.

Member Function Documentation

ref<Expr> CexExactEvaluator::getInitialValue ( const Array os,
unsigned  index 

getInitialValue - Return the initial value for a symbolic byte.

This will only be called for constant arrays if the index is out-of-bounds. If the value is unknown then the user should return a ReadExpr at the initial version of this array.

Implements klee::ExprEvaluator.

Definition at line 385 of file FastCexSolver.cpp.

References klee::ConstantExpr::alloc(), klee::ReadExpr::create(), klee::Array::getDomain(), klee::Array::getRange(), ValueRange::isFixed(), ValueRange::min(), and klee::Array::size.

Here is the call graph for this function:

Member Data Documentation

std::map<const Array*, CexObjectData*>& CexExactEvaluator::objects

Definition at line 406 of file FastCexSolver.cpp.

The documentation for this class was generated from the following file: