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 119 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 125 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 136 of file ieee_float.h.

◆ ieee_floatt() [2/4]

ieee_floatt::ieee_floatt ( const floatbv_typet type)
inlineexplicit

Definition at line 143 of file ieee_float.h.

◆ ieee_floatt() [3/4]

ieee_floatt::ieee_floatt ( )
inline

Definition at line 154 of file ieee_float.h.

◆ ieee_floatt() [4/4]

ieee_floatt::ieee_floatt ( const constant_exprt expr)
inlineexplicit

Definition at line 161 of file ieee_float.h.

References from_expr().

Member Function Documentation

◆ align()

◆ base10_digits()

mp_integer ieee_floatt::base10_digits ( const mp_integer src)
staticprotected

Definition at line 123 of file ieee_float.cpp.

Referenced by format(), and to_string_scientific().

◆ build()

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

◆ change_spec()

◆ decrement()

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

Definition at line 224 of file ieee_float.h.

References get_sign(), is_zero(), negate(), and next_representable().

Referenced by interval_domaint::assume_rec().

◆ divide_and_round()

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

◆ extract_base10()

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

Definition at line 429 of file ieee_float.cpp.

References exponent, ieee_float_spect::f, fraction, is_infinity(), is_NaN(), is_zero(), power(), and spec.

Referenced by format(), and to_string_scientific().

◆ extract_base2()

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

Definition at line 405 of file ieee_float.cpp.

References exponent, ieee_float_spect::f, fraction, is_infinity(), is_NaN(), is_zero(), and spec.

Referenced by to_string_decimal().

◆ fltmax()

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

Definition at line 207 of file ieee_float.h.

References make_fltmax().

◆ fltmin()

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

Definition at line 211 of file ieee_float.h.

References make_fltmin().

◆ format()

◆ 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 align(), ieee_float_spect::e, exponent, ieee_float_spect::f, fraction, infinity_flag, NaN_flag, power(), sign_flag, and spec.

Referenced by convert_float_literal().

◆ from_double()

void ieee_floatt::from_double ( const double  d)

◆ from_expr()

◆ from_float()

void ieee_floatt::from_float ( const float  f)

◆ from_integer()

◆ get_exponent()

const mp_integer& ieee_floatt::get_exponent ( ) const
inline

Definition at line 241 of file ieee_float.h.

References exponent.

Referenced by float_utilst::build_constant().

◆ get_fraction()

const mp_integer& ieee_floatt::get_fraction ( ) const
inline

Definition at line 242 of file ieee_float.h.

References fraction.

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 215 of file ieee_float.h.

References get_sign(), is_zero(), negate(), and next_representable().

Referenced by interval_domaint::assume_rec().

◆ is_double()

bool ieee_floatt::is_double ( ) const

Definition at line 1153 of file ieee_float.cpp.

References ieee_float_spect::e, ieee_float_spect::f, and spec.

Referenced by expr2javat::convert_constant().

◆ is_float()

bool ieee_floatt::is_float ( ) const

Definition at line 1158 of file ieee_float.cpp.

References ieee_float_spect::e, ieee_float_spect::f, and spec.

◆ is_infinity()

◆ is_NaN()

◆ is_normal()

bool ieee_floatt::is_normal ( ) const

Definition at line 362 of file ieee_float.cpp.

References ieee_float_spect::f, fraction, power(), and spec.

Referenced by pack(), and simplify_exprt::simplify_isnormal().

◆ is_zero()

◆ make_fltmax()

void ieee_floatt::make_fltmax ( )

Definition at line 1126 of file ieee_float.cpp.

References ieee_float_spect::e, ieee_float_spect::f, power(), spec, and unpack().

Referenced by align(), fltmax(), and next_representable().

◆ make_fltmin()

void ieee_floatt::make_fltmin ( )

Definition at line 1133 of file ieee_float.cpp.

References ieee_float_spect::f, power(), spec, and unpack().

Referenced by fltmin().

◆ make_minus_infinity()

void ieee_floatt::make_minus_infinity ( )

Definition at line 1147 of file ieee_float.cpp.

References make_plus_infinity(), and sign_flag.

Referenced by minus_infinity().

◆ make_NaN()

void ieee_floatt::make_NaN ( )

Definition at line 1117 of file ieee_float.cpp.

References exponent, fraction, infinity_flag, and NaN_flag.

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

◆ make_plus_infinity()

void ieee_floatt::make_plus_infinity ( )

Definition at line 1138 of file ieee_float.cpp.

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

Referenced by make_minus_infinity(), and plus_infinity().

◆ make_zero()

void ieee_floatt::make_zero ( )
inline

Definition at line 175 of file ieee_float.h.

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

Referenced by operator/=(), and zero().

◆ minus_infinity()

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

Definition at line 203 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

Definition at line 197 of file ieee_float.h.

References make_NaN().

Referenced by smt2_convt::parse_literal().

◆ negate()

void ieee_floatt::negate ( )
inline

Definition at line 167 of file ieee_float.h.

References sign_flag.

Referenced by decrement(), increment(), operator*=(), operator/=(), 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.

References get_sign(), is_infinity(), is_NaN(), is_zero(), make_fltmax(), pack(), set_sign(), and unpack().

Referenced by decrement(), and increment().

◆ 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)

◆ 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(), and spec.

◆ 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.

References to_ansi_c_string().

◆ set_sign()

void ieee_floatt::set_sign ( bool  _sign)
inline

Definition at line 172 of file ieee_float.h.

References sign_flag.

Referenced by next_representable(), operator+=(), and simplify_exprt::simplify_abs().

◆ to_ansi_c_string()

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

Definition at line 269 of file ieee_float.h.

References format().

Referenced by expr2ct::convert_constant(), operator<<(), print(), and xml().

◆ 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 infinity_flag, NaN_flag, pack(), and sign_flag.

Referenced by expr2javat::convert_constant().

◆ 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 infinity_flag, NaN_flag, pack(), and sign_flag.

Referenced by expr2javat::convert_constant().

◆ to_integer()

◆ to_string_decimal()

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

◆ 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 base10_digits(), extract_base10(), infinity_flag, integer2string(), is_zero(), NaN_flag, power(), and sign_flag.

Referenced by format().

◆ unpack()

◆ zero()

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

Definition at line 184 of file ieee_float.h.

References make_zero().

Referenced by c_typecheck_baset::do_special_functions().

Member Data Documentation

◆ exponent

◆ fraction

◆ infinity_flag

◆ NaN_flag

◆ rounding_mode

◆ sign_flag

◆ spec


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