cprover
|
Go to the source code of this file.
Functions | |
static bool | has_start_thread (const goto_programt &goto_program) |
void | thread_exit_instrumentation (goto_programt &goto_program) |
void | thread_exit_instrumentation (goto_functionst &goto_functions) |
void | mutex_init_instrumentation (const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type) |
void | mutex_init_instrumentation (const symbol_tablet &symbol_table, goto_functionst &goto_functions) |
|
static |
Definition at line 14 of file thread_instrumentation.cpp.
References goto_program_templatet< codeT, guardT >::instructions.
Referenced by thread_exit_instrumentation().
void mutex_init_instrumentation | ( | const symbol_tablet & | symbol_table, |
goto_programt & | goto_program, | ||
typet | lock_type | ||
) |
Definition at line 85 of file thread_instrumentation.cpp.
References code_function_callt::arguments(), Forall_goto_program_instructions, code_function_callt::function(), goto_program_templatet< codeT, guardT >::insert_after(), code_assignt::lhs(), symbol_tablet::symbols, to_code_assign(), and exprt::type().
Referenced by goto_instrument_parse_optionst::doit(), goto_instrument_parse_optionst::instrument_goto_program(), and mutex_init_instrumentation().
void mutex_init_instrumentation | ( | const symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions | ||
) |
Definition at line 121 of file thread_instrumentation.cpp.
References Forall_goto_functions, irept::id(), mutex_init_instrumentation(), code_typet::parameters(), typet::subtype(), symbol_tablet::symbols, and to_code_type().
void thread_exit_instrumentation | ( | goto_programt & | goto_program | ) |
Definition at line 23 of file thread_instrumentation.cpp.
References goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, exprt::op0(), exprt::op1(), and pointer_type().
Referenced by goto_instrument_parse_optionst::doit(), goto_instrument_parse_optionst::instrument_goto_program(), and thread_exit_instrumentation().
void thread_exit_instrumentation | ( | goto_functionst & | goto_functions | ) |
Definition at line 56 of file thread_instrumentation.cpp.
References forall_goto_functions, code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, has_start_thread(), thread_exit_instrumentation(), to_code_function_call(), and to_symbol_expr().