[dcl.contract.res] (original) (raw)

9 Declarations [dcl]

9.4 Function contract specifiers [dcl.contract]

9.4.2 Referring to the result object [dcl.contract.res]

The result-name-introducerintroduces the identifieras the name of a result bindingof the associated function.

If a postcondition assertion has a result-name-introducerand the return type of the function is cv void, the program is ill-formed.

A result binding denotes the object or reference returned by invocation of that function.

The type of a result binding is the return type of its associated function The optional attribute-specifier-seqof the attributed-identifierin the result-name-introducerappertains to the result binding so introduced.

[Example 1: int f() post(r : r == 1) { return 1;} int i = f(); — _end example_]

[Example 2: struct A {};struct B { B() {} B(const B&) {} };template <typename T>T f(T* const ptr) post(r: &r == ptr) { return {};} int main() { A a = f(&a); B b = f(&b); } — _end example_]

When the declared return type of a non-templated function contains a placeholder type, a postcondition-specifierwith a result-name-introducershall be present only on a definition.

[Example 3: auto g(auto&) post (r: r >= 0); auto h() post (r: r >= 0); auto k() post (r: r >= 0) { return 0;} — _end example_]