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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 2002:a24:5e90:: with SMTP id h138mr7618914itb.27.1550291414010;
        Fri, 15 Feb 2019 20:30:14 -0800 (PST)
X-Received: by 2002:a9d:518e:: with SMTP id y14mr97322otg.2.1550291413867;
 Fri, 15 Feb 2019 20:30:13 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!weretis.net!feeder7.news.weretis.net!proxad.net!feeder1-2.proxad.net!209.85.166.215.MISMATCH!y22no177983ita.0!news-out.google.com!v188ni463itb.0!nntp.google.com!y42no143994ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 15 Feb 2019 20:30:13 -0800 (PST)
In-Reply-To: <989ea6c7-b432-4214-beec-c0a50b76932c@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=50.66.161.135;
 posting-account=lzqe5AoAAADHhp_gregSufVhvwu22fBS
NNTP-Posting-Host: 50.66.161.135
References: <21f5f1ca-eabe-4ce6-9ee0-5d308d7676ff@googlegroups.com>
 <ly1s4fy0sb.fsf@pushface.org>
 <17375128-e016-4366-91ff-cd68f74689b3@googlegroups.com>
 <q3t181$9rh$1@franka.jacob-sparre.dk>
 <989ea6c7-b432-4214-beec-c0a50b76932c@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <6225c504-8085-4753-bedd-0b1e5816d2a0@googlegroups.com>
Subject: Re: GNAT proposal: note on implicit exceptions insertion
From: Brad Moore <bmoore.ada@gmail.com>
Injection-Date: Sat, 16 Feb 2019 04:30:13 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader01.eternal-september.org comp.lang.ada:55523
Date: 2019-02-15T20:30:13-08:00
List-Id: <comp.lang.ada>

One option would be to write the code you want checked in SPARK.

For example, from your example above, one could write....
 
package P with SPARK_Mode is

   subtype Index_Type is Integer range 1 .. 100;
   
   My_Array : array (Index_Type) of Boolean;
   
   procedure Foo (Index : Integer);

end P;

package body P with SPARK_Mode is

   procedure Foo (Index : Integer) is
   begin
      My_Array (Index) := True;  --  SPARK detects exception may be raised here
   end Foo;

end P;


The code compiles in Ada, but the SPARK prover complains....

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
p.adb:6:17: medium: array index check might fail (e.g. when Index = 0)

Brad