Re: Question about out parameters of unconstrained array type.

[Phil Thornley <phil.jpthornley@gmail.com>]

In article <4NedncPWdPN9GtTS4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...

[...]
> I'm sorry to have distracted you with my silly error. That's what 
> happens when one just types some code into a posting off the top of 
> one's head.
> 
> My real code is more like this:
> 
> procedure Get_Event
>     (Date        : in  Dates.Date;
>      Description : out String;
>      Status      : out Status_Type)
> --# global in Event_Array;
> --# derives Description from Event_Array, Date &
> --#         Status      from Event_Array, Date;
> is
>     I : Event_Index_Type;
> begin
>     Status      := No_Event;
>     Description := (others => ' ');   -- NOTE HERE [1]
> 
>     I := Event_Index_Type'First;
>     loop
>        -- Is this item in the event array the one we are looking for?
>        if Event_Array(I).Date = Date then
>           -- NOTE HERE [2]
>           if Description'Length < Event_Array(I).Description_Size then
>              Status := Description_Too_Long;
>           else
>              -- Copy Event_Array(I).Description_Text into Description
>              Status := Success;
>           end if;
>           exit;
>        end if;
> 
>        -- If not, then advance to the next item.
>        exit when I = Event_Index_Type'Last;
>        I := I + 1;
>     end loop;
> end Get_Event;
> 
> Without the initialization at [1] the use of Description'Length at [2] 
> produces the error Alexander mentions: "Expression contains reference(s) 
> to variable Description which has an undefined value."
> 
> However with the initialization at [1] this error goes away. Thus it 
> appears that SPARK requires that the initial value be defined before it 
> will let you use the attributes.

So it appears that the treatment of Description'Length is different when 
it appears in the range constraint of a loop statement to anywhere else. 
(This isn't completely surprising as the loop constraint gets special 
treatment for other purposes.) It might be worth raising this with the 
SPARK team - if only to try to get an authorative statement of what the 
position actually is.

For your code above, if the cost of including the initialization of the 
array is too high then the easiest way to remove the the error is 
probably to add another parameter that is the length of the Description 
string. Using Alexander's code:

package P is
   procedure Init (A : out String;
                   A_Last : in Integer);
   --# derives A from A_Last;
   --# pre A'Length = A_Last;
end P;

package body P is
   procedure Init (A : out String;
                   A_Last : in Integer) is
   begin
      for I in Positive range A'First .. A'Last
      loop
         if A_Last > 42
         then
            A (I) := 'x';
         end if;
      end loop;
   end Init;
end P;

(Note that it is valid to reference A'Length in the precondition.

Cheers,

Phil