Go to the documentation of this file.
28 if(expr.
id()==ID_floatbv_plus ||
29 expr.
id()==ID_floatbv_minus ||
30 expr.
id()==ID_floatbv_mult ||
31 expr.
id()==ID_floatbv_div ||
32 expr.
id()==ID_floatbv_div ||
33 expr.
id()==ID_floatbv_rem ||
34 expr.
id()==ID_floatbv_typecast)
40 type.
id() == ID_floatbv ||
41 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
43 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
44 expr.
id()==ID_mult || expr.
id()==ID_div ||
49 if(expr.
id()==ID_typecast)
54 const typet &dest_type=typecast_expr.
type();
56 if(dest_type.
id()==ID_floatbv &&
57 src_type.
id()==ID_floatbv)
60 dest_type.
id() == ID_floatbv &&
61 (src_type.
id() == ID_c_bit_field || src_type.
id() == ID_signedbv ||
62 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_c_enum_tag))
65 (dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
66 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_c_bit_field) &&
67 src_type.
id() == ID_floatbv)
94 type.
id() == ID_floatbv ||
95 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
97 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
98 expr.
id()==ID_mult || expr.
id()==ID_div ||
103 "arithmetic operations must have two or more operands");
113 expr.
id(expr.
id()==ID_plus?ID_floatbv_plus:
114 expr.
id()==ID_minus?ID_floatbv_minus:
115 expr.
id()==ID_mult?ID_floatbv_mult:
116 expr.
id()==ID_div?ID_floatbv_div:
117 expr.
id()==ID_rem?ID_floatbv_rem:
125 if(expr.
id()==ID_typecast)
130 const typet &dest_type=typecast_expr.
type();
132 if(dest_type.
id()==ID_floatbv &&
133 src_type.
id()==ID_floatbv)
139 expr.
id(ID_floatbv_typecast);
144 dest_type.
id() == ID_floatbv &&
145 (src_type.
id() == ID_signedbv || src_type.
id() == ID_unsignedbv ||
146 src_type.
id() == ID_c_enum_tag || src_type.
id() == ID_c_bit_field))
149 expr.
id(ID_floatbv_typecast);
154 dest_type.
id() == ID_floatbv &&
155 (src_type.
id() == ID_c_bool || src_type.
id() == ID_bool))
160 (dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
161 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_c_bit_field) &&
162 src_type.
id() == ID_floatbv)
175 expr.
id(ID_floatbv_typecast);
200 for(
auto &i : goto_function.body.instructions)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
Base class for all expressions.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define forall_operands(it, expr)
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const irep_idt & id() const
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...
nonstd::optional< T > optionalt
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
Deprecated expression utility functions.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
source_locationt & add_source_location()
Semantic type conversion.
API to expression classes.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.