CBMC
dfcc_loop_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 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_CONTRACT_MODE_H
13 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_CONTRACT_MODE_H
14 
15 #include <string>
16 
18 enum class dfcc_loop_contract_modet
19 {
21  NONE,
23  APPLY,
25  APPLY_UNWIND
26 };
27 
29 dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools(
30  bool apply_loop_contracts,
31  bool unwind_transformed_loops);
32 
33 std::string dfcc_loop_contract_mode_to_string(dfcc_loop_contract_modet mode);
34 
35 std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode);
36 
37 #endif
operator<<
std::ostream & operator<<(std::ostream &os, const dfcc_loop_contract_modet mode)
Definition: dfcc_loop_contract_mode.cpp:51
dfcc_loop_contract_mode_to_string
std::string dfcc_loop_contract_mode_to_string(dfcc_loop_contract_modet mode)
Definition: dfcc_loop_contract_mode.cpp:37
dfcc_loop_contract_mode_from_bools
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.
Definition: dfcc_loop_contract_mode.cpp:15
dfcc_loop_contract_modet
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
Definition: dfcc_loop_contract_mode.h:19
dfcc_loop_contract_modet::APPLY
@ APPLY
Apply loop contracts.
dfcc_loop_contract_modet::NONE
@ NONE
Do not apply loop contracts.
dfcc_loop_contract_modet::APPLY_UNWIND
@ APPLY_UNWIND
Apply loop contracts and unwind the resulting base + step encoding.