#include "thread_instrumentation.h"
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/string_constant.h>
#include <goto-programs/goto_model.h>

Include dependency graph for thread_instrumentation.cpp:

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)

Function Documentation

◆ has_start_thread()

static bool has_start_thread ( const goto_programt & goto_program )

static

Definition at line 17 of file thread_instrumentation.cpp.

◆ mutex_init_instrumentation() [1/2]

void mutex_init_instrumentation	(	const symbol_tablet &	symbol_table,
		goto_programt &	goto_program,
		typet	lock_type
	)

Definition at line 80 of file thread_instrumentation.cpp.

◆ mutex_init_instrumentation() [2/2]

void mutex_init_instrumentation ( goto_modelt & goto_model )

Definition at line 109 of file thread_instrumentation.cpp.

◆ thread_exit_instrumentation() [1/2]

void thread_exit_instrumentation ( goto_modelt & goto_model )

Definition at line 53 of file thread_instrumentation.cpp.

◆ thread_exit_instrumentation() [2/2]

void thread_exit_instrumentation ( goto_programt & goto_program )