postpone division and multiplication proofs

ref #47 #50
Componolit · Jul 18, 2019 · fa5df9d · fa5df9d
1 parent ad9d601
commit fa5df9d
Showing 1 changed file with 10 additions and 3 deletions.
diff --git a/src/minimal/s-arit64.adb b/src/minimal/s-arit64.adb
@@ -198,7 +198,9 @@ is
    procedure Double_Divide
      (X, Y, Z : Int64;
       Q, R    : out Int64;
-      Round   : Boolean)
+      Round   : Boolean) with
+      SPARK_Mode => Off
+      --  TODO: https://github.com/Componolit/ada-runtime/issues/50
    is
       Xu  : constant Uns64 := abs X;
       Yu  : constant Uns64 := abs Y;
@@ -305,7 +307,10 @@ is
    -- Multiply_With_Ovflo_Check --
    -------------------------------
 
-   function Multiply_With_Ovflo_Check (X, Y : Int64) return Int64 is
+   function Multiply_With_Ovflo_Check (X, Y : Int64) return Int64 with
+      SPARK_Mode => Off
+      --  TODO: https://github.com/Componolit/ada-runtime/issues/50
+   is
       Xu  : constant Uns64 := abs X;
       Xhi : constant Uns32 := Hi (Xu);
       Xlo : constant Uns32 := Lo (Xu);
@@ -376,7 +381,9 @@ is
    procedure Scaled_Divide
      (X, Y, Z : Int64;
       Q, R    : out Int64;
-      Round   : Boolean)
+      Round   : Boolean) with
+      SPARK_Mode => Off
+      --  TODO: https://github.com/Componolit/ada-runtime/issues/50
    is
       Xu  : constant Uns64 := abs X;
       Xhi : constant Uns32 := Hi (Xu);