cprover
instrumenter_pensieve.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Instrumenter
4 
5 Author:
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
13 #define CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
14 
15 #include "event_graph.h"
16 #include "goto2graph.h"
17 
18 class symbol_tablet;
19 class goto_functionst;
20 class namespacet;
21 
23 {
24 public:
26  goto_functionst &_goto_f, messaget &message)
27  : instrumentert(_symbol_table, _goto_f, message)
28  {
29  }
30 
32  {
34  }
35 
36  /* collects directly all the pairs in the graph */
38  {
40  }
41 };
42 
43 #endif // CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
void collect_pairs(namespacet &ns)
Definition: event_graph.h:540
messaget & message
Definition: goto2graph.h:280
instrumenter_pensievet(symbol_tablet &_symbol_table, goto_functionst &_goto_f, messaget &message)
graph of abstract events
namespacet ns
Definition: goto2graph.h:37
Instrumenter.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void collect_pairs_naive(namespacet &ns)
void collect_pairs_naive(namespacet &ns)
Definition: event_graph.h:546
void collect_pairs(namespacet &ns)
event_grapht egraph
Definition: goto2graph.h:283