CBMC
Loading...
Searching...
No Matches
instrumenter_pensieve.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrumenter
4
5Author:
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
18class goto_modelt;
19class namespacet;
20
22{
23public:
28
33
34 /* collects directly all the pairs in the graph */
36 {
38 }
39};
40
41#endif // CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void collect_pairs_naive()
void collect_pairs()
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:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
graph of abstract events
Instrumenter.