SPARK 整数溢出检查

我有以下程序：

procedure Main with SPARK_Mode is
   F : array (0 .. 10) of Integer := (0, 1, others => 0);
begin
   for I in 2 .. F'Last loop
      F (I) := F (I - 1) + F (I - 2);
   end loop;
end Main;

如果我跑gnatprove，我得到以下结果，指向+ sign:

中：溢出检查可能会失败

这是否意味着F (I - 1)可以等于Integer'Last，并且添加任何内容都会溢出？如果是这样，那么从程序流程中是否还不清楚这是不可能的？或者我需要在合同中注明这一点吗？如果不是，那么这意味着什么？

一个反例表明确实gnatprove在这种情况下，担心的边缘Integer:

中：溢出检查可能会失败（例如，当F = (1 => -1, others => -2147483648) and I = 2)

考虑在代码中添加循环不变式。以下是《使用 Spark 构建高完整性应用程序》一书中的示例。

procedure Copy_Into(Buffer : out Buffer_Type;
                    Source : in String) is
   Characters_To_Copy : Buffer.Count_Type := Maximum_Buffer_Size;
begin
   Buffer := (Others => ' '); -- Initialize to all blanks
   if Source'Length < Characters_To_Copy then
      Characters_To_Copy := Source'Length;
   end if;
   for Index in Buffer.Count_Type range 1..Characters_To_Copy loop
      pragma Loop_Invariant
        (Characters_To_Copy <= Source'Length and
         Characters_To_Copy = Characters_To_Copy'Loop_Entry);
      Buffer (Index) := Source(Source'First + (Index - 1));
   end loop;
end Copy_Into;