CBMC
dirtyt Class Reference

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>

+ Collaboration diagram for dirtyt:

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_idtdirty
 

Private Member Functions

void die_if_uninitialized () const
 

Detailed Description

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.

Definition at line 27 of file dirty.h.

Member Typedef Documentation

◆ goto_functiont

Constructor & Destructor Documentation

◆ dirtyt() [1/3]

dirtyt::dirtyt ( )
inline
Postcondition
dirtyt objects that are created through this constructor are not safe to use. If you copied a dirtyt (for example, by adding an object that owns a dirtyt to a container and then copying it back out), you will need to re-initialize the dirtyt by calling dirtyt::build().

Definition at line 47 of file dirty.h.

◆ dirtyt() [2/3]

dirtyt::dirtyt ( const goto_functiont goto_function)
inlineexplicit

Definition at line 51 of file dirty.h.

◆ dirtyt() [3/3]

dirtyt::dirtyt ( const goto_functionst goto_functions)
inlineexplicit

Definition at line 57 of file dirty.h.

Member Function Documentation

◆ add_function()

void dirtyt::add_function ( const goto_functiont goto_function)
inline

Definition at line 84 of file dirty.h.

◆ build() [1/2]

void dirtyt::build ( const goto_functionst goto_functions)
inline

Definition at line 90 of file dirty.h.

◆ build() [2/2]

void dirtyt::build ( const goto_functiont goto_function)
protected

Definition at line 19 of file dirty.cpp.

◆ die_if_uninitialized()

void dirtyt::die_if_uninitialized ( ) const
inlineprivate

Definition at line 30 of file dirty.h.

◆ find_dirty()

void dirtyt::find_dirty ( const exprt expr)
protected

Definition at line 60 of file dirty.cpp.

◆ find_dirty_address_of()

void dirtyt::find_dirty_address_of ( const exprt expr)
protected

Definition at line 73 of file dirty.cpp.

◆ get_dirty_ids()

const std::unordered_set<irep_idt>& dirtyt::get_dirty_ids ( ) const
inline

Definition at line 78 of file dirty.h.

◆ operator()() [1/2]

bool dirtyt::operator() ( const irep_idt id) const
inline

Definition at line 66 of file dirty.h.

◆ operator()() [2/2]

bool dirtyt::operator() ( const symbol_exprt expr) const
inline

Definition at line 72 of file dirty.h.

◆ output()

void dirtyt::output ( std::ostream &  out) const

Definition at line 102 of file dirty.cpp.

◆ search_other()

void dirtyt::search_other ( const goto_programt::instructiont instruction)
protected

Definition at line 34 of file dirty.cpp.

Member Data Documentation

◆ dirty

std::unordered_set<irep_idt> dirtyt::dirty
protected

Definition at line 103 of file dirty.h.

◆ initialized

bool dirtyt::initialized

Definition at line 40 of file dirty.h.


The documentation for this class was generated from the following files: