Re: SPARK - strange range check with array assignment

[Anh Vo <anhvofrcaus@gmail.com>]

On Tuesday, August 18, 2015 at 1:06:47 PM UTC-7, 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?
 
it went through gnatprove (2015) happily. I tested it on Windows.

Anh Vo