cprover
concurrency_instrumentationt Class Reference
Collaboration diagram for concurrency_instrumentationt:
[legend]

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_vartshared_varst
 
typedef std::map< irep_idt, thread_local_vartthread_local_varst
 

Protected Member Functions

void instrument (goto_functionst &goto_functions)
 
void instrument (goto_programt &goto_program, const is_threadedt &is_threaded)
 
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_setstvalue_sets
 
symbol_tabletsymbol_table
 
shared_varst shared_vars
 
thread_local_varst thread_local_vars
 

Detailed Description

Definition at line 22 of file concurrency.cpp.

Member Typedef Documentation

§ shared_varst

Definition at line 72 of file concurrency.cpp.

§ thread_local_varst

Definition at line 75 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 25 of file concurrency.cpp.

Member Function Documentation

§ add_array_symbols()

void concurrency_instrumentationt::add_array_symbols ( )
protected

Definition at line 200 of file concurrency.cpp.

Referenced by instrument().

§ collect() [1/2]

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

Definition at line 182 of file concurrency.cpp.

References forall_goto_program_instructions.

Referenced by instrument().

§ collect() [2/2]

§ instrument() [1/3]

void concurrency_instrumentationt::instrument ( goto_functionst goto_functions)
protected

§ instrument() [2/3]

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

§ instrument() [3/3]

void concurrency_instrumentationt::instrument ( exprt expr)
protected

§ operator()()

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

Definition at line 33 of file concurrency.cpp.

References instrument().

Member Data Documentation

§ shared_vars

shared_varst concurrency_instrumentationt::shared_vars
protected

Definition at line 73 of file concurrency.cpp.

Referenced by collect(), and instrument().

§ symbol_table

symbol_tablet& concurrency_instrumentationt::symbol_table
protected

Definition at line 40 of file concurrency.cpp.

Referenced by collect(), and instrument().

§ thread_local_vars

thread_local_varst concurrency_instrumentationt::thread_local_vars
protected

Definition at line 76 of file concurrency.cpp.

Referenced by collect().

§ value_sets

value_setst& concurrency_instrumentationt::value_sets
protected

Definition at line 39 of file concurrency.cpp.


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