cprover
Loading...
Searching...
No Matches
dfcc_loop_contract_mode.h
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
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
19{
21 NONE,
23 APPLY,
26};
27
30 bool apply_loop_contracts,
31 bool unwind_transformed_loops);
32
34
35std::ostream &operator<<(std::ostream &os, const dfcc_loop_contract_modet mode);
36
37#endif
std::string dfcc_loop_contract_mode_to_string(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.
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.