CBMC
Public Member Functions | Public Attributes | List of all members
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: