SPARK - strange range check with array assignment

SPARK - strange range check with array assignment

[Maciej Sobczak]

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

Re: SPARK - strange range check with array assignment

[Georg Bauhaus]

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.

Re: SPARK - strange range check with array assignment

[Anh Vo]

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

Re: SPARK - strange range check with array assignment

[Maciej Sobczak]

> it went through gnatprove (2015) happily. I tested it on Windows.

I have just installed SPARK 2015 on Windows and I confirm that the test passes OK. Time to upgrade. :-)

Regards,

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