CexData Class Reference

List of all members.

Public Member Functions
	CexData (ObjectFinder &finder)
	~CexData ()
void	forceExprToValue (ref< Expr > e, uint64_t value)
void	forceExprToRange (ref< Expr > e, CexValueData range)
void	fixValues ()
ValueRange	evalRangeForExpr (ref< Expr > &e)
bool	exprMustBeValue (ref< Expr > e, uint64_t value)
Public Attributes
std::map< unsigned, CexObjectData >	objectValues

---

Detailed Description

Definition at line 375 of file FastCexSolver.cpp.

---

Constructor & Destructor Documentation

CexData::CexData

(

ObjectFinder &

finder

)

[inline]

Definition at line 380 of file FastCexSolver.cpp.

References objectValues, and ObjectFinder::results.

CexData::~CexData

(

)

[inline]

Definition at line 387 of file FastCexSolver.cpp.

References objectValues.

---

Member Function Documentation

ValueRange CexData::evalRangeForExpr

(

ref< Expr > &

e

)

[inline]

Definition at line 725 of file FastCexSolver.cpp.

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

Referenced by forceExprToRange().

Here is the call graph for this function:

Here is the caller graph for this function:

bool CexData::exprMustBeValue	(	ref< Expr >	e,
		uint64_t	value
	)			[inline]

Definition at line 730 of file FastCexSolver.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

void CexData::fixValues

(

)

[inline]

Definition at line 714 of file FastCexSolver.cpp.

References ValueRange::max(), ValueRange::min(), objectValues, CexObjectData::size, and CexObjectData::values.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void CexData::forceExprToRange	(	ref< Expr >	e,
		CexValueData	range
	)			[inline]

Definition at line 397 of file FastCexSolver.cpp.

References ValueRange::binaryAnd(), klee::SelectExpr::cond, evalRangeForExpr(), ValueRange::extract(), klee::SelectExpr::falseExpr, forceExprToValue(), klee::ConcatExpr::getKid(), klee::Expr::getWidth(), klee::ReadExpr::index, klee::ConcatExpr::is2ByteConcat(), klee::ConcatExpr::is4ByteConcat(), klee::ConcatExpr::is8ByteConcat(), ValueRange::isEmpty(), ValueRange::isFixed(), klee::BinaryExpr::left, klee::bits64::maxValueOfNBits(), ValueRange::min(), ValueRange::mustEqual(), objectValues, klee::BinaryExpr::right, klee::UpdateList::root, ValueRange::set_difference(), ValueRange::set_intersection(), klee::ints::sext(), klee::CastExpr::src, klee::SelectExpr::trueExpr, klee::ReadExpr::updates, CexObjectData::values, and klee::CastExpr::width.

Referenced by forceExprToValue().

Here is the call graph for this function:

Here is the caller graph for this function:

void CexData::forceExprToValue	(	ref< Expr >	e,
		uint64_t	value
	)			[inline]

Definition at line 393 of file FastCexSolver.cpp.

References forceExprToRange().

Referenced by FastCexSolver::computeInitialValues(), FastCexSolver::computeTruth(), FastCexSolver::computeValue(), and forceExprToRange().

Here is the call graph for this function:

Here is the caller graph for this function:

---

Member Data Documentation

std::map<unsigned, CexObjectData> CexData::objectValues

Definition at line 377 of file FastCexSolver.cpp.

Referenced by CexData(), FastCexSolver::computeInitialValues(), FastCexSolver::computeValue(), evalRangeForExpr(), exprMustBeValue(), fixValues(), forceExprToRange(), and ~CexData().

---

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

• lib/Solver/FastCexSolver.cpp