Ada 抱怨我在非 volatile 时在泛型类型的函数调用中添加了一个 volatile 对象

问题描述

所以我有以下声明：

      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 是可变的，可以使用。但是，我已经删除了对 Clock 的调用，但仍然得到相同的结果。

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

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

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

解决方法

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

关于编译器错误：Ada.Containers.Vector 的当前实现使用原子操作来提高性能（参见 here 和 here）。这些原子操作（在本例中）对 System.Atomic_Counters.Atomic_Unsigned 类型的变量进行操作（参见 here）。此类型声明为 Atomic，因此是 volatile（请参阅 RM 8(3)）。