CBMC
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | Public Attributes | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
ieee_float_valuet Class Reference

An IEEE 754 floating-point value, including specificiation. More...

#include <ieee_float.h>

+ Inheritance diagram for ieee_float_valuet:
[フレーム]
[legend]
+ Collaboration diagram for ieee_float_valuet:
[フレーム]
[legend]

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
  Reinterpret this value as a native double.
 
float  to_float () const
  Reinterpret this value as a native float.
 
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
  Convert to an integer, always rounding towards zero (truncation), i.e.
 
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
 

Detailed Description

An IEEE 754 floating-point value, including specificiation.

Definition at line 116 of file ieee_float.h.

Constructor & Destructor Documentation

◆  ieee_float_valuet() [1/4]

ieee_float_valuet::ieee_float_valuet ( const ieee_float_spect &  _spec )
inlineexplicit

Definition at line 121 of file ieee_float.h.

◆  ieee_float_valuet() [2/4]

ieee_float_valuet::ieee_float_valuet ( const floatbv_typet &  type )
inlineexplicit

Definition at line 131 of file ieee_float.h.

◆  ieee_float_valuet() [3/4]

ieee_float_valuet::ieee_float_valuet ( const constant_exprt &  expr )
inlineexplicit

Definition at line 141 of file ieee_float.h.

◆  ieee_float_valuet() [4/4]

ieee_float_valuet::ieee_float_valuet ( )
inline

Definition at line 146 of file ieee_float.h.

Member Function Documentation

◆  abs()

ieee_float_valuet ieee_float_valuet::abs ( ) const

Definition at line 60 of file ieee_float.cpp.

◆  base10_digits()

mp_integer ieee_float_valuet::base10_digits ( const mp_integer &  src )
staticprotected

Definition at line 132 of file ieee_float.cpp.

◆  decrement()

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

Definition at line 242 of file ieee_float.h.

◆  extract_base10()

void ieee_float_valuet::extract_base10 ( mp_integer &  _exponent,
mp_integer &  _fraction 
) const

Definition at line 439 of file ieee_float.cpp.

◆  extract_base2()

void ieee_float_valuet::extract_base2 ( mp_integer &  _exponent,
mp_integer &  _fraction 
) const

Definition at line 415 of file ieee_float.cpp.

◆  fltmax()

static ieee_float_valuet ieee_float_valuet::fltmax ( const ieee_float_spect &  _spec )
inlinestatic

Definition at line 217 of file ieee_float.h.

◆  fltmin()

static ieee_float_valuet ieee_float_valuet::fltmin ( const ieee_float_spect &  _spec )
inlinestatic

Definition at line 225 of file ieee_float.h.

◆  format()

std::string ieee_float_valuet::format ( const format_spect &  format_spec ) const

Definition at line 72 of file ieee_float.cpp.

◆  from_double()

void ieee_float_valuet::from_double ( double  d )

Definition at line 1277 of file ieee_float.cpp.

◆  from_expr()

void ieee_float_valuet::from_expr ( const constant_exprt &  expr )

Definition at line 1250 of file ieee_float.cpp.

◆  from_float()

void ieee_float_valuet::from_float ( float  f )

Definition at line 1301 of file ieee_float.cpp.

◆  get_exponent()

const mp_integer & ieee_float_valuet::get_exponent ( ) const
inline

Definition at line 263 of file ieee_float.h.

◆  get_fraction()

const mp_integer & ieee_float_valuet::get_fraction ( ) const
inline

Definition at line 264 of file ieee_float.h.

◆  get_sign()

bool ieee_float_valuet::get_sign ( ) const
inline

Definition at line 254 of file ieee_float.h.

◆  ieee_equal()

bool ieee_float_valuet::ieee_equal ( const ieee_float_valuet &  other ) const

Definition at line 686 of file ieee_float.cpp.

◆  ieee_not_equal()

bool ieee_float_valuet::ieee_not_equal ( const ieee_float_valuet &  other ) const

Definition at line 725 of file ieee_float.cpp.

◆  increment()

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

