cprover
|
An IEEE 754 floating-point value, including specificiation. More...
#include <ieee_float.h>
Public Member Functions | |
ieee_float_valuet (const ieee_float_spect &_spec) | |
ieee_float_valuet (const floatbv_typet &type) | |
ieee_float_valuet (const constant_exprt &expr) | |
ieee_float_valuet () | |
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_negative () 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 | unpack (const mp_integer &) |
void | from_double (double) |
void | from_float (float) |
double | to_double () const |
Note that calling from_double -> to_double can return different bit patterns for NaN. | |
float | to_float () const |
Note that calling from_float -> to_float can return different bit patterns for NaN. | |
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 | 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. | |
std::string | format (const format_spect &format_spec) const |
constant_exprt | to_expr () const |
void | from_expr (const constant_exprt &expr) |
bool | operator< (const ieee_float_valuet &) const |
bool | operator<= (const ieee_float_valuet &) const |
bool | operator> (const ieee_float_valuet &) const |
bool | operator>= (const ieee_float_valuet &) const |
ieee_float_valuet | abs () const |
bool | operator== (const ieee_float_valuet &) const |
bool | operator!= (const ieee_float_valuet &) const |
bool | operator== (int) const |
bool | operator== (double) const |
bool | operator== (float) const |
bool | ieee_equal (const ieee_float_valuet &) const |
bool | ieee_not_equal (const ieee_float_valuet &) const |
Static Public Member Functions | |
static ieee_float_valuet | zero (const floatbv_typet &type) |
static ieee_float_valuet | zero (const ieee_float_spect &spec) |
static ieee_float_valuet | one (const floatbv_typet &) |
static ieee_float_valuet | one (const ieee_float_spect &) |
static ieee_float_valuet | NaN (const ieee_float_spect &_spec) |
static ieee_float_valuet | plus_infinity (const ieee_float_spect &_spec) |
static ieee_float_valuet | minus_infinity (const ieee_float_spect &_spec) |
static ieee_float_valuet | fltmax (const ieee_float_spect &_spec) |
static ieee_float_valuet | fltmin (const ieee_float_spect &_spec) |
Public Attributes | |
ieee_float_spect | spec |
Protected Member Functions | |
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 |
An IEEE 754 floating-point value, including specificiation.
Definition at line 116 of file ieee_float.h.
|
inlineexplicit |
Definition at line 121 of file ieee_float.h.
|
inlineexplicit |
Definition at line 131 of file ieee_float.h.
|
inlineexplicit |
Definition at line 141 of file ieee_float.h.
|
inline |
Definition at line 146 of file ieee_float.h.
ieee_float_valuet ieee_float_valuet::abs | ( | ) | const |
Definition at line 60 of file ieee_float.cpp.
|
staticprotected |
Definition at line 132 of file ieee_float.cpp.
|
inline |
Definition at line 242 of file ieee_float.h.
void ieee_float_valuet::extract_base10 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction ) const |
Definition at line 439 of file ieee_float.cpp.
void ieee_float_valuet::extract_base2 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction ) const |
Definition at line 415 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 217 of file ieee_float.h.
|
inlinestatic |
Definition at line 225 of file ieee_float.h.
std::string ieee_float_valuet::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 72 of file ieee_float.cpp.
void ieee_float_valuet::from_double | ( | double | d | ) |
Definition at line 1277 of file ieee_float.cpp.
void ieee_float_valuet::from_expr | ( | const constant_exprt & | expr | ) |
Definition at line 1250 of file ieee_float.cpp.
void ieee_float_valuet::from_float | ( | float | f | ) |
Definition at line 1301 of file ieee_float.cpp.
|
inline |
Definition at line 263 of file ieee_float.h.
|
inline |
Definition at line 264 of file ieee_float.h.
|
inline |
Definition at line 254 of file ieee_float.h.
bool ieee_float_valuet::ieee_equal | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 686 of file ieee_float.cpp.
bool ieee_float_valuet::ieee_not_equal | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 725 of file ieee_float.cpp.
|
inline |
Definition at line 233 of file ieee_float.h.
bool ieee_float_valuet::is_double | ( | ) | const |
Definition at line 1361 of file ieee_float.cpp.
bool ieee_float_valuet::is_float | ( | ) | const |
Definition at line 1366 of file ieee_float.cpp.
|
inline |
Definition at line 260 of file ieee_float.h.
|
inline |
Definition at line 259 of file ieee_float.h.
|
inline |
Definition at line 255 of file ieee_float.h.
bool ieee_float_valuet::is_normal | ( | ) | const |
Definition at line 372 of file ieee_float.cpp.
|
inline |
Definition at line 250 of file ieee_float.h.
void ieee_float_valuet::make_fltmax | ( | ) |
Definition at line 1334 of file ieee_float.cpp.
void ieee_float_valuet::make_fltmin | ( | ) |
Definition at line 1341 of file ieee_float.cpp.
void ieee_float_valuet::make_minus_infinity | ( | ) |
Definition at line 1355 of file ieee_float.cpp.
void ieee_float_valuet::make_NaN | ( | ) |
Definition at line 1325 of file ieee_float.cpp.
void ieee_float_valuet::make_plus_infinity | ( | ) |
Definition at line 1346 of file ieee_float.cpp.
|
inline |
Definition at line 163 of file ieee_float.h.
|
inlinestatic |
Definition at line 209 of file ieee_float.h.
|
inlinestatic |
Definition at line 195 of file ieee_float.h.
|
inline |
Definition at line 155 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 739 of file ieee_float.cpp.
|
static |
Definition at line 483 of file ieee_float.cpp.
|
static |
Definition at line 475 of file ieee_float.cpp.
bool ieee_float_valuet::operator!= | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 720 of file ieee_float.cpp.
bool ieee_float_valuet::operator< | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 584 of file ieee_float.cpp.
bool ieee_float_valuet::operator<= | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 632 of file ieee_float.cpp.
bool ieee_float_valuet::operator== | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 665 of file ieee_float.cpp.
bool ieee_float_valuet::operator== | ( | double | d | ) | const |
Definition at line 706 of file ieee_float.cpp.
bool ieee_float_valuet::operator== | ( | float | f | ) | const |
Definition at line 713 of file ieee_float.cpp.
bool ieee_float_valuet::operator== | ( | int | i | ) | const |
Definition at line 698 of file ieee_float.cpp.
bool ieee_float_valuet::operator> | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 655 of file ieee_float.cpp.
bool ieee_float_valuet::operator>= | ( | const ieee_float_valuet & | other | ) | const |
Definition at line 660 of file ieee_float.cpp.
mp_integer ieee_float_valuet::pack | ( | ) | const |
Definition at line 377 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 202 of file ieee_float.h.
void ieee_float_valuet::print | ( | std::ostream & | out | ) | const |
Definition at line 67 of file ieee_float.cpp.
|
inline |
Definition at line 160 of file ieee_float.h.
|
inline |
Definition at line 285 of file ieee_float.h.
double ieee_float_valuet::to_double | ( | ) | const |
Note that calling from_double -> to_double can return different bit patterns for NaN.
Definition at line 490 of file ieee_float.cpp.
constant_exprt ieee_float_valuet::to_expr | ( | ) | const |
Definition at line 579 of file ieee_float.cpp.
float ieee_float_valuet::to_float | ( | ) | const |
Note that calling from_float -> to_float can return different bit patterns for NaN.
Definition at line 525 of file ieee_float.cpp.
mp_integer ieee_float_valuet::to_integer | ( | ) | const |
std::string ieee_float_valuet::to_string_decimal | ( | std::size_t | precision | ) | const |
Definition at line 141 of file ieee_float.cpp.
std::string ieee_float_valuet::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 235 of file ieee_float.cpp.
void ieee_float_valuet::unpack | ( | const mp_integer & | i | ) |
Definition at line 322 of file ieee_float.cpp.
|
inlinestatic |
Definition at line 172 of file ieee_float.h.
|
inlinestatic |
Definition at line 179 of file ieee_float.h.
|
protected |
Definition at line 320 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 322 of file ieee_float.h.
|
protected |
Definition at line 319 of file ieee_float.h.
ieee_float_spect ieee_float_valuet::spec |
Definition at line 119 of file ieee_float.h.