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
17#include <optional>
18
19class code_with_contract_typet;
20class goto_modelt;
21class namespacet;
22
23void instrument_contracts(goto_modelt &);
24
25std::optional<code_with_contract_typet>
26get_contract(const irep_idt &function_identifier, const namespacet &);
27
28#endif // CPROVER_CPOVER_INSTRUMENT_CONTRACTS_H
code_with_contract_typet
Definition c_types.h:391
goto_modelt
Definition goto_model.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
get_contract
std::optional< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &)
Definition instrument_contracts.cpp:27
instrument_contracts
void instrument_contracts(goto_modelt &)
Definition instrument_contracts.cpp:552
irep_idt
dstringt irep_idt
Definition verification_result.h:16