#include <ieee_float.h>

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, UNKNOWN, NONDETERMINISTIC }

Public Member Functions
	ieee_floatt (const ieee_float_spect &_spec)

	ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode)

	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_integer &	get_exponent () const

const mp_integer &	get_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_floatt &	operator/= (const ieee_floatt &other)

ieee_floatt &	operator*= (const ieee_floatt &other)

ieee_floatt &	operator+= (const ieee_floatt &other)

ieee_floatt &	operator-= (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 constant_exprt	rounding_mode_expr (rounding_modet)

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 &dividend, const mp_integer &divisor)

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

Member Enumeration Documentation

◆ rounding_modet

enum ieee_floatt::rounding_modet

Enumerator
ROUND_TO_EVEN
ROUND_TO_MINUS_INF
ROUND_TO_PLUS_INF
ROUND_TO_ZERO
UNKNOWN
NONDETERMINISTIC

Definition at line 123 of file ieee_float.h.

Constructor & Destructor Documentation

◆ ieee_floatt() [1/5]

ieee_floatt::ieee_floatt ( const ieee_float_spect & _spec )

inlineexplicit

Definition at line 137 of file ieee_float.h.

◆ ieee_floatt() [2/5]

ieee_floatt::ieee_floatt	(	ieee_float_spect	__spec,
		rounding_modet	__rounding_mode
	)

inlineexplicit

Definition at line 144 of file ieee_float.h.

◆ ieee_floatt() [3/5]

ieee_floatt::ieee_floatt ( const floatbv_typet & type )

inlineexplicit

Definition at line 155 of file ieee_float.h.

◆ ieee_floatt() [4/5]

ieee_floatt::ieee_floatt ( )

inline

Definition at line 166 of file ieee_float.h.

◆ ieee_floatt() [5/5]

ieee_floatt::ieee_floatt ( const constant_exprt & expr )

inlineexplicit

Definition at line 173 of file ieee_float.h.

Member Function Documentation

◆ align()

void ieee_floatt::align ( )

protected

Definition at line 523 of file ieee_float.cpp.

◆ base10_digits()

mp_integer ieee_floatt::base10_digits ( const mp_integer & src )

staticprotected

Definition at line 129 of file ieee_float.cpp.

◆ build()

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

Definition at line 472 of file ieee_float.cpp.

◆ change_spec()

void ieee_floatt::change_spec ( const ieee_float_spect & dest_spec )

Definition at line 1048 of file ieee_float.cpp.

◆ decrement()

void ieee_floatt::decrement ( bool distinguish_zero = false )

inline

Definition at line 236 of file ieee_float.h.

◆ divide_and_round()

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

protected

Definition at line 651 of file ieee_float.cpp.

◆ extract_base10()

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

Definition at line 436 of file ieee_float.cpp.

◆ extract_base2()

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

Definition at line 412 of file ieee_float.cpp.

◆ fltmax()

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

inlinestatic

Definition at line 219 of file ieee_float.h.

◆ fltmin()

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

inlinestatic

Definition at line 223 of file ieee_float.h.

◆ format()

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

Definition at line 69 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 486 of file ieee_float.cpp.

◆ from_double()

void ieee_floatt::from_double ( const double d )

Definition at line 1094 of file ieee_float.cpp.

◆ from_expr()

void ieee_floatt::from_expr ( const constant_exprt & expr )

Definition at line 1067 of file ieee_float.cpp.

◆ from_float()

void ieee_floatt::from_float ( const float f )

Definition at line 1118 of file ieee_float.cpp.

◆ from_integer()

void ieee_floatt::from_integer ( const mp_integer & i )

Definition at line 515 of file ieee_float.cpp.

◆ get_exponent()

const mp_integer& ieee_floatt::get_exponent ( ) const

inline

Definition at line 253 of file ieee_float.h.

◆ get_fraction()

const mp_integer& ieee_floatt::get_fraction ( ) const

inline

Definition at line 254 of file ieee_float.h.

◆ get_sign()

bool ieee_floatt::get_sign ( ) const

inline

Definition at line 248 of file ieee_float.h.

◆ ieee_equal()

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

Definition at line 1016 of file ieee_float.cpp.

◆ ieee_not_equal()

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

Definition at line 1038 of file ieee_float.cpp.

◆ increment()

void ieee_floatt::increment ( bool distinguish_zero = false )

inline

Definition at line 227 of file ieee_float.h.

◆ is_double()

bool ieee_floatt::is_double ( ) const

Definition at line 1178 of file ieee_float.cpp.

◆ is_float()

bool ieee_floatt::is_float ( ) const

Definition at line 1183 of file ieee_float.cpp.

◆ is_infinity()

bool ieee_floatt::is_infinity ( ) const

inline

Definition at line 250 of file ieee_float.h.

◆ is_NaN()

bool ieee_floatt::is_NaN ( ) const

inline

Definition at line 249 of file ieee_float.h.

◆ is_normal()

bool ieee_floatt::is_normal ( ) const

Definition at line 369 of file ieee_float.cpp.

◆ is_zero()

bool ieee_floatt::is_zero ( ) const

inline

Definition at line 244 of file ieee_float.h.

◆ make_fltmax()

void ieee_floatt::make_fltmax ( )

Definition at line 1151 of file ieee_float.cpp.

◆ make_fltmin()

void ieee_floatt::make_fltmin ( )

Definition at line 1158 of file ieee_float.cpp.

◆ make_minus_infinity()

void ieee_floatt::make_minus_infinity ( )

Definition at line 1172 of file ieee_float.cpp.

◆ make_NaN()

