From: "G.B." <bauhaus@futureapps.invalid>
Subject: Re: SPARK internal error?
Date: Tue, 03 Mar 2015 13:17:16 +0100
Date: 2015-03-03T13:17:16+01:00 [thread overview]
Message-ID: <md48n1$jrp$1@dont-email.me> (raw)
In-Reply-To: <851b7d3c-4ac3-4fba-852d-c2975050da74@googlegroups.com>
On 03.03.15 10:54, Maciej Sobczak wrote:
> Can you reproduce it? Is it a bug in the toolset?
Same here, on a Mac with GNAT GPL 2014.
(Looking at context in the .mlw file, the line indicated
by gnatprove (showing a VC_RANGE_CHECK of I for A (I .. A'Last)?)
does not have the .to_int parts present on lines nearby.
I vaguely remember original SPARK conditions referring
to integer supersets. Not that this helps, I guess.)
next prev parent reply other threads:[~2015-03-03 12:17 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. [this message]
2015-03-03 12:58 ` G.B.
2015-03-03 15:33 ` Maciej Sobczak
2015-03-04 8:05 ` Georg Bauhaus
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