path: root/gcc/ada/libgnat/s-valuti.ads

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                      S Y S T E M . V A L _ U T I L                       --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--          Copyright (C) 1992-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 utilities 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);

with System.Case_Util;

package System.Val_Util
  with SPARK_Mode, Pure
is
   pragma Unevaluated_Use_Of_Old (Allow);

   procedure Bad_Value (S : String)
   with
     Depends => (null => S),
     Exceptional_Cases => (others => Standard.False);
   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
                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 S'Old (F) /= ' '
                  and then S'Old (L) /= ' '
                  and then
                    (if L < S'Last then
                      Only_Space_Ghost (S'Old, L + 1, S'Last))
                  and then
                    (if S'Old (F) /= ''' then
                      (for all J in S'Range =>
                        (if J in F .. L then
                           S (J) = System.Case_Util.To_Upper (S'Old (J))
                         else
                           S (J) = S'Old (J)))));
   --  This procedure scans the string S setting F to be the index of the first
   --  non-blank character of S and L to be the index of the last non-blank
   --  character of S. Any lower case characters present in S will be folded to
   --  their upper case equivalent except for character literals. If S consists
   --  of entirely blanks (including when S = "") then we return with F > L.

   procedure Scan_Sign
     (Str   : String;
      Ptr   : not null access Integer;
      Max   : Integer;
      Minus : out Boolean;
      Start : out Positive)
   with
     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
         (declare
            F : constant Positive :=
              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);
        begin
          Minus = (Str (F) = '-')
            and then Ptr.all = (if Str (F) in '+' | '-' then F + 1 else F)
            and then Start = F);
   --  The Str, Ptr, Max parameters are as for the scan routines (Str is the
   --  string to be scanned starting at Ptr.all, and Max is the index of the
   --  last character in the string). Scan_Sign first scans out any initial
   --  blanks, raising Constraint_Error if the field is all blank. It then
   --  checks for and skips an initial plus or minus, requiring a non-blank
   --  character to follow (Constraint_Error is raised if plus or minus appears
   --  at the end of the string or with a following blank). Minus is set True
   --  if a minus sign was skipped, and False otherwise. On exit Ptr.all points
   --  to the character after the sign, or to the first non-blank character
   --  if no sign is present. Start is set to the point to the first non-blank
   --  character (sign or digit after it).
   --
   --  Note: if Str is null, i.e. if Max is less than Ptr, then this is a
   --  special case of an all-blank string, and Ptr is unchanged, and hence
   --  is greater than Max as required in this case. Constraint_Error is also
   --  raised in this case.
   --
   --  This routine must not be called with Str'Last = Positive'Last. There is
   --  no check for this case, the caller must ensure this condition is met.

   procedure Scan_Plus_Sign
     (Str   : String;
      Ptr   : not null access Integer;
      Max   : Integer;
      Start : out Positive)
   with
     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
         (declare
            F : constant Positive :=
              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);
        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;
      Max  : Integer;
      Exp  : out Integer;
      Real : Boolean := False)
   with
     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 Max < Natural'Last
         and then 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)
          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)
        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
   --  exponent is scanned out, with the exponent value returned in Exp, and
   --  Ptr.all updated to point past the exponent. If the exponent field is
   --  incorrectly formed or not present, then Ptr.all is unchanged, and the
   --  returned exponent value is zero. Real indicates whether a minus sign
   --  is permitted (True = permitted). Very large exponents are handled by
   --  returning a suitable large value. If the base is zero, then any value
   --  is allowed, and otherwise the large value will either cause underflow
   --  or overflow during the scaling process which is fine.
   --
   --  This routine must not be called with Str'Last = Positive'Last. There is
   --  no check for this case, the caller must ensure this condition is met.

   procedure Scan_Trailing_Blanks (Str : String; P : Positive)
   with
     Pre => P >= Str'First
       and then 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.

   pragma Warnings
     (GNATprove, Off, """Ptr"" is not modified",
      Reason => "Ptr is actually modified when raising an exception");
   procedure Scan_Underscore
     (Str : String;
      P   : in out Natural;
      Ptr : not null access Integer;
      Max : Integer;
      Ext : Boolean)
   with
     Pre  => P in Str'Range
       and then Str (P) = '_'
       and then Max in Str'Range
       and then P < Max
       and then
         (if Ext then
            Str (P + 1) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
          else
            Str (P + 1) in '0' .. '9'),
     Post =>
       P = P'Old + 1
         and then Ptr.all'Old = Ptr.all;
   --  Called if an underscore is encountered while scanning digits. Str (P)
   --  contains the underscore. Ptr is the pointer to be returned to the
   --  ultimate caller of the scan routine, Max is the maximum subscript in
   --  Str, and Ext indicates if extended digits are allowed. In the case
   --  where the underscore is invalid, Constraint_Error is raised with Ptr
   --  set appropriately, otherwise control returns with P incremented past
   --  the underscore.
   --
   --  This routine must not be called with Str'Last = Positive'Last. There 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;