52 std::cout <<
"expand_structs_and_arrays: " 58 if(src_type.
id()==ID_struct)
64 result.
operands().resize(components.size());
67 for(
unsigned i=0; i<components.size(); i++)
69 const typet &subtype=components[i].type();
70 const irep_idt &component_name=components[i].get_name();
73 if(src.
id()==ID_struct)
75 assert(src.
operands().size()==components.size());
87 else if(src_type.
id()==ID_array)
96 throw "failed to convert array size";
104 for(std::size_t i=0; i<size_int; ++i)
110 if(src.
id()==ID_array)
124 else if(src_type.
id()==ID_vector)
130 throw "vector with non-constant size";
134 throw "failed to convert vector size";
140 operands.resize(size_int);
143 for(std::size_t i=0; i<size_int; ++i)
149 if(src.
id()==ID_vector)
166 if(src.
id()==ID_index)
172 if(!index_tmp2.is_constant())
181 throw "failed to convert array size";
188 for(std::size_t i=0; i<size_int; ++i)
198 result=
if_exprt(index_equal, new_src, result);
219 std::cout <<
"instantiate_rec: " 227 exprt tmp_symbol_member_index=
231 return tmp_symbol_member_index;
234 if(src.
id()==ID_address_of)
241 else if(src.
id()==ID_side_effect)
246 if(statement==ID_nondet)
252 nondet_symbol.
name=id;
260 throw "instantiate_rec: unexpected side effect "+
id2string(statement);
262 else if(src.
id()==ID_dereference)
268 else if(src.
id()==ID_member)
270 const typet &compound_type=
273 if(compound_type.
id()==ID_struct)
277 else if(compound_type.
id()==ID_union)
280 throw "unexpected union member";
284 throw "member expects struct or union type"+src.
pretty();
287 else if(src.
id()==ID_byte_extract_little_endian ||
288 src.
id()==ID_byte_extract_big_endian)
291 else if(src.
id()==ID_symbol)
294 assert(src.
type().
id()==ID_code ||
320 if(src_type.
id()==ID_code)
326 if(
final.
id()==ID_struct ||
327 final.
id()==ID_array ||
328 final.
id()==ID_vector)
338 if(
final.
id()==ID_if)
340 assert(
final.operands().size()==3);
347 std::string suffix=
"";
351 while(current.
id()!=ID_symbol)
355 if(current.
id()==ID_member)
359 const typet &compound_type=
362 if(compound_type.
id()==ID_struct)
371 else if(current.
id()==ID_index)
380 next=index_expr.
array();
381 suffix=index_string+suffix;
391 assert(current.
id()==ID_symbol);
393 if(current.
get_bool(ID_C_SSA_symbol))
403 std::cout <<
"read_symbol_member_index_rec " << identifier
412 return var_state.
value;
435 const exprt *current=&src;
440 const exprt *next=
nullptr;
442 if(current->
id()==ID_symbol)
444 if(current->
get_bool(ID_C_SSA_symbol))
449 else if(current->
id()==ID_member)
453 const typet &compound_type=
456 if(compound_type.
id()==ID_struct)
464 else if(current->
id()==ID_index)
469 next=&(index_expr.
array());
495 if(src.
id()==ID_dereference)
507 return address_dereferenced;
532 std::cout <<
"instantiate_rec_address: " << src.
id() <<
'\n';
535 if(src.
id()==ID_symbol)
539 else if(src.
id()==ID_index)
547 else if(src.
id()==ID_dereference)
555 else if(src.
id()==ID_member)
561 else if(src.
id()==ID_string_constant)
565 else if(src.
id()==ID_label)
569 else if(src.
id()==ID_byte_extract_big_endian ||
570 src.
id()==ID_byte_extract_little_endian)
578 else if(src.
id()==ID_if)
592 std::cout <<
"SRC: " << src.
pretty() <<
'\n';
594 throw "address of unexpected `"+src.
id_string()+
"'";
The type of an expression.
irep_idt name
The unique identifier.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
const typet & follow(const typet &src) const
symbol_tablet new_symbols
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
exprt instantiate_rec(const exprt &src, bool propagate)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const componentst & components() const
The trinary if-then-else operator.
exprt instantiate_rec_address(const exprt &src, bool propagate)
bool get_bool(const irep_namet &name) const
symbol_exprt ssa_symbol() const
side_effect_exprt & to_side_effect_expr(exprt &expr)
exprt array_theory(const exprt &src, bool propagate)
Extract member of struct or union.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
std::string array_index_as_string(const exprt &) const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt dereference(const exprt &pointer, const namespacet &ns)
exprt read(const exprt &src)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Operator to dereference a pointer.
A constant-size array type.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
const exprt & size() const
const exprt & size() const
var_statet & get_var_state(const var_mapt::var_infot &var_info)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
vector constructor from list of elements
bool has_operands() const
exprt dereference_rec(const exprt &src, bool propagate)
std::vector< exprt > operandst
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
exprt read_symbol_member_index(const exprt &src, bool propagate)
exprt expand_structs_and_arrays(const exprt &src)
typet type
Type of symbol.
State of path-based symbolic simulator.
Base class for all expressions.
const exprt & struct_op() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
irep_idt get_component_name() const
const std::string & id_string() const
#define Forall_operands(it, expr)
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
bool is_symbol_member_index(const exprt &src) const
struct constructor from list of elements
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
array constructor from list of elements
const irep_idt & get_statement() const