CBMC
Loading...
Searching...
No Matches
ieee_floatt Class Reference

An IEEE 754 value plus a rounding mode, enabling operations with rounding on values. More...

#include <ieee_float.h>

+ Inheritance diagram for ieee_floatt:
+ Collaboration diagram for ieee_floatt:

Public Types

enum  rounding_modet {
  ROUND_TO_EVEN = 0 , ROUND_TO_MINUS_INF = 1 , ROUND_TO_PLUS_INF = 2 , ROUND_TO_ZERO = 3 ,
  ROUND_TO_AWAY = 4 , UNKNOWN , NONDETERMINISTIC
}
 

Public Member Functions

rounding_modet rounding_mode () const
 
 ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode)
 
 ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode, const mp_integer &value)
 
 ieee_floatt (const floatbv_typet &type, rounding_modet __rounding_mode)
 
 ieee_floatt (const constant_exprt &expr, rounding_modet __rounding_mode)
 
 ieee_floatt (ieee_float_valuet __value, rounding_modet __rounding_mode)
 
void from_integer (const mp_integer &i)
 
void from_base10 (const mp_integer &exp, const mp_integer &frac)
 compute f * (10^e)
 
void build (const mp_integer &exp, const mp_integer &frac)
 
double to_double () const
 
float to_float () const
 
mp_integer to_integer () const
 
void change_spec (const ieee_float_spect &dest_spec)
 
ieee_floatt round_to_integral () const
 
ieee_floattoperator/= (const ieee_floatt &other)
 
ieee_floattoperator*= (const ieee_floatt &other)
 
ieee_floattoperator+= (const ieee_floatt &other)
 
ieee_floattoperator-= (const ieee_floatt &other)
 
- Public Member Functions inherited from ieee_float_valuet
 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_integerget_exponent () const
 
const mp_integerget_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 constant_exprt rounding_mode_expr (rounding_modet)
 
- Static Public Member Functions inherited from ieee_float_valuet
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)
 

Protected Member Functions

void divide_and_round (mp_integer &dividend, const mp_integer &divisor)
 
void align ()
 
- Protected Member Functions inherited from ieee_float_valuet
void next_representable (bool greater)
 Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false).
 

Protected Attributes

rounding_modet _rounding_mode
 
- Protected Attributes inherited from ieee_float_valuet
bool sign_flag
 
mp_integer exponent
 
mp_integer fraction
 
bool NaN_flag
 
bool infinity_flag
 

Additional Inherited Members

- Public Attributes inherited from ieee_float_valuet
ieee_float_spect spec
 
- Static Protected Member Functions inherited from ieee_float_valuet
static mp_integer base10_digits (const mp_integer &src)
 

Detailed Description

An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.

Definition at line 337 of file ieee_float.h.

Member Enumeration Documentation

◆ rounding_modet

Enumerator
ROUND_TO_EVEN 
ROUND_TO_MINUS_INF 
ROUND_TO_PLUS_INF 
ROUND_TO_ZERO 
ROUND_TO_AWAY 
UNKNOWN 
NONDETERMINISTIC 

Definition at line 346 of file ieee_float.h.

Constructor & Destructor Documentation

◆ ieee_floatt() [1/5]

ieee_floatt::ieee_floatt ( ieee_float_spect  __spec,
rounding_modet  __rounding_mode 
)
inline

Definition at line 365 of file ieee_float.h.

◆ ieee_floatt() [2/5]

ieee_floatt::ieee_floatt ( ieee_float_spect  __spec,
rounding_modet  __rounding_mode,
const mp_integer value 
)
inline

Definition at line 370 of file ieee_float.h.

◆ ieee_floatt() [3/5]

ieee_floatt::ieee_floatt ( const floatbv_typet type,
rounding_modet  __rounding_mode 
)
inline

Definition at line 379 of file ieee_float.h.

◆ ieee_floatt() [4/5]

ieee_floatt::ieee_floatt ( const constant_exprt expr,
rounding_modet  __rounding_mode 
)
inline

Definition at line 384 of file ieee_float.h.

◆ ieee_floatt() [5/5]

ieee_floatt::ieee_floatt ( ieee_float_valuet  __value,
rounding_modet  __rounding_mode 
)
inline

Definition at line 389 of file ieee_float.h.

Member Function Documentation

◆ align()

void ieee_floatt::align ( )
protected

Definition at line 821 of file ieee_float.cpp.

◆ build()

void ieee_floatt::build ( const mp_integer exp,
const mp_integer frac 
)

Definition at line 566 of file ieee_float.cpp.

◆ change_spec()

void ieee_floatt::change_spec ( const ieee_float_spect dest_spec)

Definition at line 1231 of file ieee_float.cpp.

◆ divide_and_round()

void ieee_floatt::divide_and_round ( mp_integer dividend,
const mp_integer divisor 
)
protected

Definition at line 954 of file ieee_float.cpp.

◆ from_base10()

void ieee_floatt::from_base10 ( const mp_integer exp,
const mp_integer frac 
)

compute f * (10^e)

Definition at line 784 of file ieee_float.cpp.

◆ from_integer()

void ieee_floatt::from_integer ( const mp_integer i)

Definition at line 813 of file ieee_float.cpp.

◆ operator*=()

ieee_floatt & ieee_floatt::operator*= ( const ieee_floatt other)

Definition at line 1097 of file ieee_float.cpp.

◆ operator+=()

ieee_floatt & ieee_floatt::operator+= ( const ieee_floatt other)

Definition at line 1133 of file ieee_float.cpp.

◆ operator-=()

ieee_floatt & ieee_floatt::operator-= ( const ieee_floatt other)

Definition at line 1224 of file ieee_float.cpp.

◆ operator/=()

ieee_floatt & ieee_floatt::operator/= ( const ieee_floatt other)

Definition at line 1023 of file ieee_float.cpp.

◆ round_to_integral()

ieee_floatt ieee_floatt::round_to_integral ( ) const

Definition at line 1371 of file ieee_float.cpp.

◆ rounding_mode()

rounding_modet ieee_floatt::rounding_mode ( ) const
inline

Definition at line 357 of file ieee_float.h.

◆ rounding_mode_expr()

constant_exprt ieee_floatt::rounding_mode_expr ( rounding_modet  rm)
static

Definition at line 561 of file ieee_float.cpp.

◆ to_double()

double ieee_floatt::to_double ( ) const

◆ to_float()

float ieee_floatt::to_float ( ) const

◆ to_integer()

mp_integer ieee_floatt::to_integer ( ) const

Definition at line 1256 of file ieee_float.cpp.

Member Data Documentation

◆ _rounding_mode

rounding_modet ieee_floatt::_rounding_mode
protected

Definition at line 419 of file ieee_float.h.


The documentation for this class was generated from the following files: