25 if(expr.
type().
id()==ID_vector)
28 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
29 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitxor ||
30 expr.
id() == ID_bitand || expr.
id() == ID_bitor || expr.
id() == ID_shl ||
31 expr.
id() == ID_lshr || expr.
id() == ID_ashr)
35 else if(expr.
id()==ID_unary_minus || expr.
id()==ID_bitnot)
38 expr.
id() == ID_vector_equal || expr.
id() == ID_vector_notequal ||
39 expr.
id() == ID_vector_lt || expr.
id() == ID_vector_le ||
40 expr.
id() == ID_vector_gt || expr.
id() == ID_vector_ge)
44 else if(expr.
id()==ID_vector)
60 if(type.
id()==ID_struct || type.
id()==ID_union)
66 else if(type.
id() == ID_code)
78 else if(type.
id()==ID_pointer ||
79 type.
id()==ID_complex ||
82 else if(type.
id()==ID_vector)
99 if(expr.
type().
id()==ID_vector)
102 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_mult ||
103 expr.
id() == ID_div || expr.
id() == ID_mod || expr.
id() == ID_bitxor ||
104 expr.
id() == ID_bitand || expr.
id() == ID_bitor || expr.
id() == ID_shl ||
105 expr.
id() == ID_lshr || expr.
id() == ID_ashr)
123 array_expr.
operands().resize(numeric_cast_v<std::size_t>(dimension));
126 for(std::size_t i=0; i<array_expr.operands().size(); i++)
138 else if(expr.
id()==ID_unary_minus || expr.
id()==ID_bitnot)
151 array_expr.
operands().resize(numeric_cast_v<std::size_t>(dimension));
154 for(std::size_t i=0; i<array_expr.operands().size(); i++)
159 unary_expr.id(),
index_exprt(unary_expr.op(), index, subtype));
165 expr.
id() == ID_vector_equal || expr.
id() == ID_vector_notequal ||
166 expr.
id() == ID_vector_lt || expr.
id() == ID_vector_le ||
167 expr.
id() == ID_vector_gt || expr.
id() == ID_vector_ge)
174 const auto dimension = numeric_cast_v<std::size_t>(vector_type.
size());
182 operands.reserve(dimension);
184 const bool is_float =
188 if(binary_expr.id() == ID_vector_notequal)
191 new_id = ID_ieee_float_notequal;
193 new_id = ID_notequal;
195 else if(binary_expr.id() == ID_vector_equal)
198 new_id = ID_ieee_float_equal;
205 new_id =
id2string(binary_expr.id()).substr(7);
208 for(std::size_t i = 0; i < dimension; ++i)
225 else if(expr.
id()==ID_vector)
229 else if(expr.
id() == ID_typecast)
233 if(op.type().id() != ID_array)
238 const auto dimension =
258 if(type.
id()==ID_struct || type.
id()==ID_union)
263 for(struct_union_typet::componentst::iterator
271 else if(type.
id() == ID_code)
279 else if(type.
id()==ID_pointer ||
280 type.
id()==ID_complex ||
285 else if(type.
id()==ID_vector)
308 for(
const auto &named_symbol : symbol_table.
symbols)
315 for(
auto &i : goto_function.body.instructions)
Array constructor from list of elements.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const parameterst & parameters() const
const typet & return_type() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
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.
The trinary if-then-else operator.
const irep_idt & id() const
Base type for structs and unions.
const componentst & components() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
typet type
Type of symbol.
exprt value
Initial value of symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
source_locationt & add_source_location()
const source_locationt & source_location() const
Generic base class for unary expressions.
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
static void remove_vector(typet &)
removes vector data type
static bool have_to_remove_vector(const typet &type)
Remove the 'vector' data type by compilation into arrays.
#define PRECONDITION(CONDITION)
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const type_with_subtypet & to_type_with_subtype(const typet &type)