SPARK实例化错误w.r.t.挥发性类型

问题描述

我大约有一个数据结构（我无法共享完整的源，但可以根据要求提供其他信息），如下所示：

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

我已经阅读了SPARK手册的corresponding parts，但是我不明白如何根据它们修复代码。 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
   ...