loop_contracts_clauset Struct Reference

#include <contracts_wrangler.h>

Collaboration diagram for loop_contracts_clauset:

Public Member Functions
	loop_contracts_clauset (std::string _identifier, std::string _invariants_str, std::string _assigns_str, std::string _decreases_str, unchecked_replace_symbolt _replace_symbol)

Public Attributes
std::string	identifier
std::string	invariants
std::string	assigns
std::string	decreases
unchecked_replace_symbolt	replace_symbol

Detailed Description

Definition at line 29 of file contracts_wrangler.h.

Constructor & Destructor Documentation

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

Definition at line 37 of file contracts_wrangler.h.

Member Data Documentation

assigns

std::string loop_contracts_clauset::assigns

Definition at line 33 of file contracts_wrangler.h.

decreases

std::string loop_contracts_clauset::decreases

Definition at line 34 of file contracts_wrangler.h.

identifier

std::string loop_contracts_clauset::identifier

Definition at line 31 of file contracts_wrangler.h.

invariants

std::string loop_contracts_clauset::invariants

Definition at line 32 of file contracts_wrangler.h.

replace_symbol

unchecked_replace_symbolt loop_contracts_clauset::replace_symbol

Definition at line 35 of file contracts_wrangler.h.

---

The documentation for this struct was generated from the following file:

• goto-instrument/contracts/contracts_wrangler.h