Definition at line 233 of file ieee_float.h.

◆  is_double()

bool ieee_float_valuet::is_double ( ) const
Returns
true iff this value is in IEEE 754 double (binary64) format

Definition at line 1361 of file ieee_float.cpp.

◆  is_float()

bool ieee_float_valuet::is_float ( ) const
Returns
true iff this value is in IEEE 754 single (binary32) format

Definition at line 1366 of file ieee_float.cpp.

◆  is_infinity()

bool ieee_float_valuet::is_infinity ( ) const
inline

Definition at line 260 of file ieee_float.h.

◆  is_NaN()

bool ieee_float_valuet::is_NaN ( ) const
inline

Definition at line 259 of file ieee_float.h.

◆  is_negative()

bool ieee_float_valuet::is_negative ( ) const
inline

Definition at line 255 of file ieee_float.h.

◆  is_normal()

bool ieee_float_valuet::is_normal ( ) const

Definition at line 372 of file ieee_float.cpp.

◆  is_zero()

bool ieee_float_valuet::is_zero ( ) const
inline

Definition at line 250 of file ieee_float.h.

◆  make_fltmax()

void ieee_float_valuet::make_fltmax ( )

Definition at line 1334 of file ieee_float.cpp.

◆  make_fltmin()

void ieee_float_valuet::make_fltmin ( )

Definition at line 1341 of file ieee_float.cpp.

◆  make_minus_infinity()

void ieee_float_valuet::make_minus_infinity ( )

Definition at line 1355 of file ieee_float.cpp.

◆  make_NaN()

void ieee_float_valuet::make_NaN ( )

Definition at line 1325 of file ieee_float.cpp.

◆  make_plus_infinity()

void ieee_float_valuet::make_plus_infinity ( )

Definition at line 1346 of file ieee_float.cpp.

◆  make_zero()

void ieee_float_valuet::make_zero ( )
inline

Definition at line 163 of file ieee_float.h.

◆  minus_infinity()

static ieee_float_valuet ieee_float_valuet::minus_infinity ( const ieee_float_spect &  _spec )
inlinestatic

Definition at line 209 of file ieee_float.h.

◆  NaN()

static ieee_float_valuet ieee_float_valuet::NaN ( const ieee_float_spect &  _spec )
inlinestatic

Definition at line 195 of file ieee_float.h.

◆  negate()

void ieee_float_valuet::negate ( )
inline

Definition at line 155 of file ieee_float.h.

◆  next_representable()

void ieee_float_valuet::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 739 of file ieee_float.cpp.

◆  one() [1/2]

ieee_float_valuet ieee_float_valuet::one ( const floatbv_typet &  type )
static

Definition at line 483 of file ieee_float.cpp.

◆  one() [2/2]

ieee_float_valuet ieee_float_valuet::one ( const ieee_float_spect &  spec )
static

Definition at line 475 of file ieee_float.cpp.

◆  operator!=()

bool ieee_float_valuet::operator!= ( const ieee_float_valuet &  other ) const

Definition at line 720 of file ieee_float.cpp.

◆  operator<()

bool ieee_float_valuet::operator< ( const ieee_float_valuet &  other ) const

Definition at line 584 of file ieee_float.cpp.

◆  operator<=()

bool ieee_float_valuet::operator<= ( const ieee_float_valuet &  other ) const

Definition at line 632 of file ieee_float.cpp.

◆  operator==() [1/4]

bool ieee_float_valuet::operator== ( const ieee_float_valuet &  other ) const

Definition at line 665 of file ieee_float.cpp.

◆  operator==() [2/4]

bool ieee_float_valuet::operator== ( double  d ) const

Definition at line 706 of file ieee_float.cpp.

◆  operator==() [3/4]

bool ieee_float_valuet::operator== ( float  f ) const

Definition at line 713 of file ieee_float.cpp.

◆  operator==() [4/4]

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

Definition at line 698 of file ieee_float.cpp.

◆  operator>()

bool ieee_float_valuet::operator> ( const ieee_float_valuet &  other ) const

