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

#include <ieee_float.h>

Inheritance diagram for ieee_float_valuet:

Collaboration diagram for ieee_float_valuet:

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

ieee_float_valuet ieee_float_valuet::fltmax ( const ieee_float_spect & _spec )

inlinestatic

Definition at line 217 of file ieee_float.h.

◆ fltmin()

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

ieee_float_valuet ieee_float_valuet::minus_infinity ( const ieee_float_spect & _spec )

inlinestatic

Definition at line 209 of file ieee_float.h.

◆ NaN()

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

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]

ieee_float_valuet ieee_float_valuet::zero ( const floatbv_typet & type )

inlinestatic

Definition at line 172 of file ieee_float.h.

◆ zero() [2/2]

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:

util/ieee_float.h
util/ieee_float.cpp

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ieee_float_valuet() [1/4]

◆ ieee_float_valuet() [2/4]

◆ ieee_float_valuet() [3/4]

◆ ieee_float_valuet() [4/4]

Member Function Documentation

◆ abs()

◆ base10_digits()

◆ decrement()

◆ extract_base10()

◆ extract_base2()

◆ fltmax()

◆ fltmin()

◆ format()

◆ from_double()

◆ from_expr()

◆ from_float()

◆ get_exponent()

◆ get_fraction()

◆ get_sign()

◆ ieee_equal()

◆ ieee_not_equal()

◆ increment()

◆ is_double()

◆ is_float()

◆ is_infinity()

◆ is_NaN()

◆ is_negative()

◆ is_normal()

◆ is_zero()

◆ make_fltmax()

◆ make_fltmin()

◆ make_minus_infinity()

◆ make_NaN()

◆ make_plus_infinity()

◆ make_zero()

◆ minus_infinity()

◆ NaN()

◆ negate()

◆ next_representable()

◆ one() [1/2]

◆ one() [2/2]

◆ operator!=()

◆ operator<()

◆ operator<=()

◆ operator==() [1/4]

◆ operator==() [2/4]

◆ operator==() [3/4]

◆ operator==() [4/4]

◆ operator>()

◆ operator>=()

◆ pack()

◆ plus_infinity()

◆ print()

◆ set_sign()

◆ to_ansi_c_string()

◆ to_double()

◆ to_expr()

◆ to_float()

◆ to_integer()

◆ to_string_decimal()

◆ to_string_scientific()

◆ unpack()

◆ zero() [1/2]

◆ zero() [2/2]

Member Data Documentation

◆ exponent

◆ fraction

◆ infinity_flag

◆ NaN_flag

◆ sign_flag

◆ spec