57 lines
3.9 KiB
Markdown
57 lines
3.9 KiB
Markdown
[dcl.contract.res]
|
||
|
||
# 9 Declarations [[dcl]](./#dcl)
|
||
|
||
## 9.4 Function contract specifiers [[dcl.contract]](dcl.contract#res)
|
||
|
||
### 9.4.2 Referring to the result object [dcl.contract.res]
|
||
|
||
[attributed-identifier:](#nt:attributed-identifier "9.4.2 Referring to the result object [dcl.contract.res]")
|
||
[*identifier*](lex.name#nt:identifier "5.11 Identifiers [lex.name]") [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]")opt
|
||
|
||
[result-name-introducer:](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]")
|
||
[*attributed-identifier*](#nt:attributed-identifier "9.4.2 Referring to the result object [dcl.contract.res]") :
|
||
|
||
[1](#1)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4822)
|
||
|
||
The [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") of a [*postcondition-specifier*](dcl.contract.func#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]") is a declaration[.](#1.sentence-1)
|
||
|
||
The [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") introduces the [*identifier*](lex.name#nt:identifier "5.11 Identifiers [lex.name]") as the name of a [*result binding*](#def:result_binding "9.4.2 Referring to the result object [dcl.contract.res]") of the associated function[.](#1.sentence-2)
|
||
|
||
If a postcondition assertion has a [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") and the return type of the function is cv void,
|
||
the program is ill-formed[.](#1.sentence-3)
|
||
|
||
A result binding denotes
|
||
the object or reference returned by
|
||
invocation of that function[.](#1.sentence-4)
|
||
|
||
The type of a result binding
|
||
is the return type of its associated function[.](#1.sentence-5)
|
||
|
||
The optional [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]") of the [*attributed-identifier*](#nt:attributed-identifier "9.4.2 Referring to the result object [dcl.contract.res]") in the [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") appertains to the result binding so introduced[.](#1.sentence-6)
|
||
|
||
[*Note [1](#note-1)*:
|
||
|
||
An [*id-expression*](expr.prim.id.general#nt:id-expression "7.5.5.1 General [expr.prim.id.general]") that names a result binding is a const lvalue ([[expr.prim.id.unqual]](expr.prim.id.unqual "7.5.5.2 Unqualified names"))[.](#1.sentence-7)
|
||
|
||
â *end note*]
|
||
|
||
[*Example [1](#example-1)*: int f() post(r : r == 1){return 1;}int i = f(); // Postcondition check succeeds. â *end example*]
|
||
|
||
[*Example [2](#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]](class.temporary "6.8.7 Temporary objects")). B b = f(&b); // The postcondition check succeeds, no temporary is introduced.} â *end example*]
|
||
|
||
[2](#2)
|
||
|
||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4882)
|
||
|
||
When the declared return type
|
||
of a non-templated function
|
||
contains a placeholder type,
|
||
a [*postcondition-specifier*](dcl.contract.func#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]") with a [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") shall be present only on a definition[.](#2.sentence-1)
|
||
|
||
[*Example [3](#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*]
|