diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index ca4c528a7e0..b94caa45b10 100644
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -772,6 +772,7 @@ GNATRTL_NONTASKING_OBJS= \
   s-vallli$(objext) \
   s-valllu$(objext) \
   s-valrea$(objext) \
+  s-valspe$(objext) \
   s-valued$(objext) \
   s-valuef$(objext) \
   s-valuei$(objext) \
@@ -785,6 +786,10 @@ GNATRTL_NONTASKING_OBJS= \
   s-veboop$(objext) \
   s-vector$(objext) \
   s-vercon$(objext) \
+  s-vs_int$(objext) \
+  s-vs_lli$(objext) \
+  s-vs_llu$(objext) \
+  s-vs_uns$(objext) \
   s-wchcnv$(objext) \
   s-wchcon$(objext) \
   s-wchjis$(objext) \
@@ -1030,6 +1035,8 @@ GNATRTL_128BIT_OBJS = \
   s-vafi128$(objext) \
   s-valllli$(objext) \
   s-vallllu$(objext) \
+  s-vsllli$(objext) \
+  s-vslllu$(objext) \
   s-widllli$(objext) \
   s-widlllu$(objext)
 
diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb
index a10dfdc82a5..3f6bfa20cb2 100644
--- a/gcc/ada/libgnat/s-imagef.adb
+++ b/gcc/ada/libgnat/s-imagef.adb
@@ -70,16 +70,14 @@ package body System.Image_F is
    --  if the small is larger than 1, and smaller than 2**(Int'Size - 1) / 10
    --  if the small is smaller than 1.
 
-   Unsigned_Width_Ghost : constant Natural := Int'Width;
-
    package Uns_Spec is new System.Value_U_Spec (Uns);
-   package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec.Uns_Params);
+   package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec);
 
    package Image_I is new System.Image_I
-     (Int                  => Int,
-      Uns                  => Uns,
-      Unsigned_Width_Ghost => Unsigned_Width_Ghost,
-      Int_Params           => Int_Spec.Int_Params);
+     (Int    => Int,
+      Uns    => Uns,
+      U_Spec => Uns_Spec,
+      I_Spec => Int_Spec);
 
    procedure Set_Image_Integer
      (V : Int;
diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb
index a56d635d9b9..cbe03e74c35 100644
--- a/gcc/ada/libgnat/s-imagei.adb
+++ b/gcc/ada/libgnat/s-imagei.adb
@@ -32,6 +32,8 @@
 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
+with System.Val_Spec;
+
 package body System.Image_I is
 
    --  Ghost code, loop invariants and assertions in this unit are meant for
@@ -149,7 +151,7 @@ package body System.Image_I is
           and then UP.Only_Decimal_Ghost (S, From => 2, To => P)
           and then UP.Scan_Based_Number_Ghost (S, From => 2, To => P)
             = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)),
-        Post => not System.Val_Util.Only_Space_Ghost (S, 1, P)
+        Post => not System.Val_Spec.Only_Space_Ghost (S, 1, P)
           and then IP.Is_Integer_Ghost (S (1 .. P))
           and then IP.Is_Value_Integer_Ghost (S (1 .. P), V);
       --  Ghost lemma to prove the value of Value_Integer from the value of
diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads
index 38c6e6e4fe2..7e39f8697bc 100644
--- a/gcc/ada/libgnat/s-imagei.ads
+++ b/gcc/ada/libgnat/s-imagei.ads
@@ -45,23 +45,26 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
-with System.Val_Util;
+with System.Value_I_Spec;
+with System.Value_U_Spec;
 
 generic
    type Int is range <>;
    type Uns is mod <>;
 
-   Unsigned_Width_Ghost : Natural;
+   --  Additional parameters for ghost subprograms used inside contracts
 
-   with package Int_Params is new System.Val_Util.Int_Params
-     (Int => Int, Uns => Uns, others => <>)
-   with Ghost;
+   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 Int_Params;
-   package UP renames IP.Uns_Params;
+   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;
diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb
index eb1d054e62d..919b401c2d2 100644
--- a/gcc/ada/libgnat/s-imageu.adb
+++ b/gcc/ada/libgnat/s-imageu.adb
@@ -31,6 +31,7 @@
 
 with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+with System.Val_Spec;
 
 package body System.Image_U is
 
@@ -54,17 +55,6 @@ package body System.Image_U is
 
    Big_10 : constant Big_Integer := Big (10) with Ghost;
 
-   --  Maximum value of exponent for 10 that fits in Uns'Base
-   function Max_Log10 return Natural is
-     (case Uns'Base'Size is
-        when 8   => 2,
-        when 16  => 4,
-        when 32  => 9,
-        when 64  => 19,
-        when 128 => 38,
-        when others => raise Program_Error)
-   with Ghost;
-
    ------------------
    -- Local Lemmas --
    ------------------
@@ -86,11 +76,6 @@ package body System.Image_U is
      Ghost,
      Post => X / Y / Z = X / (Y * Z);
 
-   procedure Lemma_Unsigned_Width_Ghost
-   with
-     Ghost,
-     Post => Unsigned_Width_Ghost = Max_Log10 + 2;
-
    ---------------------------
    -- Lemma_Div_Commutation --
    ---------------------------
@@ -117,18 +102,6 @@ package body System.Image_U is
       pragma Assert (X / YZ = XYZ + R / YZ);
    end Lemma_Div_Twice;
 
-   --------------------------------
-   -- Lemma_Unsigned_Width_Ghost --
-   --------------------------------
-
-   procedure Lemma_Unsigned_Width_Ghost is
-   begin
-      pragma Assert (Unsigned_Width_Ghost <= Max_Log10 + 2);
-      pragma Assert (Big (Uns'Last) > Big_10 ** Max_Log10);
-      pragma Assert (Big (Uns'Last) < Big_10 ** (Unsigned_Width_Ghost - 1));
-      pragma Assert (Unsigned_Width_Ghost >= Max_Log10 + 2);
-   end Lemma_Unsigned_Width_Ghost;
-
    --------------------
    -- Image_Unsigned --
    --------------------
@@ -147,12 +120,12 @@ package body System.Image_U is
           and then S'Last < Integer'Last
           and then P in 2 .. S'Last
           and then S (1) = ' '
-          and then Uns_Params.Only_Decimal_Ghost (S, From => 2, To => P)
-          and then Uns_Params.Scan_Based_Number_Ghost (S, From => 2, To => P)
-            = Uns_Params.Wrap_Option (V),
-        Post => not System.Val_Util.Only_Space_Ghost (S, 1, P)
-          and then Uns_Params.Is_Unsigned_Ghost (S (1 .. P))
-          and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V);
+          and then U_Spec.Only_Decimal_Ghost (S, From => 2, To => P)
+          and then U_Spec.Scan_Based_Number_Ghost (S, From => 2, To => P)
+            = U_Spec.Wrap_Option (V),
+        Post => not System.Val_Spec.Only_Space_Ghost (S, 1, P)
+          and then U_Spec.Is_Unsigned_Ghost (S (1 .. P))
+          and then U_Spec.Is_Value_Unsigned_Ghost (S (1 .. P), V);
       --  Ghost lemma to prove the value of Value_Unsigned from the value of
       --  Scan_Based_Number_Ghost on a decimal string.
 
@@ -166,13 +139,13 @@ package body System.Image_U is
          pragma Assert (Str'First = 1);
          pragma Assert (S (2) /= ' ');
          pragma Assert
-           (Uns_Params.Only_Decimal_Ghost (Str, From => 2, To => P));
-         Uns_Params.Prove_Scan_Based_Number_Ghost_Eq
+           (U_Spec.Only_Decimal_Ghost (Str, From => 2, To => P));
+         U_Spec.Prove_Scan_Based_Number_Ghost_Eq
            (S, Str, From => 2, To => P);
          pragma Assert
-           (Uns_Params.Scan_Based_Number_Ghost (Str, From => 2, To => P)
-            = Uns_Params.Wrap_Option (V));
-         Uns_Params.Prove_Scan_Only_Decimal_Ghost (Str, V);
+           (U_Spec.Scan_Based_Number_Ghost (Str, From => 2, To => P)
+            = U_Spec.Wrap_Option (V));
+         U_Spec.Prove_Scan_Only_Decimal_Ghost (Str, V);
       end Prove_Value_Unsigned;
 
    --  Start of processing for Image_Unsigned
@@ -227,7 +200,7 @@ package body System.Image_U is
       with
         Ghost,
         Pre  => R in 0 .. 9,
-        Post => Uns_Params.Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R;
+        Post => U_Spec.Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R;
       --  Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
       --  figure when applied to the corresponding character.
 
@@ -245,26 +218,26 @@ package body System.Image_U is
             and then (for all I in P + 1 .. Max => Prev_S (I) = S (I))
             and then S (P) in '0' .. '9'
             and then V <= Uns'Last / 10
-            and then Uns'Last - Uns_Params.Hexa_To_Unsigned_Ghost (S (P))
+            and then Uns'Last - U_Spec.Hexa_To_Unsigned_Ghost (S (P))
               >= 10 * V
             and then Prev_V =
-              V * 10 + Uns_Params.Hexa_To_Unsigned_Ghost (S (P))
+              V * 10 + U_Spec.Hexa_To_Unsigned_Ghost (S (P))
             and then
               (if P = Max then Prev_V = Res
-               else Uns_Params.Scan_Based_Number_Ghost
+               else U_Spec.Scan_Based_Number_Ghost
                  (Str  => Prev_S,
                   From => P + 1,
                   To   => Max,
                   Base => 10,
-                  Acc  => Prev_V) = Uns_Params.Wrap_Option (Res)),
+                  Acc  => Prev_V) = U_Spec.Wrap_Option (Res)),
           Post =>
             (for all I in P .. Max => S (I) in '0' .. '9')
-            and then Uns_Params.Scan_Based_Number_Ghost
+            and then U_Spec.Scan_Based_Number_Ghost
               (Str  => S,
                From => P,
                To   => Max,
                Base => 10,
-               Acc  => V) = Uns_Params.Wrap_Option (Res);
+               Acc  => V) = U_Spec.Wrap_Option (Res);
       --  Ghost lemma to prove that Scan_Based_Number_Ghost is preserved
       --  through an iteration of the loop.
 
@@ -287,17 +260,17 @@ package body System.Image_U is
       is
          pragma Unreferenced (Res);
       begin
-         Uns_Params.Lemma_Scan_Based_Number_Ghost_Step
+         U_Spec.Lemma_Scan_Based_Number_Ghost_Step
            (Str  => S,
             From => P,
             To   => Max,
             Base => 10,
             Acc  => V);
          if P < Max then
-            Uns_Params.Prove_Scan_Based_Number_Ghost_Eq
+            U_Spec.Prove_Scan_Based_Number_Ghost_Eq
               (Prev_S, S, P + 1, Max, 10, Prev_V);
          else
-            Uns_Params.Lemma_Scan_Based_Number_Ghost_Base
+            U_Spec.Lemma_Scan_Based_Number_Ghost_Base
               (Str  => S,
                From => P + 1,
                To   => Max,
@@ -314,8 +287,6 @@ package body System.Image_U is
       --  No check is done since, as documented in the specification, the
       --  caller guarantees that S is long enough to hold the result.
 
-      Lemma_Unsigned_Width_Ghost;
-
       --  First we compute the number of characters needed for representing
       --  the number.
       loop
@@ -359,7 +330,7 @@ package body System.Image_U is
          Prove_Euclidian
            (Val  => Prev_Value,
             Quot => Value,
-            Rest => Uns_Params.Hexa_To_Unsigned_Ghost (S (P + J)));
+            Rest => U_Spec.Hexa_To_Unsigned_Ghost (S (P + J)));
 
          Prove_Scan_Iter
            (S, Prev_S, Value, Prev_Value, V, P + J, P + Nb_Digits);
@@ -368,18 +339,18 @@ package body System.Image_U is
          pragma Loop_Invariant
            (for all K in S'First .. P => S (K) = S_Init (K));
          pragma Loop_Invariant
-           (Uns_Params.Only_Decimal_Ghost
+           (U_Spec.Only_Decimal_Ghost
               (S, From => P + J, To => P + Nb_Digits));
          pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1));
          pragma Loop_Invariant (Big (Value) = Big (V) / Pow);
          pragma Loop_Invariant
-           (Uns_Params.Scan_Based_Number_Ghost
+           (U_Spec.Scan_Based_Number_Ghost
               (Str  => S,
                From => P + J,
                To   => P + Nb_Digits,
                Base => 10,
                Acc  => Value)
-              = Uns_Params.Wrap_Option (V));
+              = U_Spec.Wrap_Option (V));
       end loop;
       pragma Assert (Big (Value) = Big (V) / (Big_10 ** Nb_Digits));
       pragma Assert (Value = 0);
diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads
index 1c58ea1d692..cec52636e2c 100644
--- a/gcc/ada/libgnat/s-imageu.ads
+++ b/gcc/ada/libgnat/s-imageu.ads
@@ -45,7 +45,7 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
-with System.Val_Util;
+with System.Value_U_Spec;
 
 generic
 
@@ -53,14 +53,12 @@ generic
 
    --  Additional parameters for ghost subprograms used inside contracts
 
-   Unsigned_Width_Ghost : Natural;
-
-   with package Uns_Params is new System.Val_Util.Uns_Params
-     (Uns => Uns, others => <>)
-   with Ghost;
+   with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
 
 package System.Image_U is
-   use all type Uns_Params.Uns_Option;
+   use all type U_Spec.Uns_Option;
+
+   Unsigned_Width_Ghost : constant Natural := U_Spec.Max_Log10 + 2 with Ghost;
 
    procedure Image_Unsigned
      (V : Uns;
@@ -71,7 +69,7 @@ package System.Image_U is
        and then S'Last < Integer'Last
        and then S'Last >= Unsigned_Width_Ghost,
      Post => P in S'Range
-       and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V);
+       and then U_Spec.Is_Value_Unsigned_Ghost (S (1 .. P), V);
    pragma Inline (Image_Unsigned);
    --  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
@@ -89,10 +87,10 @@ package System.Image_U is
        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 Uns_Params.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
-       and then Uns_Params.Scan_Based_Number_Ghost
+       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)
-         = Uns_Params.Wrap_Option (V);
+         = U_Spec.Wrap_Option (V);
    --  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
diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb
index fd1d9a6b2fc..fb3301a4270 100644
--- a/gcc/ada/libgnat/s-imgboo.adb
+++ b/gcc/ada/libgnat/s-imgboo.adb
@@ -37,7 +37,7 @@ pragma Assertion_Policy (Ghost          => Ignore,
                          Loop_Invariant => Ignore,
                          Assert         => Ignore);
 
-with System.Val_Util;
+with System.Val_Spec;
 
 package body System.Img_Bool
   with SPARK_Mode
@@ -58,12 +58,12 @@ is
          S (1 .. 4) := "TRUE";
          P := 4;
          pragma Assert
-           (System.Val_Util.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
+           (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
       else
          S (1 .. 5) := "FALSE";
          P := 5;
          pragma Assert
-           (System.Val_Util.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
+           (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
       end if;
    end Image_Boolean;
 
diff --git a/gcc/ada/libgnat/s-imgint.ads b/gcc/ada/libgnat/s-imgint.ads
index 320edc92f28..fe938994c5a 100644
--- a/gcc/ada/libgnat/s-imgint.ads
+++ b/gcc/ada/libgnat/s-imgint.ads
@@ -47,8 +47,8 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Image_I;
 with System.Unsigned_Types;
-with System.Val_Int;
-with System.Wid_Uns;
+with System.Vs_Int;
+with System.Vs_Uns;
 
 package System.Img_Int
   with SPARK_Mode
@@ -56,11 +56,10 @@ is
    subtype Unsigned is Unsigned_Types.Unsigned;
 
    package Impl is new Image_I
-     (Int                  => Integer,
-      Uns                  => Unsigned,
-      Unsigned_Width_Ghost =>
-         Wid_Uns.Width_Unsigned (0, Unsigned'Last),
-      Int_Params           => System.Val_Int.Impl.Spec.Int_Params);
+     (Int    => Integer,
+      Uns    => Unsigned,
+      U_Spec => System.Vs_Uns.Spec,
+      I_Spec => System.Vs_Int.Spec);
 
    procedure Image_Integer
      (V : Integer;
diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads
index 1d34e77ead3..809ca106282 100644
--- a/gcc/ada/libgnat/s-imglli.ads
+++ b/gcc/ada/libgnat/s-imglli.ads
@@ -47,8 +47,8 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Image_I;
 with System.Unsigned_Types;
-with System.Val_LLI;
-with System.Wid_LLU;
+with System.Vs_LLI;
+with System.Vs_LLU;
 
 package System.Img_LLI
   with SPARK_Mode
@@ -56,12 +56,10 @@ is
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
    package Impl is new Image_I
-     (Int                  => Long_Long_Integer,
-      Uns                  => Long_Long_Unsigned,
-      Unsigned_Width_Ghost =>
-         Wid_LLU.Width_Long_Long_Unsigned
-           (0, Long_Long_Unsigned'Last),
-      Int_Params           => System.Val_LLI.Impl.Spec.Int_Params);
+     (Int    => Long_Long_Integer,
+      Uns    => Long_Long_Unsigned,
+      U_Spec => System.Vs_LLU.Spec,
+      I_Spec => System.Vs_LLI.Spec);
 
    procedure Image_Long_Long_Integer
      (V : Long_Long_Integer;
diff --git a/gcc/ada/libgnat/s-imgllli.ads b/gcc/ada/libgnat/s-imgllli.ads
index 05dec5e4dcc..727388f3d34 100644
--- a/gcc/ada/libgnat/s-imgllli.ads
+++ b/gcc/ada/libgnat/s-imgllli.ads
@@ -47,8 +47,8 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Image_I;
 with System.Unsigned_Types;
-with System.Val_LLLI;
-with System.Wid_LLLU;
+with System.Vs_LLLI;
+with System.Vs_LLLU;
 
 package System.Img_LLLI
   with SPARK_Mode
@@ -56,12 +56,10 @@ is
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
    package Impl is new Image_I
-     (Int                  => Long_Long_Long_Integer,
-      Uns                  => Long_Long_Long_Unsigned,
-      Unsigned_Width_Ghost =>
-         Wid_LLLU.Width_Long_Long_Long_Unsigned
-           (0, Long_Long_Long_Unsigned'Last),
-      Int_Params           => System.Val_LLLI.Impl.Spec.Int_Params);
+     (Int    => Long_Long_Long_Integer,
+      Uns    => Long_Long_Long_Unsigned,
+      U_Spec => System.Vs_LLLU.Spec,
+      I_Spec => System.Vs_LLLI.Spec);
 
    procedure Image_Long_Long_Long_Integer
      (V : Long_Long_Long_Integer;
diff --git a/gcc/ada/libgnat/s-imglllu.ads b/gcc/ada/libgnat/s-imglllu.ads
index 888d782e3d1..09c8965dd81 100644
--- a/gcc/ada/libgnat/s-imglllu.ads
+++ b/gcc/ada/libgnat/s-imglllu.ads
@@ -47,8 +47,7 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Image_U;
 with System.Unsigned_Types;
-with System.Val_LLLU;
-with System.Wid_LLLU;
+with System.Vs_LLLU;
 
 package System.Img_LLLU
   with SPARK_Mode
@@ -56,11 +55,8 @@ is
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
    package Impl is new Image_U
-     (Uns                  => Long_Long_Long_Unsigned,
-      Unsigned_Width_Ghost =>
-         Wid_LLLU.Width_Long_Long_Long_Unsigned
-        (0, Long_Long_Long_Unsigned'Last),
-      Uns_Params           => System.Val_LLLU.Impl.Spec.Uns_Params);
+     (Uns    => Long_Long_Long_Unsigned,
+      U_Spec => System.Vs_LLLU.Spec);
 
    procedure Image_Long_Long_Long_Unsigned
      (V : Long_Long_Long_Unsigned;
diff --git a/gcc/ada/libgnat/s-imgllu.ads b/gcc/ada/libgnat/s-imgllu.ads
index b00dc663c81..9709c961a13 100644
--- a/gcc/ada/libgnat/s-imgllu.ads
+++ b/gcc/ada/libgnat/s-imgllu.ads
@@ -47,8 +47,7 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Image_U;
 with System.Unsigned_Types;
-with System.Val_LLU;
-with System.Wid_LLU;
+with System.Vs_LLU;
 
 package System.Img_LLU
   with SPARK_Mode
@@ -56,10 +55,8 @@ is
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
    package Impl is new Image_U
-     (Uns                  => Long_Long_Unsigned,
-      Unsigned_Width_Ghost =>
-         Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last),
-      Uns_Params           => System.Val_LLU.Impl.Spec.Uns_Params);
+     (Uns    => Long_Long_Unsigned,
+      U_Spec => System.Vs_LLU.Spec);
 
    procedure Image_Long_Long_Unsigned
      (V : Long_Long_Unsigned;
diff --git a/gcc/ada/libgnat/s-imguns.ads b/gcc/ada/libgnat/s-imguns.ads
index 2bd72164f7c..7c79a669b81 100644
--- a/gcc/ada/libgnat/s-imguns.ads
+++ b/gcc/ada/libgnat/s-imguns.ads
@@ -47,8 +47,7 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Image_U;
 with System.Unsigned_Types;
-with System.Val_Uns;
-with System.Wid_Uns;
+with System.Vs_Uns;
 
 package System.Img_Uns
   with SPARK_Mode
@@ -56,10 +55,8 @@ is
    subtype Unsigned is Unsigned_Types.Unsigned;
 
    package Impl is new Image_U
-     (Uns                  => Unsigned,
-      Unsigned_Width_Ghost =>
-         Wid_Uns.Width_Unsigned (0, Unsigned'Last),
-      Uns_Params           => System.Val_Uns.Impl.Spec.Uns_Params);
+     (Uns    => Unsigned,
+      U_Spec => System.Vs_Uns.Spec);
 
    procedure Image_Unsigned
      (V : Unsigned;
diff --git a/gcc/ada/libgnat/s-vaispe.adb b/gcc/ada/libgnat/s-vaispe.adb
index b1a38842773..a13dc6a8a2d 100644
--- a/gcc/ada/libgnat/s-vaispe.adb
+++ b/gcc/ada/libgnat/s-vaispe.adb
@@ -71,14 +71,14 @@ package body System.Value_I_Spec is
    begin
       Prove_Conversion_Is_Identity (Val, Uval);
       pragma Assert
-        (Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+        (U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
       pragma Assert
-        (Uns_Params.Scan_Split_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
-      Uns_Params.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, 10);
+        (U_Spec.Scan_Split_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+      U_Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, 10);
       pragma Assert
-        (Uns_Params.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+        (U_Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
       pragma Assert (Only_Space_Ghost
-        (Str, Uns_Params.Raw_Unsigned_Last_Ghost
+        (Str, U_Spec.Raw_Unsigned_Last_Ghost
                         (Str, Fst_Num, Str'Last), Str'Last));
       pragma Assert (Is_Integer_Ghost (Str));
       pragma Assert (Is_Value_Integer_Ghost (Str, Val));
diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads
index e74202d736e..33cc1f686bc 100644
--- a/gcc/ada/libgnat/s-vaispe.ads
+++ b/gcc/ada/libgnat/s-vaispe.ads
@@ -44,7 +44,8 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
-with System.Val_Util; use System.Val_Util;
+with System.Value_U_Spec;
+with System.Val_Spec; use System.Val_Spec;
 
 generic
 
@@ -52,12 +53,9 @@ generic
 
    type Uns is mod <>;
 
-   --  Additional parameters for specification subprograms on modular Unsigned
-   --  integers.
+   --  Additional parameters for ghost subprograms used inside contracts
 
-   with package Uns_Params is new System.Val_Util.Uns_Params
-     (Uns => Uns, others => <>)
-   with Ghost;
+   with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
 
 package System.Value_I_Spec with
    Ghost,
@@ -65,7 +63,7 @@ package System.Value_I_Spec with
    Always_Terminates
 is
    pragma Preelaborate;
-   use all type Uns_Params.Uns_Option;
+   use all type U_Spec.Uns_Option;
 
    function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
      (if Minus then Uval <= Uns (Int'Last) + 1
@@ -113,16 +111,16 @@ is
         Fst_Num   : constant Positive :=
           (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
       begin
-        Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
-          and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost
+        U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+          and then U_Spec.Raw_Unsigned_No_Overflow_Ghost
              (Str, Fst_Num, Str'Last)
           and then
             Uns_Is_Valid_Int
               (Minus => Str (Non_Blank) = '-',
-               Uval  => Uns_Params.Scan_Raw_Unsigned_Ghost
+               Uval  => U_Spec.Scan_Raw_Unsigned_Ghost
                  (Str, Fst_Num, Str'Last))
           and then Only_Space_Ghost
-            (Str, Uns_Params.Raw_Unsigned_Last_Ghost
+            (Str, U_Spec.Raw_Unsigned_Last_Ghost
              (Str, Fst_Num, Str'Last), Str'Last))
    with
      Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
@@ -140,7 +138,7 @@ is
         Fst_Num   : constant Positive :=
           (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
         Uval      : constant Uns :=
-          Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
+          U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
       begin
         Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
                        Uval  => Uval,
@@ -160,30 +158,16 @@ is
        and then Str'Length >= 2
        and then Str (Str'First) in ' ' | '-'
        and then (Str (Str'First) = '-') = (Val < 0)
-       and then Uns_Params.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
-       and then Uns_Params.Scan_Based_Number_Ghost
+       and then U_Spec.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
+       and then U_Spec.Scan_Based_Number_Ghost
          (Str, Str'First + 1, Str'Last)
-         = Uns_Params.Wrap_Option (Abs_Uns_Of_Int (Val)),
+         = U_Spec.Wrap_Option (Abs_Uns_Of_Int (Val)),
      Post => Is_Integer_Ghost (Slide_If_Necessary (Str))
        and then Is_Value_Integer_Ghost (Str, Val);
    --  Ghost lemma used in the proof of 'Image implementation, to prove that
    --  the result of Value_Integer on a decimal string is the same as the
    --  signing the result of Scan_Based_Number_Ghost.
 
-   --  Bundle Int type with other types, constants and subprograms used in
-   --  ghost code, so that this package can be instantiated once and used
-   --  multiple times as generic formal for a given Int type.
-
-   package Int_Params is new System.Val_Util.Int_Params
-     (Uns                             => Uns,
-      Int                             => Int,
-      P_Uns_Params                    => Uns_Params,
-      P_Is_Integer_Ghost              => Is_Integer_Ghost,
-      P_Is_Value_Integer_Ghost        => Is_Value_Integer_Ghost,
-      P_Is_Int_Of_Uns                 => Is_Int_Of_Uns,
-      P_Abs_Uns_Of_Int                => Abs_Uns_Of_Int,
-      P_Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost);
-
 private
 
    ----------------
diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb
index 41c54bf7d69..f988c97ff24 100644
--- a/gcc/ada/libgnat/s-valboo.adb
+++ b/gcc/ada/libgnat/s-valboo.adb
@@ -55,7 +55,7 @@ is
    begin
       Normalize_String (S, F, L);
 
-      pragma Assert (F = System.Val_Util.First_Non_Space_Ghost
+      pragma Assert (F = System.Val_Spec.First_Non_Space_Ghost
                      (S, Str'First, Str'Last));
 
       if S (F .. L) = "TRUE" then
diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads
index 4866900e1ca..d48219953a0 100644
--- a/gcc/ada/libgnat/s-valboo.ads
+++ b/gcc/ada/libgnat/s-valboo.ads
@@ -40,7 +40,7 @@ pragma Assertion_Policy (Pre            => Ignore,
                          Contract_Cases => Ignore,
                          Ghost          => Ignore);
 
-with System.Val_Util;
+with System.Val_Spec;
 
 package System.Val_Bool
   with SPARK_Mode
@@ -48,10 +48,10 @@ is
    pragma Preelaborate;
 
    function Is_Boolean_Image_Ghost (Str : String) return Boolean is
-     (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last)
+     (not System.Val_Spec.Only_Space_Ghost (Str, Str'First, Str'Last)
         and then
       (declare
-         F : constant Positive := System.Val_Util.First_Non_Space_Ghost
+         F : constant Positive := System.Val_Spec.First_Non_Space_Ghost
            (Str, Str'First, Str'Last);
        begin
          (F <= Str'Last - 3
@@ -61,7 +61,7 @@ is
           and then Str (F + 3) in 'e' | 'E'
           and then
             (if F + 3 < Str'Last then
-               System.Val_Util.Only_Space_Ghost (Str, F + 4, Str'Last)))
+               System.Val_Spec.Only_Space_Ghost (Str, F + 4, Str'Last)))
            or else
          (F <= Str'Last - 4
           and then Str (F)     in 'f' | 'F'
@@ -71,7 +71,7 @@ is
           and then Str (F + 4) in 'e' | 'E'
           and then
             (if F + 4 < Str'Last then
-               System.Val_Util.Only_Space_Ghost (Str, F + 5, Str'Last)))))
+               System.Val_Spec.Only_Space_Ghost (Str, F + 5, Str'Last)))))
    with
      Ghost;
    --  Ghost function that returns True iff Str is the image of a boolean, that
@@ -83,7 +83,7 @@ is
      Pre  => Is_Boolean_Image_Ghost (Str),
      Post =>
        Value_Boolean'Result =
-         (Str (System.Val_Util.First_Non_Space_Ghost
+         (Str (System.Val_Spec.First_Non_Space_Ghost
             (Str, Str'First, Str'Last)) in 't' | 'T');
    --  Computes Boolean'Value (Str)
 
diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index d3df7dbedd1..d8393ac3305 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -47,6 +47,8 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Unsigned_Types;
 with System.Val_Uns;
 with System.Value_I;
+with System.Vs_Int;
+with System.Vs_Uns;
 
 package System.Val_Int with SPARK_Mode is
    pragma Preelaborate;
@@ -57,7 +59,8 @@ package System.Val_Int with SPARK_Mode is
      (Int               => Integer,
       Uns               => Unsigned,
       Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
-      Uns_Params        => System.Val_Uns.Impl.Spec.Uns_Params);
+      U_Spec            => System.Vs_Uns.Spec,
+      Spec              => System.Vs_Int.Spec);
 
    procedure Scan_Integer
      (Str : String;
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index 93d96bcb0f9..fb10b668113 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -47,6 +47,8 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Unsigned_Types;
 with System.Val_LLU;
 with System.Value_I;
+with System.Vs_LLI;
+with System.Vs_LLU;
 
 package System.Val_LLI with SPARK_Mode is
    pragma Preelaborate;
@@ -57,7 +59,8 @@ package System.Val_LLI with SPARK_Mode is
      (Int               => Long_Long_Integer,
       Uns               => Long_Long_Unsigned,
       Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned,
-      Uns_Params        => System.Val_LLU.Impl.Spec.Uns_Params);
+      U_Spec            => System.Vs_LLU.Spec,
+      Spec              => System.Vs_LLI.Spec);
 
    procedure Scan_Long_Long_Integer
      (Str  : String;
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index e31b692ccde..8122da8c3ab 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -47,6 +47,8 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Unsigned_Types;
 with System.Val_LLLU;
 with System.Value_I;
+with System.Vs_LLLI;
+with System.Vs_LLLU;
 
 package System.Val_LLLI with SPARK_Mode is
    pragma Preelaborate;
@@ -57,7 +59,8 @@ package System.Val_LLLI with SPARK_Mode is
      (Int               => Long_Long_Long_Integer,
       Uns               => Long_Long_Long_Unsigned,
       Scan_Raw_Unsigned => Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
-      Uns_Params        => System.Val_LLLU.Impl.Spec.Uns_Params);
+      U_Spec            => System.Vs_LLLU.Spec,
+      Spec              => System.Vs_LLLI.Spec);
 
    procedure Scan_Long_Long_Long_Integer
      (Str  : String;
diff --git a/gcc/ada/libgnat/s-vallllu.ads b/gcc/ada/libgnat/s-vallllu.ads
index 4dcf4c8ec83..0957f843ad0 100644
--- a/gcc/ada/libgnat/s-vallllu.ads
+++ b/gcc/ada/libgnat/s-vallllu.ads
@@ -46,13 +46,14 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Unsigned_Types;
 with System.Value_U;
+with System.Vs_LLLU;
 
 package System.Val_LLLU with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
-   package Impl is new Value_U (Long_Long_Long_Unsigned);
+   package Impl is new Value_U (Long_Long_Long_Unsigned, System.Vs_LLLU.Spec);
 
    procedure Scan_Raw_Long_Long_Long_Unsigned
      (Str : String;
diff --git a/gcc/ada/libgnat/s-valllu.ads b/gcc/ada/libgnat/s-valllu.ads
index c4d73d0b9b2..e8605054a24 100644
--- a/gcc/ada/libgnat/s-valllu.ads
+++ b/gcc/ada/libgnat/s-valllu.ads
@@ -46,13 +46,14 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Unsigned_Types;
 with System.Value_U;
+with System.Vs_LLU;
 
 package System.Val_LLU with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
-   package Impl is new Value_U (Long_Long_Unsigned);
+   package Impl is new Value_U (Long_Long_Unsigned, System.Vs_LLU.Spec);
 
    procedure Scan_Raw_Long_Long_Unsigned
      (Str : String;
diff --git a/gcc/ada/libgnat/s-valspe.adb b/gcc/ada/libgnat/s-valspe.adb
new file mode 100644
index 00000000000..56e6ed77209
--- /dev/null
+++ b/gcc/ada/libgnat/s-valspe.adb
@@ -0,0 +1,82 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                      S Y S T E M . V A L _ S P E C                       --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  Ghost code, loop invariants and assertions in this unit are meant for
+--  analysis only, not for run-time checking, as it would be too costly
+--  otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
+package body System.Val_Spec
+  with SPARK_Mode
+is
+
+   ---------------------------
+   -- First_Non_Space_Ghost --
+   ---------------------------
+
+   function First_Non_Space_Ghost
+     (S        : String;
+      From, To : Integer) return Positive
+   is
+   begin
+      for J in From .. To loop
+         if S (J) /= ' ' then
+            return J;
+         end if;
+
+         pragma Loop_Invariant (for all K in From .. J => S (K) = ' ');
+      end loop;
+
+      raise Program_Error;
+   end First_Non_Space_Ghost;
+
+   -----------------------
+   -- Last_Number_Ghost --
+   -----------------------
+
+   function Last_Number_Ghost (Str : String) return Positive is
+   begin
+      for J in Str'Range loop
+         if Str (J) not in '0' .. '9' | '_' then
+            return J - 1;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Str'First .. J => Str (K) in '0' .. '9' | '_');
+      end loop;
+
+      return Str'Last;
+   end Last_Number_Ghost;
+
+end System.Val_Spec;
diff --git a/gcc/ada/libgnat/s-valspe.ads b/gcc/ada/libgnat/s-valspe.ads
new file mode 100644
index 00000000000..dd861e5029f
--- /dev/null
+++ b/gcc/ada/libgnat/s-valspe.ads
@@ -0,0 +1,211 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                      S Y S T E M . V A L _ S P E C                       --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package provides some common specification functions used by the
+--  s-valxxx files.
+
+--  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);
+
+package System.Val_Spec with
+  SPARK_Mode,
+  Pure,
+  Ghost
+is
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is
+      (for all J in From .. To => S (J) = ' ')
+   with
+     Pre  => From > To or else (From >= S'First and then To <= S'Last),
+     Post => True;
+   --  Ghost function that returns True if S has only space characters from
+   --  index From to index To.
+
+   function First_Non_Space_Ghost
+     (S        : String;
+      From, To : Integer) return Positive
+   with
+     Pre  => From in S'Range
+       and then To in S'Range
+       and then not Only_Space_Ghost (S, From, To),
+     Post => First_Non_Space_Ghost'Result in From .. To
+       and then S (First_Non_Space_Ghost'Result) /= ' '
+       and then Only_Space_Ghost
+         (S, From, First_Non_Space_Ghost'Result - 1);
+   --  Ghost function that returns the index of the first non-space character
+   --  in S, which necessarily exists given the precondition on S.
+
+   function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean
+   is
+      (for all J in From .. To => Str (J) in '0' .. '9' | '_')
+   with
+     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+   --  Ghost function that returns True if S has only number characters from
+   --  index From to index To.
+
+   function Last_Number_Ghost (Str : String) return Positive
+   with
+     Pre  => Str /= "" and then Str (Str'First) in '0' .. '9',
+     Post => Last_Number_Ghost'Result in Str'Range
+       and then (if Last_Number_Ghost'Result < Str'Last then
+                   Str (Last_Number_Ghost'Result + 1) not in '0' .. '9' | '_')
+       and then Only_Number_Ghost (Str, Str'First, Last_Number_Ghost'Result);
+   --  Ghost function that returns the index of the last character in S that
+   --  is either a figure or underscore, which necessarily exists given the
+   --  precondition on Str.
+
+   function Is_Natural_Format_Ghost (Str : String) return Boolean is
+     (Str /= ""
+        and then Str (Str'First) in '0' .. '9'
+        and then
+        (declare
+           L : constant Positive := Last_Number_Ghost (Str);
+         begin
+           Str (L) in '0' .. '9'
+             and then (for all J in Str'First .. L =>
+                         (if Str (J) = '_' then Str (J + 1) /= '_'))));
+   --  Ghost function that determines if Str has the correct format for a
+   --  natural number, consisting in a sequence of figures possibly separated
+   --  by single underscores. It may be followed by other characters.
+
+   function Starts_As_Exponent_Format_Ghost
+     (Str  : String;
+      Real : Boolean := False) return Boolean
+   is
+     (Str'Length > 1
+      and then Str (Str'First) in 'E' | 'e'
+      and then
+        (declare
+            Plus_Sign  : constant Boolean := Str (Str'First + 1) = '+';
+            Minus_Sign : constant Boolean := Str (Str'First + 1) = '-';
+            Sign       : constant Boolean := Plus_Sign or Minus_Sign;
+         begin
+           (if Minus_Sign then Real)
+            and then (if Sign then Str'Length > 2)
+            and then
+              (declare
+                 Start : constant Natural :=
+                  (if Sign then Str'First + 2 else Str'First + 1);
+               begin
+                 Str (Start) in '0' .. '9')));
+   --  Ghost function that determines if Str is recognized as something which
+   --  might be an exponent, ie. it starts with an 'e', capitalized or not,
+   --  followed by an optional sign which can only be '-' if we are working on
+   --  real numbers (Real is True), and then a digit in decimal notation.
+
+   function Is_Opt_Exponent_Format_Ghost
+     (Str  : String;
+      Real : Boolean := False) return Boolean
+   is
+     (not Starts_As_Exponent_Format_Ghost (Str, Real)
+      or else
+        (declare
+           Start : constant Natural :=
+             (if Str (Str'First + 1) in '+' | '-' then Str'First + 2
+              else Str'First + 1);
+         begin Is_Natural_Format_Ghost (Str (Start .. Str'Last))));
+   --  Ghost function that determines if Str has the correct format for an
+   --  optional exponent, that is, either it does not start as an exponent, or
+   --  it is in a correct format for a natural number.
+
+   function Scan_Natural_Ghost
+     (Str : String;
+      P   : Natural;
+      Acc : Natural)
+      return Natural
+   with
+     Subprogram_Variant => (Increases => P),
+     Pre => Str /= "" and then Str (Str'First) in '0' .. '9'
+       and then Str'Last < Natural'Last
+       and then P in Str'First .. Last_Number_Ghost (Str) + 1;
+   --  Ghost function that recursively computes the natural number in Str, up
+   --  to the first number greater or equal to Natural'Last / 10, assuming Acc
+   --  has been scanned already and scanning continues at index P.
+
+   function Scan_Exponent_Ghost
+     (Str  : String;
+      Real : Boolean := False)
+      return Integer
+   is
+     (declare
+        Plus_Sign  : constant Boolean := Str (Str'First + 1) = '+';
+        Minus_Sign : constant Boolean := Str (Str'First + 1) = '-';
+        Sign       : constant Boolean := Plus_Sign or Minus_Sign;
+        Start      : constant Natural :=
+          (if Sign then Str'First + 2 else Str'First + 1);
+        Value      : constant Natural :=
+          Scan_Natural_Ghost (Str (Start .. Str'Last), Start, 0);
+      begin
+        (if Minus_Sign then -Value else Value))
+   with
+     Pre  => Str'Last < Natural'Last
+       and then Starts_As_Exponent_Format_Ghost (Str, Real),
+     Post => (if not Real then Scan_Exponent_Ghost'Result >= 0);
+   --  Ghost function that scans an exponent
+
+private
+
+   ------------------------
+   -- Scan_Natural_Ghost --
+   ------------------------
+
+   function Scan_Natural_Ghost
+     (Str : String;
+      P   : Natural;
+      Acc : Natural)
+      return Natural
+   is
+     (if P > Str'Last
+        or else Str (P) not in '0' .. '9' | '_'
+        or else Acc >= Integer'Last / 10
+      then
+        Acc
+      elsif Str (P) = '_' then
+        Scan_Natural_Ghost (Str, P + 1, Acc)
+      else
+        (declare
+           Shift_Acc : constant Natural :=
+             Acc * 10 +
+               (Integer'(Character'Pos (Str (P))) -
+                  Integer'(Character'Pos ('0')));
+         begin
+           Scan_Natural_Ghost (Str, P + 1, Shift_Acc)));
+
+end System.Val_Spec;
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index 5932a0108b7..71bfc0cbf7d 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -29,6 +29,8 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+with System.Val_Util; use System.Val_Util;
+
 package body System.Value_I is
 
    --  Ghost code, loop invariants and assertions in this unit are meant for
@@ -98,7 +100,7 @@ package body System.Value_I is
 
       Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
       pragma Assert
-        (Uval = Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
+        (Uval = U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
 
       --  Deal with overflow cases, and also with largest negative number
 
@@ -175,7 +177,7 @@ package body System.Value_I is
             end;
 
             pragma Assert
-              (P = Uns_Params.Raw_Unsigned_Last_Ghost
+              (P = U_Spec.Raw_Unsigned_Last_Ghost
                  (Str, Fst_Num, Str'Last));
 
             Scan_Trailing_Blanks (Str, P);
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index 0ff25f51718..baf1f866535 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -38,8 +38,9 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
-with System.Val_Util; use System.Val_Util;
+with System.Val_Spec; use System.Val_Spec;
 with System.Value_I_Spec;
+with System.Value_U_Spec;
 
 generic
 
@@ -55,15 +56,13 @@ generic
 
    --  Additional parameters for ghost subprograms used inside contracts
 
-   with package Uns_Params is new System.Val_Util.Uns_Params
-     (Uns => Uns, others => <>)
+   with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
+   with package Spec is new System.Value_I_Spec
+     (Int => Int, Uns => Uns, U_Spec => U_Spec)
    with Ghost;
 
 package System.Value_I is
    pragma Preelaborate;
-   use all type Uns_Params.Uns_Option;
-
-   package Spec is new System.Value_I_Spec (Int, Uns, Uns_Params);
 
    procedure Scan_Integer
      (Str : String;
@@ -84,12 +83,12 @@ package System.Value_I is
               (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
                else Non_Blank);
           begin
-            Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
-              and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost
+            U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
+              and then U_Spec.Raw_Unsigned_No_Overflow_Ghost
                 (Str, Fst_Num, Max)
               and then Spec.Uns_Is_Valid_Int
                 (Minus => Str (Non_Blank) = '-',
-                 Uval  => Uns_Params.Scan_Raw_Unsigned_Ghost
+                 Uval  => U_Spec.Scan_Raw_Unsigned_Ghost
                    (Str, Fst_Num, Max))),
     Post =>
       (declare
@@ -99,12 +98,12 @@ package System.Value_I is
            (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
             else Non_Blank);
          Uval      : constant Uns :=
-            Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
+            U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
        begin
            Spec.Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
                                Uval  => Uval,
                                Val   => Res)
-           and then Ptr.all = Uns_Params.Raw_Unsigned_Last_Ghost
+           and then Ptr.all = U_Spec.Raw_Unsigned_Last_Ghost
              (Str, Fst_Num, Max));
    --  This procedure scans the string starting at Str (Ptr.all) for a valid
    --  integer according to the syntax described in (RM 3.5(43)). The substring
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index 9c77caa3bcb..7aeed3bed0d 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -30,6 +30,7 @@
 ------------------------------------------------------------------------------
 
 with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
+with System.Val_Util;             use System.Val_Util;
 
 package body System.Value_U is
 
diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads
index 6cc0260d101..fabaa36d627 100644
--- a/gcc/ada/libgnat/s-valueu.ads
+++ b/gcc/ada/libgnat/s-valueu.ads
@@ -45,17 +45,19 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Subprogram_Variant => Ignore);
 
 with System.Value_U_Spec;
-with System.Val_Util; use System.Val_Util;
+with System.Val_Spec; use System.Val_Spec;
 
 generic
 
    type Uns is mod <>;
 
+   --  Additional parameters for ghost subprograms used inside contracts
+
+   with package Spec is new System.Value_U_Spec (Uns => Uns) with Ghost;
+
 package System.Value_U is
    pragma Preelaborate;
 
-   package Spec is new System.Value_U_Spec (Uns);
-
    procedure Scan_Raw_Unsigned
      (Str : String;
       Ptr : not null access Integer;
diff --git a/gcc/ada/libgnat/s-valuns.ads b/gcc/ada/libgnat/s-valuns.ads
index 357e5d67bba..11761539e4b 100644
--- a/gcc/ada/libgnat/s-valuns.ads
+++ b/gcc/ada/libgnat/s-valuns.ads
@@ -46,13 +46,14 @@ pragma Assertion_Policy (Pre                => Ignore,
 
 with System.Unsigned_Types;
 with System.Value_U;
+with System.Vs_Uns;
 
 package System.Val_Uns with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Unsigned is Unsigned_Types.Unsigned;
 
-   package Impl is new Value_U (Unsigned);
+   package Impl is new Value_U (Unsigned, System.Vs_Uns.Spec);
 
    procedure Scan_Raw_Unsigned
      (Str : String;
diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb
index ee37c1a636b..5dfc307a46a 100644
--- a/gcc/ada/libgnat/s-valuti.adb
+++ b/gcc/ada/libgnat/s-valuti.adb
@@ -62,44 +62,6 @@ is
       end if;
    end Bad_Value;
 
-   ---------------------------
-   -- First_Non_Space_Ghost --
-   ---------------------------
-
-   function First_Non_Space_Ghost
-     (S        : String;
-      From, To : Integer) return Positive
-   is
-   begin
-      for J in From .. To loop
-         if S (J) /= ' ' then
-            return J;
-         end if;
-
-         pragma Loop_Invariant (for all K in From .. J => S (K) = ' ');
-      end loop;
-
-      raise Program_Error;
-   end First_Non_Space_Ghost;
-
-   -----------------------
-   -- Last_Number_Ghost --
-   -----------------------
-
-   function Last_Number_Ghost (Str : String) return Positive is
-   begin
-      for J in Str'Range loop
-         if Str (J) not in '0' .. '9' | '_' then
-            return J - 1;
-         end if;
-
-         pragma Loop_Invariant
-           (for all K in Str'First .. J => Str (K) in '0' .. '9' | '_');
-      end loop;
-
-      return Str'Last;
-   end Last_Number_Ghost;
-
    ----------------------
    -- Normalize_String --
    ----------------------
@@ -224,10 +186,10 @@ is
 
       declare
          Rest : constant String := Str (P .. Max) with Ghost;
-         Last : constant Natural := Last_Number_Ghost (Rest) with Ghost;
+         Last : constant Natural := Sp.Last_Number_Ghost (Rest) with Ghost;
 
       begin
-         pragma Assert (Is_Natural_Format_Ghost (Rest));
+         pragma Assert (Sp.Is_Natural_Format_Ghost (Rest));
 
          loop
             pragma Assert (Str (P) in '0' .. '9');
@@ -240,8 +202,8 @@ is
             pragma Loop_Invariant (P in Rest'First .. Last);
             pragma Loop_Invariant (Str (P) in '0' .. '9');
             pragma Loop_Invariant
-              (Scan_Natural_Ghost (Rest, Rest'First, 0)
-               = Scan_Natural_Ghost (Rest, P + 1, X));
+              (Sp.Scan_Natural_Ghost (Rest, Rest'First, 0)
+               = Sp.Scan_Natural_Ghost (Rest, P + 1, X));
 
             P := P + 1;
 
@@ -301,7 +263,7 @@ is
 
       Start := P;
 
-      pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
+      pragma Assert (Start = Sp.First_Non_Space_Ghost (Str, Ptr.all, Max));
 
       --  Skip past an initial plus sign
 
@@ -357,7 +319,7 @@ is
 
       Start := P;
 
-      pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
+      pragma Assert (Start = Sp.First_Non_Space_Ghost (Str, Ptr.all, Max));
 
       --  Remember an initial minus sign
 
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 22d0612bc32..cdd56c0de68 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -43,12 +43,15 @@ pragma Assertion_Policy (Pre            => Ignore,
                          Ghost          => Ignore);
 
 with System.Case_Util;
+with System.Val_Spec;
 
 package System.Val_Util
   with SPARK_Mode, Pure
 is
    pragma Unevaluated_Use_Of_Old (Allow);
 
+   package Sp renames System.Val_Spec;
+
    procedure Bad_Value (S : String)
    with
      Depends => (null => S),
@@ -56,46 +59,22 @@ is
    pragma No_Return (Bad_Value);
    --  Raises constraint error with message: bad input for 'Value: "xxx"
 
-   function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is
-      (for all J in From .. To => S (J) = ' ')
-   with
-     Ghost,
-     Pre  => From > To or else (From >= S'First and then To <= S'Last),
-     Post => True;
-   --  Ghost function that returns True if S has only space characters from
-   --  index From to index To.
-
-   function First_Non_Space_Ghost
-     (S        : String;
-      From, To : Integer) return Positive
-   with
-     Ghost,
-     Pre  => From in S'Range
-       and then To in S'Range
-       and then not Only_Space_Ghost (S, From, To),
-     Post => First_Non_Space_Ghost'Result in From .. To
-       and then S (First_Non_Space_Ghost'Result) /= ' '
-       and then Only_Space_Ghost
-         (S, From, First_Non_Space_Ghost'Result - 1);
-   --  Ghost function that returns the index of the first non-space character
-   --  in S, which necessarily exists given the precondition on S.
-
    procedure Normalize_String
      (S    : in out String;
       F, L : out Integer)
    with
-     Post => (if Only_Space_Ghost (S'Old, S'First, S'Last) then
+     Post => (if Sp.Only_Space_Ghost (S'Old, S'First, S'Last) then
                 F > L
               else
                 F >= S'First
                   and then L <= S'Last
                   and then F <= L
-                  and then Only_Space_Ghost (S'Old, S'First, F - 1)
+                  and then Sp.Only_Space_Ghost (S'Old, S'First, F - 1)
                   and then S'Old (F) /= ' '
                   and then S'Old (L) /= ' '
                   and then
                     (if L < S'Last then
-                      Only_Space_Ghost (S'Old, L + 1, S'Last))
+                      Sp.Only_Space_Ghost (S'Old, L + 1, S'Last))
                   and then
                     (if S'Old (F) /= ''' then
                       (for all J in S'Range =>
@@ -119,18 +98,18 @@ is
      Pre  =>
        --  Ptr.all .. Max is either an empty range, or a valid range in Str
        (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
-       and then not Only_Space_Ghost (Str, Ptr.all, Max)
+       and then not Sp.Only_Space_Ghost (Str, Ptr.all, Max)
        and then
          (declare
             F : constant Positive :=
-              First_Non_Space_Ghost (Str, Ptr.all, Max);
+              Sp.First_Non_Space_Ghost (Str, Ptr.all, Max);
           begin
             (if Str (F) in '+' | '-' then
                F <= Max - 1 and then Str (F + 1) /= ' ')),
      Post =>
        (declare
           F : constant Positive :=
-            First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
+            Sp.First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
         begin
           Minus = (Str (F) = '-')
             and then Ptr.all = (if Str (F) in '+' | '-' then F + 1 else F)
@@ -164,142 +143,24 @@ is
      Pre  =>
        --  Ptr.all .. Max is either an empty range, or a valid range in Str
        (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
-       and then not Only_Space_Ghost (Str, Ptr.all, Max)
+       and then not Sp.Only_Space_Ghost (Str, Ptr.all, Max)
        and then
          (declare
             F : constant Positive :=
-              First_Non_Space_Ghost (Str, Ptr.all, Max);
+              Sp.First_Non_Space_Ghost (Str, Ptr.all, Max);
           begin
             (if Str (F) = '+' then
                F <= Max - 1 and then Str (F + 1) /= ' ')),
      Post =>
        (declare
           F : constant Positive :=
-            First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
+            Sp.First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
         begin
           Ptr.all = (if Str (F) = '+' then F + 1 else F)
             and then Start = F);
    --  Same as Scan_Sign, but allows only plus, not minus. This is used for
    --  modular types.
 
-   function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean
-   is
-      (for all J in From .. To => Str (J) in '0' .. '9' | '_')
-   with
-     Ghost,
-     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
-   --  Ghost function that returns True if S has only number characters from
-   --  index From to index To.
-
-   function Last_Number_Ghost (Str : String) return Positive
-   with
-     Ghost,
-     Pre  => Str /= "" and then Str (Str'First) in '0' .. '9',
-     Post => Last_Number_Ghost'Result in Str'Range
-       and then (if Last_Number_Ghost'Result < Str'Last then
-                   Str (Last_Number_Ghost'Result + 1) not in '0' .. '9' | '_')
-       and then Only_Number_Ghost (Str, Str'First, Last_Number_Ghost'Result);
-   --  Ghost function that returns the index of the last character in S that
-   --  is either a figure or underscore, which necessarily exists given the
-   --  precondition on Str.
-
-   function Is_Natural_Format_Ghost (Str : String) return Boolean is
-     (Str /= ""
-        and then Str (Str'First) in '0' .. '9'
-        and then
-        (declare
-           L : constant Positive := Last_Number_Ghost (Str);
-         begin
-           Str (L) in '0' .. '9'
-             and then (for all J in Str'First .. L =>
-                         (if Str (J) = '_' then Str (J + 1) /= '_'))))
-   with
-     Ghost;
-   --  Ghost function that determines if Str has the correct format for a
-   --  natural number, consisting in a sequence of figures possibly separated
-   --  by single underscores. It may be followed by other characters.
-
-   function Starts_As_Exponent_Format_Ghost
-     (Str  : String;
-      Real : Boolean := False) return Boolean
-   is
-     (Str'Length > 1
-      and then Str (Str'First) in 'E' | 'e'
-      and then
-        (declare
-            Plus_Sign  : constant Boolean := Str (Str'First + 1) = '+';
-            Minus_Sign : constant Boolean := Str (Str'First + 1) = '-';
-            Sign       : constant Boolean := Plus_Sign or Minus_Sign;
-         begin
-           (if Minus_Sign then Real)
-            and then (if Sign then Str'Length > 2)
-            and then
-              (declare
-                 Start : constant Natural :=
-                  (if Sign then Str'First + 2 else Str'First + 1);
-               begin
-                 Str (Start) in '0' .. '9')))
-   with
-     Ghost;
-   --  Ghost function that determines if Str is recognized as something which
-   --  might be an exponent, ie. it starts with an 'e', capitalized or not,
-   --  followed by an optional sign which can only be '-' if we are working on
-   --  real numbers (Real is True), and then a digit in decimal notation.
-
-   function Is_Opt_Exponent_Format_Ghost
-     (Str  : String;
-      Real : Boolean := False) return Boolean
-   is
-     (not Starts_As_Exponent_Format_Ghost (Str, Real)
-      or else
-        (declare
-           Start : constant Natural :=
-             (if Str (Str'First + 1) in '+' | '-' then Str'First + 2
-              else Str'First + 1);
-         begin Is_Natural_Format_Ghost (Str (Start .. Str'Last))))
-   with
-     Ghost;
-   --  Ghost function that determines if Str has the correct format for an
-   --  optional exponent, that is, either it does not start as an exponent, or
-   --  it is in a correct format for a natural number.
-
-   function Scan_Natural_Ghost
-     (Str : String;
-      P   : Natural;
-      Acc : Natural)
-      return Natural
-   with
-     Ghost,
-     Subprogram_Variant => (Increases => P),
-     Pre => Str /= "" and then Str (Str'First) in '0' .. '9'
-       and then Str'Last < Natural'Last
-       and then P in Str'First .. Last_Number_Ghost (Str) + 1;
-   --  Ghost function that recursively computes the natural number in Str, up
-   --  to the first number greater or equal to Natural'Last / 10, assuming Acc
-   --  has been scanned already and scanning continues at index P.
-
-   function Scan_Exponent_Ghost
-     (Str  : String;
-      Real : Boolean := False)
-      return Integer
-   is
-     (declare
-        Plus_Sign  : constant Boolean := Str (Str'First + 1) = '+';
-        Minus_Sign : constant Boolean := Str (Str'First + 1) = '-';
-        Sign       : constant Boolean := Plus_Sign or Minus_Sign;
-        Start      : constant Natural :=
-          (if Sign then Str'First + 2 else Str'First + 1);
-        Value      : constant Natural :=
-          Scan_Natural_Ghost (Str (Start .. Str'Last), Start, 0);
-      begin
-        (if Minus_Sign then -Value else Value))
-   with
-     Ghost,
-     Pre  => Str'Last < Natural'Last
-       and then Starts_As_Exponent_Format_Ghost (Str, Real),
-     Post => (if not Real then Scan_Exponent_Ghost'Result >= 0);
-   --  Ghost function that scans an exponent
-
    procedure Scan_Exponent
      (Str  : String;
       Ptr  : not null access Integer;
@@ -311,14 +172,15 @@ is
        --  Ptr.all .. Max is either an empty range, or a valid range in Str
        (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
          and then Max < Natural'Last
-         and then Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real),
+         and then Sp.Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real),
      Post =>
-       (if Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real)
-        then Exp = Scan_Exponent_Ghost (Str (Ptr.all'Old .. Max), Real)
+       (if Sp.Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real)
+        then Exp = Sp.Scan_Exponent_Ghost (Str (Ptr.all'Old .. Max), Real)
           and then
           (if Str (Ptr.all'Old + 1) in '-' | '+' then
-             Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 2 .. Max)) + 1
-           else Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 1 .. Max)) + 1)
+             Ptr.all = Sp.Last_Number_Ghost (Str (Ptr.all'Old + 2 .. Max)) + 1
+           else
+             Ptr.all = Sp.Last_Number_Ghost (Str (Ptr.all'Old + 1 .. Max)) + 1)
         else Exp = 0 and Ptr.all = Ptr.all'Old);
    --  Called to scan a possible exponent. Str, Ptr, Max are as described above
    --  for Scan_Sign. If Ptr.all < Max and Str (Ptr.all) = 'E' or 'e', then an
@@ -337,7 +199,7 @@ is
    procedure Scan_Trailing_Blanks (Str : String; P : Positive)
    with
      Pre => P >= Str'First
-       and then Only_Space_Ghost (Str, P, Str'Last);
+       and then Sp.Only_Space_Ghost (Str, P, Str'Last);
    --  Checks that the remainder of the field Str (P .. Str'Last) is all
    --  blanks. Raises Constraint_Error if a non-blank character is found.
 
@@ -375,302 +237,4 @@ is
    --  no check for this case, the caller must ensure this condition is met.
    pragma Warnings (GNATprove, On, """Ptr"" is not modified");
 
-   --  Bundle Uns type with other types, constants and subprograms used in
-   --  ghost code, so that this package can be instantiated once and used
-   --  multiple times as generic formal for a given Uns type.
-   generic
-      type Uns is mod <>;
-      type P_Uns_Option is private with Ghost;
-      with function P_Wrap_Option (Value : Uns) return P_Uns_Option
-        with Ghost;
-      with function P_Hexa_To_Unsigned_Ghost (X : Character) return Uns
-        with Ghost;
-      with function P_Scan_Overflows_Ghost
-        (Digit : Uns;
-         Base  : Uns;
-         Acc   : Uns) return Boolean
-        with Ghost;
-      with function P_Is_Raw_Unsigned_Format_Ghost
-        (Str : String) return Boolean
-        with Ghost;
-      with function P_Scan_Split_No_Overflow_Ghost
-        (Str      : String;
-         From, To : Integer)
-      return Boolean
-        with Ghost;
-      with function P_Raw_Unsigned_No_Overflow_Ghost
-        (Str      : String;
-         From, To : Integer)
-      return Boolean
-        with Ghost;
-
-      with function P_Exponent_Unsigned_Ghost
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10) return P_Uns_Option
-        with Ghost;
-      with procedure P_Lemma_Exponent_Unsigned_Ghost_Base
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10)
-        with Ghost;
-      with procedure P_Lemma_Exponent_Unsigned_Ghost_Overflow
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10)
-        with Ghost;
-      with procedure P_Lemma_Exponent_Unsigned_Ghost_Step
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10)
-        with Ghost;
-
-      with function P_Scan_Raw_Unsigned_Ghost
-        (Str      : String;
-         From, To : Integer)
-      return Uns
-        with Ghost;
-      with procedure P_Lemma_Scan_Based_Number_Ghost_Base
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-        with Ghost;
-      with procedure P_Lemma_Scan_Based_Number_Ghost_Underscore
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-        with Ghost;
-      with procedure P_Lemma_Scan_Based_Number_Ghost_Overflow
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-        with Ghost;
-      with procedure P_Lemma_Scan_Based_Number_Ghost_Step
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-        with Ghost;
-
-      with function P_Raw_Unsigned_Last_Ghost
-        (Str      : String;
-         From, To : Integer)
-      return Positive
-        with Ghost;
-      with function P_Only_Decimal_Ghost
-        (Str      : String;
-         From, To : Integer)
-      return Boolean
-        with Ghost;
-      with function P_Scan_Based_Number_Ghost
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-      return P_Uns_Option
-        with Ghost;
-      with function P_Is_Unsigned_Ghost (Str : String) return Boolean
-        with Ghost;
-      with function P_Is_Value_Unsigned_Ghost
-        (Str : String;
-         Val : Uns) return Boolean
-        with Ghost;
-
-      with procedure P_Prove_Scan_Only_Decimal_Ghost
-        (Str : String;
-         Val : Uns)
-        with Ghost;
-      with procedure P_Prove_Scan_Based_Number_Ghost_Eq
-        (Str1, Str2 : String;
-         From, To   : Integer;
-         Base       : Uns := 10;
-         Acc        : Uns := 0)
-        with Ghost;
-
-   package Uns_Params is
-      subtype Uns_Option is P_Uns_Option with Ghost;
-      function Wrap_Option (Value : Uns) return Uns_Option renames
-        P_Wrap_Option;
-      function Hexa_To_Unsigned_Ghost
-        (X : Character) return Uns
-         renames P_Hexa_To_Unsigned_Ghost;
-      function Scan_Overflows_Ghost
-        (Digit : Uns;
-         Base  : Uns;
-         Acc   : Uns) return Boolean
-         renames P_Scan_Overflows_Ghost;
-      function Is_Raw_Unsigned_Format_Ghost
-        (Str : String) return Boolean
-         renames P_Is_Raw_Unsigned_Format_Ghost;
-      function Scan_Split_No_Overflow_Ghost
-        (Str      : String;
-         From, To : Integer) return Boolean
-         renames P_Scan_Split_No_Overflow_Ghost;
-      function Raw_Unsigned_No_Overflow_Ghost
-        (Str      : String;
-         From, To : Integer) return Boolean
-         renames P_Raw_Unsigned_No_Overflow_Ghost;
-
-      function Exponent_Unsigned_Ghost
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10) return Uns_Option
-         renames P_Exponent_Unsigned_Ghost;
-      procedure Lemma_Exponent_Unsigned_Ghost_Base
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10)
-         renames P_Lemma_Exponent_Unsigned_Ghost_Base;
-      procedure Lemma_Exponent_Unsigned_Ghost_Overflow
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10)
-         renames P_Lemma_Exponent_Unsigned_Ghost_Overflow;
-      procedure Lemma_Exponent_Unsigned_Ghost_Step
-        (Value : Uns;
-         Exp   : Natural;
-         Base  : Uns := 10)
-         renames P_Lemma_Exponent_Unsigned_Ghost_Step;
-
-      function Scan_Raw_Unsigned_Ghost
-        (Str      : String;
-         From, To : Integer) return Uns
-         renames P_Scan_Raw_Unsigned_Ghost;
-      procedure Lemma_Scan_Based_Number_Ghost_Base
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-         renames P_Lemma_Scan_Based_Number_Ghost_Base;
-      procedure Lemma_Scan_Based_Number_Ghost_Underscore
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-         renames P_Lemma_Scan_Based_Number_Ghost_Underscore;
-      procedure Lemma_Scan_Based_Number_Ghost_Overflow
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-         renames P_Lemma_Scan_Based_Number_Ghost_Overflow;
-      procedure Lemma_Scan_Based_Number_Ghost_Step
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-         renames P_Lemma_Scan_Based_Number_Ghost_Step;
-
-      function Raw_Unsigned_Last_Ghost
-        (Str      : String;
-         From, To : Integer) return Positive
-         renames P_Raw_Unsigned_Last_Ghost;
-      function Only_Decimal_Ghost
-        (Str      : String;
-         From, To : Integer) return Boolean
-         renames P_Only_Decimal_Ghost;
-      function Scan_Based_Number_Ghost
-        (Str      : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0) return Uns_Option
-         renames P_Scan_Based_Number_Ghost;
-      function Is_Unsigned_Ghost (Str : String) return Boolean
-         renames P_Is_Unsigned_Ghost;
-      function Is_Value_Unsigned_Ghost
-        (Str : String;
-         Val : Uns) return Boolean
-         renames P_Is_Value_Unsigned_Ghost;
-
-      procedure Prove_Scan_Only_Decimal_Ghost
-        (Str : String;
-         Val : Uns)
-         renames P_Prove_Scan_Only_Decimal_Ghost;
-      procedure Prove_Scan_Based_Number_Ghost_Eq
-        (Str1, Str2 : String;
-         From, To   : Integer;
-         Base       : Uns := 10;
-         Acc        : Uns := 0)
-      renames P_Prove_Scan_Based_Number_Ghost_Eq;
-   end Uns_Params;
-
-   --  Bundle Int type with other types, constants and subprograms used in
-   --  ghost code, so that this package can be instantiated once and used
-   --  multiple times as generic formal for a given Int type.
-   generic
-      type Int is range <>;
-      type Uns is mod <>;
-
-      with package P_Uns_Params is new System.Val_Util.Uns_Params
-        (Uns => Uns, others => <>)
-         with Ghost;
-
-      with function P_Abs_Uns_Of_Int (Val : Int) return Uns
-         with Ghost;
-      with function P_Is_Int_Of_Uns
-        (Minus : Boolean;
-         Uval  : Uns;
-         Val   : Int)
-      return Boolean
-         with Ghost;
-      with function P_Is_Integer_Ghost (Str : String) return Boolean
-         with Ghost;
-      with function P_Is_Value_Integer_Ghost
-        (Str : String;
-         Val : Int) return Boolean
-         with Ghost;
-      with procedure P_Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
-         with Ghost;
-
-   package Int_Params is
-      package Uns_Params renames P_Uns_Params;
-      function Abs_Uns_Of_Int (Val : Int) return Uns renames
-        P_Abs_Uns_Of_Int;
-      function Is_Int_Of_Uns
-        (Minus : Boolean;
-         Uval  : Uns;
-         Val   : Int)
-      return Boolean
-         renames P_Is_Int_Of_Uns;
-      function Is_Integer_Ghost (Str : String) return Boolean renames
-        P_Is_Integer_Ghost;
-      function Is_Value_Integer_Ghost
-        (Str : String;
-         Val : Int) return Boolean
-         renames P_Is_Value_Integer_Ghost;
-      procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) renames
-        P_Prove_Scan_Only_Decimal_Ghost;
-   end Int_Params;
-
-private
-
-   ------------------------
-   -- Scan_Natural_Ghost --
-   ------------------------
-
-   function Scan_Natural_Ghost
-     (Str : String;
-      P   : Natural;
-      Acc : Natural)
-      return Natural
-   is
-     (if P > Str'Last
-        or else Str (P) not in '0' .. '9' | '_'
-        or else Acc >= Integer'Last / 10
-      then
-        Acc
-      elsif Str (P) = '_' then
-        Scan_Natural_Ghost (Str, P + 1, Acc)
-      else
-        (declare
-           Shift_Acc : constant Natural :=
-             Acc * 10 +
-               (Integer'(Character'Pos (Str (P))) -
-                  Integer'(Character'Pos ('0')));
-         begin
-           Scan_Natural_Ghost (Str, P + 1, Shift_Acc)));
-
 end System.Val_Util;
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads
index bdd97b52e07..a6f81d715c4 100644
--- a/gcc/ada/libgnat/s-vauspe.ads
+++ b/gcc/ada/libgnat/s-vauspe.ads
@@ -44,7 +44,7 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
-with System.Val_Util; use System.Val_Util;
+with System.Val_Spec; use System.Val_Spec;
 
 generic
 
@@ -57,6 +57,17 @@ package System.Value_U_Spec with
 is
    pragma Preelaborate;
 
+   --  Maximum value of exponent for 10 that fits in Uns'Base
+   function Max_Log10 return Natural is
+     (case Uns'Base'Size is
+        when 8   => 2,
+        when 16  => 4,
+        when 32  => 9,
+        when 64  => 19,
+        when 128 => 38,
+        when others => raise Program_Error)
+   with Ghost;
+
    type Uns_Option (Overflow : Boolean := False) is record
       case Overflow is
          when True =>
@@ -598,46 +609,6 @@ is
    --  ghost code, so that this package can be instantiated once and used
    --  multiple times as generic formal for a given Int type.
 
-   package Uns_Params is new System.Val_Util.Uns_Params
-     (Uns                                        => Uns,
-      P_Uns_Option                               => Uns_Option,
-      P_Wrap_Option                              => Wrap_Option,
-      P_Hexa_To_Unsigned_Ghost                   => Hexa_To_Unsigned_Ghost,
-      P_Scan_Overflows_Ghost                     => Scan_Overflows_Ghost,
-      P_Is_Raw_Unsigned_Format_Ghost             =>
-         Is_Raw_Unsigned_Format_Ghost,
-      P_Scan_Split_No_Overflow_Ghost             =>
-         Scan_Split_No_Overflow_Ghost,
-      P_Raw_Unsigned_No_Overflow_Ghost           =>
-         Raw_Unsigned_No_Overflow_Ghost,
-      P_Exponent_Unsigned_Ghost                  => Exponent_Unsigned_Ghost,
-      P_Lemma_Exponent_Unsigned_Ghost_Base       =>
-         Lemma_Exponent_Unsigned_Ghost_Base,
-      P_Lemma_Exponent_Unsigned_Ghost_Overflow   =>
-         Lemma_Exponent_Unsigned_Ghost_Overflow,
-      P_Lemma_Exponent_Unsigned_Ghost_Step       =>
-         Lemma_Exponent_Unsigned_Ghost_Step,
-      P_Scan_Raw_Unsigned_Ghost                  => Scan_Raw_Unsigned_Ghost,
-      P_Lemma_Scan_Based_Number_Ghost_Base       =>
-         Lemma_Scan_Based_Number_Ghost_Base,
-      P_Lemma_Scan_Based_Number_Ghost_Underscore =>
-         Lemma_Scan_Based_Number_Ghost_Underscore,
-      P_Lemma_Scan_Based_Number_Ghost_Overflow   =>
-         Lemma_Scan_Based_Number_Ghost_Overflow,
-      P_Lemma_Scan_Based_Number_Ghost_Step       =>
-         Lemma_Scan_Based_Number_Ghost_Step,
-      P_Raw_Unsigned_Last_Ghost                  => Raw_Unsigned_Last_Ghost,
-      P_Only_Decimal_Ghost                       => Only_Decimal_Ghost,
-      P_Scan_Based_Number_Ghost                  => Scan_Based_Number_Ghost,
-      P_Is_Unsigned_Ghost                        =>
-         Is_Unsigned_Ghost,
-      P_Is_Value_Unsigned_Ghost                  =>
-         Is_Value_Unsigned_Ghost,
-      P_Prove_Scan_Only_Decimal_Ghost            =>
-         Prove_Scan_Only_Decimal_Ghost,
-      P_Prove_Scan_Based_Number_Ghost_Eq         =>
-         Prove_Scan_Based_Number_Ghost_Eq);
-
 private
 
    ----------------
diff --git a/gcc/ada/libgnat/s-vs_int.ads b/gcc/ada/libgnat/s-vs_int.ads
new file mode 100644
index 00000000000..739a30c4389
--- /dev/null
+++ b/gcc/ada/libgnat/s-vs_int.ads
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                         S Y S T E M . V S _ I N T                        --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains specification functions for scanning signed Integer
+--  values for use in Text_IO.Integer_IO, and the Value attribute.
+
+--  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.Unsigned_Types;
+with System.Value_I_Spec;
+with System.Vs_Uns;
+
+package System.Vs_Int with SPARK_Mode, Ghost is
+   pragma Preelaborate;
+
+   subtype Unsigned is Unsigned_Types.Unsigned;
+
+   package Spec is new System.Value_I_Spec
+     (Integer, Unsigned, System.Vs_Uns.Spec);
+
+end System.Vs_Int;
diff --git a/gcc/ada/libgnat/s-vs_lli.ads b/gcc/ada/libgnat/s-vs_lli.ads
new file mode 100644
index 00000000000..e3a1179fb98
--- /dev/null
+++ b/gcc/ada/libgnat/s-vs_lli.ads
@@ -0,0 +1,60 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                         S Y S T E M . V S _ L L I                        --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains specification functions for scanning
+--  Long_Long_Integer values for use in Text_IO.Integer_IO, and the Value
+--  attribute.
+
+--  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.Unsigned_Types;
+with System.Value_I_Spec;
+with System.Vs_LLU;
+
+package System.Vs_LLI with SPARK_Mode, Ghost is
+   pragma Preelaborate;
+
+   subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
+
+   package Spec is new System.Value_I_Spec
+     (Long_Long_Integer, Long_Long_Unsigned, System.Vs_LLU.Spec);
+
+end System.Vs_LLI;
diff --git a/gcc/ada/libgnat/s-vs_llu.ads b/gcc/ada/libgnat/s-vs_llu.ads
new file mode 100644
index 00000000000..f6d933485c4
--- /dev/null
+++ b/gcc/ada/libgnat/s-vs_llu.ads
@@ -0,0 +1,58 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                         S Y S T E M . V S _ L L U                        --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains specification functions for scanning
+--  Long_Long_Unsigned values for use in Text_IO.Modular_IO, and the Value
+--  attribute.
+
+--  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.Unsigned_Types;
+with System.Value_U_Spec;
+
+package System.Vs_LLU with SPARK_Mode, Ghost is
+   pragma Preelaborate;
+
+   subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
+
+   package Spec is new System.Value_U_Spec (Long_Long_Unsigned);
+
+end System.Vs_LLU;
diff --git a/gcc/ada/libgnat/s-vs_uns.ads b/gcc/ada/libgnat/s-vs_uns.ads
new file mode 100644
index 00000000000..5f21684aa69
--- /dev/null
+++ b/gcc/ada/libgnat/s-vs_uns.ads
@@ -0,0 +1,57 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                         S Y S T E M . V S _ U N S                        --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains specification functions for scanning modular Unsigned
+--  values for use in Text_IO.Modular_IO, and the Value attribute.
+
+--  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.Unsigned_Types;
+with System.Value_U_Spec;
+
+package System.Vs_Uns with SPARK_Mode, Ghost is
+   pragma Preelaborate;
+
+   subtype Unsigned is Unsigned_Types.Unsigned;
+
+   package Spec is new System.Value_U_Spec (Unsigned);
+
+end System.Vs_Uns;
diff --git a/gcc/ada/libgnat/s-vsllli.ads b/gcc/ada/libgnat/s-vsllli.ads
new file mode 100644
index 00000000000..f70290b93de
--- /dev/null
+++ b/gcc/ada/libgnat/s-vsllli.ads
@@ -0,0 +1,60 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                        S Y S T E M . V S _ L L L I                       --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains specification functions for scanning
+--  Long_Long_Long_Integer values for use in Text_IO.Integer_IO, and the Value
+--  attribute.
+
+--  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.Unsigned_Types;
+with System.Value_I_Spec;
+with System.Vs_LLLU;
+
+package System.Vs_LLLI with SPARK_Mode, Ghost is
+   pragma Preelaborate;
+
+   subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
+
+   package Spec is new System.Value_I_Spec
+     (Long_Long_Long_Integer, Long_Long_Long_Unsigned, System.Vs_LLLU.Spec);
+
+end System.Vs_LLLI;
diff --git a/gcc/ada/libgnat/s-vslllu.ads b/gcc/ada/libgnat/s-vslllu.ads
new file mode 100644
index 00000000000..0a53cfe9b9f
--- /dev/null
+++ b/gcc/ada/libgnat/s-vslllu.ads
@@ -0,0 +1,58 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                        S Y S T E M . V S _ L L L U                       --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2023-2023, Free Software Foundation, Inc.         --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains specification functions for scanning
+--  Long_Long_Long_Unsigned values for use in Text_IO.Modular_IO, and the Value
+--  attribute.
+
+--  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.Unsigned_Types;
+with System.Value_U_Spec;
+
+package System.Vs_LLLU with SPARK_Mode, Ghost is
+   pragma Preelaborate;
+
+   subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
+
+   package Spec is new System.Value_U_Spec (Long_Long_Long_Unsigned);
+
+end System.Vs_LLLU;
