API to expression classes for floating-point arithmetic. More...

#include "std_expr.h"

Include dependency graph for floatbv_expr.h:

This graph shows which files directly or indirectly include this file:

Classes
class	floatbv_typecast_exprt
	Semantic type conversion from/to floating-point formats. More...

class	floatbv_round_to_integral_exprt
	Round a floating-point number to an integral value considering the given rounding mode. More...

class	isnan_exprt
	Evaluates to true if the operand is NaN. More...

class	isinf_exprt
	Evaluates to true if the operand is infinite. More...

class	isfinite_exprt
	Evaluates to true if the operand is finite. More...

class	isnormal_exprt
	Evaluates to true if the operand is a normal number. More...

class	ieee_float_equal_exprt
	IEEE-floating-point equality. More...

class	ieee_float_notequal_exprt
	IEEE floating-point disequality. More...

class	ieee_float_op_exprt
	IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2). More...

class	floatbv_mod_exprt
	IEEE floating-point mod. More...

class	floatbv_rem_exprt
	IEEE floating-point rem. More...

Functions
template<>
bool	can_cast_expr< floatbv_typecast_exprt > (const exprt &base)

void	validate_expr (const floatbv_typecast_exprt &value)

const floatbv_typecast_exprt &	to_floatbv_typecast_expr (const exprt &expr)
	Cast an exprt to a floatbv_typecast_exprt.

floatbv_typecast_exprt &	to_floatbv_typecast_expr (exprt &expr)
	Cast an exprt to a floatbv_typecast_exprt.

template<>
bool	can_cast_expr< floatbv_round_to_integral_exprt > (const exprt &base)

const floatbv_round_to_integral_exprt &	to_floatbv_round_to_integral_expr (const exprt &expr)
	Cast an exprt to a floatbv_round_to_integral_exprt.

floatbv_round_to_integral_exprt &	to_floatbv_round_to_integral_expr (exprt &expr)
	Cast an exprt to a floatbv_round_to_integral_exprt.

template<>
bool	can_cast_expr< isnan_exprt > (const exprt &base)

void	validate_expr (const isnan_exprt &value)

const isnan_exprt &	to_isnan_expr (const exprt &expr)
	Cast an exprt to a isnan_exprt.

isnan_exprt &	to_isnan_expr (exprt &expr)
	Cast an exprt to a isnan_exprt.

template<>
bool	can_cast_expr< isinf_exprt > (const exprt &base)

void	validate_expr (const isinf_exprt &value)

const isinf_exprt &	to_isinf_expr (const exprt &expr)
	Cast an exprt to a isinf_exprt.

isinf_exprt &	to_isinf_expr (exprt &expr)
	Cast an exprt to a isinf_exprt.

template<>
bool	can_cast_expr< isfinite_exprt > (const exprt &base)

void	validate_expr (const isfinite_exprt &value)

const isfinite_exprt &	to_isfinite_expr (const exprt &expr)
	Cast an exprt to a isfinite_exprt.

isfinite_exprt &	to_isfinite_expr (exprt &expr)
	Cast an exprt to a isfinite_exprt.

template<>
bool	can_cast_expr< isnormal_exprt > (const exprt &base)

void	validate_expr (const isnormal_exprt &value)

const isnormal_exprt &	to_isnormal_expr (const exprt &expr)
	Cast an exprt to a isnormal_exprt.

isnormal_exprt &	to_isnormal_expr (exprt &expr)
	Cast an exprt to a isnormal_exprt.

template<>
bool	can_cast_expr< ieee_float_equal_exprt > (const exprt &base)

void	validate_expr (const ieee_float_equal_exprt &value)

const ieee_float_equal_exprt &	to_ieee_float_equal_expr (const exprt &expr)
	Cast an exprt to an ieee_float_equal_exprt.

ieee_float_equal_exprt &	to_ieee_float_equal_expr (exprt &expr)
	Cast an exprt to an ieee_float_equal_exprt.

template<>
bool	can_cast_expr< ieee_float_notequal_exprt > (const exprt &base)

void	validate_expr (const ieee_float_notequal_exprt &value)

const ieee_float_notequal_exprt &	to_ieee_float_notequal_expr (const exprt &expr)
	Cast an exprt to an ieee_float_notequal_exprt.

ieee_float_notequal_exprt &	to_ieee_float_notequal_expr (exprt &expr)
	Cast an exprt to an ieee_float_notequal_exprt.

template<>
bool	can_cast_expr< ieee_float_op_exprt > (const exprt &base)

void	validate_expr (const ieee_float_op_exprt &value)

const ieee_float_op_exprt &	to_ieee_float_op_expr (const exprt &expr)
	Cast an exprt to an ieee_float_op_exprt.

