CBMC
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
concurrency_instrumentationt Class Reference
+ Collaboration diagram for concurrency_instrumentationt:

Classes

class  shared_vart
 
class  thread_local_vart
 

Public Member Functions

 concurrency_instrumentationt (value_setst &_value_sets, symbol_tablet &_symbol_table)
 
void operator() (goto_functionst &goto_functions)
 

Protected Types

typedef std::map< irep_idt, shared_vart > shared_varst
 
typedef std::map< irep_idt, thread_local_vart > thread_local_varst
 

Protected Member Functions

void instrument (goto_functionst &goto_functions)
 
void instrument (goto_programt &goto_program)
 
void instrument (exprt &expr)
 
void collect (const goto_programt &goto_program, const is_threadedt &is_threaded)
 
void collect (const exprt &expr)
 
void add_array_symbols ()
 

Protected Attributes

value_setst & value_sets
 
symbol_tablet & symbol_table
 
shared_varst shared_vars
 
thread_local_varst thread_local_vars
 

Detailed Description

Definition at line 23 of file concurrency.cpp.

Member Typedef Documentation

◆ shared_varst

typedef std::map<irep_idt, shared_vart> concurrency_instrumentationt::shared_varst
protected

Definition at line 71 of file concurrency.cpp.

◆ thread_local_varst

typedef std::map<irep_idt, thread_local_vart> concurrency_instrumentationt::thread_local_varst
protected

Definition at line 74 of file concurrency.cpp.

Constructor & Destructor Documentation

◆ concurrency_instrumentationt()

concurrency_instrumentationt::concurrency_instrumentationt ( value_setst &  _value_sets,
symbol_tablet &  _symbol_table 
)
inline

Definition at line 26 of file concurrency.cpp.

Member Function Documentation

◆ add_array_symbols()

void concurrency_instrumentationt::add_array_symbols ( )
protected

Definition at line 168 of file concurrency.cpp.

◆ collect() [1/2]

void concurrency_instrumentationt::collect ( const exprt &  expr)
protected

Definition at line 128 of file concurrency.cpp.

◆ collect() [2/2]

void concurrency_instrumentationt::collect ( const goto_programt &  goto_program,
const is_threadedt &  is_threaded 
)
protected

Definition at line 157 of file concurrency.cpp.

◆ instrument() [1/3]

void concurrency_instrumentationt::instrument ( exprt &  expr)
protected

Definition at line 78 of file concurrency.cpp.

◆ instrument() [2/3]

void concurrency_instrumentationt::instrument ( goto_functionst &  goto_functions)
protected

Definition at line 173 of file concurrency.cpp.

◆ instrument() [3/3]

void concurrency_instrumentationt::instrument ( goto_programt &  goto_program)
protected

Definition at line 100 of file concurrency.cpp.

◆ operator()()

void concurrency_instrumentationt::operator() ( goto_functionst &  goto_functions)
inline

Definition at line 34 of file concurrency.cpp.

Member Data Documentation

◆ shared_vars

shared_varst concurrency_instrumentationt::shared_vars
protected

Definition at line 72 of file concurrency.cpp.

◆ symbol_table

symbol_tablet& concurrency_instrumentationt::symbol_table
protected

Definition at line 41 of file concurrency.cpp.

◆ thread_local_vars

thread_local_varst concurrency_instrumentationt::thread_local_vars
protected

Definition at line 75 of file concurrency.cpp.

◆ value_sets

value_setst& concurrency_instrumentationt::value_sets
protected

Definition at line 40 of file concurrency.cpp.

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