cprover
|
#include <float_utils.h>
Classes | |
struct | biased_floatt |
struct | rounding_mode_bitst |
struct | unbiased_floatt |
struct | unpacked_floatt |
Public Types | |
enum class | relt { LT , LE , EQ , GT , GE } |
Static Public Member Functions | |
static literalt | sign_bit (const bvt &src) |
Public Attributes | |
rounding_mode_bitst | rounding_mode_bits |
ieee_float_spect | spec |
Protected Attributes | |
propt & | prop |
bv_utilst | bv_utils |
Definition at line 17 of file float_utils.h.
|
strong |
Enumerator | |
---|---|
LT | |
LE | |
EQ | |
GT | |
GE |
Definition at line 138 of file float_utils.h.
|
inlineexplicit |
Definition at line 69 of file float_utils.h.
|
inline |
Definition at line 75 of file float_utils.h.
|
inlinevirtual |
Definition at line 84 of file float_utils.h.
Definition at line 570 of file float_utils.cpp.
Definition at line 111 of file float_utils.h.
Definition at line 1193 of file float_utils.cpp.
Definition at line 247 of file float_utils.cpp.
|
protected |
takes an unbiased float, and applies the bias
Definition at line 1163 of file float_utils.cpp.
bvt float_utilst::build_constant | ( | const ieee_floatt & | src | ) |
Definition at line 139 of file float_utils.cpp.
bvt float_utilst::conversion | ( | const bvt & | src, |
const ieee_float_spect & | dest_spec | ||
) |
Definition at line 152 of file float_utils.cpp.
Definition at line 1320 of file float_utils.cpp.
Definition at line 1327 of file float_utils.cpp.
make sure exponent is not too small; the exponent is unbiased
Definition at line 836 of file float_utils.cpp.
Definition at line 464 of file float_utils.cpp.
Definition at line 711 of file float_utils.cpp.
Definition at line 724 of file float_utils.cpp.
Definition at line 737 of file float_utils.cpp.
|
protected |
rounding decision for fraction using sticky bit
Definition at line 943 of file float_utils.cpp.
Definition at line 32 of file float_utils.cpp.
Definition at line 50 of file float_utils.cpp.
ieee_floatt float_utilst::get | ( | const bvt & | src | ) | const |
Definition at line 1271 of file float_utils.cpp.
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 685 of file float_utils.cpp.
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 691 of file float_utils.cpp.
Definition at line 677 of file float_utils.cpp.
Definition at line 696 of file float_utils.cpp.
Definition at line 705 of file float_utils.cpp.
Definition at line 223 of file float_utils.cpp.
Definition at line 668 of file float_utils.cpp.
Definition at line 659 of file float_utils.cpp.
|
protected |
Limits the shift distance.
Definition at line 389 of file float_utils.cpp.
Definition at line 412 of file float_utils.cpp.
Definition at line 561 of file float_utils.cpp.
normalize fraction/exponent pair returns 'zero' if fraction is zero
Reimplemented in float_approximationt.
Definition at line 747 of file float_utils.cpp.
|
protected |
Definition at line 1240 of file float_utils.cpp.
Definition at line 578 of file float_utils.cpp.
Definition at line 543 of file float_utils.cpp.
|
protected |
Definition at line 1100 of file float_utils.cpp.
|
protected |
Definition at line 1001 of file float_utils.cpp.
|
protectedvirtual |
Definition at line 904 of file float_utils.cpp.
Definition at line 15 of file float_utils.cpp.
Definition at line 92 of file float_utils.h.
|
protected |
Definition at line 1285 of file float_utils.cpp.
Definition at line 116 of file float_utils.h.
Definition at line 1202 of file float_utils.cpp.
|
protected |
Subtracts the exponents.
Definition at line 231 of file float_utils.cpp.
Definition at line 81 of file float_utils.cpp.
Definition at line 67 of file float_utils.cpp.
Definition at line 74 of file float_utils.cpp.
|
protected |
Definition at line 1211 of file float_utils.cpp.
|
protected |
Definition at line 155 of file float_utils.h.
|
protected |
Definition at line 154 of file float_utils.h.
rounding_mode_bitst float_utilst::rounding_mode_bits |
Definition at line 67 of file float_utils.h.
ieee_float_spect float_utilst::spec |
Definition at line 88 of file float_utils.h.