klee
CexRangeEvaluator Class Reference
Inheritance diagram for CexRangeEvaluator:
Collaboration diagram for CexRangeEvaluator:

Public Member Functions

 CexRangeEvaluator (std::map< const Array *, CexObjectData * > &_objects)
 
ValueRange getInitialReadRange (const Array &array, ValueRange index)
 
- Public Member Functions inherited from klee::ExprRangeEvaluator< ValueRange >
 ExprRangeEvaluator ()
 
virtual ~ExprRangeEvaluator ()
 
ValueRange evaluate (const ref< Expr > &e)
 

Public Attributes

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

Additional Inherited Members

- Protected Member Functions inherited from klee::ExprRangeEvaluator< ValueRange >
virtual ValueRange getInitialReadRange (const Array &os, ValueRange index)=0
 
ValueRange evalRead (const UpdateList &ul, ValueRange index)
 

Detailed Description

Definition at line 353 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

◆ CexRangeEvaluator()

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

Definition at line 356 of file FastCexSolver.cpp.

Member Function Documentation

◆ getInitialReadRange()

ValueRange CexRangeEvaluator::getInitialReadRange ( const Array os,
ValueRange  index 
)
inlinevirtual

getInitialReadRange - Return a range for the initial value of the given array (which may be constant), for the given range of indices.

Implements klee::ExprRangeEvaluator< ValueRange >.

Definition at line 359 of file FastCexSolver.cpp.

References klee::Array::constantValues, klee::Array::isConstantArray(), ValueRange::isFixed(), ValueRange::min(), and klee::Array::size.

Here is the call graph for this function:

Member Data Documentation

◆ objects

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

Definition at line 355 of file FastCexSolver.cpp.


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