From: Georg Bauhaus <bauhaus@futureapps.invalid>
Subject: Re: SPARK internal error?
Date: Wed, 04 Mar 2015 09:05:38 +0100
Date: 2015-03-04T09:05:38+01:00 [thread overview]
Message-ID: <md6eb7$3hr$1@dont-email.me> (raw)
In-Reply-To: <cf7fc6ed-d27c-4739-8a3d-3f2b039cdf6c@googlegroups.com>
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?
next prev parent reply other threads:[~2015-03-04 8:05 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2015-03-03 9:54 SPARK internal error? Maciej Sobczak
2015-03-03 12:17 ` G.B.
2015-03-03 12:58 ` G.B.
2015-03-03 15:33 ` Maciej Sobczak
2015-03-04 8:05 ` Georg Bauhaus [this message]
2015-03-04 14:47 ` joakim.strandberg
2015-03-04 22:42 ` Peter Chapin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox