CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_contract_mode.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7Date: 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
27std::ostream &operator<<(std::ostream &os, const dfcc_contract_modet mode)
28{
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