Inheritance diagram for CexExactEvaluator:

Collaboration diagram for CexExactEvaluator:

[legend]

Public Member Functions
	CexExactEvaluator (std::map< const Array , CexObjectData > &_objects)

Public Member Functions inherited from klee::ExprEvaluator
	ExprEvaluator ()

virtual ref< Expr >	getInitialValue (const Array &os, unsigned index)=0

Public Member Functions inherited from klee::ExprVisitor
ref< Expr >	visit (const ref< Expr > &e)

Public Attributes
std::map< const Array , CexObjectData > &	objects

Protected Member Functions
ref< Expr >	getInitialValue (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)

Action	visitExprPost (const Expr &e)

Protected Member Functions inherited from klee::ExprVisitor
	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 &)

Detailed Description

Definition at line 391 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

◆ CexExactEvaluator()

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

inline

Definition at line 415 of file FastCexSolver.cpp.

Member Function Documentation

◆ getInitialValue()

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

inlineprotectedvirtual

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 393 of file FastCexSolver.cpp.

References klee::Array::getDomain(), klee::Array::getRange(), ValueRange::isFixed(), ValueRange::min(), objects, and klee::Array::size.

Here is the call graph for this function: