|
Gem #17: Pragma No_Return, Part 2 (functions)
Author: Bob Duff, AdaCore
Abstract:
Ada Gem #17 — GNAT warns about functions that might reach their “end”,
and sometimes these warnings are false alarms.
Pragma No_Return can be used to suppress such false alarms.
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.
Posted
in Ada / Ada 2005, Development Log, Devt log - Gem of the Week
Have your own idea for a Gem?
If you have an idea for a Gem you would like to contribute please feel free to contact us at: gems@adacore.com