ada_answers_gem_logo_fourth
Next Next

Gem #134 :  Erroneous Execution - Part 3

Let's get started...

We showed how this:

X : Natural := ...;
Y : Integer := X + 1;

if Y > 0 then
    Put_Line (Y'Img);
end if;

can end up printing a negative number if checks are suppressed.

In fact, a good compiler will warn that "Y > 0" is necessarily True, so the code is silly, and you can fix it. But you can't count on that. Optimizers are capable of much more subtle reasoning, which might not produce a warning. For example, suppose we have a procedure:

procedure Print_If_Positive (Y : Integer) is
begin
    if Y > 0 then
        Put_Line (Y'Img);
    end if;
end Print_If_Positive;

It seems "obvious" that Print_If_Positive will never print a negative number. But in the presence of erroneousness, that reasoning doesn't work:

X : Natural := ...;
Y : Integer := X + 1;

Print_If_Positive (Y);

The optimizer might decide to inline the call, and then optimize as in the previous example.

Other language features that can cause erroneous execution include:

  • Shared variables (erroneous if multiple tasks fail to synchronize)
  • Address clauses
  • Unchecked_Conversion
  • Interface to other languages
  • Machine-code insertions
  • User-defined storage pools
  • Unchecked_Deallocation

A complete list can be found by looking up "erroneous" in the RM index, or by searching the RM. Every case of erroneous execution is documented under the heading "Erroneous Execution".

You should try to minimize the use of such features. When you need to use them, try to encapsulate them so you can reason about them locally. And be careful.

As for suppressing checks: Don't suppress unless you need the added efficiency and you have confidence that the checks won't fail. If you do suppress checks, run regression tests on a regular basis in both modes (suppressed and not suppressed).

The final part of this Gem series will explain the rationale behind the concept  of erroneous execution in Ada.

Bob Duff
AdaCore

 
 

Comments on Gems are now closed.