Re: SPARK - strange range check with array assignment

[Georg Bauhaus <bauhaus@futureapps.invalid>]

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.