CBMC
Loading...
Searching...
No Matches
interrupt.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interrupt Instrumentation for Goto Programs
4
5Author: Daniel Kroening
6
7Date: 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
19class goto_modelt;
20class message_handlert;
21class value_setst;
22
23void interrupt(
24 value_setst &,
25 goto_modelt &,
26 const irep_idt &interrupt_handler,
27 message_handlert &);
28
29#endif // CPROVER_GOTO_INSTRUMENT_INTERRUPT_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:27
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