cprover
Loading...
Searching...
No Matches
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_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)
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 23 of file concurrency.cpp.

Member Typedef Documentation

◆ shared_varst

Definition at line 71 of file concurrency.cpp.

◆ thread_local_varst

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: