0

我在 SPARK 包中有一个过程，它从非 SPARK 包中调用一些函数。

procedure do_monitoring is
   U_C1 : constant Float := Sim.Get_U_C1;
   I_L1 : constant Float := Sim.Get_I_L1;
   U_C2 : constant Float := Sim.Get_U_C2;
   I_L2 : constant Float := Sim.Get_I_L2;
begin
   pragma Assert (U_C1 in Float_Signed1000);
   pragma Assert (I_L1 in Float_Signed1000);
   pragma Assert (U_C2 in Float_Signed1000);
   pragma Assert (I_L2 in Float_Signed1000);
   --  Monitor PFC intermediate voltage
   monitor_signal (monitor_pfc_voltage, U_C1);
   --  Monitor PFC inductor current
   monitor_signal (monitor_pfc_current, I_L1);
   --  Monitor output voltage
   monitor_signal (monitor_output_voltage, U_C2);
   --  Monitor output inductor current
   monitor_signal (monitor_output_current, I_L2);
end do_monitoring;

GNAT 为我info: implicit function contract not available for proof (<function_name> may not return)从全局受保护类型调用函数的所有四个声明行提供了。

受保护类型函数在非 SPARK 包中定义如下，并使用Sim_Out在受保护类型私有部分中声明的记录。所有记录值都用 初始化0.0。

function Get_I_L1 return Float is
begin
   return Sim_Out.I_L1;
end Get_I_L1;

function Get_U_C1 return Float is
begin
   return Sim_Out.U_C1;
end Get_U_C1;

function Get_I_L2 return Float is
begin
   return Sim_Out.I_L2;
end Get_I_L2;

function Get_U_C2 return Float is
begin
   return Sim_Out.U_C2;
end Get_U_C2;

有什么替代方案可以解决这个问题？我确实已经添加了一些编译指示来为证明者提供额外的信息subtype Float_Signed1000 is Float range -1_000.0 .. 1_000.0，但这并没有像我预期的那样奏效。

我想在这里就这个话题提出你的建议。

4

1 回答 1

3

如果允许我编辑Sim包，我可以说例如

package Sim
with SPARK_Mode
is
   function Get return Float
   with Annotate => (Gnatprove, Terminating);
end Sim;

（那是使用AdaCore的spark2017版本），并跟进一个非SPARK的body

package body Sim is
   function Get return Float is (42.0);
end Sim;

报告显示 Sim.Get 已被跳过。

我不知道 SPARK2014 的后续版本对此有何反应，因为用户指南的含义是Annotate为证明者设置了一个目标，但我们不允许它查看身体Sim检查。

参考手册中可能还有更多内容 - 访问 adacore.com，选择 Resources/Documentation/SPARK。

于 2018-01-24T10:14:31.560 回答