|
CBMC
|
Enum type representing the contract checking and replacement modes. More...
#include <string>
Include dependency graph for dfcc_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_contract_modet { CHECK , REPLACE } |
| Enum type representing the contract checking and replacement modes. More... | |
Functions | |
| std::string | dfcc_contract_mode_to_string (const dfcc_contract_modet mode) |
| std::ostream & | operator<< (std::ostream &os, const dfcc_contract_modet mode) |
Enum type representing the contract checking and replacement modes.
Definition in file dfcc_contract_mode.h.
|
strong |
Enum type representing the contract checking and replacement modes.
| Enumerator | |
|---|---|
| CHECK | |
| REPLACE | |
Definition at line 19 of file dfcc_contract_mode.h.
| std::string dfcc_contract_mode_to_string | ( | const dfcc_contract_modet | mode | ) |
Definition at line 15 of file dfcc_contract_mode.cpp.
| std::ostream & operator<< | ( | std::ostream & | os, |
| const dfcc_contract_modet | mode | ||
| ) |
Definition at line 27 of file dfcc_contract_mode.cpp.