cprover
Loading...
Searching...
No Matches
instrument_contracts.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument Contracts
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CPROVER_INSTRUMENT_CONTRACTS_H
13#define CPROVER_CPROVER_INSTRUMENT_CONTRACTS_H
14
15#include <util/irep.h>
16#include <util/optional.h>
17
19class goto_modelt;
20class namespacet;
21
23
25get_contract(const irep_idt &function_identifier, const namespacet &);
26
27#endif // CPROVER_CPOVER_INSTRUMENT_CONTRACTS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
optionalt< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &)
void instrument_contracts(goto_modelt &)