ieee_float_op_exprt &	to_ieee_float_op_expr (exprt &expr)
	Cast an exprt to an ieee_float_op_exprt.

const floatbv_mod_exprt &	to_floatbv_mod_expr (const exprt &expr)
	Cast an exprt to a floatbv_mod_exprt.

floatbv_mod_exprt &	to_floatbv_mod_expr (exprt &expr)
	Cast an exprt to a floatbv_mod_exprt.

const floatbv_rem_exprt &	to_floatbv_rem_expr (const exprt &expr)
	Cast an exprt to a floatbv_rem_exprt.

floatbv_rem_exprt &	to_floatbv_rem_expr (exprt &expr)
	Cast an exprt to a floatbv_rem_exprt.

constant_exprt	floatbv_rounding_mode (unsigned)
	returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendation in C11 5.2.4.2.2

Detailed Description

API to expression classes for floating-point arithmetic.

Definition in file floatbv_expr.h.

Function Documentation

◆ can_cast_expr< floatbv_round_to_integral_exprt >()

template<>

bool can_cast_expr< floatbv_round_to_integral_exprt > ( const exprt & base )

inline

Definition at line 122 of file floatbv_expr.h.

◆ can_cast_expr< floatbv_typecast_exprt >()

template<>

bool can_cast_expr< floatbv_typecast_exprt > ( const exprt & base )

inline

Definition at line 52 of file floatbv_expr.h.

◆ can_cast_expr< ieee_float_equal_exprt >()

template<>

bool can_cast_expr< ieee_float_equal_exprt > ( const exprt & base )

inline

Definition at line 340 of file floatbv_expr.h.

◆ can_cast_expr< ieee_float_notequal_exprt >()

template<>

bool can_cast_expr< ieee_float_notequal_exprt > ( const exprt & base )

inline

Definition at line 388 of file floatbv_expr.h.

◆ can_cast_expr< ieee_float_op_exprt >()

template<>

bool can_cast_expr< ieee_float_op_exprt > ( const exprt & base )

inline

Definition at line 471 of file floatbv_expr.h.

◆ can_cast_expr< isfinite_exprt >()

template<>

bool can_cast_expr< isfinite_exprt > ( const exprt & base )

inline

Definition at line 249 of file floatbv_expr.h.

◆ can_cast_expr< isinf_exprt >()

template<>

bool can_cast_expr< isinf_exprt > ( const exprt & base )

inline

Definition at line 205 of file floatbv_expr.h.

◆ can_cast_expr< isnan_exprt >()

template<>

bool can_cast_expr< isnan_exprt > ( const exprt & base )

inline

Definition at line 161 of file floatbv_expr.h.

◆ can_cast_expr< isnormal_exprt >()

template<>

bool can_cast_expr< isnormal_exprt > ( const exprt & base )

inline

Definition at line 293 of file floatbv_expr.h.

◆ floatbv_rounding_mode()

constant_exprt floatbv_rounding_mode ( unsigned rm )

returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendation in C11 5.2.4.2.2

Definition at line 14 of file floatbv_expr.cpp.

◆ to_floatbv_mod_expr() [1/2]

const floatbv_mod_exprt & to_floatbv_mod_expr ( const exprt & expr )

inline

Cast an exprt to a floatbv_mod_exprt.

expr must be known to be floatbv_mod_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_mod_exprt

Definition at line 523 of file floatbv_expr.h.

◆ to_floatbv_mod_expr() [2/2]

floatbv_mod_exprt & to_floatbv_mod_expr ( exprt & expr )

inline

Cast an exprt to a floatbv_mod_exprt.

expr must be known to be floatbv_mod_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_mod_exprt

Definition at line 531 of file floatbv_expr.h.

◆ to_floatbv_rem_expr() [1/2]

const floatbv_rem_exprt & to_floatbv_rem_expr ( const exprt & expr )

inline

Cast an exprt to a floatbv_rem_exprt.

expr must be known to be floatbv_rem_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_rem_exprt

Definition at line 556 of file floatbv_expr.h.

◆ to_floatbv_rem_expr() [2/2]

floatbv_rem_exprt & to_floatbv_rem_expr ( exprt & expr )

inline

Cast an exprt to a floatbv_rem_exprt.

expr must be known to be floatbv_rem_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_rem_exprt

Definition at line 564 of file floatbv_expr.h.

◆ to_floatbv_round_to_integral_expr() [1/2]

const floatbv_round_to_integral_exprt & to_floatbv_round_to_integral_expr ( const exprt & expr )

inline

Cast an exprt to a floatbv_round_to_integral_exprt.

expr must be known to be floatbv_round_to_integral_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_round_to_integral_exprt

Definition at line 134 of file floatbv_expr.h.

◆ to_floatbv_round_to_integral_expr() [2/2]

