25 if(expr.
id()==ID_floatbv_plus ||
26 expr.
id()==ID_floatbv_minus ||
27 expr.
id()==ID_floatbv_mult ||
28 expr.
id()==ID_floatbv_div ||
29 expr.
id()==ID_floatbv_div ||
30 expr.
id()==ID_floatbv_rem ||
31 expr.
id()==ID_floatbv_typecast)
37 type.
id() == ID_floatbv ||
38 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
40 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
41 expr.
id()==ID_mult || expr.
id()==ID_div ||
46 if(expr.
id()==ID_typecast)
51 const typet &dest_type=typecast_expr.
type();
53 if(dest_type.
id()==ID_floatbv &&
54 src_type.
id()==ID_floatbv)
56 else if(dest_type.
id()==ID_floatbv &&
57 (src_type.
id()==ID_c_bool ||
58 src_type.
id()==ID_signedbv ||
59 src_type.
id()==ID_unsignedbv ||
60 src_type.
id()==ID_c_enum_tag))
62 else if((dest_type.
id()==ID_signedbv ||
63 dest_type.
id()==ID_unsignedbv ||
64 dest_type.
id()==ID_c_enum_tag) &&
65 src_type.
id()==ID_floatbv)
90 type.
id() == ID_floatbv ||
91 (type.
id() == ID_complex && type.
subtype().
id() == ID_floatbv))
93 if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
94 expr.
id()==ID_mult || expr.
id()==ID_div ||
99 "arithmetic operations must have two or more operands");
109 expr.
id(expr.
id()==ID_plus?ID_floatbv_plus:
110 expr.
id()==ID_minus?ID_floatbv_minus:
111 expr.
id()==ID_mult?ID_floatbv_mult:
112 expr.
id()==ID_div?ID_floatbv_div:
113 expr.
id()==ID_rem?ID_floatbv_rem:
117 expr.
op2()=rounding_mode;
121 if(expr.
id()==ID_typecast)
126 const typet &dest_type=typecast_expr.
type();
128 if(dest_type.
id()==ID_floatbv &&
129 src_type.
id()==ID_floatbv)
135 expr.
id(ID_floatbv_typecast);
137 expr.
op1()=rounding_mode;
139 else if(dest_type.
id()==ID_floatbv &&
140 (src_type.
id()==ID_c_bool ||
141 src_type.
id()==ID_signedbv ||
142 src_type.
id()==ID_unsignedbv ||
143 src_type.
id()==ID_c_enum_tag))
146 expr.
id(ID_floatbv_typecast);
148 expr.
op1()=rounding_mode;
150 else if((dest_type.
id()==ID_signedbv ||
151 dest_type.
id()==ID_unsignedbv ||
152 dest_type.
id()==ID_c_enum_tag) &&
153 src_type.
id()==ID_floatbv)
166 expr.
id(ID_floatbv_typecast);
The type of an expression, extends irept.
Semantic type conversion.
static bool have_to_adjust_float_expressions(const exprt &expr)
Deprecated expression utility functions.
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
#define CHECK_RETURN(CONDITION)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
const irep_idt & id() const
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
#define forall_operands(it, expr)
A collection of goto functions.
Base class for all expressions.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().