CBMC
instrument_contracts.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Instrument Contracts
4 
5 Author: 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 
19 class code_with_contract_typet;
20 class goto_modelt;
21 class namespacet;
22 
23 void instrument_contracts(goto_modelt &);
24 
25 std::optional<code_with_contract_typet>
26 get_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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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:94
instrument_contracts
void instrument_contracts(goto_modelt &)
Definition: instrument_contracts.cpp:552
get_contract
std::optional< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &)
Definition: instrument_contracts.cpp:27