27 for(entriest::const_iterator it=
r_entries.begin();
31 out << it->second.object <<
" if " 38 for(entriest::const_iterator it=
w_entries.begin();
42 out << it->second.object <<
" if " 49 if(target->is_assign())
51 assert(target->code.operands().size()==2);
52 assign(target->code.op0(), target->code.op1());
54 else if(target->is_goto() ||
55 target->is_assume() ||
60 else if(target->is_function_call())
68 for(code_function_callt::argumentst::const_iterator
69 it=code_function_call.
arguments().begin();
75 write(code_function_call.
lhs());
82 read_write_rec(lhs,
false,
true,
"",
guardt());
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);
121 read_write_rec(expr.
op0(),
r, w,
"."+component_name+suffix, guard);
123 else if(expr.
id()==ID_index)
127 read_write_rec(expr.
op0(),
r, w,
"[]"+suffix, guard);
128 read(expr.
op1(), guard);
130 else if(expr.
id()==ID_dereference)
134 read(expr.
op0(), guard);
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)
159 read_write_rec(*it, r, w, suffix, guard);
164 read_write_rec(tmp, r, w, suffix, guard);
169 else if(expr.
id()==ID_typecast)
172 read_write_rec(expr.
op0(),
r, w, suffix, guard);
174 else if(expr.
id()==ID_address_of)
178 else if(expr.
id()==ID_if)
181 read(expr.
op0(), guard);
184 true_guard.add(expr.
op0());
185 read_write_rec(expr.
op1(),
r, w, suffix, true_guard);
187 guardt false_guard(guard);
189 read_write_rec(expr.
op2(),
r, w, suffix, false_guard);
194 read_write_rec(*it, r, w, suffix, guard);
200 if(
function.
id()==ID_symbol)
204 goto_functionst::function_mapt::const_iterator f_it=
205 goto_functions.function_map.find(
id);
207 if(f_it!=goto_functions.function_map.end())
214 for(goto_functionst::function_mapt::const_iterator
215 g_it=goto_functions.function_map.begin();
216 g_it!=goto_functions.function_map.end(); ++g_it)
217 local_may(g_it->second);
231 else if(
function.
id()==ID_if)
233 compute_rec(
to_if_expr(
function).true_case());
234 compute_rec(
to_if_expr(
function).false_case());
virtual void track_deref(const entryt &entry, bool read)
const std::string & id2string(const irep_idt &d)
void output(std::ostream &out) const
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
virtual void reset_track_deref()
void compute_rec(const exprt &function)
const irep_idt & id() const
exprt dereference(const exprt &pointer, const namespacet &ns)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
#define forall_operands(it, expr)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const std::string & get_string(const irep_namet &name) const
Expression to hold a symbol (variable)
void assign(const exprt &lhs, const exprt &rhs)
virtual void set_track_deref()
#define forall_goto_program_instructions(it, program)
const code_function_callt & to_code_function_call(const codet &code)
Race Detection for Threaded Goto Programs.