12#ifndef CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
13#define CPROVER_GOTO_INSTRUMENT_WMM_INSTRUMENTER_PENSIEVE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void collect_pairs_naive()
instrumenter_pensievet(goto_modelt &_goto_model, messaget &message)
void collect_pairs_naive()
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...