Go to the documentation of this file.
34 if(expr.
id()==ID_floatbv_plus ||
35 expr.
id()==ID_floatbv_minus ||
36 expr.
id()==ID_floatbv_mult ||
37 expr.
id()==ID_floatbv_div ||
38 expr.
id()==ID_floatbv_div ||
39 expr.
id()==ID_floatbv_rem ||
40 expr.
id()==ID_floatbv_typecast)
46 type.
id() == ID_floatbv ||
47 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
50 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
55 if(expr.
id()==ID_typecast)
60 const typet &dest_type=typecast_expr.
type();
62 if(dest_type.
id()==ID_floatbv &&
63 src_type.
id()==ID_floatbv)
66 dest_type.
id() == ID_floatbv &&
67 (src_type.
id() == ID_c_bit_field || src_type.
id() == ID_signedbv ||
68 src_type.
id() == ID_unsignedbv || src_type.
id() == ID_c_enum_tag))
71 (dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
72 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_c_bit_field) &&
73 src_type.
id() == ID_floatbv)
100 type.
id() == ID_floatbv ||
101 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
104 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
109 "arithmetic operations must have two or more operands");
119 expr.
id(expr.
id()==ID_plus?ID_floatbv_plus:
120 expr.
id()==ID_minus?ID_floatbv_minus:
121 expr.
id()==ID_mult?ID_floatbv_mult:
122 expr.
id()==ID_div?ID_floatbv_div:
130 if(expr.
id()==ID_typecast)
135 const typet &dest_type=typecast_expr.
type();
137 if(dest_type.
id()==ID_floatbv &&
138 src_type.
id()==ID_floatbv)
144 expr.
id(ID_floatbv_typecast);
149 dest_type.
id() == ID_floatbv &&
150 (src_type.
id() == ID_signedbv || src_type.
id() == ID_unsignedbv ||
151 src_type.
id() == ID_c_enum_tag || src_type.
id() == ID_c_bit_field))
154 expr.
id(ID_floatbv_typecast);
159 dest_type.
id() == ID_floatbv &&
160 (src_type.
id() == ID_c_bool || src_type.
id() == ID_bool))
165 (dest_type.
id() == ID_signedbv || dest_type.
id() == ID_unsignedbv ||
166 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_c_bit_field) &&
167 src_type.
id() == ID_floatbv)
180 expr.
id(ID_floatbv_typecast);
205 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
function_mapt function_map
Expression to hold a symbol (variable)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
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 irep_idt & id() const
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
API to expression classes for floating-point arithmetic.
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
::goto_functiont goto_functiont
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Deprecated expression utility functions.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
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.