CBMC
Public Attributes | List of all members
c_wranglert::functiont Struct Reference
+ Collaboration diagram for c_wranglert::functiont:

Public Attributes

std::vector< contract_clauset > contract
 
std::vector< loop_invariantt > loop_invariants
 
std::vector< assertiont > assertions
 
optionalt< std::string > stub
 
bool remove_static = false
 

Detailed Description

Definition at line 80 of file c_wrangler.cpp.

Member Data Documentation

◆ assertions

std::vector<assertiont> c_wranglert::functiont::assertions

Definition at line 85 of file c_wrangler.cpp.

◆ contract

std::vector<contract_clauset> c_wranglert::functiont::contract

Definition at line 83 of file c_wrangler.cpp.

◆ loop_invariants

std::vector<loop_invariantt> c_wranglert::functiont::loop_invariants

Definition at line 84 of file c_wrangler.cpp.

◆ remove_static

bool c_wranglert::functiont::remove_static = false

Definition at line 87 of file c_wrangler.cpp.

◆ stub

optionalt<std::string> c_wranglert::functiont::stub

Definition at line 86 of file c_wrangler.cpp.

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