cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
15
std::string
dfcc_contract_mode_to_string
(
const
dfcc_contract_modet
mode)
16
{
17
switch
(mode)
18
{
19
case
dfcc_contract_modet::CHECK
:
20
return
"dfcc_contract_modet::CHECK"
;
21
case
dfcc_contract_modet::REPLACE
:
22
return
"dfcc_contract_modet::REPLACE"
;
23
}
24
UNREACHABLE
;
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
}
operator<<
std::ostream & operator<<(std::ostream &os, const dfcc_contract_modet mode)
Definition
dfcc_contract_mode.cpp:27
dfcc_contract_mode_to_string
std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode)
Definition
dfcc_contract_mode.cpp:15
dfcc_contract_mode.h
Enum type representing the contract checking and replacement modes.
dfcc_contract_modet
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Definition
dfcc_contract_mode.h:20
dfcc_contract_modet::REPLACE
@ REPLACE
Definition
dfcc_contract_mode.h:22
dfcc_contract_modet::CHECK
@ CHECK
Definition
dfcc_contract_mode.h:21
invariant.h
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition
invariant.h:525
goto-instrument
contracts
dynamic-frames
dfcc_contract_mode.cpp
Generated by
1.17.0