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	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...

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. More...

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

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. More...

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

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. More...

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

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. More...

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

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. More...

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

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. More...

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

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. More...

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

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. More...

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

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 More...

Detailed Description

API to expression classes for floating-point arithmetic.

Definition in file floatbv_expr.h.

Function Documentation

◆ 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 276 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 324 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 407 of file floatbv_expr.h.

◆ can_cast_expr< isfinite_exprt >()

template<>

bool can_cast_expr< isfinite_exprt > ( const exprt & base )

inline

Definition at line 185 of file floatbv_expr.h.

◆ can_cast_expr< isinf_exprt >()

template<>

bool can_cast_expr< isinf_exprt > ( const exprt & base )

inline

Definition at line 141 of file floatbv_expr.h.

◆ can_cast_expr< isnan_exprt >()

template<>

bool can_cast_expr< isnan_exprt > ( const exprt & base )

inline

Definition at line 97 of file floatbv_expr.h.

◆ can_cast_expr< isnormal_exprt >()

template<>

bool can_cast_expr< isnormal_exprt > ( const exprt & base )

inline

Definition at line 229 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_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 292 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 302 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 341 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 351 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 425 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 434 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 201 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 210 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 157 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 166 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 113 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 122 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 245 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 254 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 281 of file floatbv_expr.h.

◆ validate_expr() [3/8]

void validate_expr ( const ieee_float_notequal_exprt & value )

inline

Definition at line 329 of file floatbv_expr.h.

◆ validate_expr() [4/8]

void validate_expr ( const ieee_float_op_exprt & value )

inline

Definition at line 413 of file floatbv_expr.h.

◆ validate_expr() [5/8]

void validate_expr ( const isfinite_exprt & value )

inline

Definition at line 190 of file floatbv_expr.h.

◆ validate_expr() [6/8]

void validate_expr ( const isinf_exprt & value )

inline

Definition at line 146 of file floatbv_expr.h.

◆ validate_expr() [7/8]

void validate_expr ( const isnan_exprt & value )

inline

Definition at line 102 of file floatbv_expr.h.

◆ validate_expr() [8/8]

void validate_expr ( const isnormal_exprt & value )

inline

Definition at line 234 of file floatbv_expr.h.

Classes

Functions

Detailed Description

Function Documentation

◆ 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_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]