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 const auto &assignment =
target->get_assign();
52 assign(assignment.lhs(), assignment.rhs());
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();
89 const std::string &suffix,
92 if(expr.
id()==ID_symbol)
114 else if(expr.
id()==ID_member)
117 const std::string &component_name =
118 id2string(member_expr.get_component_name());
120 member_expr.compound(),
123 "." + component_name + suffix,
126 else if(expr.
id()==ID_index)
130 read_write_rec(index_expr.array(),
r, w,
"[]" + suffix, guard_conjuncts);
131 read(index_expr.index(), guard_conjuncts);
133 else if(expr.
id()==ID_dereference)
140 const std::set<exprt> aliases=local_may.
get(
target, expr);
141 for(std::set<exprt>::const_iterator it=aliases.begin();
145 #ifndef LOCAL_MAY_SOUND
146 if(it->id()==ID_unknown)
171 else if(expr.
id()==ID_typecast)
175 else if(expr.
id()==ID_address_of)
179 else if(expr.
id()==ID_if)
182 read(if_expr.cond(), guard_conjuncts);
185 true_guard.push_back(if_expr.cond());
189 false_guard.push_back(
not_exprt(if_expr.cond()));
201 if(
function.
id()==ID_symbol)
205 goto_functionst::function_mapt::const_iterator f_it =
215 for(goto_functionst::function_mapt::const_iterator
218 local_may(g_it->second);
237 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
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 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.
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.
const irep_idt function_id
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)
std::vector< exprt > operandst
virtual void track_deref(const entryt &, bool read)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const irep_idt & get(const irep_namet &name) const
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
Race Detection for Threaded Goto Programs.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void write(const exprt &expr)
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 dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
API to expression classes.
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()