1 files changed, 2 insertions, 43 deletions

diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads
index 720de40..8640a5b 100644
--- a/gcc/ada/libgnat/s-imageu.ads
+++ b/gcc/ada/libgnat/s-imageu.ads
@@ -33,44 +33,15 @@
 --  and ``Ada.Text_IO.Modular_IO`` conversions routines for modular 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_U_Spec;
-
 generic
-
    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;
-
 package System.Image_U is
-   use all type U_Spec.Uns_Option;
-
-   Unsigned_Width_Ghost : constant Natural := U_Spec.Max_Log10 + 2 with Ghost;
 
    procedure Image_Unsigned
      (V : Uns;
       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 U_Spec.Is_Value_Unsigned_Ghost (S (1 .. P), V);
-   pragma Inline (Image_Unsigned);
+      P : out Natural) with Inline;
    --  Computes Uns'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.
@@ -78,19 +49,7 @@ package System.Image_U is
    procedure Set_Image_Unsigned
      (V : Uns;
       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 P <= S'Last - Unsigned_Width_Ghost + 1,
-     Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
-       and then P in P'Old + 1 .. S'Last
-       and then U_Spec.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
-       and then U_Spec.Scan_Based_Number_Ghost
-         (S, From => P'Old + 1, To => P)
-         = U_Spec.Wrap_Option (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 Uns'Image (V) except that no leading space is stored. The caller