The aspect
No_Return may
now be specified for functions (
Aspect No_Return for functions (AI12-0269),
not just procedures (see RM
6.5.1),
but the reason that such a function
never returns must be that it raises an exception (rather than containing
an endless loop). As for procedures, there will be a check at compile
time that the function does not contain any explicit return statements,
and a check at run-time that it does not run into the final end.