Hi-Lite high integrity showcase and overflow errors

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

http://www.open-do.org/projects/hi-lite/a-lighter-introduction-to-hi-lite/
introduces AdaCore's new proof tools. This introduction makes me worry
about integrity, pardon me.

I have included the procedure Mult from the example, after correcting
it as suggested by the text. Mult should perform saturating arithmetic.

The high integrity example program fails miserably. (C programmers
should have a good laugh.)

The program compiles without any warnings. It also behaves as
instructed, but not as intended, I suppose. It either terminates
with an overflow check failure, or with a range check failure,
depending on whether GNAT was run in Ada mode (-gnato), or in GNAT mode.

So to ask a provocative question, what is the use of all these tools
if they still lead to programs that overflow so easily?

Or am I just incorrectly assuming thing and X * Y will make the tools
complain fiercely about possible overflow?

Or that this is just an example procedure and the real Mult and Add will
of course use suitable algorithms for testing the feasibility of the
arithmetical operations?


procedure Alicebob is

    type My_Int is range 0 .. 10_000;

    function Mult (X , Y : My_Int) return My_Int is
    begin
       if X * Y < 10_000 then
          return X * Y;
       else
          return 10_000;
       end if;
    end Mult;

begin
    if Mult (1000, 33) /= 10_000 then
       raise Program_Error;
    end if;
end Alicebob;