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: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: SPARK - strange range check with array assignment
Date: Wed, 19 Aug 2015 00:07:18 +0200
Organization: A noiseless patient Spider
Message-ID: <mr0a7f$ba1$1@dont-email.me>
References: <6cd2abfc-63e4-4821-b8d3-143ec25f4619@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: Tue, 18 Aug 2015 22:05:35 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="a6ee0cade24da99d9bc38b7faa265682";
	logging-data="11585"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18oTtT2yLaGN744n0OCi1ZMsxqNSWAaoPM="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:31.0) Gecko/20100101 Thunderbird/31.7.0
In-Reply-To: <6cd2abfc-63e4-4821-b8d3-143ec25f4619@googlegroups.com>
Cancel-Lock: sha1:WIKMlGnE8top9VVHZx6w6SWURGA=
Xref: news.eternal-september.org comp.lang.ada:27498
Date: 2015-08-19T00:07:18+02:00
List-Id: <comp.lang.ada>

On 18.08.15 22:06, Maciej Sobczak wrote:
> Consider (extracted from a bigger problem):
>
> -- p.ads:
> pragma SPARK_Mode;
>
> package P is
>
>     procedure Foo (S : in out String)
>        with Pre => S'Length > 3;
>
> end P;
>
> -- p.adb:
> pragma SPARK_Mode;
>
> package body P is
>
>     procedure Foo (S : in out String)
>     is
>     begin
>        S (S'First .. S'First + 2) := "abc";  -- HERE
>     end Foo;
>
> end P;
>
>
> Foo is intended to overwrite the beginning of the given string.
> GNATProve (2014) says:
>
> p.adb:8:37: warning: range check might fail
>
> Curiously, the assertion added just before the failing line:
>
>        pragma Assert (S'First + 2 in S'Range);
>
> passes without any warning.
>
> What value or expression above is subject to a range check that might fail?

Maybe there are hints at some historic reasons in two quotes from [1] about
the original SPARK:

"SPARK does not have array slices". (p.103)
"It is important to realize that since all constraints have to be static
  it follows that all arrays have static bounds. Thus we cannot declare
  an array in SPARK whose bounds are not known until the program executes.
  This may be felt rather irksome but is necessary if the space occupied
  by the program is to be predictably bounded." (p.96)

[1] Barnes, John (1997). High Integrity Ada. The SPARK Approach.