klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::floats Namespace Reference

Functions

double UInt64AsDouble (uint64_t bits)
 
float UInt64AsFloat (uint64_t bits)
 
uint64_t DoubleAsUInt64 (double d)
 
uint64_t FloatAsUInt64 (float f)
 
uint64_t add (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t sub (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t mul (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t div (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t mod (uint64_t l, uint64_t r, unsigned inWidth)
 
bool isNaN (uint64_t l, unsigned inWidth)
 
uint64_t eq (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t ne (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t lt (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t le (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t gt (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t ge (uint64_t l, uint64_t r, unsigned inWidth)
 
uint64_t trunc (uint64_t l, unsigned outWidth, unsigned inWidth)
 
uint64_t ext (uint64_t l, unsigned outWidth, unsigned inWidth)
 
uint64_t toUnsignedInt (uint64_t l, unsigned outWidth, unsigned inWidth)
 
uint64_t toSignedInt (uint64_t l, unsigned outWidth, unsigned inWidth)
 
uint64_t UnsignedIntToFP (uint64_t l, unsigned outWidth)
 
uint64_t SignedIntToFP (uint64_t l, unsigned outWidth, unsigned inWidth)
 

Variables

const unsigned FLT_BITS = 32
 
const unsigned DBL_BITS = 64
 

Function Documentation

uint64_t klee::floats::add ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 82 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::div ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 109 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::DoubleAsUInt64 ( double  d)
inline

Definition at line 52 of file FloatEvaluation.h.

Referenced by add(), div(), ext(), mod(), mul(), SignedIntToFP(), sub(), and UnsignedIntToFP().

Here is the caller graph for this function:

uint64_t klee::floats::eq ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 140 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Referenced by klee::Executor::replaceReadWithSymbolic().

Here is the call graph for this function:

Here is the caller graph for this function:

uint64_t klee::floats::ext ( uint64_t  l,
unsigned  outWidth,
unsigned  inWidth 
)
inline

Definition at line 208 of file FloatEvaluation.h.

References DoubleAsUInt64(), klee::bits64::truncateToNBits(), and UInt64AsFloat().

Referenced by externalsAndGlobalsCheck().

Here is the call graph for this function:

Here is the caller graph for this function:

uint64_t klee::floats::FloatAsUInt64 ( float  f)
inline

Definition at line 60 of file FloatEvaluation.h.

Referenced by add(), div(), mod(), mul(), SignedIntToFP(), sub(), trunc(), and UnsignedIntToFP().

Here is the caller graph for this function:

uint64_t klee::floats::ge ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 180 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::gt ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 172 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

bool klee::floats::isNaN ( uint64_t  l,
unsigned  inWidth 
)
inline

Definition at line 132 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::le ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 164 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::lt ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 156 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::mod ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 118 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::mul ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 100 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::ne ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 148 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().

Referenced by klee::STPBuilder::constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

uint64_t klee::floats::SignedIntToFP ( uint64_t  l,
unsigned  outWidth,
unsigned  inWidth 
)
inline

Definition at line 249 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::ints::sext(), and klee::bits64::truncateToNBits().

Here is the call graph for this function:

uint64_t klee::floats::sub ( uint64_t  l,
uint64_t  r,
unsigned  inWidth 
)
inline

Definition at line 91 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Referenced by klee::STPBuilder::constructMulByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

uint64_t klee::floats::toSignedInt ( uint64_t  l,
unsigned  outWidth,
unsigned  inWidth 
)
inline

Definition at line 231 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::toUnsignedInt ( uint64_t  l,
unsigned  outWidth,
unsigned  inWidth 
)
inline

Definition at line 222 of file FloatEvaluation.h.

References DBL_BITS, FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().

Here is the call graph for this function:

uint64_t klee::floats::trunc ( uint64_t  l,
unsigned  outWidth,
unsigned  inWidth 
)
inline

Definition at line 194 of file FloatEvaluation.h.

References FloatAsUInt64(), klee::bits64::truncateToNBits(), and UInt64AsDouble().

Referenced by EqExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

double klee::floats::UInt64AsDouble ( uint64_t  bits)
inline

Definition at line 30 of file FloatEvaluation.h.

Referenced by add(), div(), eq(), ge(), gt(), isNaN(), le(), lt(), mod(), mul(), ne(), sub(), toSignedInt(), toUnsignedInt(), and trunc().

Here is the caller graph for this function:

float klee::floats::UInt64AsFloat ( uint64_t  bits)
inline

Definition at line 38 of file FloatEvaluation.h.

Referenced by add(), div(), eq(), ext(), ge(), gt(), isNaN(), le(), lt(), mod(), mul(), ne(), sub(), toSignedInt(), and toUnsignedInt().

Here is the caller graph for this function:

uint64_t klee::floats::UnsignedIntToFP ( uint64_t  l,
unsigned  outWidth 
)
inline

Definition at line 240 of file FloatEvaluation.h.

References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, and klee::bits64::truncateToNBits().

Here is the call graph for this function:

Variable Documentation

const unsigned klee::floats::DBL_BITS = 64
const unsigned klee::floats::FLT_BITS = 32