klee
Public Member Functions | Public Attributes | List of all members
CexData Class Reference

Public Member Functions

 CexData (const CexData &)
 
void operator= (const CexData &)
 
 CexData ()
 
 ~CexData ()
 
CexObjectData & getObjectData (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< Expr > evaluatePossible (ref< Expr > e)
 
ref< Expr > evaluateExact (ref< Expr > e)
 
void dump ()
 

Public Attributes

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

Detailed Description

Definition at line 419 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

◆ CexData() [1/2]

CexData::CexData ( const CexData &  )

◆ CexData() [2/2]

CexData::CexData ( )
inline

Definition at line 427 of file FastCexSolver.cpp.

◆ ~CexData()

CexData::~CexData ( )
inline

Definition at line 428 of file FastCexSolver.cpp.

References objects.

Member Function Documentation

◆ dump()

void CexData::dump ( )
inline

Definition at line 946 of file FastCexSolver.cpp.

References CexObjectData::getExactValues(), CexObjectData::getPossibleValues(), and objects.

Referenced by propogateValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ evalRangeForExpr()

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

Definition at line 931 of file FastCexSolver.cpp.

References klee::ExprRangeEvaluator< T >::evaluate(), and objects.

Referenced by propogateExactValues(), and propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ evaluateExact()

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

Definition at line 942 of file FastCexSolver.cpp.

References objects, and klee::ExprVisitor::visit().

Referenced by propogateValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ evaluatePossible()

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

References objects, and 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:

◆ getObjectData()

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

Definition at line 434 of file FastCexSolver.cpp.

References objects.

Referenced by propogateExactValues(), and propogatePossibleValues().

Here is the caller graph for this function:

◆ operator=()

void CexData::operator= ( const CexData &  )

◆ propogateExactValue()

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

Definition at line 447 of file FastCexSolver.cpp.

References propogateExactValues().

Referenced by propogateExactValues(), and propogateValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ propogateExactValues()

void CexData::propogateExactValues ( ref< Expr >  e,
CexValueData  range 
)
inline

Definition at line 791 of file FastCexSolver.cpp.

References klee::Array::constantValues, evalRangeForExpr(), CexObjectData::getExactValues(), klee::Expr::getKid(), klee::Expr::getKind(), getObjectData(), klee::Expr::getWidth(), klee::UpdateList::head, klee::ReadExpr::index, klee::Array::isConstantArray(), ValueRange::isFixed(), klee::BinaryExpr::left, ValueRange::max(), ValueRange::mayEqual(), ValueRange::min(), ValueRange::mustEqual(), propogateExactValue(), propogateExactValues(), klee::BinaryExpr::right, klee::UpdateList::root, CexObjectData::setExactValues(), and klee::ReadExpr::updates.

Referenced by propogateExactValue(), and propogateExactValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ propogatePossibleValue()

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

Definition at line 443 of file FastCexSolver.cpp.

References propogatePossibleValues().

Referenced by propogatePossibleValues(), and propogateValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ propogatePossibleValues()

void CexData::propogatePossibleValues ( ref< Expr >  e,
CexValueData  range 
)
inline

Definition at line 451 of file FastCexSolver.cpp.

References ValueRange::binaryAnd(), klee::SelectExpr::cond, evalRangeForExpr(), ValueRange::extract(), klee::SelectExpr::falseExpr, klee::ConcatExpr::getKid(), klee::Expr::getKid(), klee::Expr::getKind(), getObjectData(), CexObjectData::getPossibleValues(), klee::Expr::getWidth(), klee::ReadExpr::index, input, ValueRange::isEmpty(), ValueRange::isFixed(), klee::BinaryExpr::left, ValueRange::max(), klee::bits32::maxValueOfNBits(), ValueRange::min(), ValueRange::mustEqual(), propogatePossibleValue(), propogatePossibleValues(), klee::BinaryExpr::right, klee::UpdateList::root, ValueRange::set_difference(), ValueRange::set_intersection(), CexObjectData::setPossibleValue(), CexObjectData::setPossibleValues(), klee::CastExpr::src, klee::SelectExpr::trueExpr, klee::ReadExpr::updates, and klee::CastExpr::width.

Referenced by propogatePossibleValue(), and propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

Member Data Documentation

◆ objects

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

Definition at line 421 of file FastCexSolver.cpp.

Referenced by dump(), evalRangeForExpr(), evaluateExact(), evaluatePossible(), getObjectData(), and ~CexData().

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