CBMC
|
Enumeration representing the instrumentation mode for loop contracts. More...
#include <string>
Go to the source code of this file.
Enumerations | |
enum class | dfcc_loop_contract_modet { NONE , APPLY , APPLY_UNWIND } |
Enumeration representing the instrumentation mode for loop contracts. More... | |
Functions | |
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. More... | |
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) |
Enumeration representing the instrumentation mode for loop contracts.
Definition in file dfcc_loop_contract_mode.h.
|
strong |
Enumeration representing the instrumentation mode for loop contracts.
Enumerator | |
---|---|
NONE | Do not apply loop contracts. |
APPLY | Apply loop contracts. |
APPLY_UNWIND | Apply loop contracts and unwind the resulting base + step encoding. |
Definition at line 18 of file dfcc_loop_contract_mode.h.
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 at line 15 of file dfcc_loop_contract_mode.cpp.
std::string dfcc_loop_contract_mode_to_string | ( | dfcc_loop_contract_modet | mode | ) |
Definition at line 37 of file dfcc_loop_contract_mode.cpp.
std::ostream& operator<< | ( | std::ostream & | os, |
const dfcc_loop_contract_modet | mode | ||
) |
Definition at line 51 of file dfcc_loop_contract_mode.cpp.