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