Fix SPARK warning regarding nonvolatile functions
authorAdrian-Ken Rueegsegger <ken@codelabs.ch>
Mon, 2 Oct 2017 15:56:26 +0000 (17:56 +0200)
committerAdrian-Ken Rueegsegger <ken@codelabs.ch>
Fri, 27 Oct 2017 10:42:36 +0000 (12:42 +0200)
Convert functions to procedures with out parameter. Making them volatile
functions is not an option since this is not legal in SPARK see also
GNAT ticket [QA04-034].

The warning corrected by these changes is:

 Nonvolatile function with effectively volatile parameter is not
 allowed in SPARK

Signed-off-by: Adrian-Ken Rueegsegger <ken@codelabs.ch>
src/hw-dbc-events.adb
src/hw-dbc-transfer_rings.adb
src/hw-dbc-trbs.adb
src/hw-dbc-trbs.ads

index fab3f31a671bba3bfd986baa715b0101f4e026f0..98e8c2aed34880863d0db14a2566d9f6dc4a22c0 100644 (file)
@@ -64,8 +64,11 @@ is
 
    function Ready return Boolean
    is
 
    function Ready return Boolean
    is
+      Current_Cycle : Bit;
    begin
    begin
-      return TRBs.Get_Cycle (Ring (Next)) = CCS;
+      TRBs.Get_Cycle (Data  => Ring (Next),
+                      Cycle => Current_Cycle);
+      return Current_Cycle = CCS;
    end Ready;
 
    procedure Update_Dequeue_Ptr
    end Ready;
 
    procedure Update_Dequeue_Ptr
@@ -97,13 +100,22 @@ is
    procedure Handle_Transfer_Event
    is
       use type Word8;
    procedure Handle_Transfer_Event
    is
       use type Word8;
-      ID : constant Word8 := TRBs.Get_Slot_ID (Ring (Next));
-      EP : constant Natural := TRBs.Get_Endpoint_ID (Ring (Next));
-      Pointer : constant Word64 := TRBs.Get_Parameter (Ring (Next));
-      Length : constant Natural := TRBs.Get_Event_Length (Ring (Next));
-      CC : constant TRBs.Completion_Code :=
-         TRBs.Get_Completion_Code (Ring (Next));
+      CC         : TRBs.Completion_Code;
+      Length, EP : Natural;
+      Pointer    : Word64;
+      ID         : Word8;
    begin
    begin
+      TRBs.Get_Slot_ID (Data    => Ring (Next),
+                        Slot_ID => ID);
+      TRBs.Get_Endpoint_ID (Data        => Ring (Next),
+                            Endpoint_ID => EP);
+      TRBs.Get_Parameter (Data      => Ring (Next),
+                          Parameter => Pointer);
+      TRBs.Get_Event_Length (Data   => Ring (Next),
+                             Length => Length);
+      TRBs.Get_Completion_Code (Data => Ring (Next),
+                                Code => CC);
+
       if ID = 1 and EP in Endpoint_Range then
          pragma Debug (Debug_TD_Events, Debug.Put ("TD finished; Length: "));
          pragma Debug (Debug_TD_Events, Debug.Put_Int32 (Int32 (Length)));
       if ID = 1 and EP in Endpoint_Range then
          pragma Debug (Debug_TD_Events, Debug.Put ("TD finished; Length: "));
          pragma Debug (Debug_TD_Events, Debug.Put_Int32 (Int32 (Length)));
@@ -134,7 +146,8 @@ is
    is
       CC : TRBs.Completion_Code;
    begin
    is
       CC : TRBs.Completion_Code;
    begin
-      CC := TRBs.Get_Completion_Code (Ring (Next));
+      TRBs.Get_Completion_Code (Data => Ring (Next),
+                                Code => CC);
       case CC is
       when TRBs.Event_Ring_Full_Error =>
          pragma Debug (Debug.Put_Line ("Event ring full!"));
       case CC is
       when TRBs.Event_Ring_Full_Error =>
          pragma Debug (Debug.Put_Line ("Event ring full!"));
@@ -156,7 +169,8 @@ is
    is
       TRB_Type : TRBs.TRB_Types;
    begin
    is
       TRB_Type : TRBs.TRB_Types;
    begin
-      TRB_Type := TRBs.Get_Type (Ring (Next));
+      TRBs.Get_Type (Data     => Ring (Next),
+                     TRB_Type => TRB_Type);
       case TRB_Type is
          when TRBs.Transfer_Event =>
             Handle_Transfer_Event;
       case TRB_Type is
          when TRBs.Transfer_Event =>
             Handle_Transfer_Event;
index cb2eb7e032f87200f344782159afe7d1623b6f10..921b21a577af283567570fa92ec98c656556e52e 100644 (file)
@@ -203,17 +203,30 @@ is
          while Pointers (EP).Dequeue /= Current loop
             -- Finish transfers that have been skipped by the controller
             pragma Debug (Debug.Put_Line ("WARNING: Skipped TD."));
          while Pointers (EP).Dequeue /= Current loop
             -- Finish transfers that have been skipped by the controller
             pragma Debug (Debug.Put_Line ("WARNING: Skipped TD."));
-            Transfer_Info.Finish
-              (DMA_Physical      => TRBs.Get_Parameter
-                                      (Rings (EP) (Pointers (EP).Dequeue)),
-               Status            => Controller_Error,
-               Remaining_Length  => Max_Bulk_Size);
+            declare
+               Cur_Address : Word64;
+            begin
+               TRBs.Get_Parameter
+                 (Data      => Rings (EP) (Pointers (EP).Dequeue),
+                  Parameter => Cur_Address);
+               Transfer_Info.Finish
+                 (DMA_Physical      => Cur_Address,
+                  Status            => Controller_Error,
+                  Remaining_Length  => Max_Bulk_Size);
+            end;
             Dequeue_TRB (EP);
          end loop;
             Dequeue_TRB (EP);
          end loop;
-         Transfer_Info.Finish
-           (DMA_Physical      => TRBs.Get_Parameter (Rings (EP) (Current)),
-            Status            => Status,
-            Remaining_Length  => Remaining_Length);
+         declare
+            Cur_Address : Word64;
+         begin
+            TRBs.Get_Parameter
+              (Data      => Rings (EP) (Current),
+               Parameter => Cur_Address);
+            Transfer_Info.Finish
+              (DMA_Physical      => Cur_Address,
+               Status            => Status,
+               Remaining_Length  => Remaining_Length);
+         end;
          Dequeue_TRB (EP);
       end if;
 
          Dequeue_TRB (EP);
       end if;
 
index 59e4e1a12446910dd4eae96596d135d6e2f5033e..365bb744049644e518a4897bc66872aa122bb559 100644 (file)
@@ -58,20 +58,20 @@ is
         (Word32 (Length) and 16#1_ffff#);
    end Set_Length;
 
         (Word32 (Length) and 16#1_ffff#);
    end Set_Length;
 
-   function Get_Event_Length (Data : T) return Natural
+   procedure Get_Event_Length (Data : in T; Length : out Natural)
    is
       Status : constant Word32 := Data.Status;
    begin
    is
       Status : constant Word32 := Data.Status;
    begin
-      return Natural (Status and 16#ff_ffff#);
+      Length := Natural (Status and 16#ff_ffff#);
    end Get_Event_Length;
 
    ----------------------------------------------------------------------------
 
    end Get_Event_Length;
 
    ----------------------------------------------------------------------------
 
-   function Get_Completion_Code (Data : T) return Completion_Code
+   procedure Get_Completion_Code (Data : in T; Code : out Completion_Code)
    is
       Status : constant Word32 := Data.Status;
    begin
    is
       Status : constant Word32 := Data.Status;
    begin
-      return Completion_Code (Shift_Right (Status, 24));
+      Code := Completion_Code (Shift_Right (Status, 24));
    end Get_Completion_Code;
 
    ----------------------------------------------------------------------------
    end Get_Completion_Code;
 
    ----------------------------------------------------------------------------
@@ -83,11 +83,11 @@ is
       Data.Control := (Control and not 1) or Word32 (Cycle);
    end Set_Cycle;
 
       Data.Control := (Control and not 1) or Word32 (Cycle);
    end Set_Cycle;
 
-   function Get_Cycle (Data : T) return Bit
+   procedure Get_Cycle (Data : in T; Cycle : out Bit)
    is
       Control : constant Word32 := Data.Control;
    begin
    is
       Control : constant Word32 := Data.Control;
    begin
-      return Bit (Control and 1);
+      Cycle := Bit (Control and 1);
    end Get_Cycle;
 
    procedure Set_Toggle_Cycle (Data : in out T)
    end Get_Cycle;
 
    procedure Set_Toggle_Cycle (Data : in out T)
@@ -121,27 +121,27 @@ is
         Shift_Left (Word32 (TRB_Type), 10);
    end Set_Type;
 
         Shift_Left (Word32 (TRB_Type), 10);
    end Set_Type;
 
-   function Get_Type (Data : T) return TRB_Types
+   procedure Get_Type (Data : in T; TRB_Type : out TRB_Types)
    is
       Control : constant Word32 := Data.Control;
    begin
    is
       Control : constant Word32 := Data.Control;
    begin
-      return TRB_Types (Shift_Right (Control, 10) and 63);
+      TRB_Type := TRB_Types (Shift_Right (Control, 10) and 63);
    end Get_Type;
 
    ----------------------------------------------------------------------------
 
    end Get_Type;
 
    ----------------------------------------------------------------------------
 
-   function Get_Endpoint_ID (Data : T) return Natural
+   procedure Get_Endpoint_ID (Data : in T; Endpoint_ID : out Natural)
    is
       Control : constant Word32 := Data.Control;
    begin
    is
       Control : constant Word32 := Data.Control;
    begin
-      return Natural (Shift_Right (Control, 16) and 16#1f#);
+      Endpoint_ID := Natural (Shift_Right (Control, 16) and 16#1f#);
    end Get_Endpoint_ID;
 
    end Get_Endpoint_ID;
 
-   function Get_Slot_ID (Data : T) return Word8
+   procedure Get_Slot_ID (Data : in T; Slot_ID : out Word8)
    is
       Control : constant Word32 := Data.Control;
    begin
    is
       Control : constant Word32 := Data.Control;
    begin
-      return Word8 (Shift_Right (Control, 24));
+      Slot_ID := Word8 (Shift_Right (Control, 24));
    end Get_Slot_ID;
 
    ----------------------------------------------------------------------------
    end Get_Slot_ID;
 
    ----------------------------------------------------------------------------
@@ -152,11 +152,10 @@ is
       Data.Parameter := Parameter;
    end Set_Parameter;
 
       Data.Parameter := Parameter;
    end Set_Parameter;
 
-   function Get_Parameter (Data : T) return Word64
+   procedure Get_Parameter (Data : in T; Parameter : out Word64)
    is
    is
-      Result : constant Word64 := Data.Parameter;
    begin
    begin
-      return Result;
+      Parameter := Data.Parameter;
    end Get_Parameter;
 
    ----------------------------------------------------------------------------
    end Get_Parameter;
 
    ----------------------------------------------------------------------------
index e0855a1753f30df781599bd44d3a70a8d784bf7e..950bea850a3398d426feb19ee0fcd92c291e46c1 100644 (file)
@@ -119,23 +119,23 @@ private package HW.DbC.TRBs is
    ----------------------------------------------------------------------------
 
    procedure Set_Length (Data : in out T; Length : in Natural);
    ----------------------------------------------------------------------------
 
    procedure Set_Length (Data : in out T; Length : in Natural);
-   function Get_Event_Length (Data : T) return Natural;
+   procedure Get_Event_Length (Data : in T; Length : out Natural);
 
 
-   function Get_Completion_Code (Data : T) return Completion_Code;
+   procedure Get_Completion_Code (Data : in T; Code : out Completion_Code);
 
    procedure Set_Cycle (Data : in out T; Cycle : in Bit);
 
    procedure Set_Cycle (Data : in out T; Cycle : in Bit);
-   function Get_Cycle (Data : T) return Bit;
+   procedure Get_Cycle (Data : in T; Cycle : out Bit);
    procedure Set_ISP (Data : in out T);
    procedure Set_IOC (Data : in out T);
 
    procedure Set_Type (Data : in out T; TRB_Type : in TRB_Types);
    procedure Set_ISP (Data : in out T);
    procedure Set_IOC (Data : in out T);
 
    procedure Set_Type (Data : in out T; TRB_Type : in TRB_Types);
-   function Get_Type (Data : T) return TRB_Types;
+   procedure Get_Type (Data : in T; TRB_Type : out TRB_Types);
 
 
-   function Get_Endpoint_ID (Data : T) return Natural;
-   function Get_Slot_ID (Data : T) return Word8;
+   procedure Get_Endpoint_ID (Data : in T; Endpoint_ID : out Natural);
+   procedure Get_Slot_ID (Data : in T; Slot_ID : out Word8);
 
    procedure Set_Parameter (Data : in out T; Parameter : Word64);
 
    procedure Set_Parameter (Data : in out T; Parameter : Word64);
-   function Get_Parameter (Data : T) return Word64;
+   procedure Get_Parameter (Data : in T; Parameter : out Word64);
 
    procedure Clear (TR : out T; PCS : in Bit);
    procedure Clear_Ring (TR : out Transfer_Ring; PCS : in Bit);
 
    procedure Clear (TR : out T; PCS : in Bit);
    procedure Clear_Ring (TR : out Transfer_Ring; PCS : in Bit);