P1323R2 Contract postconditions and return type deduction

source/declarations.tex

@@ -8316,13 +8316,19 @@
 The attribute may be applied to the function type of a function declaration.
 A postcondition may introduce an identifier to represent
 the glvalue result or the prvalue result object of the function.
+When the declared return type of a non-templated function
+contains a placeholder type,
+the optional \grammarterm{identifier} shall only be present in a definition.
 \begin{example}
 \begin{codeblock}
 int f(char * c)
   [[ensures res: res > 0 && c != nullptr]];
 
 int g(double * p)
   [[ensures audit res: res != 0 && p != nullptr && *p <= 0.0]];
+
+auto h(int x)
+  [[ensures res: true]];       // error: cannot name the return value
 \end{codeblock}
 \end{example}
 
@@ -8436,7 +8442,10 @@
 \pnum
 The predicate of a contract condition has the same semantic restrictions
 as if it appeared as the first \grammarterm{expression-statement}
-in the body of the function it applies to.
+in the body of the function it applies to,
+except that the return type of the function is
+known in a contract condition appertaining to its definition,
+even if the return type contains a placeholder type.
 
 \pnum
 A precondition is checked by evaluating its predicate

source/templates.tex

@@ -5085,6 +5085,11 @@
 \mname{func}\iref{dcl.fct.def.general}, where any enclosing function is a
 template, a member of a class template, or a generic lambda,
 
+\item
+the \grammarterm{identifier} introduced in
+a postcondition\iref{dcl.attr.contract} to represent the result of
+a templated function whose declared return type contains a placeholder type,
+
 \item
 a
 \grammarterm{template-id}