Re: Question about out parameters of unconstrained array type.

["Peter C. Chapin" <PChapin@vtc.vsc.edu>]

On 2012-02-25 13:20, Phil Thornley wrote:

> I think that you may be misinterpreting the SPARK error message:
>
>    15        for I in 1 .. S'Length loop
>                       ^
> ***        Syntax Error      : reserved word "IN" cannot be followed by
>             INTEGER_NUMBER here.
>
> The error here is that the loop index has an anonymous subtype.

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.

Peter