CBMC
dfcc_contract_mode.cpp
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 
7 Date: March 2023
8 
9 \*******************************************************************/
10 
11 #include "dfcc_contract_mode.h"
12 
13 #include <util/invariant.h>
14 
16 {
17  switch(mode)
18  {
20  return "dfcc_contract_modet::CHECK";
22  return "dfcc_contract_modet::REPLACE";
23  }
25 }
26 
27 std::ostream &operator<<(std::ostream &os, const dfcc_contract_modet mode)
28 {
29  os << dfcc_contract_mode_to_string(mode);
30  return os;
31 }
std::ostream & operator<<(std::ostream &os, const dfcc_contract_modet mode)
std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode)
Enum type representing the contract checking and replacement modes.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525