AI22-0093-1
!standard 6.5.1(4/3) 24-04-16 AI22-0093-1/03
!standard 6.5.1(5.1/5)
!class binding interpretation 23-12-22
!status Amendment 1-2022 24-02-22
!status WG9 Approved 24-06-10
!status ARG Approved 15-0-0 24-02-22
!status work item 23-12-22
!status received 23-12-19
!submitter Stephen Baird
!priority Low
!difficulty Easy
!qualifier Error
!subject Problems with No_Return
The usual restrictions apply to the return expression of a nonreturning expression function.
A nonreturning procedure specification cannot be completed with a null procedure.
For nonreturning functions, we have a rule that restricts the contents of the expression of the return statement of such a function. But an expression function has no return statement. Do these restrictions apply to the return expression of a nonreturning expression function? (Yes.)
In considering solutions to the previous issue, we needed to be careful that the wording worked when an expression function is the completion of a nonreturning function specification. But the wording that disallows nonreturning null procedures doesn't prevent a null procedure from completing a nonreturning procedure specification. Should this be illegal? (Yes.)
(See summary.)
Replace 6.5.1(4/3):
Aspect No_Return shall not be specified for a null procedure nor an instance of a generic unit.
with:
A subprogram defined by a null_procedure_declaration shall not be nonreturning. For an instance of a generic subprogram, any specification of aspect No_Return shall be confirming.
Modify AARM 6.5.1(4.a/3):
AARM Reason: A null procedure cannot have the appropriate nonreturning semantics, as it does not raise an exception or loop forever.{ Therefore, we do not allow the aspect No_Return to be specified True on a null procedure, nor can a null_procedure_declaration complete a procedure that has aspect No_Return specified True.
Generic instances always inherit whether or not they are nonreturning from the generic unit. Thus we only allow writing a confirming aspect specification.} End AARM Reason.
Replace 6.5.1(5.1/5):
Any return statement that applies to a nonreturning function or generic function shall be a simple_return_statement with an expression that is a raise_expression, a call on a nonreturning function, or a parenthesized expression of one of these.
with:
An extended_return_statement shall not apply to a nonreturning function or generic function. Any return expression of a nonreturning function or generic function shall be a raise_expression, a call on a nonreturning function, or a parenthesized expression of one of these.
The model for expression functions is that they are a function whose body consists of nothing but a single simple_return_statement. We explicitly define the Dynamic Semantics that way, but we did not do that for Legality Rules or Static Semantics as all of the rules are written in terms of a syntactic construct which does not appear in an expression function. Indeed, the Legality Rules that apply to return statements either explicitly include expression functions (the limited rules in 7.5), are repeated in 6.8 (the discriminants accessibility check), or are judged to be impossible since one cannot declare a type in an expression function (tagged type accessibility checks). Clearly, we need to do that in 6.5.1 as well.
Since 6.5 and 6.8 define the term “return expression” specifically to make it easier to word rules like these, we change the wording to use that term rather than having to have duplicative rules solely for expression functions. We have to have an explicit rule to prevent the use of extended return statements (as those can have return expressions), but that makes the intent clearer anyway.
Not extending the ban on nonreturning null procedures to completions most likely was an oversight when null procedures were allowed as completions in Ada 2012 (they were not originally allowed as completions). We note that the language is well-defined without such a ban, in that a nonreturning procedure that tried to return is defined to raise Program_Error. That clearly would apply to a null procedure. However, that would cause implementation work as currently null procedures do nothing other than contract evaluation - this would be the first time that the procedure itself had to execute some code. That is likely to be more disruptive to implementations than simply detecting the problem, and our usual design principle is to reject constructs which will unconditionally raise an exception.
“Nonreturning” is a property of a subprogram, which applies to both the specification and the body of a subprogram. Specifying the aspect No_Return normally only occurs on subprogram specifications, and does not happen on bodies. So the wording must talk about “nonreturning” rather than about the aspect directly, in order that restrictions apply to completions as well as the specifications of subprograms.
The rule rewrite allows a confirming No_Return aspect on null procedures and generic instances. This is useless for null procedures but could provide valuable documentation for generic instances. And it is more consistent with the rest of the language which generally tries to allow confirming aspects even when the aspect value is not allowed to be changed.
@drepl
Aspect No_Return shall not be specified for a null procedure nor an instance of a generic unit.
@dby
A subprogram defined by a @fa{null_procedure_declaration} shall not be nonreturning. For an instance of a generic subprogram, any specification of aspect No_Return shall be confirming.
@drepl
Any return statement that applies to a nonreturning function or generic function shall be a @fa{simple_return_statement} with an @fa{expression} that is a @fa{raise_expression}, a call on a nonreturning function, or a parenthesized @fa{expression} of one of these.
@dby
An @fa{extended_return_statement} shall not apply to a nonreturning function or generic function. Any return expression of a nonreturning function or generic function shall be a @fa{raise_expression}, a call on a nonreturning function, or a parenthesized expression of one of these.
An ACATS B-Test should be constructed to check that the restrictions on nonreturning expression functions are enforced (including when the expression function is a completion). Another ACATS B-Test should be constructed to check that null procedures completing a nonreturning procedure specification are rejected.