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;
176 const std::string &suffix,
220 const exprt &
function,
223 ns(_goto_model.symbol_table),
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)
_rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
void read(const exprt &expr, 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
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
rw_set_baset & operator+=(const rw_set_baset &other)
bool has_w_entry(irep_idt object) const
bool has_r_entry(irep_idt object) const
virtual void track_deref(const entryt &, bool read)
std::unordered_map< irep_idt, entryt > entriest
virtual void reset_track_deref()
rw_set_baset(const namespacet &_ns, message_handlert &message_handler)
void swap(rw_set_baset &other)
void output(std::ostream &out) const
virtual void set_track_deref()
message_handlert & message_handler
virtual ~rw_set_baset()=default
const goto_functionst & goto_functions
void compute_rec(const exprt &function)
rw_set_functiont(value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function, message_handlert &message_handler)
rw_set_loct(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
std::map< const irep_idt, const irep_idt > dereferenced_from
rw_set_with_trackt(const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
std::vector< entryt > dereferenced
void track_deref(const entryt &entry, bool read)
std::set< irep_idt > set_reads
Expression to hold a symbol (variable)
int __CPROVER_ID java::java io InputStream read
Field-insensitive, location-sensitive may-alias analysis.
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
API to expression classes.
entryt(const symbol_exprt &_symbol_expr, const irep_idt &_object, const exprt &_guard)