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.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Received: by 10.52.52.130 with SMTP id t2mr3982180vdo.5.1439928405507;
        Tue, 18 Aug 2015 13:06:45 -0700 (PDT)
X-Received: by 10.140.39.165 with SMTP id v34mr114535qgv.25.1439928405488;
 Tue, 18 Aug 2015 13:06:45 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!feeder.erje.net!us.feeder.erje.net!newspeer1.nac.net!border2.nntp.dca1.giganews.com!nntp.giganews.com!69no1962791qgi.0!news-out.google.com!78ni16119qge.1!nntp.google.com!y105no1433053qge.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 18 Aug 2015 13:06:45 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=213.108.152.51;
 posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 213.108.152.51
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <6cd2abfc-63e4-4821-b8d3-143ec25f4619@googlegroups.com>
Subject: SPARK - strange range check with array assignment
From: Maciej Sobczak <see.my.homepage@gmail.com>
Injection-Date: Tue, 18 Aug 2015 20:06:45 +0000
Content-Type: text/plain; charset=ISO-8859-1
Xref: news.eternal-september.org comp.lang.ada:27495
Date: 2015-08-18T13:06:45-07:00
List-Id: <comp.lang.ada>

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?

-- 
Maciej Sobczak * http://www.inspirel.com