3.9 KiB
[dcl.contract.res]
9 Declarations [dcl]
9.4 Function contract specifiers [dcl.contract]
9.4.2 Referring to the result object [dcl.contract.res]
attributed-identifier:
identifier attribute-specifier-seqopt
result-name-introducer:
attributed-identifier :
The result-name-introducer of a postcondition-specifier is a declaration.
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 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]
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 valueauto k() post (r: r >= 0) // OK{return 0;} â end example]