cprover
Loading...
Searching...
No Matches
dfcc_loop_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
12
13#include <util/invariant.h>
14
16 bool apply_loop_contracts,
17 bool unwind_transformed_loops)
18{
19 if(apply_loop_contracts)
20 {
21 if(unwind_transformed_loops)
22 {
24 }
25 else
26 {
28 }
29 }
30 else
31 {
33 }
34}
35
36std::string
38{
39 switch(mode)
40 {
42 return "dfcc_loop_contract_modet::NONE";
44 return "dfcc_loop_contract_modet::APPLY";
46 return "dfcc_loop_contract_modet::APPLY_UNWIND";
47 }
49}
50
51std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode)
52{
54 return os;
55}
std::string dfcc_loop_contract_mode_to_string(const dfcc_loop_contract_modet mode)
std::ostream & operator<<(std::ostream &os, const dfcc_loop_contract_modet mode)
dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools(bool apply_loop_contracts, bool unwind_transformed_loops)
Generates an enum value from boolean flags for application and unwinding.
Enumeration representing the instrumentation mode for loop contracts.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
@ APPLY
Apply loop contracts.
@ NONE
Do not apply loop contracts.
@ APPLY_UNWIND
Apply loop contracts and unwind the resulting base + step encoding.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525