CBMC
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 #include <util/irep.h>
18 
19 class goto_modelt;
20 class value_setst;
21 
22 void interrupt(
23  value_setst &,
24  goto_modelt &,
25  const irep_idt &interrupt_handler);
26 
27 #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:36
goto_modelt
Definition: goto_model.h:25
value_setst
Definition: value_sets.h:21
interrupt
void interrupt(value_setst &, goto_modelt &, const irep_idt &interrupt_handler)
Definition: interrupt.cpp:188
irep.h