tmp/tmpatbf03it/{from.md → to.md}
RENAMED
|
@@ -0,0 +1,86 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
### Referring to the result object <a id="dcl.contract.res">[[dcl.contract.res]]</a>
|
| 2 |
+
|
| 3 |
+
``` bnf
|
| 4 |
+
attributed-identifier:
|
| 5 |
+
identifier attribute-specifier-seqₒₚₜ
|
| 6 |
+
```
|
| 7 |
+
|
| 8 |
+
``` bnf
|
| 9 |
+
result-name-introducer:
|
| 10 |
+
attributed-identifier ':'
|
| 11 |
+
```
|
| 12 |
+
|
| 13 |
+
The *result-name-introducer* of a *postcondition-specifier* is a
|
| 14 |
+
declaration. The *result-name-introducer* introduces the *identifier* as
|
| 15 |
+
the name of a *result binding* of the associated function. If a
|
| 16 |
+
postcondition assertion has a *result-name-introducer* and the return
|
| 17 |
+
type of the function is cv `void`, the program is ill-formed. A result
|
| 18 |
+
binding denotes the object or reference returned by invocation of that
|
| 19 |
+
function. The type of a result binding is the return type of its
|
| 20 |
+
associated function. The optional *attribute-specifier-seq* of the
|
| 21 |
+
*attributed-identifier* in the *result-name-introducer* appertains to
|
| 22 |
+
the result binding so introduced.
|
| 23 |
+
|
| 24 |
+
[*Note 1*: An *id-expression* that names a result binding is a `const`
|
| 25 |
+
lvalue [[expr.prim.id.unqual]]. — *end note*]
|
| 26 |
+
|
| 27 |
+
[*Example 1*:
|
| 28 |
+
|
| 29 |
+
``` cpp
|
| 30 |
+
int f()
|
| 31 |
+
post(r : r == 1)
|
| 32 |
+
{
|
| 33 |
+
return 1;
|
| 34 |
+
}
|
| 35 |
+
int i = f(); // Postcondition check succeeds.
|
| 36 |
+
```
|
| 37 |
+
|
| 38 |
+
— *end example*]
|
| 39 |
+
|
| 40 |
+
[*Example 2*:
|
| 41 |
+
|
| 42 |
+
``` cpp
|
| 43 |
+
struct A {};
|
| 44 |
+
struct B {
|
| 45 |
+
B() {}
|
| 46 |
+
B(const B&) {}
|
| 47 |
+
};
|
| 48 |
+
|
| 49 |
+
template <typename T>
|
| 50 |
+
T f(T* const ptr)
|
| 51 |
+
post(r: &r == ptr)
|
| 52 |
+
{
|
| 53 |
+
return {};
|
| 54 |
+
}
|
| 55 |
+
|
| 56 |
+
int main() {
|
| 57 |
+
A a = f(&a); // The postcondition check can fail if the implementation introduces
|
| 58 |
+
// a temporary for the return value[class.temporary].
|
| 59 |
+
B b = f(&b); // The postcondition check succeeds, no temporary is introduced.
|
| 60 |
+
}
|
| 61 |
+
```
|
| 62 |
+
|
| 63 |
+
— *end example*]
|
| 64 |
+
|
| 65 |
+
When the declared return type of a non-templated function contains a
|
| 66 |
+
placeholder type, a *postcondition-specifier* with a
|
| 67 |
+
*result-name-introducer* shall be present only on a definition.
|
| 68 |
+
|
| 69 |
+
[*Example 3*:
|
| 70 |
+
|
| 71 |
+
``` cpp
|
| 72 |
+
auto g(auto&)
|
| 73 |
+
post (r: r >= 0); // OK, g is a template.
|
| 74 |
+
|
| 75 |
+
auto h()
|
| 76 |
+
post (r: r >= 0); // error: cannot name the return value
|
| 77 |
+
|
| 78 |
+
auto k()
|
| 79 |
+
post (r: r >= 0) // OK
|
| 80 |
+
{
|
| 81 |
+
return 0;
|
| 82 |
+
}
|
| 83 |
+
```
|
| 84 |
+
|
| 85 |
+
— *end example*]
|
| 86 |
+
|