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();
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
exprt guard
Guard for gotos, assume, assert.
The type of an expression.
bool is_function_call() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
symbol_tablet symbol_table
Symbol table.
bool get_bool(const irep_namet &name) const
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
This class represents an instruction in the GOTO intermediate representation.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
API to expression classes.
void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
A generic container class for the GOTO intermediate representation of one function.
Base class for all expressions.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
#define Forall_operands(it, expr)
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
void remove(const irep_namet &name)
bool is_volatile(const symbol_tablet &symbol_table, const typet &src)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
goto_functionst goto_functions
GOTO functions.
const code_function_callt & to_code_function_call(const codet &code)