Go to the documentation of this file.
14 #ifndef CPROVER_GOTO_INSTRUMENT_RW_SET_H
15 #define CPROVER_GOTO_INSTRUMENT_RW_SET_H
59 typedef std::unordered_map<irep_idt, entryt>
entriest;
90 void output(std::ostream &out)
const;
110 #define forall_rw_set_r_entries(it, rw_set) \
111 for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \
112 it!=(rw_set).r_entries.end(); it++)
114 #define forall_rw_set_w_entries(it, rw_set) \
115 for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \
116 it!=(rw_set).w_entries.end(); it++)
181 const std::string &suffix,
195 :
_rw_set_loct(_ns, _value_sets, _function_id, _target, may)
217 const exprt &
function):
219 ns(_goto_model.symbol_table),
256 :
_rw_set_loct(_ns, _value_sets, _function_id, _target, may),
264 :
_rw_set_loct(_ns, _value_sets, _function_id, _target),
301 #endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function)
std::vector< entryt > dereferenced
const goto_functionst & goto_functions
rw_set_baset(const namespacet &_ns)
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
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)
Expression to hold a symbol (variable)
virtual ~rw_set_baset()=default
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
virtual void reset_track_deref()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void track_deref(const entryt &entry, bool read)
rw_set_with_trackt(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
const irep_idt function_id
Field-insensitive, location-sensitive may-alias analysis.
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
void swap(rw_set_baset &other)
std::vector< exprt > operandst
virtual void track_deref(const entryt &, bool read)
entryt(const symbol_exprt &_symbol_expr, const irep_idt &_object, const exprt &_guard)
A collection of goto functions.
bool has_w_entry(irep_idt object) const
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const exprt::operandst &guard_conjuncts)
std::map< const irep_idt, const irep_idt > dereferenced_from
void write(const exprt &expr)
std::unordered_map< irep_idt, entryt > entriest
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
rw_set_baset & operator+=(const rw_set_baset &other)
bool has_r_entry(irep_idt object) const
void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
API to expression classes.
std::set< irep_idt > set_reads
void output(std::ostream &out) const
virtual void set_track_deref()