cprover
ieee_floatt Class Reference

#include <ieee_float.h>

Collaboration diagram for ieee_floatt:
[legend]

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_integerget_exponent () const
 
const mp_integerget_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_floattoperator/= (const ieee_floatt &other)
 
ieee_floattoperator*= (const ieee_floatt &other)
 
ieee_floattoperator+= (const ieee_floatt &other)
 
ieee_floattoperator-= (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 &fraction, const mp_integer &factor)
 
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
 

Detailed Description

Definition at line 108 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 
UNKNOWN 
NONDETERMINISTIC 

Definition at line 114 of file ieee_float.h.

Constructor & Destructor Documentation

§ ieee_floatt() [1/4]

ieee_floatt::ieee_floatt ( const ieee_float_spect _spec)
inlineexplicit

Definition at line 125 of file ieee_float.h.

§ ieee_floatt() [2/4]

ieee_floatt::ieee_floatt ( const floatbv_typet type)
inlineexplicit

Definition at line 132 of file ieee_float.h.

§ ieee_floatt() [3/4]

ieee_floatt::ieee_floatt ( )
inline

Definition at line 143 of file ieee_float.h.

§ ieee_floatt() [4/4]

ieee_floatt::ieee_floatt ( const constant_exprt expr)
inlineexplicit

Definition at line 150 of file ieee_float.h.

References from_expr().

Member Function Documentation

§ align()

void ieee_floatt::align ( )
protected

Definition at line 516 of file ieee_float.cpp.

References power().

§ base10_digits()

mp_integer ieee_floatt::base10_digits ( const mp_integer src)
staticprotected

Definition at line 123 of file ieee_float.cpp.

§ build()

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

Definition at line 465 of file ieee_float.cpp.

Referenced by convert_float_literal(), and smt2_convt::convert_typecast().

§ change_spec()

void ieee_floatt::change_spec ( const ieee_float_spect dest_spec)

§ decrement()

void ieee_floatt::decrement ( bool  distinguish_zero = false)
inline

Definition at line 213 of file ieee_float.h.

Referenced by interval_domaint::assume_rec().

§ divide_and_round()

void ieee_floatt::divide_and_round ( mp_integer fraction,
const mp_integer factor 
)
protected

Definition at line 636 of file ieee_float.cpp.

§ extract_base10()

void ieee_floatt::extract_base10 ( mp_integer _exponent,
mp_integer _fraction 
) const

Definition at line 429 of file ieee_float.cpp.

References power().

§ extract_base2()

void ieee_floatt::extract_base2 ( mp_integer _exponent,
mp_integer _fraction 
) const

Definition at line 405 of file ieee_float.cpp.

§ fltmax()

static ieee_floatt ieee_floatt::fltmax ( const ieee_float_spect _spec)
inlinestatic

Definition at line 196 of file ieee_float.h.

References make_fltmax().

§ fltmin()

static ieee_floatt ieee_floatt::fltmin ( const ieee_float_spect _spec)
inlinestatic

Definition at line 200 of file ieee_float.h.

References make_fltmin().

§ format()

std::string ieee_floatt::format ( const format_spect format_spec) const

§ from_base10()

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

compute f * (10^e)

Definition at line 479 of file ieee_float.cpp.

References power().

Referenced by convert_float_literal().

§ from_double()

void ieee_floatt::from_double ( const double  d)

Definition at line 1078 of file ieee_float.cpp.

§ from_expr()

§ from_float()

void ieee_floatt::from_float ( const float  f)

Definition at line 1098 of file ieee_float.cpp.

References ieee_float_spect::f.

§ from_integer()

§ get_exponent()

const mp_integer& ieee_floatt::get_exponent ( ) const
inline

Definition at line 230 of file ieee_float.h.

Referenced by float_utilst::build_constant().

§ get_fraction()

const mp_integer& ieee_floatt::get_fraction ( ) const
inline

Definition at line 231 of file ieee_float.h.

References ieee_float_spect::f, from_integer(), and to_integer().

Referenced by float_utilst::build_constant().

§ get_sign()

bool ieee_floatt::get_sign ( ) const
inline

§ ieee_equal()

bool ieee_floatt::ieee_equal ( const ieee_floatt other) const

Definition at line 1000 of file ieee_float.cpp.

References is_zero(), NaN_flag, and spec.

Referenced by simplify_exprt::simplify_ieee_float_relation().

§ ieee_not_equal()

bool ieee_floatt::ieee_not_equal ( const ieee_floatt other) const

Definition at line 1022 of file ieee_float.cpp.

References is_zero(), NaN_flag, and spec.

Referenced by simplify_exprt::simplify_ieee_float_relation().

§ increment()

void ieee_floatt::increment ( bool  distinguish_zero = false)
inline

Definition at line 204 of file ieee_float.h.

Referenced by interval_domaint::assume_rec().

§ is_double()

bool ieee_floatt::is_double ( ) const

Definition at line 1153 of file ieee_float.cpp.

§ is_float()

bool ieee_floatt::is_float ( ) const

Definition at line 1158 of file ieee_float.cpp.

§ is_infinity()

bool ieee_floatt::is_infinity ( ) const
inline

§ is_NaN()

bool ieee_floatt::is_NaN ( ) const
inline

§ is_normal()

bool ieee_floatt::is_normal ( ) const

Definition at line 362 of file ieee_float.cpp.

References power().

Referenced by simplify_exprt::simplify_isnormal().

§ is_zero()

bool ieee_floatt::is_zero ( ) const
inline

§ make_fltmax()

void ieee_floatt::make_fltmax ( )

Definition at line 1126 of file ieee_float.cpp.

