klee
|
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 |
|
inline |
Definition at line 84 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 111 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 54 of file FloatEvaluation.h.
Referenced by add(), div(), ext(), mod(), mul(), SignedIntToFP(), sub(), and UnsignedIntToFP().
|
inline |
Definition at line 144 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
Referenced by klee::Executor::replaceReadWithSymbolic().
|
inline |
Definition at line 212 of file FloatEvaluation.h.
References DoubleAsUInt64(), ext(), klee::bits64::truncateToNBits(), and UInt64AsFloat().
Referenced by ext(), externalsAndGlobalsCheck(), and klee::Executor::terminateStateOnError().
|
inline |
Definition at line 62 of file FloatEvaluation.h.
Referenced by add(), div(), mod(), mul(), SignedIntToFP(), sub(), trunc(), and UnsignedIntToFP().
|
inline |
Definition at line 184 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 176 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 134 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 168 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 160 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 120 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 102 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 152 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 253 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::ints::sext(), and klee::bits64::truncateToNBits().
|
inline |
Definition at line 93 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
Referenced by klee::ComputeMultConstants64().
|
inline |
Definition at line 235 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 226 of file FloatEvaluation.h.
References DBL_BITS, FLT_BITS, klee::bits64::truncateToNBits(), UInt64AsDouble(), and UInt64AsFloat().
|
inline |
Definition at line 198 of file FloatEvaluation.h.
References FloatAsUInt64(), trunc(), klee::bits64::truncateToNBits(), and UInt64AsDouble().
Referenced by EqExpr_createPartialR(), klee::IntrinsicCleanerPass::runOnBasicBlock(), and trunc().
|
inline |
|
inline |
|
inline |
Definition at line 244 of file FloatEvaluation.h.
References DBL_BITS, DoubleAsUInt64(), FloatAsUInt64(), FLT_BITS, and klee::bits64::truncateToNBits().
const unsigned klee::floats::DBL_BITS = 64 |
Definition at line 75 of file FloatEvaluation.h.
Referenced by add(), div(), eq(), ge(), gt(), isNaN(), le(), lt(), mod(), mul(), ne(), SignedIntToFP(), sub(), toSignedInt(), toUnsignedInt(), and UnsignedIntToFP().
const unsigned klee::floats::FLT_BITS = 32 |
Definition at line 74 of file FloatEvaluation.h.
Referenced by add(), div(), eq(), ge(), gt(), isNaN(), le(), lt(), mod(), mul(), ne(), SignedIntToFP(), sub(), toSignedInt(), toUnsignedInt(), and UnsignedIntToFP().