29 if(expr.
id()==ID_floatbv_plus ||
30 expr.
id()==ID_floatbv_minus ||
31 expr.
id()==ID_floatbv_mult ||
32 expr.
id()==ID_floatbv_div ||
33 expr.
id()==ID_floatbv_div ||
34 expr.
id()==ID_floatbv_rem ||
35 expr.
id()==ID_floatbv_typecast)
41 type.
id() == ID_floatbv ||
42 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
44 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
45 expr.
id()==ID_mult || expr.
id()==ID_div ||
50 if(expr.
id()==ID_typecast)
55 const typet &dest_type=typecast_expr.
type();
57 if(dest_type.
id()==ID_floatbv &&
58 src_type.
id()==ID_floatbv)
61 dest_type.
id() == ID_floatbv &&
62 (src_type.
id() == ID_c_bit_field || src_type.
id() == ID_signedbv ||
63 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_c_enum_tag))
66 (dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
67 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_c_bit_field) &&
68 src_type.
id() == ID_floatbv)
95 type.
id() == ID_floatbv ||
96 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
98 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
99 expr.
id()==ID_mult || expr.
id()==ID_div ||
104 "arithmetic operations must have two or more operands");
114 expr.
id(expr.
id()==ID_plus?ID_floatbv_plus:
115 expr.
id()==ID_minus?ID_floatbv_minus:
116 expr.
id()==ID_mult?ID_floatbv_mult:
117 expr.
id()==ID_div?ID_floatbv_div:
118 expr.
id()==ID_rem?ID_floatbv_rem:
126 if(expr.
id()==ID_typecast)
131 const typet &dest_type=typecast_expr.
type();
133 if(dest_type.
id()==ID_floatbv &&
134 src_type.
id()==ID_floatbv)
140 expr.
id(ID_floatbv_typecast);
145 dest_type.
id() == ID_floatbv &&
146 (src_type.
id() == ID_signedbv || src_type.
id() == ID_unsignedbv ||
147 src_type.
id() == ID_c_enum_tag || src_type.
id() == ID_c_bit_field))
150 expr.
id(ID_floatbv_typecast);
155 dest_type.
id() == ID_floatbv &&
156 (src_type.
id() == ID_c_bool || src_type.
id() == ID_bool))
161 (dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
162 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_c_bit_field) &&
163 src_type.
id() == ID_floatbv)
176 expr.
id(ID_floatbv_typecast);
201 for(
auto &i : goto_function.body.instructions)
static bool have_to_adjust_float_expressions(const exprt &expr)
Iterate over an expression and check it or any of its subexpressions are floating point operations th...
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
#define forall_operands(it, expr)
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
nonstd::optional< T > optionalt
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.