An IEEE 754 value plus a rounding mode, enabling operations with rounding on values. More...

#include <ieee_float.h>

Inheritance diagram for ieee_floatt:

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

Public Member Functions
rounding_modet	rounding_mode () const

	ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode)

	ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode, const mp_integer &value)

	ieee_floatt (const floatbv_typet &type, rounding_modet __rounding_mode)

	ieee_floatt (const constant_exprt &expr, rounding_modet __rounding_mode)

	ieee_floatt (ieee_float_valuet __value, rounding_modet __rounding_mode)

void	from_integer (const mp_integer &i)

void	from_base10 (const mp_integer &exp, const mp_integer &frac)
	compute f * (10^e)

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

double	to_double () const

float	to_float () const

mp_integer	to_integer () const

void	change_spec (const ieee_float_spect &dest_spec)

ieee_floatt	round_to_integral () const

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)

Public Member Functions inherited from ieee_float_valuet
	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
	Note that calling from_double -> to_double can return different bit patterns for NaN.

float	to_float () const
	Note that calling from_float -> to_float can return different bit patterns for NaN.

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	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 constant_exprt	rounding_mode_expr (rounding_modet)

Static Public Member Functions inherited from ieee_float_valuet
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)

Protected Member Functions
void	divide_and_round (mp_integer &dividend, const mp_integer &divisor)

void	align ()

Protected Member Functions inherited from ieee_float_valuet
void	next_representable (bool greater)
	Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false).

Protected Attributes
rounding_modet	_rounding_mode

Protected Attributes inherited from ieee_float_valuet
bool	sign_flag

mp_integer	exponent

mp_integer	fraction

bool	NaN_flag

bool	infinity_flag

Additional Inherited Members
Public Attributes inherited from ieee_float_valuet
ieee_float_spect	spec

Static Protected Member Functions inherited from ieee_float_valuet
static mp_integer	base10_digits (const mp_integer &src)

Detailed Description

An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.

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

Definition at line 346 of file ieee_float.h.

Constructor & Destructor Documentation

◆ ieee_floatt() [1/5]

ieee_floatt::ieee_floatt	(	ieee_float_spect	__spec,
		rounding_modet	__rounding_mode
	)

inline

Definition at line 365 of file ieee_float.h.

◆ ieee_floatt() [2/5]

ieee_floatt::ieee_floatt	(	ieee_float_spect	__spec,
		rounding_modet	__rounding_mode,
		const mp_integer &	value
	)

inline

Definition at line 370 of file ieee_float.h.

◆ ieee_floatt() [3/5]

ieee_floatt::ieee_floatt	(	const floatbv_typet &	type,
		rounding_modet	__rounding_mode
	)

inline

Definition at line 379 of file ieee_float.h.

◆ ieee_floatt() [4/5]

ieee_floatt::ieee_floatt	(	const constant_exprt &	expr,
		rounding_modet	__rounding_mode
	)

inline

Definition at line 384 of file ieee_float.h.

◆ ieee_floatt() [5/5]

ieee_floatt::ieee_floatt	(	ieee_float_valuet	__value,
		rounding_modet	__rounding_mode
	)

inline

Definition at line 389 of file ieee_float.h.

Member Function Documentation

◆ align()

void ieee_floatt::align ( )

protected

Definition at line 821 of file ieee_float.cpp.

◆ build()

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

Definition at line 566 of file ieee_float.cpp.

◆ change_spec()

void ieee_floatt::change_spec ( const ieee_float_spect & dest_spec )

Definition at line 1231 of file ieee_float.cpp.

◆ divide_and_round()

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

protected

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

◆ from_integer()

void ieee_floatt::from_integer ( const mp_integer & i )

Definition at line 813 of file ieee_float.cpp.

◆ operator*=()

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

Definition at line 1097 of file ieee_float.cpp.

◆ operator+=()

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

Definition at line 1133 of file ieee_float.cpp.

◆ operator-=()

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

Definition at line 1224 of file ieee_float.cpp.

◆ operator/=()

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

Definition at line 1023 of file ieee_float.cpp.

◆ round_to_integral()

ieee_floatt ieee_floatt::round_to_integral ( ) const

Definition at line 1371 of file ieee_float.cpp.

◆ rounding_mode()

rounding_modet ieee_floatt::rounding_mode ( ) const

inline

Definition at line 357 of file ieee_float.h.

◆ rounding_mode_expr()

constant_exprt ieee_floatt::rounding_mode_expr ( rounding_modet rm )

static

Definition at line 561 of file ieee_float.cpp.

◆ to_double()

double ieee_floatt::to_double ( ) const

◆ to_float()

float ieee_floatt::to_float ( ) const

◆ to_integer()

mp_integer ieee_floatt::to_integer ( ) const

Definition at line 1256 of file ieee_float.cpp.

Member Data Documentation

◆ _rounding_mode

rounding_modet ieee_floatt::_rounding_mode

protected

Definition at line 419 of file ieee_float.h.

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

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

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

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

◆ build()

◆ change_spec()

◆ divide_and_round()

◆ from_base10()

◆ from_integer()

◆ operator*=()

◆ operator+=()

◆ operator-=()

◆ operator/=()

◆ round_to_integral()

◆ rounding_mode()

◆ rounding_mode_expr()

◆ to_double()

◆ to_float()

◆ to_integer()

Member Data Documentation

◆ _rounding_mode