Question about SPARK flow error.

["Peter C. Chapin" <pcc482719@gmail.com>]

My example isn't complete enough to compile, but I could work up a complete
example if necessary. Hopefully this will be accurate and complete enough...

Consider the following procedure:

procedure Add_Item
   (Item : in Some_Type; Index : out Index_Type) is

   Found : Boolean;
begin
   Found := False;

   -- Let's see if the Item already exists in the storage.
   for I in Index_Type range Index_Type'First .. Size loop
      if Storage(I) = Item then
         Index := I;     -- It does. Return the current position.
         Found := True;
         exit;
      end if;
   end loop;

   if not Found then
      -- The Item does not already exist. Install it in the next slot.
      Storage(Next_Index) := Item;
      Index := Next_Index;    -- Return where we installed it.

      -- Play around with Size and Next_Index to set them up for next time
      -- (not shown).
   end if;
end Add_Item;

SPARK gives me an error, "Flow Error 602 - The undefined initial value of
Index may be used in the derivation of Index." I understand this to mean that
there is a path through the procedure where Index (being an out parameter) is
never given a value. So SPARK might be thinking, "Okay... the loop might run
to completion without ever setting Index inside the inner conditional
statement. Then it might skip over the next conditional statement and thus
never set Index at all."

However, if I'm not mistaken that can't actually happen. If the conditional
statement inside the loop never runs, Found will still be False and the
second conditional will definitely execute. Index will receive a value either
inside the loop or later.

Am I missing something or is this reasoning outside of the abilities of
SPARK's flow analysis? Is there some other idiomatic way I should be handling
this sort of situation?

Thanks

Peter