1 files changed, 1 insertions, 61 deletions
diff --git a/gcc/ada/libgnat/s-arit32.ads b/gcc/ada/libgnat/s-arit32.ads
index a8abbdc..856dd59 100644
--- a/gcc/ada/libgnat/s-arit32.ads
+++ b/gcc/ada/libgnat/s-arit32.ads
@@ -33,79 +33,19 @@
 --  signed integer values in cases where either overflow checking is
 --  required, or intermediate results are longer than 32 bits.
 
---  Preconditions in this unit are meant for analysis only, not for run-time
---  checking, so that the expected exceptions are raised. This is enforced
---  by setting the corresponding assertion policy to Ignore. Postconditions
---  and contract cases should not be executed at runtime as well, in order
---  not to slow down the execution of these functions.
-
-pragma Assertion_Policy (Pre            => Ignore,
-                         Post           => Ignore,
-                         Contract_Cases => Ignore,
-                         Ghost          => Ignore);
-
 with Interfaces;
-with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
 package System.Arith_32
   with Pure, SPARK_Mode
 is
-   use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer;
    use type Interfaces.Integer_32;
 
    subtype Int32 is Interfaces.Integer_32;
 
-   subtype Big_Integer is
-     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer
-   with Ghost;
-
-   package Signed_Conversion is new
-     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Signed_Conversions
-     (Int => Int32);
-
-   function Big (Arg : Int32) return Big_Integer is
-     (Signed_Conversion.To_Big_Integer (Arg))
-   with Ghost;
-
-   function In_Int32_Range (Arg : Big_Integer) return Boolean is
-     (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range
-       (Arg, Big (Int32'First), Big (Int32'Last)))
-   with Ghost;
-
-   function Same_Sign (X, Y : Big_Integer) return Boolean is
-     (X = Big (Int32'(0))
-        or else Y = Big (Int32'(0))
-        or else (X < Big (Int32'(0))) = (Y < Big (Int32'(0))))
-   with Ghost;
-
-   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
-     (if abs R > (abs Y - Big (Int32'(1))) / Big (Int32'(2)) then
-       (if Same_Sign (X, Y) then Q + Big (Int32'(1))
-        else Q - Big (Int32'(1)))
-      else
-        Q)
-   with
-     Ghost,
-     Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
-
    procedure Scaled_Divide32
      (X, Y, Z : Int32;
       Q, R    : out Int32;
-      Round   : Boolean)
-   with
-     Pre  => Z /= 0
-       and then In_Int32_Range
-         (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
-                                        Big (X) * Big (Y) / Big (Z),
-                                        Big (X) * Big (Y) rem Big (Z))
-          else Big (X) * Big (Y) / Big (Z)),
-     Post => Big (R) = Big (X) * Big (Y) rem Big (Z)
-       and then
-         (if Round then
-            Big (Q) = Round_Quotient (Big (X) * Big (Y), Big (Z),
-                                      Big (X) * Big (Y) / Big (Z), Big (R))
-          else
-            Big (Q) = Big (X) * Big (Y) / Big (Z));
+      Round   : Boolean);
    --  Performs the division of (``X`` * ``Y``) / ``Z``, storing the quotient
    --  in ``Q`` and the remainder in ``R``.
    --