Go to the documentation of this file.
26 if(src.
id()==ID_symbol)
28 symbol_tablet::symbolst::const_iterator s_it=
30 assert(s_it!=symbol_table.
symbols.end());
31 return is_volatile(symbol_table, s_it->second.type);
42 if(expr.
id()==ID_symbol ||
43 expr.
id()==ID_dereference)
52 expr.
swap(nondet_expr);
65 else if(expr.
id()==ID_index)
70 else if(expr.
id()==ID_member)
74 else if(expr.
id()==ID_dereference)
103 for(exprt::operandst::iterator
104 it=code_function_call.
arguments().begin();
105 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
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
const irep_idt & get_identifier() const
const irep_idt & id() const
void remove(const irep_namet &name)
const code_function_callt & to_code_function_call(const codet &code)
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
#define Forall_goto_functions(it, functions)
A side_effect_exprt that returns a non-deterministically chosen value.
bool is_volatile(const symbol_tablet &symbol_table, const typet &src)
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)
exprt guard
Guard for gotos, assume, assert.
A generic container class for the GOTO intermediate representation of one function.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
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.