14 #ifndef CPROVER_ANALYSES_DIRTY_H
15 #define CPROVER_ANALYSES_DIRTY_H
22 #include <unordered_set>
34 "Uninitialized dirtyt. This dirtyt was constructed using the default "
35 "constructor and not subsequently initialized using "
59 build(goto_functions);
64 void output(std::ostream &out)
const;
95 build(gf_entry.second);
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
bool operator()(const symbol_exprt &expr) const
void add_function(const goto_functiont &goto_function)
void build(const goto_functionst &goto_functions)
void find_dirty(const exprt &expr)
bool operator()(const irep_idt &id) const
const std::unordered_set< irep_idt > & get_dirty_ids() const
void find_dirty_address_of(const exprt &expr)
void output(std::ostream &out) const
dirtyt(const goto_functionst &goto_functions)
std::unordered_set< irep_idt > dirty
dirtyt(const goto_functiont &goto_function)
void search_other(const goto_programt::instructiont &instruction)
void die_if_uninitialized() const
goto_functionst::goto_functiont goto_functiont
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
bool operator()(const symbol_exprt &expr) const
std::unordered_set< irep_idt > dirty_processed_functions
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.
bool operator()(const irep_idt &id) const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Goto Programs with Functions.
#define PRECONDITION(CONDITION)
API to expression classes.