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.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 border2.nntp.dca1.giganews.com!nntp.giganews.com!news.glorb.com!feeder.erje.net!eu.feeder.erje.net!eternal-september.org!feeder.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: SPARK internal error?
Date: Wed, 04 Mar 2015 09:05:38 +0100
Organization: A noiseless patient Spider
Message-ID: <md6eb7$3hr$1@dont-email.me>
References: <851b7d3c-4ac3-4fba-852d-c2975050da74@googlegroups.com>
 <md4b3s$suf$1@dont-email.me>
 <cf7fc6ed-d27c-4739-8a3d-3f2b039cdf6c@googlegroups.com>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 4 Mar 2015 08:04:55 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="9d0a4007d6908fc6312165e622121d34";
 logging-data="3643"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX19QNQIU6bHZ9HPHx6QOLVEWP/cKK4kpXvk="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:31.0) Gecko/20100101 Thunderbird/31.5.0
In-Reply-To: <cf7fc6ed-d27c-4739-8a3d-3f2b039cdf6c@googlegroups.com>
Cancel-Lock: sha1:OKPbQrwAdRREsR7I6LnckwfYMM8=
Xref: number.nntp.giganews.com comp.lang.ada:192407
Date: 2015-03-04T09:05:38+01:00
List-Id: <comp.lang.ada>

On 03.03.15 16:33, Maciej Sobczak wrote:
>>               declare
>> >                  X : My_Array (I .. A'Last) := (others => 0);
> Yes, in the line above.  But why?

Looking back, as SPARK originally did not permit dynamic (array) bounds,
maybe there is new circuitry in GNATprove so that, whatever is to be
diagnosed isn't properly diagnosed by the currently available implementation?