cprover
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 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 26 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 46 of file dirty.h.

◆ dirtyt() [2/3]

dirtyt::dirtyt ( const goto_functiont goto_function)
inlineexplicit

Definition at line 50 of file dirty.h.

◆ dirtyt() [3/3]

dirtyt::dirtyt ( const goto_functionst goto_functions)
inlineexplicit

Definition at line 56 of file dirty.h.

Member Function Documentation

◆ add_function()

void dirtyt::add_function ( const goto_functiont goto_function)
inline

Definition at line 83 of file dirty.h.

◆ build() [1/2]

void dirtyt::build ( const goto_functionst goto_functions)
inline

Definition at line 89 of file dirty.h.

◆ build() [2/2]

void dirtyt::build ( const goto_functiont goto_function)
protected

Definition at line 18 of file dirty.cpp.

◆ die_if_uninitialized()

void dirtyt::die_if_uninitialized ( ) const
inlineprivate

Definition at line 29 of file dirty.h.

◆ find_dirty()

void dirtyt::find_dirty ( const exprt expr)
protected

Definition at line 24 of file dirty.cpp.

◆ find_dirty_address_of()

void dirtyt::find_dirty_address_of ( const exprt expr)
protected

Definition at line 37 of file dirty.cpp.

◆ get_dirty_ids()

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

Definition at line 77 of file dirty.h.

◆ operator()() [1/2]

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

Definition at line 65 of file dirty.h.

◆ operator()() [2/2]

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

Definition at line 71 of file dirty.h.

◆ output()

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

Definition at line 67 of file dirty.cpp.

Member Data Documentation

◆ dirty

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

Definition at line 102 of file dirty.h.

◆ initialized

bool dirtyt::initialized

Definition at line 39 of file dirty.h.


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