1

如何在 SPARK Ada 中实例化非库级包？

说我有类似的东西：

subtype Die is Integer range 1..6;
package Random_Die
is
  new Ada.Numerics.Discrete_Random(Die);

这给了我错误：

instantiation error at a-nudira.ads.45
incorrect placement of "Spark_Mode"
Random_Die is not a libray level package

大概我需要为 Ada.Numerics.Discrete_Random 关闭 SPARK_Mode，但我无法找到放置 pragma 的正确位置。

4

2 回答 2

1

该消息与Ada.Numerics.Discrete_Random. Spark-2014 希望您制作未命名的包，Unnamed例如，在库级别，就像 Jacob Sparre Andersen 在他的回答中提到的那样。以机智：

with Ada.Numerics.Discrete_Random;

--procedure Outer is
   package Unnamed
      with Spark_Mode => On
   is
      subtype Die is Integer range 1..6;
      package Random_Die
      is
        new Ada.Numerics.Discrete_Random(Die);
   end Unnamed;
--begin
--   null;
--end Outer;

删除评论的连字符并翻译会Outer产生您的错误消息。Unnamed按原样翻译可以正常工作，并且gnatprove没有任何抱怨。换句话说，Unnamed就是一个库级别的包。Outer里面不是，这使得 GNAT 发出诊断消息。

于 2017-07-09T21:31:01.427 回答
1

泛型仅在实例化时由 SPARK 检查。:-(

错误消息看起来像是您试图将 SPARK_Mode 方面放在泛型内的某个位置。那不管用。您应该将SPARK_Mode => On方面放在实例化通用包的单元上。

于 2017-06-30T06:42:05.020 回答