void ieee_floatt::make_NaN ( )

Definition at line 1142 of file ieee_float.cpp.

◆ make_plus_infinity()

void ieee_floatt::make_plus_infinity ( )

Definition at line 1163 of file ieee_float.cpp.

◆ make_zero()

void ieee_floatt::make_zero ( )

inline

Definition at line 187 of file ieee_float.h.

◆ minus_infinity()

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

inlinestatic

Definition at line 215 of file ieee_float.h.

◆ NaN()

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

inlinestatic

Definition at line 209 of file ieee_float.h.

◆ negate()

void ieee_floatt::negate ( )

inline

Definition at line 179 of file ieee_float.h.

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

◆ operator!=()

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

Definition at line 1033 of file ieee_float.cpp.

◆ operator*=()

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

Definition at line 781 of file ieee_float.cpp.

◆ operator+=()

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

Definition at line 817 of file ieee_float.cpp.

◆ operator-=()

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

Definition at line 908 of file ieee_float.cpp.

◆ operator/=()

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

Definition at line 707 of file ieee_float.cpp.

◆ operator<()

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

Definition at line 915 of file ieee_float.cpp.

◆ operator<=()

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

Definition at line 961 of file ieee_float.cpp.

◆ operator==() [1/2]

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

Definition at line 994 of file ieee_float.cpp.

◆ operator==() [2/2]

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

Definition at line 1026 of file ieee_float.cpp.

◆ operator>()

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

Definition at line 984 of file ieee_float.cpp.

◆ operator>=()

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

Definition at line 989 of file ieee_float.cpp.

◆ pack()

mp_integer ieee_floatt::pack ( ) const

Definition at line 374 of file ieee_float.cpp.

◆ plus_infinity()

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

inlinestatic

Definition at line 212 of file ieee_float.h.

◆ print()

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

Definition at line 64 of file ieee_float.cpp.

◆ rounding_mode_expr()

constant_exprt ieee_floatt::rounding_mode_expr ( rounding_modet rm )

static

Definition at line 59 of file ieee_float.cpp.

◆ set_sign()

void ieee_floatt::set_sign ( bool _sign )

inline

Definition at line 184 of file ieee_float.h.

◆ to_ansi_c_string()

std::string ieee_floatt::to_ansi_c_string ( ) const

inline

Definition at line 281 of file ieee_float.h.

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

◆ to_expr()

constant_exprt ieee_floatt::to_expr ( ) const

Definition at line 702 of file ieee_float.cpp.

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

◆ to_integer()

mp_integer ieee_floatt::to_integer ( ) const

Definition at line 1073 of file ieee_float.cpp.

◆ to_string_decimal()

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

Definition at line 138 of file ieee_float.cpp.

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

◆ unpack()

void ieee_floatt::unpack ( const mp_integer & i )

Definition at line 319 of file ieee_float.cpp.

◆ zero()

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

inlinestatic

Definition at line 196 of file ieee_float.h.

Member Data Documentation

◆ exponent

mp_integer ieee_floatt::exponent

protected

Definition at line 322 of file ieee_float.h.

◆ fraction

mp_integer ieee_floatt::fraction

protected

Definition at line 323 of file ieee_float.h.

◆ infinity_flag

bool ieee_floatt::infinity_flag

protected

Definition at line 324 of file ieee_float.h.

◆ NaN_flag

bool ieee_floatt::NaN_flag

protected

Definition at line 324 of file ieee_float.h.

◆ rounding_mode

rounding_modet ieee_floatt::rounding_mode

Definition at line 133 of file ieee_float.h.

◆ sign_flag

bool ieee_floatt::sign_flag

protected

Definition at line 321 of file ieee_float.h.

◆ spec

ieee_float_spect ieee_floatt::spec

Definition at line 135 of file ieee_float.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/ieee_float.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/ieee_float.cpp

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ rounding_modet

Constructor & Destructor Documentation

◆ ieee_floatt() [1/5]

◆ ieee_floatt() [2/5]

◆ ieee_floatt() [3/5]

◆ ieee_floatt() [4/5]

◆ ieee_floatt() [5/5]

Member Function Documentation

◆ align()

◆ base10_digits()

◆ build()

◆ change_spec()

◆ decrement()

◆ divide_and_round()

◆ extract_base10()

◆ extract_base2()

◆ fltmax()

◆ fltmin()

◆ format()

◆ from_base10()

◆ from_double()

◆ from_expr()

◆ from_float()

◆ from_integer()

◆ get_exponent()

◆ get_fraction()

◆ get_sign()

◆ ieee_equal()

◆ ieee_not_equal()

◆ increment()

◆ is_double()

◆ is_float()

◆ is_infinity()

◆ is_NaN()

◆ is_normal()

◆ is_zero()

◆ make_fltmax()

◆ make_fltmin()

◆ make_minus_infinity()

◆ make_NaN()

◆ make_plus_infinity()

◆ make_zero()

◆ minus_infinity()

◆ NaN()

◆ negate()

◆ next_representable()

◆ operator!=()

◆ operator*=()

◆ operator+=()

◆ operator-=()

◆ operator/=()

◆ operator<()

◆ operator<=()

◆ operator==() [1/2]

◆ operator==() [2/2]

◆ operator>()

◆ operator>=()

◆ pack()

◆ plus_infinity()

◆ print()

◆ rounding_mode_expr()

◆ set_sign()

◆ to_ansi_c_string()

◆ to_double()

◆ to_expr()

◆ to_float()

◆ to_integer()

◆ to_string_decimal()

◆ to_string_scientific()

◆ unpack()

◆ zero()