在SPARK Ada中实例化非库级软件包

如何在SPARK Ada中实例化非库级软件包？在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

大概我需要打开SPARK_Mode关闭Ada.Numerics.Discrete_Random，但我不能工作出正确的地方放置杂注。

来源

2017-06-30 digitig

泛型只有在实例化时才由SPARK检查。 :-(

错误消息看起来像你试图把SPARK_Mode方面某处通用内部，这是行不通的。你应该把SPARK_Mode => On方面本机上实例化的通用包装。

来源

2017-06-30 06:42:05

SPARK_Mode * I *的唯一提及是包含我引用的代码的整个包上的SPARK_Mode => On。错误消息指向a-nudira.ads.45，它表示SPARK_Mode => Off，但a- ndira.ads是GNAT发行版的标准库模块，而不是我自己的代码。 – digitig

奇怪。那么也许你应该简单地按照要求去做，并且将'Ada.Numerics.Discrete_Random'的通用实例化成一个库级包。 –

消息是不是这么多Ada.Numerics.Discrete_Random星火-2014要你让你命名包，Unnamed，也就是说，是在图书馆的水平，像雅各Sparre - 安德森his answer提到要晓得：。

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-09 21:31:01 B98

在SPARK Ada中实例化非库级软件包

回答

相关问题