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

Public Member Functions

 ValueRange ()
 
 ValueRange (const ref< ConstantExpr > &ce)
 
 ValueRange (uint64_t value)
 
 ValueRange (uint64_t _min, uint64_t _max)
 
 ValueRange (const ValueRange &b)
 
void print (llvm::raw_ostream &os) const
 
bool isEmpty () const
 
bool contains (uint64_t value) const
 
bool intersects (const ValueRange &b) const
 
bool isFullRange (unsigned bits)
 
ValueRange set_intersection (const ValueRange &b) const
 
ValueRange set_union (const ValueRange &b) const
 
ValueRange set_difference (const ValueRange &b) const
 
ValueRange binaryAnd (const ValueRange &b) const
 
ValueRange binaryAnd (uint64_t b) const
 
ValueRange binaryOr (ValueRange b) const
 
ValueRange binaryOr (uint64_t b) const
 
ValueRange binaryXor (ValueRange b) const
 
ValueRange binaryShiftLeft (unsigned bits) const
 
ValueRange binaryShiftRight (unsigned bits) const
 
ValueRange concat (const ValueRange &b, unsigned bits) const
 
ValueRange extract (uint64_t lowBit, uint64_t maxBit) const
 
ValueRange add (const ValueRange &b, unsigned width) const
 
ValueRange sub (const ValueRange &b, unsigned width) const
 
ValueRange mul (const ValueRange &b, unsigned width) const
 
ValueRange udiv (const ValueRange &b, unsigned width) const
 
ValueRange sdiv (const ValueRange &b, unsigned width) const
 
ValueRange urem (const ValueRange &b, unsigned width) const
 
ValueRange srem (const ValueRange &b, unsigned width) const
 
bool isFixed () const
 
bool operator== (const ValueRange &b) const
 
bool operator!= (const ValueRange &b) const
 
bool mustEqual (const uint64_t b) const
 
bool mayEqual (const uint64_t b) const
 
bool mustEqual (const ValueRange &b) const
 
bool mayEqual (const ValueRange &b) const
 
uint64_t min () const
 
uint64_t max () const
 
int64_t minSigned (unsigned bits) const
 
int64_t maxSigned (unsigned bits) const
 

Private Attributes

uint64_t m_min
 
uint64_t m_max
 

Detailed Description

Definition at line 100 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

ValueRange::ValueRange ( )
inline

Definition at line 105 of file FastCexSolver.cpp.

ValueRange::ValueRange ( const ref< ConstantExpr > &  ce)
inline

Definition at line 106 of file FastCexSolver.cpp.

References klee::ConstantExpr::getLimitedValue().

Here is the call graph for this function:

ValueRange::ValueRange ( uint64_t  value)
inline

Definition at line 110 of file FastCexSolver.cpp.

ValueRange::ValueRange ( uint64_t  _min,
uint64_t  _max 
)
inline

Definition at line 111 of file FastCexSolver.cpp.

ValueRange::ValueRange ( const ValueRange b)
inline

Definition at line 112 of file FastCexSolver.cpp.

Member Function Documentation

ValueRange ValueRange::add ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 205 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

ValueRange ValueRange::binaryAnd ( const ValueRange b) const
inline

Definition at line 158 of file FastCexSolver.cpp.

References isEmpty(), isFixed(), m_max, m_min, maxAND(), and minAND().

Referenced by extract(), and CexData::propogatePossibleValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ValueRange ValueRange::binaryAnd ( uint64_t  b) const
inline

Definition at line 168 of file FastCexSolver.cpp.

References binaryAnd().

Referenced by binaryAnd().

Here is the call graph for this function:

Here is the caller graph for this function:

ValueRange ValueRange::binaryOr ( ValueRange  b) const
inline

Definition at line 169 of file FastCexSolver.cpp.

References isEmpty(), isFixed(), m_max, m_min, maxOR(), and minOR().

Referenced by concat().

Here is the call graph for this function:

Here is the caller graph for this function:

ValueRange ValueRange::binaryOr ( uint64_t  b) const
inline

Definition at line 179 of file FastCexSolver.cpp.

References binaryOr().

Referenced by binaryOr().

Here is the call graph for this function:

Here is the caller graph for this function:

ValueRange ValueRange::binaryShiftLeft ( unsigned  bits) const
inline

Definition at line 191 of file FastCexSolver.cpp.

ValueRange ValueRange::binaryShiftRight ( unsigned  bits) const
inline

Definition at line 194 of file FastCexSolver.cpp.

ValueRange ValueRange::binaryXor ( ValueRange  b) const
inline

