Gem #17: Pragma No_Return, Part 2 (functions)

by Bob Duff —AdaCore

Let's get started…

A function should always return a value or raise an exception. That is, reaching the "end" of a function is an error. In Ada, this error is detected in two ways:

1. Every function must contain at least one return statement. This rule is too liberal, because some control-flow path might bypass the return statement. This rule is too conservative, because it requires a return even when all you want to do is raise an exception:

      function F (...) return ... is
      begin
         raise Not_Yet_Implemented;  --  Illegal!
      end F;

Function F isn't WRONG -- it's just not finished. In my opinion, this rule should have been abolished, and replaced with a control-flow analysis similar to what GNAT does (see below).

2. If a function reaches its "end", Program_Error is raised. This catches all such errors, but it's unsatisfying; a compile-time check would be better.

Indeed, GNAT provides an effective compile-time check: it gives a warning if there is any control-flow path that might reach the "end":

      function F (...) return ... is
      begin
         if Some_Condition then
            return Something;
         elsif Some_Other_Condition then
            return Something_Else;
         end if;
         --  CAN get here!
      end F;

There is a bug, if Some_Condition and Some_Other_Condition don't cover all the cases, and GNAT will warn. We can fix it in several ways, such as:

      function F (...) return ... is
      begin
         if Some_Condition then
            return Something;
         elsif Some_Other_Condition then
            return Something_Else;
         else
            raise Some_Exception;
         end if;
      end F;

or:

      function F (...) return ... is
      begin
         if Some_Condition then
            return Something;
         else
            pragma Assert (Some_Other_Condition);
            return Something_Else;
         end if;
      end F;

or (and here's the No_Return):

   procedure Log_Error (...);
   pragma No_Return (Log_Error);

   function F (...) return ... is
   begin
      if Some_Condition then
         return Something;
      elsif Some_Other_Condition then
         return Something_Else;
      else
         Log_Error (...);
      end if;
   end F;

GNAT will not cry wolf on the last three versions of F, because it does a simple control-flow analysis to prove that every path reaches either a return statement, or a raise statement, or a non-returning procedure (which presumably contains a raise statement, directly or indirectly).

One way to look at it is that pragma No_Return allows you to wrap a raise statement in a slightly higher level abstraction, without losing the above-mentioned control-flow analysis. No_Return is part of the contract; F relies on Log_Error not returning, and the compiler ensures that the body of Log_Error obeys that contract.