klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CexData Class Reference

Public Member Functions

 CexData (const CexData &)
 
void operator= (const CexData &)
 
 CexData ()
 
 ~CexData ()
 
CexObjectDatagetObjectData (const Array *A)
 
void propogatePossibleValue (ref< Expr > e, uint64_t value)
 
void propogateExactValue (ref< Expr > e, uint64_t value)
 
void propogatePossibleValues (ref< Expr > e, CexValueData range)
 
void propogateExactValues (ref< Expr > e, CexValueData range)
 
ValueRange evalRangeForExpr (const ref< Expr > &e)
 
ref< ExprevaluatePossible (ref< Expr > e)
 
ref< ExprevaluateExact (ref< Expr > e)
 
void dump ()
 

Public Attributes

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

Detailed Description

Definition at line 411 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

CexData::CexData ( const CexData )
CexData::CexData ( )
inline

Definition at line 419 of file FastCexSolver.cpp.

CexData::~CexData ( )
inline

Definition at line 420 of file FastCexSolver.cpp.

Member Function Documentation

void CexData::dump ( )
inline

Definition at line 937 of file FastCexSolver.cpp.

References CexObjectData::getExactValues(), CexObjectData::getPossibleValues(), klee::Array::name, and klee::Array::size.

Referenced by propogateValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ValueRange CexData::evalRangeForExpr ( const ref< Expr > &  e)
inline

Definition at line 922 of file FastCexSolver.cpp.

References klee::ExprRangeEvaluator< T >::evaluate().

Here is the call graph for this function:

ref<Expr> CexData::evaluateExact ( ref< Expr e)
inline

Definition at line 933 of file FastCexSolver.cpp.

References klee::ExprVisitor::visit().

Referenced by propogateValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ref<Expr> CexData::evaluatePossible ( ref< Expr e)
inline

evaluate - Try to evaluate the given expression using a consistent fixed value for the current set of possible ranges.

Definition at line 929 of file FastCexSolver.cpp.

References klee::ExprVisitor::visit().

Referenced by FastCexSolver::computeInitialValues(), FastCexSolver::computeValue(), and propogateValues().

Here is the call graph for this function:

Here is the caller graph for this function:

CexObjectData& CexData::getObjectData ( const Array A)
inline

Definition at line 426 of file FastCexSolver.cpp.

References klee::Array::size.

void CexData::operator= ( const CexData )
void CexData::propogateExactValue ( ref< Expr e,
uint64_t  value 
)
inline

Definition at line 439 of file FastCexSolver.cpp.

Referenced by propogateValues().

Here is the caller graph for this function:

void CexData::propogatePossibleValue ( ref< Expr e,
uint64_t  value 
)
inline

Definition at line 435 of file FastCexSolver.cpp.

Referenced by propogateValues().

Here is the caller graph for this function:

Member Data Documentation

std::map<const Array*, CexObjectData*> CexData::objects

Definition at line 413 of file FastCexSolver.cpp.


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