cprover
interrupt.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Interrupt Instrumentation for Goto Programs
4
5
Author: Daniel Kroening
6
7
Date: September 2011
8
9
\*******************************************************************/
10
13
14
#ifndef CPROVER_GOTO_INSTRUMENT_INTERRUPT_H
15
#define CPROVER_GOTO_INSTRUMENT_INTERRUPT_H
16
17
class
goto_modelt
;
18
19
#include "
rw_set.h
"
20
21
void
interrupt
(
22
value_setst
&,
23
goto_modelt
&,
24
const
irep_idt
&interrupt_handler);
25
26
#endif // CPROVER_GOTO_INSTRUMENT_INTERRUPT_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
goto_modelt
Definition:
goto_model.h:26
value_setst
Definition:
value_sets.h:22
rw_set.h
Race Detection for Threaded Goto Programs.
interrupt
void interrupt(value_setst &, goto_modelt &, const irep_idt &interrupt_handler)
Definition:
interrupt.cpp:182
goto-instrument
interrupt.h
Generated by
1.8.20