14 #ifndef CPROVER_GOTO_INSTRUMENT_RW_SET_H 15 #define CPROVER_GOTO_INSTRUMENT_RW_SET_H 56 typedef std::unordered_map<irep_idt, entryt, irep_id_hash>
entriest;
74 return r_entries.empty() && w_entries.empty();
79 return w_entries.find(
object)!=w_entries.end();
84 return r_entries.find(
object)!=r_entries.end();
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++) 124 value_sets(_value_sets),
133 value_sets(_value_sets),
151 read_write_rec(expr,
true,
false,
"",
guardt());
156 read_write_rec(expr,
true,
false,
"", guard);
161 read_write_rec(expr,
false,
true,
"",
guardt());
166 void assign(
const exprt &lhs,
const exprt &rhs);
171 const std::string &suffix,
208 const exprt &
function):
210 value_sets(_value_sets),
211 goto_functions(_goto_functions)
213 compute_rec(
function);
222 void compute_rec(
const exprt &
function);
269 if(dereferencing && dereferenced.empty())
271 dereferenced.insert(dereferenced.begin(), entry);
273 set_reads.insert(entry.object);
275 else if(dereferencing && !dereferenced.empty())
276 dereferenced_from.insert(
277 std::make_pair(entry.object, dereferenced.front().object));
288 dereferenced.clear();
292 #endif // CPROVER_GOTO_INSTRUMENT_RW_SET_H _rw_set_loct(const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
virtual void track_deref(const entryt &entry, bool read)
void swap(rw_set_baset &other)
void output(std::ostream &out) const
rw_set_functiont(value_setst &_value_sets, const namespacet &_ns, const goto_functionst &_goto_functions, const exprt &function)
std::ostream & operator<<(std::ostream &out, const rw_set_baset &rw_set)
Goto Programs with Functions.
std::map< const irep_idt, const irep_idt > dereferenced_from
virtual void reset_track_deref()
rw_set_baset & operator+=(const rw_set_baset &other)
instructionst::const_iterator const_targett
The boolean constant true.
bool has_r_entry(irep_idt object) const
bool has_w_entry(irep_idt object) const
std::unordered_map< irep_idt, entryt, irep_id_hash > entriest
API to expression classes.
const goto_programt::const_targett target
std::set< irep_idt > set_reads
const goto_functionst & goto_functions
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
std::vector< entryt > dereferenced
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)
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.