Definition at line 655 of file ieee_float.cpp.

◆  operator>=()

bool ieee_float_valuet::operator>= ( const ieee_float_valuet &  other ) const

Definition at line 660 of file ieee_float.cpp.

◆  pack()

mp_integer ieee_float_valuet::pack ( ) const

Definition at line 377 of file ieee_float.cpp.

◆  plus_infinity()

static ieee_float_valuet ieee_float_valuet::plus_infinity ( const ieee_float_spect &  _spec )
inlinestatic

Definition at line 202 of file ieee_float.h.

◆  print()

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

Definition at line 67 of file ieee_float.cpp.

◆  set_sign()

void ieee_float_valuet::set_sign ( bool  _sign )
inline

Definition at line 160 of file ieee_float.h.

◆  to_ansi_c_string()

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

Definition at line 316 of file ieee_float.h.

◆  to_double()

double ieee_float_valuet::to_double ( ) const

Reinterpret this value as a native double.

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

This is a bit-exact reinterpretation of the packed IEEE 754 representation, not a rounding conversion, and therefore does not depend on any rounding mode.

Precondition
the value is in IEEE 754 double (binary64) format, i.e. is_double returns true.
Returns
the corresponding double

Definition at line 490 of file ieee_float.cpp.

◆  to_expr()

constant_exprt ieee_float_valuet::to_expr ( ) const

Definition at line 579 of file ieee_float.cpp.

◆  to_float()

float ieee_float_valuet::to_float ( ) const

Reinterpret this value as a native float.

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

This is a bit-exact reinterpretation of the packed IEEE 754 representation, not a rounding conversion, and therefore does not depend on any rounding mode.

Note
from_float() followed by to_float() may return a different bit pattern for NaN.
Precondition
the value is in IEEE 754 single (binary32) format, i.e. is_float returns true.
Returns
the corresponding float

Definition at line 525 of file ieee_float.cpp.

◆  to_integer()

mp_integer ieee_float_valuet::to_integer ( ) const

Convert to an integer, always rounding towards zero (truncation), i.e.

modelling a C cast such as (int)f. NaN, infinities and zero map to 0.

Because the rounding is fixed (truncation), this conversion does not depend on any rounding mode and so belongs on ieee_float_valuet rather than ieee_floatt. A rounding-mode-respecting float-to-integer conversion (the analogue of lrint) would instead belong on ieee_floatt; see also ieee_floatt::round_to_integral, which rounds to an integral floating-point value according to the configured rounding mode.

Returns
the truncated integer value

Definition at line 1256 of file ieee_float.cpp.

◆  to_string_decimal()

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

Definition at line 141 of file ieee_float.cpp.

◆  to_string_scientific()

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.

◆  unpack()

void ieee_float_valuet::unpack ( const mp_integer &  i )

Definition at line 322 of file ieee_float.cpp.

◆  zero() [1/2]

static ieee_float_valuet ieee_float_valuet::zero ( const floatbv_typet &  type )
inlinestatic

Definition at line 172 of file ieee_float.h.

◆  zero() [2/2]

static ieee_float_valuet ieee_float_valuet::zero ( const ieee_float_spect &  spec )
inlinestatic

Definition at line 179 of file ieee_float.h.

Member Data Documentation

◆  exponent

mp_integer ieee_float_valuet::exponent
protected

Definition at line 351 of file ieee_float.h.

◆  fraction

mp_integer ieee_float_valuet::fraction
protected

Definition at line 352 of file ieee_float.h.

◆  infinity_flag

bool ieee_float_valuet::infinity_flag
protected

Definition at line 353 of file ieee_float.h.

◆  NaN_flag

bool ieee_float_valuet::NaN_flag
protected

Definition at line 353 of file ieee_float.h.

◆  sign_flag

bool ieee_float_valuet::sign_flag
protected

Definition at line 350 of file ieee_float.h.

◆  spec

ieee_float_spect ieee_float_valuet::spec

Definition at line 119 of file ieee_float.h.

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

AltStyle によって変換されたページ (->オリジナル) /