cprover
|
#include <ieee_float.h>
Public Types | |
enum | rounding_modet { ROUND_TO_EVEN =0, ROUND_TO_MINUS_INF =1, ROUND_TO_PLUS_INF =2, ROUND_TO_ZERO =3, UNKNOWN, NONDETERMINISTIC } |
Public Member Functions | |
ieee_floatt (const ieee_float_spect &_spec) | |
ieee_floatt (const floatbv_typet &type) | |
ieee_floatt () | |
ieee_floatt (const constant_exprt &expr) | |
void | negate () |
void | set_sign (bool _sign) |
void | make_zero () |
void | make_NaN () |
void | make_plus_infinity () |
void | make_minus_infinity () |
void | make_fltmax () |
void | make_fltmin () |
void | increment (bool distinguish_zero=false) |
void | decrement (bool distinguish_zero=false) |
bool | is_zero () const |
bool | get_sign () const |
bool | is_NaN () const |
bool | is_infinity () const |
bool | is_normal () const |
const mp_integer & | get_exponent () const |
const mp_integer & | get_fraction () const |
void | from_integer (const mp_integer &i) |
void | from_base10 (const mp_integer &exp, const mp_integer &frac) |
compute f * (10^e) More... | |
void | build (const mp_integer &exp, const mp_integer &frac) |
void | unpack (const mp_integer &i) |
void | from_double (const double d) |
void | from_float (const float f) |
double | to_double () const |
Note that calling from_double -> to_double can return different bit patterns for NaN. More... | |
float | to_float () const |
Note that calling from_float -> to_float can return different bit patterns for NaN. More... | |
bool | is_double () const |
bool | is_float () const |
mp_integer | pack () const |
void | extract_base2 (mp_integer &_exponent, mp_integer &_fraction) const |
void | extract_base10 (mp_integer &_exponent, mp_integer &_fraction) const |
mp_integer | to_integer () const |
void | change_spec (const ieee_float_spect &dest_spec) |
void | print (std::ostream &out) const |
std::string | to_ansi_c_string () const |
std::string | to_string_decimal (std::size_t precision) const |
std::string | to_string_scientific (std::size_t precision) const |
format as [-]d.ddde+-d Note that printf always produces at least two digits for the exponent. More... | |
std::string | format (const format_spect &format_spec) const |
constant_exprt | to_expr () const |
void | from_expr (const constant_exprt &expr) |
ieee_floatt & | operator/= (const ieee_floatt &other) |
ieee_floatt & | operator*= (const ieee_floatt &other) |
ieee_floatt & | operator+= (const ieee_floatt &other) |
ieee_floatt & | operator-= (const ieee_floatt &other) |
bool | operator< (const ieee_floatt &other) const |
bool | operator<= (const ieee_floatt &other) const |
bool | operator> (const ieee_floatt &other) const |
bool | operator>= (const ieee_floatt &other) const |
bool | operator== (const ieee_floatt &other) const |
bool | operator!= (const ieee_floatt &other) const |
bool | operator== (int i) const |
bool | ieee_equal (const ieee_floatt &other) const |
bool | ieee_not_equal (const ieee_floatt &other) const |
Static Public Member Functions | |
static ieee_floatt | zero (const floatbv_typet &type) |
static ieee_floatt | NaN (const ieee_float_spect &_spec) |
static ieee_floatt | plus_infinity (const ieee_float_spect &_spec) |
static ieee_floatt | minus_infinity (const ieee_float_spect &_spec) |
static ieee_floatt | fltmax (const ieee_float_spect &_spec) |
static ieee_floatt | fltmin (const ieee_float_spect &_spec) |
Public Attributes | |
rounding_modet | rounding_mode |
ieee_float_spect | spec |
Protected Member Functions | |
void | divide_and_round (mp_integer ÷nd, const mp_integer &divisor) |
void | align () |
void | next_representable (bool greater) |
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false). More... | |
Static Protected Member Functions | |
static mp_integer | base10_digits (const mp_integer &src) |
Protected Attributes | |
bool | sign_flag |
mp_integer | exponent |
mp_integer | fraction |
bool | NaN_flag |
bool | infinity_flag |
Definition at line 119 of file ieee_float.h.
Enumerator | |
---|---|
ROUND_TO_EVEN | |
ROUND_TO_MINUS_INF | |
ROUND_TO_PLUS_INF | |
ROUND_TO_ZERO | |
UNKNOWN | |
NONDETERMINISTIC |
Definition at line 125 of file ieee_float.h.
|
inlineexplicit |
Definition at line 136 of file ieee_float.h.
|
inlineexplicit |
Definition at line 143 of file ieee_float.h.
|
inline |
Definition at line 154 of file ieee_float.h.
|
inlineexplicit |
Definition at line 161 of file ieee_float.h.
|
protected |
Definition at line 519 of file ieee_float.cpp.
|
staticprotected |
Definition at line 125 of file ieee_float.cpp.
void ieee_floatt::build | ( | const mp_integer & | exp, |
const mp_integer & | frac | ||
) |
Definition at line 468 of file ieee_float.cpp.
void ieee_floatt::change_spec | ( | const ieee_float_spect & | dest_spec | ) |
Definition at line 1044 of file ieee_float.cpp.
|
inline |
Definition at line 224 of file ieee_float.h.
|
protected |
Definition at line 647 of file ieee_float.cpp.
void ieee_floatt::extract_base10 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction | ||
) | const |
Definition at line 432 of file ieee_float.cpp.
void ieee_floatt::extract_base2 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction | ||
) | const |
Definition at line 408 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 207 of file ieee_float.h.
|
inlinestatic |
Definition at line 211 of file ieee_float.h.
std::string ieee_floatt::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 65 of file ieee_float.cpp.
void ieee_floatt::from_base10 | ( | const mp_integer & | exp, |
const mp_integer & | frac | ||
) |
compute f * (10^e)
Definition at line 482 of file ieee_float.cpp.
void ieee_floatt::from_double | ( | const double | d | ) |
Definition at line 1090 of file ieee_float.cpp.
void ieee_floatt::from_expr | ( | const constant_exprt & | expr | ) |
Definition at line 1063 of file ieee_float.cpp.
void ieee_floatt::from_float | ( | const float | f | ) |
Definition at line 1114 of file ieee_float.cpp.
void ieee_floatt::from_integer | ( | const mp_integer & | i | ) |
Definition at line 511 of file ieee_float.cpp.
|
inline |
Definition at line 241 of file ieee_float.h.
|
inline |
Definition at line 242 of file ieee_float.h.
|
inline |
Definition at line 236 of file ieee_float.h.
bool ieee_floatt::ieee_equal | ( | const ieee_floatt & | other | ) | const |
Definition at line 1012 of file ieee_float.cpp.
bool ieee_floatt::ieee_not_equal | ( | const ieee_floatt & | other | ) | const |
Definition at line 1034 of file ieee_float.cpp.
|
inline |
Definition at line 215 of file ieee_float.h.
bool ieee_floatt::is_double | ( | ) | const |
Definition at line 1174 of file ieee_float.cpp.
bool ieee_floatt::is_float | ( | ) | const |
Definition at line 1179 of file ieee_float.cpp.
|
inline |
Definition at line 238 of file ieee_float.h.
|
inline |
Definition at line 237 of file ieee_float.h.
bool ieee_floatt::is_normal | ( | ) | const |
Definition at line 365 of file ieee_float.cpp.
|
inline |
Definition at line 232 of file ieee_float.h.
void ieee_floatt::make_fltmax | ( | ) |
Definition at line 1147 of file ieee_float.cpp.
void ieee_floatt::make_fltmin | ( | ) |
Definition at line 1154 of file ieee_float.cpp.
void ieee_floatt::make_minus_infinity | ( | ) |
Definition at line 1168 of file ieee_float.cpp.
void ieee_floatt::make_NaN | ( | ) |
Definition at line 1138 of file ieee_float.cpp.
void ieee_floatt::make_plus_infinity | ( | ) |
Definition at line 1159 of file ieee_float.cpp.
|
inline |
Definition at line 175 of file ieee_float.h.
|
inlinestatic |
Definition at line 203 of file ieee_float.h.
|
inlinestatic |
Definition at line 197 of file ieee_float.h.
|
inline |
Definition at line 167 of file ieee_float.h.
|
protected |
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false).
Definition at line 1251 of file ieee_float.cpp.
bool ieee_floatt::operator!= | ( | const ieee_floatt & | other | ) | const |
Definition at line 1029 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator*= | ( | const ieee_floatt & | other | ) |
Definition at line 777 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator+= | ( | const ieee_floatt & | other | ) |
Definition at line 813 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator-= | ( | const ieee_floatt & | other | ) |
Definition at line 904 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator/= | ( | const ieee_floatt & | other | ) |
Definition at line 703 of file ieee_float.cpp.
bool ieee_floatt::operator< | ( | const ieee_floatt & | other | ) | const |
Definition at line 911 of file ieee_float.cpp.
bool ieee_floatt::operator<= | ( | const ieee_floatt & | other | ) | const |
Definition at line 957 of file ieee_float.cpp.
bool ieee_floatt::operator== | ( | const ieee_floatt & | other | ) | const |
Definition at line 990 of file ieee_float.cpp.
bool ieee_floatt::operator== | ( | int | i | ) | const |
Definition at line 1022 of file ieee_float.cpp.
bool ieee_floatt::operator> | ( | const ieee_floatt & | other | ) | const |
Definition at line 980 of file ieee_float.cpp.
bool ieee_floatt::operator>= | ( | const ieee_floatt & | other | ) | const |
Definition at line 985 of file ieee_float.cpp.
mp_integer ieee_floatt::pack | ( | ) | const |
Definition at line 370 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 200 of file ieee_float.h.
void ieee_floatt::print | ( | std::ostream & | out | ) | const |
Definition at line 60 of file ieee_float.cpp.
|
inline |
Definition at line 172 of file ieee_float.h.
|
inline |
Definition at line 269 of file ieee_float.h.
double ieee_floatt::to_double | ( | ) | const |
Note that calling from_double -> to_double can return different bit patterns for NaN.
Definition at line 1186 of file ieee_float.cpp.
constant_exprt ieee_floatt::to_expr | ( | ) | const |
Definition at line 698 of file ieee_float.cpp.
float ieee_floatt::to_float | ( | ) | const |
Note that calling from_float -> to_float can return different bit patterns for NaN.
Definition at line 1217 of file ieee_float.cpp.
mp_integer ieee_floatt::to_integer | ( | ) | const |
Definition at line 1069 of file ieee_float.cpp.
std::string ieee_floatt::to_string_decimal | ( | std::size_t | precision | ) | const |
Definition at line 134 of file ieee_float.cpp.
std::string ieee_floatt::to_string_scientific | ( | std::size_t | precision | ) | const |
format as [-]d.ddde+-d Note that printf always produces at least two digits for the exponent.
Definition at line 228 of file ieee_float.cpp.
void ieee_floatt::unpack | ( | const mp_integer & | i | ) |
Definition at line 315 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 184 of file ieee_float.h.
|
protected |
Definition at line 310 of file ieee_float.h.
|
protected |
Definition at line 311 of file ieee_float.h.
|
protected |
Definition at line 312 of file ieee_float.h.
|
protected |
Definition at line 312 of file ieee_float.h.
rounding_modet ieee_floatt::rounding_mode |
Definition at line 132 of file ieee_float.h.
|
protected |
Definition at line 309 of file ieee_float.h.
ieee_float_spect ieee_floatt::spec |
Definition at line 134 of file ieee_float.h.