14 #ifndef CPROVER_GOTO_INSTRUMENT_RW_SET_H 15 #define CPROVER_GOTO_INSTRUMENT_RW_SET_H 56 typedef std::unordered_map<irep_idt, entryt>
entriest;
87 void output(std::ostream &out)
const;
107 #define forall_rw_set_r_entries(it, rw_set) \ 108 for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \ 109 it!=(rw_set).r_entries.end(); it++) 111 #define forall_rw_set_w_entries(it, rw_set) \ 112 for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \ 113 it!=(rw_set).w_entries.end(); it++) 172 const std::string &suffix,
206 const exprt &
function):
208 ns(_goto_model.symbol_table),
288 #endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H _rw_set_loct(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
void swap(rw_set_baset &other)
rw_set_with_trackt(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
void output(std::ostream &out) const
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function)
std::map< const irep_idt, const irep_idt > dereferenced_from
virtual ~rw_set_baset()=default
virtual void reset_track_deref()
rw_set_baset & operator+=(const rw_set_baset &other)
void compute_rec(const exprt &function)
The Boolean constant true.
bool has_r_entry(irep_idt object) const
bool has_w_entry(irep_idt object) const
virtual void track_deref(const entryt &, bool read)
API to expression classes.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const goto_programt::const_targett target
A collection of goto functions.
std::set< irep_idt > set_reads
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const goto_functionst & goto_functions
A generic container class for the GOTO intermediate representation of one function.
std::vector< entryt > dereferenced
void read_write_rec(const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard)
void track_deref(const entryt &entry, bool read)
rw_set_baset(const namespacet &_ns)
Base class for all expressions.
Expression to hold a symbol (variable)
std::unordered_map< irep_idt, entryt > entriest
void assign(const exprt &lhs, const exprt &rhs)
void write(const exprt &expr)
virtual void set_track_deref()
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
void read(const exprt &expr, const guardt &guard)
void read(const exprt &expr)
Field-insensitive, location-sensitive may-alias analysis.