9 Declarations [dcl]

9.4 Function contract specifiers [dcl.contract]

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

1
#
The result-name-introducer introduces the identifier as the name of a result binding of the associated function.
If a postcondition assertion has a result-name-introducer and 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-seq of the attributed-identifier in the result-name-introducer appertains to the result binding so introduced.
[Note 1: 
An id-expression that names a result binding is a const lvalue ([expr.prim.id.unqual]).
— end note]
[Example 1: int f() post(r : r == 1) { return 1; } int i = f(); // Postcondition check succeeds. — 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); // The postcondition check can fail if the implementation introduces // a temporary for the return value ([class.temporary]). B b = f(&b); // The postcondition check succeeds, no temporary is introduced. } — end example]
2
#
When the declared return type of a non-templated function contains a placeholder type, a postcondition-specifier with a result-name-introducer shall be present only on a definition.
[Example 3: auto g(auto&) post (r: r >= 0); // OK, g is a template. auto h() post (r: r >= 0); // error: cannot name the return value auto k() post (r: r >= 0) // OK { return 0; } — end example]