Go to the documentation of this file.
14 #ifndef CPROVER_ANALYSES_DIRTY_H
15 #define CPROVER_ANALYSES_DIRTY_H
17 #include <unordered_set>
33 "Uninitialized dirtyt. This dirtyt was constructed using the default "
34 "constructor and not subsequently initialized using "
58 build(goto_functions);
63 void output(std::ostream &out)
const;
139 #endif // CPROVER_ANALYSES_DIRTY_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool operator()(const irep_idt &id) const
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
dirtyt(const goto_functiont &goto_function)
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
void add_function(const goto_functiont &goto_function)
Base class for all expressions.
bool operator()(const irep_idt &id) const
const std::unordered_set< irep_idt > & get_dirty_ids() const
void build(const goto_functionst &goto_functions)
dirtyt(const goto_functionst &goto_functions)
Expression to hold a symbol (variable)
void find_dirty(const exprt &expr)
goto_functionst::goto_functiont goto_functiont
std::unordered_set< irep_idt > dirty_processed_functions
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
std::unordered_set< irep_idt > dirty
A goto function, consisting of function type (see type), function body (see body),...
bool operator()(const symbol_exprt &expr) const
::goto_functiont goto_functiont
A collection of goto functions.
void output(std::ostream &out) const
void die_if_uninitialized() const
bool operator()(const symbol_exprt &expr) const
Goto Programs with Functions.
#define forall_goto_functions(it, functions)
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
API to expression classes.
void find_dirty_address_of(const exprt &expr)