Disable SPARK for Copy_DMA_[In|Out] body
authorAdrian-Ken Rueegsegger <ken@codelabs.ch>
Tue, 3 Oct 2017 10:25:13 +0000 (12:25 +0200)
committerAdrian-Ken Rueegsegger <ken@codelabs.ch>
Fri, 27 Oct 2017 10:43:01 +0000 (12:43 +0200)
The procedures use a memory overlay which is problematic in SPARK.

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

index 3465597..5fa6827 100644 (file)
@@ -96,11 +96,17 @@ is
    subtype DMA_Range is Natural range 0 .. Max_Bulk_Size - 1;
    subtype DMA_Buffer is Buffer (DMA_Range);
 
+   procedure Copy_DMA_In
+     (Id       : in     Transfer_Id;
+      Buf      : in out Buffer;
+      Len      : in     Natural;
+      DMA_Off  : in     Natural);
    procedure Copy_DMA_In
      (Id       : in     Transfer_Id;
       Buf      : in out Buffer;
       Len      : in     Natural;
       DMA_Off  : in     Natural)
+   with SPARK_Mode => Off
    is
       DMA_Buf : DMA_Buffer
       with Address => System'To_Address (Transfer_Info.Physical (Id));
@@ -110,12 +116,19 @@ is
          DMA_Buf (DMA_Off .. DMA_Off + DMA_Len - 1);
    end Copy_DMA_In;
 
+   procedure Copy_DMA_Out
+     (Id       : Transfer_Id;
+      Buf      : Buffer;
+      Off      : Natural;
+      Len      : Natural;
+      DMA_Off  : Natural := 0);
    procedure Copy_DMA_Out
      (Id       : Transfer_Id;
       Buf      : Buffer;
       Off      : Natural;
       Len      : Natural;
       DMA_Off  : Natural := 0)
+   with SPARK_Mode => Off
    is
       DMA_Buf : DMA_Buffer
       with Address => System'To_Address (Transfer_Info.Physical (Id));