25 for(entriest::const_iterator it=
r_entries.begin();
29 out << it->second.object <<
" if "
30 <<
from_expr(
ns, it->second.object, it->second.guard) <<
'\n';
36 for(entriest::const_iterator it=
w_entries.begin();
40 out << it->second.object <<
" if "
41 <<
from_expr(
ns, it->second.object, it->second.guard) <<
'\n';
51 else if(
target->is_goto() ||
57 else if(
target->is_function_call())
62 for(code_function_callt::argumentst::const_iterator it =
63 target->call_arguments().begin();
64 it !=
target->call_arguments().end();
68 if(
target->call_lhs().is_not_nil())
83 const std::string &suffix,
86 if(expr.
id()==ID_symbol)
108 else if(expr.
id()==ID_member)
111 const std::string &component_name =
112 id2string(member_expr.get_component_name());
114 member_expr.compound(),
117 "." + component_name + suffix,
120 else if(expr.
id()==ID_index)
124 read_write_rec(index_expr.array(),
r, w,
"[]" + suffix, guard_conjuncts);
125 read(index_expr.index(), guard_conjuncts);
127 else if(expr.
id()==ID_dereference)
134 const std::set<exprt> aliases=local_may.
get(
target, expr);
135 for(std::set<exprt>::const_iterator it=aliases.begin();
139 #ifndef LOCAL_MAY_SOUND
140 if(it->id()==ID_unknown)
165 else if(expr.
id()==ID_typecast)
169 else if(expr.
id()==ID_address_of)
173 else if(expr.
id()==ID_if)
176 read(if_expr.cond(), guard_conjuncts);
179 true_guard.push_back(if_expr.cond());
183 false_guard.push_back(
not_exprt(if_expr.cond()));
188 for(
const auto &op : expr.
operands())
195 if(
function.
id()==ID_symbol)
199 goto_functionst::function_mapt::const_iterator f_it =
209 for(goto_functionst::function_mapt::const_iterator
212 local_may(g_it->second);
230 else if(
function.
id()==ID_if)
void assign(const exprt &lhs, const exprt &rhs)
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
const irep_idt function_id
void read(const exprt &expr)
void write(const exprt &expr)
const goto_programt::const_targett target
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
virtual void track_deref(const entryt &, bool read)
virtual void reset_track_deref()
void output(std::ostream &out) const
virtual void set_track_deref()
message_handlert & message_handler
const goto_functionst & goto_functions
void compute_rec(const exprt &function)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
#define forall_goto_program_instructions(it, program)
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Race Detection for Threaded Goto Programs.
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.