Definition at line 180 of file FastCexSolver.cpp.

References isFixed(), klee::bits64::isPowerOfTwo(), m_max, m_min, and klee::bits64::withoutRightmostBit().

Here is the call graph for this function:

ValueRange ValueRange::concat ( const ValueRange b,
unsigned  bits 
) const
inline

Definition at line 198 of file FastCexSolver.cpp.

References binaryOr().

Here is the call graph for this function:

bool ValueRange::contains ( uint64_t  value) const
inline

Definition at line 125 of file FastCexSolver.cpp.

ValueRange ValueRange::extract ( uint64_t  lowBit,
uint64_t  maxBit 
) const
inline

Definition at line 201 of file FastCexSolver.cpp.

References binaryAnd(), and klee::bits64::maxValueOfNBits().

Referenced by CexData::propogatePossibleValues().

Here is the call graph for this function:

Here is the caller graph for this function:

bool ValueRange::intersects ( const ValueRange b) const
inline

Definition at line 128 of file FastCexSolver.cpp.

bool ValueRange::isEmpty ( ) const
inline

Definition at line 122 of file FastCexSolver.cpp.

Referenced by binaryAnd(), binaryOr(), CexData::propogatePossibleValues(), and set_difference().

Here is the caller graph for this function:

bool ValueRange::isFixed ( ) const
inline
bool ValueRange::isFullRange ( unsigned  bits)
inline

Definition at line 132 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

uint64_t ValueRange::max ( ) const
inline

Definition at line 249 of file FastCexSolver.cpp.

Referenced by CexObjectData::getPossibleValue(), CexData::propogateExactValues(), and CexData::propogatePossibleValues().

Here is the caller graph for this function:

int64_t ValueRange::maxSigned ( unsigned  bits) const
inline

Definition at line 270 of file FastCexSolver.cpp.

References klee::ints::sext().

Here is the call graph for this function:

bool ValueRange::mayEqual ( const uint64_t  b) const
inline

Definition at line 237 of file FastCexSolver.cpp.

Referenced by CexData::propogateExactValues().

Here is the caller graph for this function:

bool ValueRange::mayEqual ( const ValueRange b) const
inline

Definition at line 242 of file FastCexSolver.cpp.

uint64_t ValueRange::min ( ) const
inline
int64_t ValueRange::minSigned ( unsigned  bits) const
inline

Definition at line 254 of file FastCexSolver.cpp.

References klee::ints::sext().

Here is the call graph for this function:

ValueRange ValueRange::mul ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 211 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

bool ValueRange::mustEqual ( const uint64_t  b) const
inline

Definition at line 236 of file FastCexSolver.cpp.

Referenced by CexData::propogateExactValues(), and CexData::propogatePossibleValues().

Here is the caller graph for this function:

bool ValueRange::mustEqual ( const ValueRange b) const
inline

Definition at line 239 of file FastCexSolver.cpp.

References isFixed(), and m_min.

Here is the call graph for this function:

bool ValueRange::operator!= ( const ValueRange b) const
inline

Definition at line 234 of file FastCexSolver.cpp.

bool ValueRange::operator== ( const ValueRange b) const
inline

Definition at line 231 of file FastCexSolver.cpp.

References m_max, and m_min.

void ValueRange::print ( llvm::raw_ostream &  os) const
inline

Definition at line 114 of file FastCexSolver.cpp.

Referenced by operator<<().

Here is the caller graph for this function:

ValueRange ValueRange::sdiv ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 217 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

ValueRange ValueRange::set_difference ( const ValueRange b) const
inline

Definition at line 142 of file FastCexSolver.cpp.

References isEmpty(), m_max, and m_min.

Referenced by CexData::propogatePossibleValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ValueRange ValueRange::set_intersection ( const ValueRange b) const
inline

Definition at line 136 of file FastCexSolver.cpp.

References m_max, and m_min.

Referenced by CexData::propogatePossibleValues().

Here is the caller graph for this function:

ValueRange ValueRange::set_union ( const ValueRange b) const
inline

Definition at line 139 of file FastCexSolver.cpp.

References m_max, and m_min.

ValueRange ValueRange::srem ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 223 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

ValueRange ValueRange::sub ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 208 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

ValueRange ValueRange::udiv ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 214 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

ValueRange ValueRange::urem ( const ValueRange b,
unsigned  width 
) const
inline

Definition at line 220 of file FastCexSolver.cpp.

References klee::bits64::maxValueOfNBits().

Here is the call graph for this function:

Member Data Documentation

uint64_t ValueRange::m_max
private
uint64_t ValueRange::m_min
private

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