floatbv_round_to_integral_exprt & to_floatbv_round_to_integral_expr ( exprt & expr )

inline

Cast an exprt to a floatbv_round_to_integral_exprt.

expr must be known to be floatbv_round_to_integral_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_round_to_integral_exprt

Definition at line 143 of file floatbv_expr.h.

◆ to_floatbv_typecast_expr() [1/2]

const floatbv_typecast_exprt & to_floatbv_typecast_expr ( const exprt & expr )

inline

Cast an exprt to a floatbv_typecast_exprt.

expr must be known to be floatbv_typecast_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_typecast_exprt

Definition at line 68 of file floatbv_expr.h.

◆ to_floatbv_typecast_expr() [2/2]

floatbv_typecast_exprt & to_floatbv_typecast_expr ( exprt & expr )

inline

Cast an exprt to a floatbv_typecast_exprt.

expr must be known to be floatbv_typecast_exprt.

Parameters

expr	Source expression

Returns: Object of type floatbv_typecast_exprt

Definition at line 78 of file floatbv_expr.h.

◆ to_ieee_float_equal_expr() [1/2]

const ieee_float_equal_exprt & to_ieee_float_equal_expr ( const exprt & expr )

inline

Cast an exprt to an ieee_float_equal_exprt.

expr must be known to be ieee_float_equal_exprt.

Parameters

expr	Source expression

Returns: Object of type ieee_float_equal_exprt

Definition at line 356 of file floatbv_expr.h.

◆ to_ieee_float_equal_expr() [2/2]

ieee_float_equal_exprt & to_ieee_float_equal_expr ( exprt & expr )

inline

Cast an exprt to an ieee_float_equal_exprt.

expr must be known to be ieee_float_equal_exprt.

Parameters

expr	Source expression

Returns: Object of type ieee_float_equal_exprt

Definition at line 366 of file floatbv_expr.h.

◆ to_ieee_float_notequal_expr() [1/2]

const ieee_float_notequal_exprt & to_ieee_float_notequal_expr ( const exprt & expr )

inline

Cast an exprt to an ieee_float_notequal_exprt.

expr must be known to be ieee_float_notequal_exprt.

Parameters

expr	Source expression

Returns: Object of type ieee_float_notequal_exprt

Definition at line 405 of file floatbv_expr.h.

◆ to_ieee_float_notequal_expr() [2/2]

ieee_float_notequal_exprt & to_ieee_float_notequal_expr ( exprt & expr )

inline

Cast an exprt to an ieee_float_notequal_exprt.

expr must be known to be ieee_float_notequal_exprt.

Parameters

expr	Source expression

Returns: Object of type ieee_float_notequal_exprt

Definition at line 415 of file floatbv_expr.h.

◆ to_ieee_float_op_expr() [1/2]

const ieee_float_op_exprt & to_ieee_float_op_expr ( const exprt & expr )

inline

Cast an exprt to an ieee_float_op_exprt.

expr must be known to be ieee_float_op_exprt.

Parameters

expr	Source expression

Returns: Object of type ieee_float_op_exprt

Definition at line 489 of file floatbv_expr.h.

◆ to_ieee_float_op_expr() [2/2]

ieee_float_op_exprt & to_ieee_float_op_expr ( exprt & expr )

inline

Cast an exprt to an ieee_float_op_exprt.

expr must be known to be ieee_float_op_exprt.

Parameters

expr	Source expression

Returns: Object of type ieee_float_op_exprt

Definition at line 498 of file floatbv_expr.h.

◆ to_isfinite_expr() [1/2]

const isfinite_exprt & to_isfinite_expr ( const exprt & expr )

inline

Cast an exprt to a isfinite_exprt.

expr must be known to be isfinite_exprt.

Parameters

expr	Source expression

Returns: Object of type isfinite_exprt

Definition at line 265 of file floatbv_expr.h.

◆ to_isfinite_expr() [2/2]

isfinite_exprt & to_isfinite_expr ( exprt & expr )

inline

Cast an exprt to a isfinite_exprt.

expr must be known to be isfinite_exprt.

Parameters

expr	Source expression

Returns: Object of type isfinite_exprt

Definition at line 274 of file floatbv_expr.h.

◆ to_isinf_expr() [1/2]

const isinf_exprt & to_isinf_expr ( const exprt & expr )

inline

Cast an exprt to a isinf_exprt.

expr must be known to be isinf_exprt.

Parameters

expr	Source expression

Returns: Object of type isinf_exprt

Definition at line 221 of file floatbv_expr.h.

◆ to_isinf_expr() [2/2]

isinf_exprt & to_isinf_expr ( exprt & expr )

inline

Cast an exprt to a isinf_exprt.

expr must be known to be isinf_exprt.

Parameters

expr	Source expression

