Контракт с неявной функцией недоступен для подтверждения

Question

У меня есть процедура в пакете SPARK, которая вызывает некоторые функции из пакета none 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 но это не сработало, как я ожидал.

Я хотел бы здесь ваши советы по этой теме.

Answer 1

Если мне разрешено редактировать Sim пакет, я могу сказать, например

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

(это использует версию AdaCore spark2017), и последуйте с не-SPARK телом

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

Отчет показывает, что Sim.Get был пропущен.

Как более поздние выпуски SPARK2014 отреагируют на это, я не знаю, потому что из Руководства пользователя вытекает, что Annotate ставит цель для прувера, и тем не менее мы не позволили ему заглянуть в тело Sim Проверять.

Может быть, есть еще что-то в Справочном руководстве - перейдите на adacore.com, выберите Ресурсы / Документация /SPARK.