From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,834610f4f567e94b,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.180.82.226 with SMTP id l2mr3214933wiy.1.1347408734938;
        Tue, 11 Sep 2012 17:12:14 -0700 (PDT)
Path: 
 ed8ni19548877wib.0!nntp.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.138.MISMATCH!xlned.com!feeder5.xlned.com!feed.xsnews.nl!border-2.ams.xsnews.nl!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsgate.cuhk.edu.hk!goblin2!goblin.stu.neva.ru!news.karotte.org!uucp.gnuu.de!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Mon, 03 Sep 2012 23:56:27 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:15.0) Gecko/20120824 Thunderbird/15.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Hi-Lite high integrity showcase and overflow errors
Message-ID: <5045278b$0$6576$9b4e6d93@newsspool3.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 03 Sep 2012 23:56:27 CEST
NNTP-Posting-Host: 5fbf6394.newsspool3.arcor-online.net
X-Trace: 
 DXC=O6`<J6o]5Un>jlK2>IgHGdMcF=Q^Z^V3h4Fo<]lROoRa8kF<OcfhCOk2^a?VURO\ooPCY\c7>ejVh5k0eMiK[ogbF>_1GXE@U:e
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-09-03T23:56:27+02:00
List-Id: <comp.lang.ada>

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;