#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: