Gem #16: Pragma No_Return

by Bob Duff —AdaCore

Let's get started…

Did he ever return,
No he never returned
And his fate is still unlearn'd
He may ride forever
'neath the streets of Boston
He's the man who never returned.
-- from "Charlie on the M.T.A."
-- by The Kingston Trio

It is occassionally useful to have a procedure that never returns normally, where "normally" means reaching the "end" or executing a "return;". For example, a procedure might format an error message based on its parameters, send the message to a log file, and then unconditionally raise an exception. Other ways to avoid returning normally are to loop forever, and to wait upon an entry barrier that never becomes True.

Such procedures are unusual, and therefore deserve to be documented. A comment works, but pragma No_Return is better because the compiler makes sure that the procedure does not, in fact, return:

   procedure Log_Error (...);
   pragma No_Return (Log_Error);  --  Mark it as a non-returning procedure.

   procedure Log_Error (...) is
   begin
      Put_Line (...);
      raise Some_Error;
   end Log_Error;

Pragma No_Return in Ada 2005 was inspired by the implementation-defined pragma No_Return that has existed in GNAT for some time. Now it's a standard feature of the Ada language.

According to the Ada RM, if a non-returning procedure reaches the "end", Program_Error is raised. But that's just a tripping hazard; what we really want is a compile-time check. In fact, if there is any control-flow path that can reach the "end" of a supposedly non-returning procedure, GNAT will give a warning. As always, you can tell GNAT to treat warnings as errors. These warnings are necessarily conservative, so you might sometimes need to use pragma Warnings (Off) to prevent the compiler from "crying wolf".

See also paragraph 6.5.1(1.a/2) of the Annotated Ada Reference Manual, regarding pragma No_Deposit: http://www.adaic.org/standards/05aarm/html/AA-6-5-1.html