cprover
|
#include "thread_instrumentation.h"
#include <util/c_types.h>
#include <util/string_constant.h>
#include <goto-programs/goto_model.h>
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_modelt &goto_model) |
void | mutex_init_instrumentation (const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type) |
void | mutex_init_instrumentation (goto_modelt &goto_model) |
|
static |
Definition at line 16 of file thread_instrumentation.cpp.
References goto_program, and goto_programt::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, goto_programt::insert_after(), code_assignt::lhs(), goto_modelt::symbol_table, symbol_table_baset::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 | ( | goto_modelt & | goto_model | ) |
Definition at line 121 of file thread_instrumentation.cpp.
References Forall_goto_functions, goto_modelt::goto_functions, irept::id(), mutex_init_instrumentation(), code_typet::parameters(), typet::subtype(), goto_modelt::symbol_table, symbol_table_baset::symbols, and to_code_type().
void thread_exit_instrumentation | ( | goto_programt & | goto_program | ) |
Definition at line 25 of file thread_instrumentation.cpp.
References goto_program, goto_programt::insert_before_swap(), goto_programt::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_modelt & | goto_model | ) |
Definition at line 57 of file thread_instrumentation.cpp.
References forall_goto_functions, code_function_callt::function(), goto_functionst::function_map, goto_modelt::goto_functions, has_start_thread(), thread_exit_instrumentation(), to_code_function_call(), and to_symbol_expr().