Go to the documentation of this file.
27 for(entriest::const_iterator it=
r_entries.begin();
31 out << it->second.object <<
" if "
32 <<
from_expr(
ns, it->second.object, it->second.guard) <<
'\n';
38 for(entriest::const_iterator it=
w_entries.begin();
42 out << it->second.object <<
" if "
43 <<
from_expr(
ns, it->second.object, it->second.guard) <<
'\n';
51 assert(
target->code.operands().size()==2);
54 else if(
target->is_goto() ||
60 else if(
target->is_function_call())
68 for(code_function_callt::argumentst::const_iterator
69 it=code_function_call.
arguments().begin();
88 const std::string &suffix,
91 if(expr.
id()==ID_symbol)
117 else if(expr.
id()==ID_member)
120 const std::string &component_name=expr.
get_string(ID_component_name);
123 else if(expr.
id()==ID_index)
130 else if(expr.
id()==ID_dereference)
138 const std::set<exprt> aliases=local_may.
get(
target, expr);
139 for(std::set<exprt>::const_iterator it=aliases.begin();
143 #ifndef LOCAL_MAY_SOUND
144 if(it->id()==ID_unknown)
169 else if(expr.
id()==ID_typecast)
174 else if(expr.
id()==ID_address_of)
178 else if(expr.
id()==ID_if)
184 true_guard.add(expr.
op0());
187 guardt false_guard(guard);
200 if(
function.
id()==ID_symbol)
204 goto_functionst::function_mapt::const_iterator f_it=
214 for(goto_functionst::function_mapt::const_iterator
217 local_may(g_it->second);
231 else if(
function.
id()==ID_if)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const goto_functionst & goto_functions
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
void assign(const exprt &lhs, const exprt &rhs)
const goto_programt::const_targett target
Base class for all expressions.
void compute_rec(const exprt &function)
void read(const exprt &expr)
function_mapt function_map
Expression to hold a symbol (variable)
virtual void reset_track_deref()
codet representation of a function call statement.
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard)
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
const irep_idt & get_identifier() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
virtual void track_deref(const entryt &, bool read)
const std::string & get_string(const irep_namet &name) const
const irep_idt & get(const irep_namet &name) const
void write(const exprt &expr)
A generic container class for the GOTO intermediate representation of one function.
exprt dereference(const exprt &pointer, const namespacet &ns)
Dereference the given pointer-expression.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void output(std::ostream &out) const
#define forall_goto_program_instructions(it, program)
virtual void set_track_deref()