CBMC
dfcc_contract_mode.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 Date: August 2022
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_MODE_H
14 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_MODE_H
15 
16 #include <string>
17 
20 {
21  CHECK,
22  REPLACE
23 };
24 
26 
27 std::ostream &operator<<(std::ostream &os, const dfcc_contract_modet mode);
28 
29 #endif
std::ostream & operator<<(std::ostream &os, const dfcc_contract_modet mode)
std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode)
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.