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 message_handlert;
21 class value_setst;
22 
23 void interrupt(
24  value_setst &,
25  goto_modelt &,
26  const irep_idt &interrupt_handler,
27  message_handlert &);
28 
29 #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:38
goto_modelt
Definition: goto_model.h:27
message_handlert
Definition: message.h:28
value_setst
Definition: value_sets.h:22
interrupt
void interrupt(value_setst &, goto_modelt &, const irep_idt &interrupt_handler, message_handlert &)
Definition: interrupt.cpp:188