cprover
|
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, 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_setst & | value_sets |
symbol_tablet & | symbol_table |
shared_varst | shared_vars |
thread_local_varst | thread_local_vars |
Definition at line 22 of file concurrency.cpp.
|
protected |
Definition at line 72 of file concurrency.cpp.
|
protected |
Definition at line 75 of file concurrency.cpp.
|
inline |
Definition at line 25 of file concurrency.cpp.
|
protected |
Definition at line 200 of file concurrency.cpp.
Referenced by instrument().
|
protected |
Definition at line 182 of file concurrency.cpp.
References forall_goto_program_instructions, and goto_program.
Referenced by instrument().
|
protected |
Definition at line 140 of file concurrency.cpp.
References find_symbols(), symbol_exprt::get_identifier(), symbolt::is_state_var, symbolt::is_thread_local, namespacet::lookup(), shared_vars, symbol_table, thread_local_vars, to_symbol_expr(), symbolt::type, concurrency_instrumentationt::shared_vart::type, and concurrency_instrumentationt::thread_local_vart::type.
|
protected |
Definition at line 205 of file concurrency.cpp.
References add_array_symbols(), collect(), Forall_goto_functions, forall_goto_functions, and symbol_table.
Referenced by instrument(), and operator()().
|
protected |
Definition at line 112 of file concurrency.cpp.
References code_function_callt::arguments(), Forall_expr, code_function_callt::function(), goto_program, goto_programt::instructions, instrument(), code_assignt::rhs(), to_code_assign(), and to_code_function_call().
|
protected |
Definition at line 79 of file concurrency.cpp.
References find_symbols(), symbol_exprt::get_identifier(), replace_symbolt::insert(), shared_vars, and to_symbol_expr().
|
inline |
Definition at line 33 of file concurrency.cpp.
References instrument().
|
protected |
Definition at line 73 of file concurrency.cpp.
Referenced by collect(), and instrument().
|
protected |
Definition at line 40 of file concurrency.cpp.
Referenced by collect(), and instrument().
|
protected |
Definition at line 76 of file concurrency.cpp.
Referenced by collect().
|
protected |
Definition at line 39 of file concurrency.cpp.