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;
104 #define forall_rw_set_r_entries(it, rw_set) \ 105 for(rw_set_baset::entriest::const_iterator it=(rw_set).r_entries.begin(); \ 106 it!=(rw_set).r_entries.end(); it++) 108 #define forall_rw_set_w_entries(it, rw_set) \ 109 for(rw_set_baset::entriest::const_iterator it=(rw_set).w_entries.begin(); \ 110 it!=(rw_set).w_entries.end(); it++) 169 const std::string &suffix,
203 const exprt &
function):
205 ns(_goto_model.symbol_table),
270 std::make_pair(entry.object,
dereferenced.front().object));
285 #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
const goto_programt::const_targett target
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.