Implicit Function Contract not available for Proof

I've got a procedure in a SPARK package that calls some functions from a none SPARK package.

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 provides me with info: implicit function contract not available for proof (<function_name> may not return) for all four declaration lines where I call functions from global protected types.

The protected types functions are defined in a non SPARK package as follows and use the record Sim_Out which is declared within the protected types private section. All of the records values are initialised with 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;

What are the alternatives to solve this? I did already add some pragmas to provide the prover with additional information subtype Float_Signed1000 is Float range -1_000.0 .. 1_000.0 but that didn't work out as I expected.

I'd like to here your advice on this topic.

Solution

If I'm allowed to edit the Sim package, I can say for example

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

(that’s using AdaCore’s spark2017 version), and follow up with a non-SPARK body

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

The report shows that Sim.Get has been skipped.

How later releases of SPARK2014 will react to this I don't know, because the implication from the User Guide is that Annotate sets up a goal for the prover, and yet we’ve not allowed it to look into the body of Sim to check.

Maybe there’s some more in the Reference Manual - go to adacore.com, select Resources/Documentation/SPARK.