From: "G.B." <bauhaus@futureapps.invalid>
Subject: Re: SPARK internal error?
Date: Tue, 03 Mar 2015 13:58:16 +0100
Date: 2015-03-03T13:58:16+01:00 [thread overview]
Message-ID: <md4b3s$suf$1@dont-email.me> (raw)
In-Reply-To: <851b7d3c-4ac3-4fba-852d-c2975050da74@googlegroups.com>
On 03.03.15 10:54, Maciej Sobczak wrote:
> procedure Sort (A : in out My_Array) is
> begin
> for I in A'Range loop
> Min_To_Left (A (I .. A'Last));
>
> pragma Loop_Invariant
> (for all J in I .. A'Last =>
> A (I) <= A (J));
> end loop;
> end Sort;
The following passes and makes gnatprove produce
warning addressing range/pre/post/loop_invariant:
procedure Sort (A : in out My_Array) is
begin
for I in A'Range loop
declare
X : My_Array (I .. A'Last) := (others => 0);
begin
for K in I .. A'Last loop
X (K) := A (K);
end loop;
Min_To_Left (X);
for K in I .. A'Last loop
A (K) := X (K);
end loop;
end;
pragma Loop_Invariant
((for all J in I .. A'Last =>
A (I) <= A (J)));
end loop;
end Sort;
next prev parent reply other threads:[~2015-03-03 12:58 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. [this message]
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