Go to the documentation of this file.
43 if(type.
id()==ID_struct)
47 for(
const auto &comp : struct_type.
components())
52 member_expr.
type()=comp.type();
57 else if(type.
id()==ID_pointer)
64 if(subtype.
id()!=ID_code &&
65 subtype.
id()!=ID_empty)
87 if(expr.
id()==ID_symbol &&
93 if(obj_identifier!=
"goto_symex::\\guard")
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
void symex_assign(statet &, const code_assignt &)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
static unsigned dynamic_counter
The type of an expression, extends irept.
typet type
Type of symbol.
The trinary if-then-else operator.
Base class for all expressions.
irep_idt get_object_name() const
irep_idt base_name
Base (non-scoped) name.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void trigger_auto_object(const exprt &, statet &)
Expression to hold a symbol (variable)
Expression providing an SSA-renamed symbol of expressions.
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().
bool get_bool(const irep_namet &name) const
irep_idt mode
Language mode.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
The null pointer constant.
const std::string & id2string(const irep_idt &d)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
#define forall_operands(it, expr)
const exprt & struct_op() const
void initialize_auto_object(const exprt &, statet &)
const irep_idt & get_identifier() const
exprt make_auto_object(const typet &, statet &)
pointer_typet pointer_type(const typet &subtype)
const irep_idt & id() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
A side_effect_exprt that returns a non-deterministically chosen value.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Extract member of struct or union.
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool has_prefix(const std::string &s, const std::string &prefix)
Operator to return the address of an object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A codet representing an assignment in the program.
const source_locationt & source_location() const
current_namest current_names
void set_component_name(const irep_idt &component_name)
irep_idt name
The unique identifier.