cprover
|
#include <dirty.h>
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
dirtyt () | |
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 std::unordered_set< irep_idt > & | get_dirty_ids () const |
void | add_function (const goto_functiont &goto_function) |
void | build (const goto_functionst &goto_functions) |
Public Attributes | |
bool | initialized |
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 | |
std::unordered_set< irep_idt > | dirty |
Private Member Functions | |
void | die_if_uninitialized () const |
|
inline |
|
inlineexplicit |
Definition at line 47 of file dirty.h.
References build(), and initialized.
|
inlineexplicit |
|
inline |
Definition at line 80 of file dirty.h.
References build(), and initialized.
Referenced by incremental_dirtyt::populate_dirty_for_function().
|
inline |
Definition at line 86 of file dirty.h.
References forall_goto_functions, initialized, and PRECONDITION.
Referenced by add_function(), and dirtyt().
|
protected |
Definition at line 18 of file dirty.cpp.
References goto_functiont::body, find_dirty(), and forall_goto_program_instructions.
|
inlineprivate |
Definition at line 26 of file dirty.h.
References initialized, and INVARIANT.
Referenced by get_dirty_ids(), operator()(), and output().
|
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 |
Definition at line 74 of file dirty.h.
References die_if_uninitialized(), and dirty.
|
inline |
Definition at line 62 of file dirty.h.
References die_if_uninitialized(), and dirty.
Referenced by operator()().
|
inline |
Definition at line 68 of file dirty.h.
References die_if_uninitialized(), symbol_exprt::get_identifier(), and operator()().
void dirtyt::output | ( | std::ostream & | out | ) | const |
Definition at line 70 of file dirty.cpp.
References die_if_uninitialized(), and dirty.
Referenced by operator<<().
|
protected |
Definition at line 99 of file dirty.h.
Referenced by find_dirty_address_of(), get_dirty_ids(), operator()(), and output().
bool dirtyt::initialized |
Definition at line 36 of file dirty.h.
Referenced by add_function(), build(), die_if_uninitialized(), and dirtyt().