我的数据结构大致如下(我无法共享完整来源,但可以根据要求提供其他信息):
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 手册的相应部分,但我无法理解如何根据它们修复我的代码。短暂性脑缺血发作。
看起来好像您正在
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
...