cprover
|
#include <dirty.h>
Public Types | |
typedef std::unordered_set< irep_idt, irep_id_hash > | id_sett |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
dirtyt (const goto_functiont &goto_function) | |
dirtyt (const goto_functionst &goto_functions) | |
void | output (std::ostream &out) const |
bool | operator() (const irep_idt &id) const |
bool | operator() (const symbol_exprt &expr) const |
const id_sett & | get_dirty_ids () const |
Protected Member Functions | |
void | build (const goto_functiont &goto_function) |
void | find_dirty (const exprt &expr) |
void | find_dirty_address_of (const exprt &expr) |
Protected Attributes | |
id_sett | dirty |
typedef goto_functionst::goto_functiont dirtyt::goto_functiont |
typedef std::unordered_set<irep_idt, irep_id_hash> dirtyt::id_sett |
|
inlineexplicit |
|
inlineexplicit |
Definition at line 33 of file dirty.h.
References build(), forall_goto_functions, and output().
|
protected |
Definition at line 18 of file dirty.cpp.
References find_dirty(), and forall_goto_program_instructions.
Referenced by dirtyt(), and get_dirty_ids().
|
protected |
Definition at line 27 of file dirty.cpp.
References find_dirty_address_of(), forall_operands, irept::id(), address_of_exprt::object(), and to_address_of_expr().
Referenced by build(), and find_dirty_address_of().
|
protected |
Definition at line 40 of file dirty.cpp.
References dirty, find_dirty(), symbol_exprt::get_identifier(), irept::id(), to_dereference_expr(), to_if_expr(), to_index_expr(), to_member_expr(), and to_symbol_expr().
Referenced by find_dirty().
|
inline |
|
inline |
|
inline |
Definition at line 46 of file dirty.h.
References symbol_exprt::get_identifier(), and operator()().
void dirtyt::output | ( | std::ostream & | out | ) | const |
Definition at line 70 of file dirty.cpp.
References dirty.
Referenced by dirtyt(), and operator<<().
|
protected |
Definition at line 60 of file dirty.h.
Referenced by find_dirty_address_of(), get_dirty_ids(), operator()(), and output().