ada - Ada 抱怨我在函数调用中添加了一个 volatile 对象而不是 volatile 的泛型类型

Question

所以我有以下声明：

      record
         String1 : String (1 .. 64);
         String2 : String (1 .. 64);
         Timestamp : Time;
         Int1 : Long_Long_Integer;
         String3 : Unbounded_String;
      end record;

它用于

package My_Vectors is new Vectors (Index_Type => Positive, Element_Type => Object);

这会产生编译错误： volatile object cannot act as actual in a call (SPARK RM 7.1.3(10))

现在，Clock使用的是 volatile 。但是我已经删除了对的调用Clock，我仍然得到相同的结果。

此外，我尝试将Object类型替换为类型，Integer并且我没有来自 Ada 编译器的任何投诉。有人可以解释一下吗，因为我看不出这是如何将易失性对象放入实际的任何地方。

刚刚尝试使用以下记录，我得到了相同的结果：

type My_Record is
      record
         A: Integer;
         B: Integer;
         C: String(1 .. 64);
      end record;

Answer 1

SPARK 不支持标准的 Ada 容器（参见SPARK RM 14.8）。请改用 SPARK 兼容容器Ada.Containers.Formal_Vectors（另请参阅此处和此处）。

关于编译器错误：当前的实现Ada.Containers.Vector使用原子操作来提高性能（参见此处和此处）。这些原子操作（在这种情况下）对类型的变量进行操作System.Atomic_Counters.Atomic_Unsigned（参见此处）。此类型被声明为Atomic易失性（参见RM 8(3)）。