References power().

Referenced by fltmax().

§ make_fltmin()

void ieee_floatt::make_fltmin ( )

Definition at line 1133 of file ieee_float.cpp.

References power().

Referenced by fltmin().

§ make_minus_infinity()

void ieee_floatt::make_minus_infinity ( )

Definition at line 1147 of file ieee_float.cpp.

Referenced by minus_infinity().

§ make_NaN()

void ieee_floatt::make_NaN ( )

Definition at line 1117 of file ieee_float.cpp.

Referenced by NaN().

§ make_plus_infinity()

void ieee_floatt::make_plus_infinity ( )

Definition at line 1138 of file ieee_float.cpp.

Referenced by plus_infinity().

§ make_zero()

void ieee_floatt::make_zero ( )
inline

Definition at line 164 of file ieee_float.h.

Referenced by zero().

§ minus_infinity()

static ieee_floatt ieee_floatt::minus_infinity ( const ieee_float_spect _spec)
inlinestatic

Definition at line 192 of file ieee_float.h.

References make_minus_infinity().

Referenced by goto_checkt::nan_check(), and smt2_convt::parse_literal().

§ NaN()

static ieee_floatt ieee_floatt::NaN ( const ieee_float_spect _spec)
inlinestatic

§ negate()

void ieee_floatt::negate ( )
inline

Definition at line 156 of file ieee_float.h.

Referenced by exprt::negate(), and simplify_exprt::simplify_unary_minus().

§ next_representable()

void ieee_floatt::next_representable ( bool  greater)
protected

Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false).

Definition at line 1228 of file ieee_float.cpp.

§ operator!=()

bool ieee_floatt::operator!= ( const ieee_floatt other) const

Definition at line 1017 of file ieee_float.cpp.

§ operator*=()

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

§ operator+=()

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

Definition at line 803 of file ieee_float.cpp.

References exponent, fraction, get_sign(), infinity_flag, is_zero(), NaN_flag, power(), sign_flag, and spec.

§ operator-=()

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

Definition at line 892 of file ieee_float.cpp.

References sign_flag.

§ operator/=()

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

§ operator<()

bool ieee_floatt::operator< ( const ieee_floatt other) const

Definition at line 899 of file ieee_float.cpp.

References exponent, fraction, infinity_flag, is_zero(), NaN_flag, and sign_flag.

§ operator<=()

bool ieee_floatt::operator<= ( const ieee_floatt other) const

Definition at line 945 of file ieee_float.cpp.

References exponent, fraction, infinity_flag, is_zero(), NaN_flag, and sign_flag.

§ operator==() [1/2]

bool ieee_floatt::operator== ( const ieee_floatt other) const

Definition at line 978 of file ieee_float.cpp.

References exponent, fraction, infinity_flag, NaN_flag, and sign_flag.

§ operator==() [2/2]

bool ieee_floatt::operator== ( int  i) const

Definition at line 1010 of file ieee_float.cpp.

References from_integer().

§ operator>()

bool ieee_floatt::operator> ( const ieee_floatt other) const

Definition at line 968 of file ieee_float.cpp.

§ operator>=()

bool ieee_floatt::operator>= ( const ieee_floatt other) const

Definition at line 973 of file ieee_float.cpp.

§ pack()

§ plus_infinity()

static ieee_floatt ieee_floatt::plus_infinity ( const ieee_float_spect _spec)
inlinestatic

§ print()

void ieee_floatt::print ( std::ostream &  out) const

Definition at line 58 of file ieee_float.cpp.

§ set_sign()

void ieee_floatt::set_sign ( bool  _sign)
inline

§ to_ansi_c_string()

std::string ieee_floatt::to_ansi_c_string ( ) const
inline

§ to_double()

double ieee_floatt::to_double ( ) const

Note that calling from_double -> to_double can return different bit patterns for NaN.

Definition at line 1165 of file ieee_float.cpp.

References ieee_float_spect::f.

§ to_expr()

§ to_float()

float ieee_floatt::to_float ( ) const

Note that calling from_float -> to_float can return different bit patterns for NaN.

Definition at line 1194 of file ieee_float.cpp.

References ieee_float_spect::f.

§ to_integer()

mp_integer ieee_floatt::to_integer ( ) const

§ to_string_decimal()

std::string ieee_floatt::to_string_decimal ( std::size_t  precision) const

Definition at line 132 of file ieee_float.cpp.

References dot(), integer2size_t(), integer2string(), power(), and r.

§ to_string_scientific()

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 225 of file ieee_float.cpp.

References integer2string(), and power().

§ unpack()

void ieee_floatt::unpack ( const mp_integer i)

§ zero()

static ieee_floatt ieee_floatt::zero ( const floatbv_typet type)
inlinestatic

Definition at line 173 of file ieee_float.h.

References make_zero().

Member Data Documentation

§ exponent

mp_integer ieee_floatt::exponent
protected

Definition at line 299 of file ieee_float.h.

Referenced by operator*=(), operator+=(), operator/=(), operator<(), operator<=(), and operator==().

§ fraction

mp_integer ieee_floatt::fraction
protected

Definition at line 300 of file ieee_float.h.

Referenced by operator*=(), operator+=(), operator/=(), operator<(), operator<=(), and operator==().

§ infinity_flag

bool ieee_floatt::infinity_flag
protected

Definition at line 301 of file ieee_float.h.

Referenced by operator*=(), operator+=(), operator/=(), operator<(), operator<=(), and operator==().

§ NaN_flag

bool ieee_floatt::NaN_flag
protected

§ rounding_mode

§ sign_flag

bool ieee_floatt::sign_flag
protected

§ spec


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