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
30 bool apply_loop_contracts,
31 bool unwind_transformed_loops);
std::ostream & operator<<(std::ostream &os, const dfcc_loop_contract_modet mode)
std::string dfcc_loop_contract_mode_to_string(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.