1 files changed, 2 insertions, 60 deletions

diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads
index e500f74..8d3b939 100644
--- a/gcc/ada/libgnat/s-imagei.ads
+++ b/gcc/ada/libgnat/s-imagei.ads
@@ -33,48 +33,14 @@
 --  and ``Ada.Text_IO.Integer_IO`` conversions routines for signed integer
 --  types.
 
---  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,
-                         Subprogram_Variant => Ignore);
-
-with System.Value_I_Spec;
-with System.Value_U_Spec;
-
 generic
    type Int is range <>;
-   type Uns is mod <>;
-
-   --  Additional parameters for ghost subprograms used inside contracts
-
-   with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
-   with package I_Spec is new System.Value_I_Spec
-     (Int => Int, Uns => Uns, U_Spec => U_Spec) with Ghost;
-
 package System.Image_I is
-   package IP renames I_Spec;
-   package UP renames U_Spec;
-   use type UP.Uns_Option;
-
-   Unsigned_Width_Ghost : constant Natural := U_Spec.Max_Log10 + 2 with Ghost;
 
    procedure Image_Integer
      (V : Int;
       S : in out String;
-      P : out Natural)
-   with
-     Pre  => S'First = 1
-       and then S'Last < Integer'Last
-       and then S'Last >= Unsigned_Width_Ghost,
-     Post => P in S'Range
-       and then IP.Is_Value_Integer_Ghost (S (1 .. P), V);
+      P : out Natural);
    --  Computes Int'Image (V) and stores the result in S (1 .. P)
    --  setting the resulting value of P. The caller guarantees that S
    --  is long enough to hold the result, and that S'First is 1.
@@ -82,31 +48,7 @@ package System.Image_I is
    procedure Set_Image_Integer
      (V : Int;
       S : in out String;
-      P : in out Natural)
-   with
-     Pre  => P < Integer'Last
-       and then S'Last < Integer'Last
-       and then S'First <= P + 1
-       and then S'First <= S'Last
-       and then
-         (if V >= 0 then
-            P <= S'Last - Unsigned_Width_Ghost + 1
-          else
-            P <= S'Last - Unsigned_Width_Ghost),
-     Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
-       and then
-         (declare
-            Minus  : constant Boolean := S (P'Old + 1) = '-';
-            Offset : constant Positive := (if V >= 0 then 1 else 2);
-            Abs_V  : constant Uns := IP.Abs_Uns_Of_Int (V);
-          begin
-            Minus = (V < 0)
-              and then P in P'Old + Offset .. S'Last
-              and then UP.Only_Decimal_Ghost
-                (S, From => P'Old + Offset, To => P)
-              and then UP.Scan_Based_Number_Ghost
-                (S, From => P'Old + Offset, To => P)
-                = UP.Wrap_Option (Abs_V));
+      P : in out Natural);
    --  Stores the image of V in S starting at S (P + 1), P is updated to point
    --  to the last character stored. The value stored is identical to the value
    --  of Int'Image (V) except that no leading space is stored when V is