#include <contracts_wrangler.h>
Definition at line 29 of file contracts_wrangler.h.
◆ loop_contracts_clauset()
loop_contracts_clauset::loop_contracts_clauset |
( |
std::string |
_identifier, |
|
|
std::string |
_invariants_str, |
|
|
std::string |
_assigns_str, |
|
|
std::string |
_decreases_str, |
|
|
unchecked_replace_symbolt |
_replace_symbol |
|
) |
| |
|
inline |
◆ assigns
std::string loop_contracts_clauset::assigns |
◆ decreases
std::string loop_contracts_clauset::decreases |
◆ identifier
std::string loop_contracts_clauset::identifier |
◆ invariants
std::string loop_contracts_clauset::invariants |
◆ replace_symbol
The documentation for this struct was generated from the following file: