Fix SPARK warning regarding interfering context

The warning fixed by the change is:

 Call to a volatile function in interfering context is not allowed in
 SPARK

Signed-off-by: Adrian-Ken Rueegsegger <ken@codelabs.ch>

diff --git a/src/hw-dbc-events.adb b/src/hw-dbc-events.adb
index 98e8c2aed34880863d0db14a2566d9f6dc4a22c0..ba74f0fc0d6d7336926ba6f689df5507a8658bc4 100644 (file)
--- a/src/hw-dbc-events.adb
+++ b/src/hw-dbc-events.adb
@@ -188,10 +188,12 @@ is
 
    procedure Handle_Events
    is
-      Update_Ptr : Boolean;
+      Update_Ptr : constant Boolean := Ready;
+      Is_Ready   : Boolean;
    begin
-      Update_Ptr := Ready;
-      while Ready loop
+      loop
+         Is_Ready := Ready;
+         exit when not Is_Ready;
          Handle_Event;
       end loop;
       if Update_Ptr then

diff --git a/src/hw-dbc.adb b/src/hw-dbc.adb
index ea4f228e449a2d52f6d1f8718f9c82bb9eaedf79..b0fc1e5fdaa4c93fad359a20b0b38f27c16b5525 100644 (file)
--- a/src/hw-dbc.adb
+++ b/src/hw-dbc.adb
@@ -189,7 +189,11 @@ is
          loop
             Op_Regs.Read (CNR, Controller_Not_Ready);
             exit when CNR = 0;
-            Success := not Time.Timed_Out (Deadline);
+            declare
+               Timed_Out : constant Boolean := Time.Timed_Out (Deadline);
+            begin
+               Success := not Timed_Out;
+            end;
             exit when not Success;
          end loop;
          pragma Debug (not Success, Debug.Put_Line
@@ -329,8 +333,8 @@ is
       Timed_Out : Boolean;
    begin
       if Regs.Byte_Offset /= 0 then
-         Timed_Out := Now or else Time.Timed_Out (DbC_Poll_Deadline);
-         if Timed_Out then
+         Timed_Out := Time.Timed_Out (DbC_Poll_Deadline);
+         if Now or else Timed_Out then
             Regs.Read (Temp8, DbC_Enable);
             if Temp8 = 1 then
                Regs.Read (Temp8, Current_Connect_Status);