CBMC
dfcc_loop_contract_mode.h File Reference

Enumeration representing the instrumentation mode for loop contracts. More...

#include <string>
+ Include dependency graph for dfcc_loop_contract_mode.h:
+ This graph shows which files directly or indirectly include this file:

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)
 

Detailed Description

Enumeration representing the instrumentation mode for loop contracts.

Definition in file dfcc_loop_contract_mode.h.

Enumeration Type Documentation

◆ dfcc_loop_contract_modet

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.

Function Documentation

◆ 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 at line 15 of file dfcc_loop_contract_mode.cpp.

◆ dfcc_loop_contract_mode_to_string()

std::string dfcc_loop_contract_mode_to_string ( dfcc_loop_contract_modet  mode)

Definition at line 37 of file dfcc_loop_contract_mode.cpp.

◆ operator<<()

std::ostream& operator<< ( std::ostream &  os,
const dfcc_loop_contract_modet  mode 
)

Definition at line 51 of file dfcc_loop_contract_mode.cpp.