CBMC
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 goto_modelt;
19 class namespacet;
20 
22 {
23 public:
25  : instrumentert(_goto_model, message)
26  {
27  }
28 
30  {
32  }
33 
34  /* collects directly all the pairs in the graph */
36  {
38  }
39 };
40 
41 #endif // CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
void collect_pairs_naive()
Definition: event_graph.h:584
void collect_pairs()
Definition: event_graph.h:578
instrumenter_pensievet(goto_modelt &_goto_model, messaget &message)
event_grapht egraph
Definition: goto2graph.h:309
messaget & message
Definition: goto2graph.h:306
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
graph of abstract events
Instrumenter.