Go to the documentation of this file.
25 src.
id() == ID_struct_tag || src.
id() == ID_union_tag ||
26 src.
id() == ID_c_enum_tag)
39 if(expr.
id()==ID_symbol ||
40 expr.
id()==ID_dereference)
50 expr.
swap(nondet_expr);
63 else if(expr.
id()==ID_index)
68 else if(expr.
id()==ID_member)
72 else if(expr.
id()==ID_dereference)
101 for(exprt::operandst::iterator
102 it=code_function_call.
arguments().begin();
103 it!=code_function_call.
arguments().end();
#define Forall_goto_program_instructions(it, program)
#define Forall_operands(it, expr)
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Base class for all expressions.
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
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.
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
codet code
Do not read or modify directly – use get_X() instead.
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
bool has_condition() const
Does this instruction have a condition?
const irep_idt & id() const
void remove(const irep_namet &name)
const code_function_callt & to_code_function_call(const codet &code)
#define Forall_goto_functions(it, functions)
A side_effect_exprt that returns a non-deterministically chosen value.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
goto_functionst goto_functions
GOTO functions.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A generic container class for the GOTO intermediate representation of one function.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
static bool is_volatile(const namespacet &ns, const typet &src)
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
bool is_function_call() const
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.