CBMC
thread_instrumentation.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#ifndef CPROVER_GOTO_INSTRUMENT_THREAD_INSTRUMENTATION_H
11
#define CPROVER_GOTO_INSTRUMENT_THREAD_INSTRUMENTATION_H
12
13
class
goto_modelt
;
14
15
void
thread_exit_instrumentation
(
goto_modelt
&);
16
void
mutex_init_instrumentation
(
goto_modelt
&);
17
18
#endif // CPROVER_GOTO_INSTRUMENT_THREAD_INSTRUMENTATION_H
goto_modelt
Definition:
goto_model.h:25
thread_exit_instrumentation
void thread_exit_instrumentation(goto_modelt &)
Definition:
thread_instrumentation.cpp:56
mutex_init_instrumentation
void mutex_init_instrumentation(goto_modelt &)
Definition:
thread_instrumentation.cpp:112
src
goto-instrument
thread_instrumentation.h
Generated by
1.8.17