CBMC
|
Dirty variables are ones which have their address taken so we can't reliably work out where they may be assigned and are also considered shared state in the presence of multi-threading. More...
#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 | search_other (const goto_programt::instructiont &instruction) |
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 |
Dirty variables are ones which have their address taken so we can't reliably work out where they may be assigned and are also considered shared state in the presence of multi-threading.
|
inline |
|
inlineexplicit |
|
inlineexplicit |
|
inline |
|
inline |
|
protected |
|
protected |
|
inline |
|
inline |
|
protected |