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 } |
Static Public Member Functions | |
static constant_exprt | rounding_mode_expr (rounding_modet) |
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). | |
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 115 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 122 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.
|
inlineexplicit |
Definition at line 154 of file ieee_float.h.
|
inline |
Definition at line 165 of file ieee_float.h.
|
inlineexplicit |
Definition at line 172 of file ieee_float.h.
|
protected |
Definition at line 524 of file ieee_float.cpp.
|
staticprotected |
Definition at line 130 of file ieee_float.cpp.
void ieee_floatt::build | ( | const mp_integer & | exp, |
const mp_integer & | frac ) |
Definition at line 473 of file ieee_float.cpp.
void ieee_floatt::change_spec | ( | const ieee_float_spect & | dest_spec | ) |
Definition at line 1049 of file ieee_float.cpp.
Definition at line 235 of file ieee_float.h.
|
protected |
Definition at line 652 of file ieee_float.cpp.
void ieee_floatt::extract_base10 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction ) const |
Definition at line 437 of file ieee_float.cpp.
void ieee_floatt::extract_base2 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction ) const |
Definition at line 413 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 218 of file ieee_float.h.
|
inlinestatic |
Definition at line 222 of file ieee_float.h.
std::string ieee_floatt::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 70 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 487 of file ieee_float.cpp.
Definition at line 1095 of file ieee_float.cpp.
void ieee_floatt::from_expr | ( | const constant_exprt & | expr | ) |
Definition at line 1068 of file ieee_float.cpp.
Definition at line 1119 of file ieee_float.cpp.
void ieee_floatt::from_integer | ( | const mp_integer & | i | ) |
Definition at line 516 of file ieee_float.cpp.
|
inline |
Definition at line 252 of file ieee_float.h.
|
inline |
Definition at line 253 of file ieee_float.h.
|
inline |
Definition at line 247 of file ieee_float.h.
bool ieee_floatt::ieee_equal | ( | const ieee_floatt & | other | ) | const |
Definition at line 1017 of file ieee_float.cpp.
bool ieee_floatt::ieee_not_equal | ( | const ieee_floatt & | other | ) | const |
Definition at line 1039 of file ieee_float.cpp.
Definition at line 226 of file ieee_float.h.
bool ieee_floatt::is_double | ( | ) | const |
Definition at line 1179 of file ieee_float.cpp.
bool ieee_floatt::is_float | ( | ) | const |
Definition at line 1184 of file ieee_float.cpp.
|
inline |
Definition at line 249 of file ieee_float.h.
|
inline |
Definition at line 248 of file ieee_float.h.
bool ieee_floatt::is_normal | ( | ) | const |
Definition at line 370 of file ieee_float.cpp.
|
inline |
Definition at line 243 of file ieee_float.h.
void ieee_floatt::make_fltmax | ( | ) |
Definition at line 1152 of file ieee_float.cpp.
void ieee_floatt::make_fltmin | ( | ) |
Definition at line 1159 of file ieee_float.cpp.
void ieee_floatt::make_minus_infinity | ( | ) |
Definition at line 1173 of file ieee_float.cpp.
void ieee_floatt::make_NaN | ( | ) |
Definition at line 1143 of file ieee_float.cpp.
void ieee_floatt::make_plus_infinity | ( | ) |
Definition at line 1164 of file ieee_float.cpp.
|
inline |
Definition at line 186 of file ieee_float.h.
|
inlinestatic |
Definition at line 214 of file ieee_float.h.
|
inlinestatic |
Definition at line 208 of file ieee_float.h.
|
inline |
Definition at line 178 of file ieee_float.h.
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false).
Definition at line 1256 of file ieee_float.cpp.
bool ieee_floatt::operator!= | ( | const ieee_floatt & | other | ) | const |
Definition at line 1034 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator*= | ( | const ieee_floatt & | other | ) |
Definition at line 782 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator+= | ( | const ieee_floatt & | other | ) |
Definition at line 818 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator-= | ( | const ieee_floatt & | other | ) |
Definition at line 909 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator/= | ( | const ieee_floatt & | other | ) |
Definition at line 708 of file ieee_float.cpp.
bool ieee_floatt::operator< | ( | const ieee_floatt & | other | ) | const |
Definition at line 916 of file ieee_float.cpp.
bool ieee_floatt::operator<= | ( | const ieee_floatt & | other | ) | const |
Definition at line 962 of file ieee_float.cpp.
bool ieee_floatt::operator== | ( | const ieee_floatt & | other | ) | const |
Definition at line 995 of file ieee_float.cpp.
Definition at line 1027 of file ieee_float.cpp.
bool ieee_floatt::operator> | ( | const ieee_floatt & | other | ) | const |
Definition at line 985 of file ieee_float.cpp.
bool ieee_floatt::operator>= | ( | const ieee_floatt & | other | ) | const |
Definition at line 990 of file ieee_float.cpp.
mp_integer ieee_floatt::pack | ( | ) | const |
Definition at line 375 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 211 of file ieee_float.h.
void ieee_floatt::print | ( | std::ostream & | out | ) | const |
Definition at line 65 of file ieee_float.cpp.
|
static |
Definition at line 60 of file ieee_float.cpp.
Definition at line 183 of file ieee_float.h.
|
inline |
Definition at line 280 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 1191 of file ieee_float.cpp.
constant_exprt ieee_floatt::to_expr | ( | ) | const |
Definition at line 703 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 1222 of file ieee_float.cpp.
mp_integer ieee_floatt::to_integer | ( | ) | const |
Definition at line 1074 of file ieee_float.cpp.
std::string ieee_floatt::to_string_decimal | ( | std::size_t | precision | ) | const |
Definition at line 139 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 233 of file ieee_float.cpp.
void ieee_floatt::unpack | ( | const mp_integer & | i | ) |
Definition at line 320 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 195 of file ieee_float.h.
|
protected |
Definition at line 321 of file ieee_float.h.
|
protected |
Definition at line 322 of file ieee_float.h.
|
protected |
Definition at line 323 of file ieee_float.h.
|
protected |
Definition at line 323 of file ieee_float.h.
rounding_modet ieee_floatt::rounding_mode |
Definition at line 132 of file ieee_float.h.
|
protected |
Definition at line 320 of file ieee_float.h.
ieee_float_spect ieee_floatt::spec |
Definition at line 134 of file ieee_float.h.