14 #ifndef CPROVER_ANALYSES_DIRTY_H 15 #define CPROVER_ANALYSES_DIRTY_H 17 #include <unordered_set> 30 "Uninitialized dirtyt. This dirtyt was constructed using the default " 31 "constructor and not subsequently initialized using " 55 build(goto_functions);
60 void output(std::ostream &out)
const;
99 std::unordered_set<irep_idt>
dirty;
136 #endif // CPROVER_ANALYSES_DIRTY_H void add_function(const goto_functiont &goto_function)
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
void find_dirty_address_of(const exprt &expr)
bool operator()(const irep_idt &id) const
void die_if_uninitialized() const
const irep_idt & get_identifier() const
Goto Programs with Functions.
goto_functionst::goto_functiont goto_functiont
#define INVARIANT(CONDITION, REASON)
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
void build(const goto_functionst &goto_functions)
API to expression classes.
::goto_functiont goto_functiont
bool operator()(const irep_idt &id) const
#define PRECONDITION(CONDITION)
bool operator()(const symbol_exprt &expr) const
dirtyt(const goto_functionst &goto_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.
void find_dirty(const exprt &expr)
const std::unordered_set< irep_idt > & get_dirty_ids() const
Base class for all expressions.
std::unordered_set< irep_idt > dirty
std::unordered_set< irep_idt > dirty_processed_functions
Expression to hold a symbol (variable)
#define forall_goto_functions(it, functions)
void output(std::ostream &out) const
dirtyt(const goto_functiont &goto_function)
bool operator()(const symbol_exprt &expr) const