data-structures - SPARK 实例化错误 w.r.t. volatile 类型

标签 data-structures types ada spark-ada

我有一个大约的数据结构(我无法分享完整的源代码,但可以根据要求提供其他信息)如下:

generic
    type Item_Type is private;
package Util.Pool is
    type Pool is limited new Ada.Finalization.Limited_Controlled with private;

    procedure Get_Available (From: in out Pool; Available: out Natural);
    overriding procedure Finalize (Object: in out Pool);
private
    type Item_Array is array (Positive range <>) of Item_Type;
    type Item_Array_Access is access all Item_Array;

    Null_Item_Array: constant Item_Array_Access := null;

    protected type Protected_Pool is
        function Get_Available return Natural;
    private
        Available: Natural := 0;
        Items: Item_Array_Access := Null_Item_Array;
    end Protected_Pool;

    type Pool is limited new Ada.Finalization.Limited_Controlled with record
        List: Protected_Pool;
    end record;
end Util.Pool;
完整代码编译时没有错误和警告,但 SPARK 证明步骤失败并显示以下内容:
gnatprove -PX:\Path\To\project.gpr -j0 --mode=flow --ide-progress-bar -u main.adb
Phase 1 of 2: generation of Global contracts ...
main.adb:11:05: instantiation error at util-pool.ads:34
main.adb:11:05: effectively volatile type "Protected_Pool" must be declared at library level (SPARK RM 7.1.3(3))
main.adb:11:05: instantiation error at util-pool.ads:45
main.adb:11:05: component "List" of non-volatile type "Pool" cannot be volatile
gnatprove: error during generation of Global contracts
我已阅读 corresponding parts SPARK 手册,但我不明白如何根据它们修复我的代码。 TIA。

最佳答案

看起来好像您正在 Main 中实例化泛型.这不是“在图书馆级别”。
实例化为库级包,应该工作得更好。这需要进入一个文件(在这种情况下)my_util_pool.ads :

with Util.Pool;
package My_Util_Pool is new Util.Pool (Integer);
main.adb现在开始
with My_Util_Pool;
with ...;
procedure Main is
   ...

关于data-structures - SPARK 实例化错误 w.r.t. volatile 类型,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/64719529/

相关文章:

Ada:循环导致后面的代码无法访问

java - 在java中使用链表乘多项式

swift - 如何创建引用特定函数的函数类型的类型别名

algorithm - 查找具有路径压缩而不按等级并集的集合

javascript - typescript : Why does keyof {} have the type never?

c++ - 在 VC++ 中将 unsigned long 转换为 int?

string - 如何从 Ada 中的其他字符串构建字符串?

random - Ada 随机数是相同的

c - 创建链表时不需要创建实际节点吗?

java - 如何使用ListIterator向空列表添加元素?