1 files changed, 35 insertions, 4 deletions
diff --git a/gcc/ada/libgnat/s-imglllu.ads b/gcc/ada/libgnat/s-imglllu.ads
index ae918c4..0116aa8 100644
--- a/gcc/ada/libgnat/s-imglllu.ads
+++ b/gcc/ada/libgnat/s-imglllu.ads
@@ -33,15 +33,46 @@
 --  modular integer types larger than Long_Long_Unsigned, and also for
 --  conversion operations required in Text_IO.Modular_IO for such 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.Image_U;
 with System.Unsigned_Types;
+with System.Val_LLLU;
+with System.Wid_LLLU;
 
-package System.Img_LLLU is
-   pragma Pure;
-
+package System.Img_LLLU
+  with SPARK_Mode
+is
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
-   package Impl is new Image_U (Long_Long_Long_Unsigned);
+   package Impl is new Image_U
+     (Uns                                => Long_Long_Long_Unsigned,
+      Uns_Option                         => Val_LLLU.Impl.Uns_Option,
+      Unsigned_Width_Ghost               =>
+         Wid_LLLU.Width_Long_Long_Long_Unsigned
+        (0, Long_Long_Long_Unsigned'Last),
+      Only_Decimal_Ghost                 => Val_LLLU.Impl.Only_Decimal_Ghost,
+      Hexa_To_Unsigned_Ghost             =>
+         Val_LLLU.Impl.Hexa_To_Unsigned_Ghost,
+      Wrap_Option                        => Val_LLLU.Impl.Wrap_Option,
+      Scan_Based_Number_Ghost            =>
+         Val_LLLU.Impl.Scan_Based_Number_Ghost,
+      Is_Unsigned_Ghost                  => Val_LLLU.Impl.Is_Unsigned_Ghost,
+      Value_Unsigned                     => Val_LLLU.Impl.Value_Unsigned,
+      Prove_Iter_Scan_Based_Number_Ghost =>
+         Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
+      Prove_Scan_Only_Decimal_Ghost      =>
+         Val_LLLU.Impl.Prove_Scan_Only_Decimal_Ghost);
 
    procedure Image_Long_Long_Long_Unsigned
      (V : Long_Long_Long_Unsigned;