隐函数契约不可供证明
隐函数契约不可供证明
提问于 2018-01-23 20:50:31
我有一个过程，在一个火花包，调用一些功能，从一个无火花包。
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)。
受保护类型函数在无火花包中定义如下，并使用在受保护类型私有部分中声明的记录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，但这并没有像我预期的那样奏效。
我想在这里给你关于这个话题的建议。
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-01-24 10:14:31
如果允许我编辑Sim包，我可以举例说
package Sim
with SPARK_Mode
is
function Get return Float
with Annotate => (Gnatprove, Terminating);
end Sim;(这是使用AdaCore的spark2017版本)，并跟进一个非火花体
package body Sim is
function Get return Float is (42.0);
end Sim;报告显示，Sim.Get已被跳过。
我不知道SPARK2014以后的版本会如何对此做出反应，因为用户指南的含义是Annotate为验证者设置了一个目标，但是我们不允许它检查Sim的主体。
也许参考手册中还有更多--转到adacore.com，选择参考资料/文档/火花。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/48410587
复制相关文章
相似问题
腾讯云开发者
