Re: Question about out parameters of unconstrained array type.

[Alexander Senier <mail@senier.net>]

On Sat, 25 Feb 2012 18:20:42 -0000
Phil Thornley <phil.jpthornley@gmail.com> wrote:

> there is no syntax or semantic error reported. (You will get the usual 
> flow error if you assign individual values of the string in the loop, 
> but that's another problem all together.)
> 
> In fact the LRM states that this usage is permitted. See Section 4.1:
> "... the name of an unconstrained array object (formal parameter) shall 
> only appear in the following contexts:
>    1  as the prefix of an attribute reference;
>    2  ..."

As you say, using attributes of out parameters of an unconstrained array type
is no problem when used inside a loop iteration scheme in SPARK. However, it
seems to be when using the attribute elsewhere:

  1 package P is
  2    procedure Init (A : out String);
  3    --# derives A from ;
  4 end P;

  1 package body P is
  2    procedure Init (A : out String) is
  3    begin
  4       for I in Positive range A'First .. A'Last
  5       loop
  6          if A'Length > 42
  7          then
  8             A (I) := 'x';
  9          end if;
 10       end loop;
 11    end Init;
 12 end P;

The example yields the two expected flow errors you mention (line 8 and 11).
However, the use of A'Length in line 6 also lead to an (unexpected) flow error
(same for 'First and 'Last):

p.adb:6:13: Flow Error  20 - Expression contains reference(s) to variable A
which has an undefined value.

Regards
Alex