Returns: Object of type isinf_exprt

Definition at line 230 of file floatbv_expr.h.

◆ to_isnan_expr() [1/2]

const isnan_exprt & to_isnan_expr ( const exprt & expr )

inline

Cast an exprt to a isnan_exprt.

expr must be known to be isnan_exprt.

Parameters

expr	Source expression

Returns: Object of type isnan_exprt

Definition at line 177 of file floatbv_expr.h.

◆ to_isnan_expr() [2/2]

isnan_exprt & to_isnan_expr ( exprt & expr )

inline

Cast an exprt to a isnan_exprt.

expr must be known to be isnan_exprt.

Parameters

expr	Source expression

Returns: Object of type isnan_exprt

Definition at line 186 of file floatbv_expr.h.

◆ to_isnormal_expr() [1/2]

const isnormal_exprt & to_isnormal_expr ( const exprt & expr )

inline

Cast an exprt to a isnormal_exprt.

expr must be known to be isnormal_exprt.

Parameters

expr	Source expression

Returns: Object of type isnormal_exprt

Definition at line 309 of file floatbv_expr.h.

◆ to_isnormal_expr() [2/2]

isnormal_exprt & to_isnormal_expr ( exprt & expr )

inline

Cast an exprt to a isnormal_exprt.

expr must be known to be isnormal_exprt.

Parameters

expr	Source expression

Returns: Object of type isnormal_exprt

Definition at line 318 of file floatbv_expr.h.

◆ validate_expr() [1/8]

void validate_expr ( const floatbv_typecast_exprt & value )

inline

Definition at line 57 of file floatbv_expr.h.

◆ validate_expr() [2/8]

void validate_expr ( const ieee_float_equal_exprt & value )

inline

Definition at line 345 of file floatbv_expr.h.

◆ validate_expr() [3/8]

void validate_expr ( const ieee_float_notequal_exprt & value )

inline

Definition at line 393 of file floatbv_expr.h.

◆ validate_expr() [4/8]

void validate_expr ( const ieee_float_op_exprt & value )

inline

Definition at line 477 of file floatbv_expr.h.

◆ validate_expr() [5/8]

void validate_expr ( const isfinite_exprt & value )

inline

Definition at line 254 of file floatbv_expr.h.

◆ validate_expr() [6/8]

void validate_expr ( const isinf_exprt & value )

inline

Definition at line 210 of file floatbv_expr.h.

◆ validate_expr() [7/8]

void validate_expr ( const isnan_exprt & value )

inline

Definition at line 166 of file floatbv_expr.h.

◆ validate_expr() [8/8]

void validate_expr ( const isnormal_exprt & value )

inline

Definition at line 298 of file floatbv_expr.h.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_expr< floatbv_round_to_integral_exprt >()

◆ can_cast_expr< floatbv_typecast_exprt >()

◆ can_cast_expr< ieee_float_equal_exprt >()

◆ can_cast_expr< ieee_float_notequal_exprt >()

◆ can_cast_expr< ieee_float_op_exprt >()

◆ can_cast_expr< isfinite_exprt >()

◆ can_cast_expr< isinf_exprt >()

◆ can_cast_expr< isnan_exprt >()

◆ can_cast_expr< isnormal_exprt >()

◆ floatbv_rounding_mode()

◆ to_floatbv_mod_expr() [1/2]

◆ to_floatbv_mod_expr() [2/2]

◆ to_floatbv_rem_expr() [1/2]

◆ to_floatbv_rem_expr() [2/2]

◆ to_floatbv_round_to_integral_expr() [1/2]

◆ to_floatbv_round_to_integral_expr() [2/2]

◆ to_floatbv_typecast_expr() [1/2]

◆ to_floatbv_typecast_expr() [2/2]

◆ to_ieee_float_equal_expr() [1/2]

◆ to_ieee_float_equal_expr() [2/2]

◆ to_ieee_float_notequal_expr() [1/2]

◆ to_ieee_float_notequal_expr() [2/2]

◆ to_ieee_float_op_expr() [1/2]

◆ to_ieee_float_op_expr() [2/2]

◆ to_isfinite_expr() [1/2]

◆ to_isfinite_expr() [2/2]

◆ to_isinf_expr() [1/2]

◆ to_isinf_expr() [2/2]

◆ to_isnan_expr() [1/2]

◆ to_isnan_expr() [2/2]

◆ to_isnormal_expr() [1/2]

◆ to_isnormal_expr() [2/2]

◆ validate_expr() [1/8]

◆ validate_expr() [2/8]

◆ validate_expr() [3/8]

◆ validate_expr() [4/8]

◆ validate_expr() [5/8]

◆ validate_expr() [6/8]

◆ validate_expr() [7/8]

◆ validate_expr() [8/8]