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

【问题标题】：Ada complaining that I've added a volatile object in a function call to generic type when not volatileAda 抱怨我在函数调用中添加了一个 volatile 对象而不是 volatile 的泛型类型
【发布时间】：2021-01-12 16:43:21
【问题描述】：

所以我有以下声明：

      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 编译器的任何投诉。有人可以解释一下吗，因为我看不出这是如何将 volatile 对象放入实际的任何地方。

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

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

【问题讨论】：

我不是 Spark 专家，但 Unbounded_String 在这里看起来有问题（它是一种访问类型！）：您可以使用 Bounded_String 或带有 String(1..discriminant) 的可区分记录吗？跨度>
谢谢；正在尝试，因为您的评论很有帮助，但没有帮助。

标签： ada spark-ada

【解决方案1】：

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，因此是易失的（参见RM 8(3)）。

【讨论】：