在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中實例化非庫級軟件包

回答

相關問題