[Ada] Proof of System.Val_Uns at gold level

gcc/ada/

	* libgnat/a-tiinau.ads: Use a procedure for the Scan parameter
	instead of a function with side-effects.
	* libgnat/a-tiinau.adb: Idem.
	* libgnat/a-wtinau.ads: Idem.
	* libgnat/a-wtinau.adb: Idem.
	* libgnat/a-ztinau.ads: Idem.
	* libgnat/a-ztinau.adb: Idem.
	* libgnat/s-valint.ads: Change the function with side-effects
	Scan_Integer into a procedure
	* libgnat/s-vallli.ads: Idem.
	* libgnat/s-valllli.ads: Idem.
	* libgnat/s-vallllu.ads: Add SPARK_Mode and pragma to ignore
	assertions in instance.
	* libgnat/s-valllu.ads: Idem.
	* libgnat/s-valuns.ads: Idem.
	* libgnat/s-valuei.ads: Use a procedure for the
	Scan_Raw_Unsigned parameter instead of a function with
	side-effects and change the function with side-effects
	Scan_Integer into a procedure.
	* libgnat/s-valuei.adb: Idem.
	* libgnat/s-valuti.ads: Introduce a ghost function that scans an
	exponent and complete the postcondition of Scan_Exponent to also
	describe the value of Ptr after the call. Fix the postcondition
	of Scan_Underscore. Simplify the definition of
	Scan_Natural_Ghost.
	* libgnat/s-valuti.adb: Idem.
	* libgnat/s-valboo.ads, libgnat/s-valboo.adb: Update calls to
	First_Non_Space_Ghost.
	* libgnat/s-valueu.ads: Add functional contracts.
	* libgnat/s-valueu.adb: Idem.

20 files changed, 1066 insertions, 115 deletions

diff --git a/gcc/ada/libgnat/a-tiinau.adb b/gcc/ada/libgnat/a-tiinau.adb
index f95d34a..100c5c4 100644
--- a/gcc/ada/libgnat/a-tiinau.adb
+++ b/gcc/ada/libgnat/a-tiinau.adb
@@ -54,7 +54,7 @@ package body Ada.Text_IO.Integer_Aux is
          Load_Integer (File, Buf, Stop);
       end if;
 
-      Item := Scan (Buf, Ptr'Access, Stop);
+      Scan (Buf, Ptr'Access, Stop, Item);
       Check_End_Of_Field (Buf, Stop, Ptr, Width);
    end Get;
 
@@ -71,7 +71,7 @@ package body Ada.Text_IO.Integer_Aux is
 
    begin
       String_Skip (From, Pos);
-      Item := Scan (From, Pos'Access, From'Last);
+      Scan (From, Pos'Access, From'Last, Item);
       Last := Pos - 1;
 
    exception
diff --git a/gcc/ada/libgnat/a-tiinau.ads b/gcc/ada/libgnat/a-tiinau.ads
index d995f24..75eb915 100644
--- a/gcc/ada/libgnat/a-tiinau.ads
+++ b/gcc/ada/libgnat/a-tiinau.ads
@@ -38,8 +38,11 @@
 private generic
    type Num is (<>);
 
-   with function Scan
-     (Str : String; Ptr : not null access Integer; Max : Integer) return Num;
+   with procedure Scan
+     (Str : String;
+      Ptr : not null access Integer;
+      Max : Integer;
+      Res : out Num);
    with procedure Set_Image
      (V : Num; S : in out String; P : in out Natural);
    with procedure Set_Image_Width
diff --git a/gcc/ada/libgnat/a-wtinau.adb b/gcc/ada/libgnat/a-wtinau.adb
index 3934d9b..0628cc6 100644
--- a/gcc/ada/libgnat/a-wtinau.adb
+++ b/gcc/ada/libgnat/a-wtinau.adb
@@ -54,7 +54,7 @@ package body Ada.Wide_Text_IO.Integer_Aux is
          Load_Integer (File, Buf, Stop);
       end if;
 
-      Item := Scan (Buf, Ptr'Access, Stop);
+      Scan (Buf, Ptr'Access, Stop, Item);
       Check_End_Of_Field (Buf, Stop, Ptr, Width);
    end Get;
 
@@ -71,7 +71,7 @@ package body Ada.Wide_Text_IO.Integer_Aux is
 
    begin
       String_Skip (From, Pos);
-      Item := Scan (From, Pos'Access, From'Last);
+      Scan (From, Pos'Access, From'Last, Item);
       Last := Pos - 1;
 
    exception
diff --git a/gcc/ada/libgnat/a-wtinau.ads b/gcc/ada/libgnat/a-wtinau.ads
index 97138b1..37ac2d1 100644
--- a/gcc/ada/libgnat/a-wtinau.ads
+++ b/gcc/ada/libgnat/a-wtinau.ads
@@ -38,8 +38,11 @@
 private generic
    type Num is (<>);
 
-   with function Scan
-     (Str : String; Ptr : not null access Integer; Max : Integer) return Num;
+   with procedure Scan
+     (Str : String;
+      Ptr : not null access Integer;
+      Max : Integer;
+      Res : out Num);
    with procedure Set_Image
      (V : Num; S : in out String; P : in out Natural);
    with procedure Set_Image_Width
diff --git a/gcc/ada/libgnat/a-ztinau.adb b/gcc/ada/libgnat/a-ztinau.adb
index 9f4c4c8..d7df8ef 100644
--- a/gcc/ada/libgnat/a-ztinau.adb
+++ b/gcc/ada/libgnat/a-ztinau.adb
@@ -54,7 +54,7 @@ package body Ada.Wide_Wide_Text_IO.Integer_Aux is
          Load_Integer (File, Buf, Stop);
       end if;
 
-      Item := Scan (Buf, Ptr'Access, Stop);
+      Scan (Buf, Ptr'Access, Stop, Item);
       Check_End_Of_Field (Buf, Stop, Ptr, Width);
    end Get;
 
@@ -71,7 +71,7 @@ package body Ada.Wide_Wide_Text_IO.Integer_Aux is
 
    begin
       String_Skip (From, Pos);
-      Item := Scan (From, Pos'Access, From'Last);
+      Scan (From, Pos'Access, From'Last, Item);
       Last := Pos - 1;
 
    exception
diff --git a/gcc/ada/libgnat/a-ztinau.ads b/gcc/ada/libgnat/a-ztinau.ads
index 79374f4..c1871af 100644
--- a/gcc/ada/libgnat/a-ztinau.ads
+++ b/gcc/ada/libgnat/a-ztinau.ads
@@ -38,8 +38,11 @@
 private generic
    type Num is (<>);
 
-   with function Scan
-     (Str : String; Ptr : not null access Integer; Max : Integer) return Num;
+   with procedure Scan
+     (Str : String;
+      Ptr : not null access Integer;
+      Max : Integer;
+      Res : out Num);
    with procedure Set_Image
      (V : Num; S : in out String; P : in out Natural);
    with procedure Set_Image_Width
diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb
index 2bc1b15..54b1265 100644
--- a/gcc/ada/libgnat/s-valboo.adb
+++ b/gcc/ada/libgnat/s-valboo.adb
@@ -55,7 +55,8 @@ is
    begin
       Normalize_String (S, F, L);
 
-      pragma Assert (F = System.Val_Util.First_Non_Space_Ghost (S));
+      pragma Assert (F = System.Val_Util.First_Non_Space_Ghost
+                     (S, Str'First, Str'Last));
 
       if S (F .. L) = "TRUE" then
          return True;
diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads
index 3cd8538..a9afc45 100644
--- a/gcc/ada/libgnat/s-valboo.ads
+++ b/gcc/ada/libgnat/s-valboo.ads
@@ -51,7 +51,8 @@ is
      (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last)
         and then
       (declare
-         F : constant Positive := System.Val_Util.First_Non_Space_Ghost (Str);
+         F : constant Positive := System.Val_Util.First_Non_Space_Ghost
+           (Str, Str'First, Str'Last);
        begin
          (F <= Str'Last - 3
           and then Str (F)     in 't' | 'T'
@@ -82,7 +83,8 @@ is
      Pre  => Is_Boolean_Image_Ghost (Str),
      Post =>
        Value_Boolean'Result =
-         (Str (System.Val_Util.First_Non_Space_Ghost (Str)) in 't' | 'T');
+         (Str (System.Val_Util.First_Non_Space_Ghost
+            (Str, Str'First, Str'Last)) in 't' | 'T');
    --  Computes Boolean'Value (Str)
 
 end System.Val_Bool;
diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index d85fa75..4fef265 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -43,10 +43,11 @@ package System.Val_Int is
 
    package Impl is new Value_I (Integer, Unsigned, Val_Uns.Scan_Raw_Unsigned);
 
-   function Scan_Integer
+   procedure Scan_Integer
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Integer
+      Max : Integer;
+      Res : out Integer)
      renames Impl.Scan_Integer;
 
    function Value_Integer (Str : String) return Integer
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index 79098b5..ce1d9ee 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -46,10 +46,11 @@ package System.Val_LLI is
               Long_Long_Unsigned,
               Val_LLU.Scan_Raw_Long_Long_Unsigned);
 
-   function Scan_Long_Long_Integer
+   procedure Scan_Long_Long_Integer
      (Str  : String;
       Ptr  : not null access Integer;
-      Max  : Integer) return Long_Long_Integer
+      Max  : Integer;
+      Res  : out Long_Long_Integer)
      renames Impl.Scan_Integer;
 
    function Value_Long_Long_Integer (Str : String) return Long_Long_Integer
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index 3890ef3..176000a 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -46,10 +46,11 @@ package System.Val_LLLI is
               Long_Long_Long_Unsigned,
               Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned);
 
-   function Scan_Long_Long_Long_Integer
+   procedure Scan_Long_Long_Long_Integer
      (Str  : String;
       Ptr  : not null access Integer;
-      Max  : Integer) return Long_Long_Long_Integer
+      Max  : Integer;
+      Res  : out  Long_Long_Long_Integer)
      renames Impl.Scan_Integer;
 
    function Value_Long_Long_Long_Integer
diff --git a/gcc/ada/libgnat/s-vallllu.ads b/gcc/ada/libgnat/s-vallllu.ads
index db74864..c6c9ece 100644
--- a/gcc/ada/libgnat/s-vallllu.ads
+++ b/gcc/ada/libgnat/s-vallllu.ads
@@ -32,26 +32,40 @@
 --  This package contains routines for scanning modular 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;
 
-package System.Val_LLLU is
+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);
 
-   function Scan_Raw_Long_Long_Long_Unsigned
+   procedure Scan_Raw_Long_Long_Long_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Long_Long_Long_Unsigned
+      Max : Integer;
+      Res : out Long_Long_Long_Unsigned)
      renames Impl.Scan_Raw_Unsigned;
 
-   function Scan_Long_Long_Long_Unsigned
+   procedure Scan_Long_Long_Long_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Long_Long_Long_Unsigned
+      Max : Integer;
+      Res : out Long_Long_Long_Unsigned)
      renames Impl.Scan_Unsigned;
 
    function Value_Long_Long_Long_Unsigned
diff --git a/gcc/ada/libgnat/s-valllu.ads b/gcc/ada/libgnat/s-valllu.ads
index 9c01152..0a5cb34 100644
--- a/gcc/ada/libgnat/s-valllu.ads
+++ b/gcc/ada/libgnat/s-valllu.ads
@@ -32,26 +32,40 @@
 --  This package contains routines for scanning modular 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;
 
-package System.Val_LLU is
+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);
 
-   function Scan_Raw_Long_Long_Unsigned
+   procedure Scan_Raw_Long_Long_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Long_Long_Unsigned
+      Max : Integer;
+      Res : out Long_Long_Unsigned)
      renames Impl.Scan_Raw_Unsigned;
 
-   function Scan_Long_Long_Unsigned
+   procedure Scan_Long_Long_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Long_Long_Unsigned
+      Max : Integer;
+      Res : out Long_Long_Unsigned)
      renames Impl.Scan_Unsigned;
 
    function Value_Long_Long_Unsigned
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index b89443f..83828d3 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -37,10 +37,11 @@ package body System.Value_I is
    -- Scan_Integer --
    ------------------
 
-   function Scan_Integer
+   procedure Scan_Integer
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Int
+      Max : Integer;
+      Res : out Int)
    is
       Uval : Uns;
       --  Unsigned result
@@ -59,13 +60,13 @@ package body System.Value_I is
          Bad_Value (Str);
       end if;
 
-      Uval := Scan_Raw_Unsigned (Str, Ptr, Max);
+      Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
 
       --  Deal with overflow cases, and also with largest negative number
 
       if Uval > Uns (Int'Last) then
          if Minus and then Uval = Uns (-(Int'First)) then
-            return Int'First;
+            Res := Int'First;
          else
             Bad_Value (Str);
          end if;
@@ -73,12 +74,12 @@ package body System.Value_I is
       --  Negative values
 
       elsif Minus then
-         return -(Int (Uval));
+         Res := -(Int (Uval));
 
       --  Positive values
 
       else
-         return Int (Uval);
+         Res := Int (Uval);
       end if;
    end Scan_Integer;
 
@@ -106,7 +107,7 @@ package body System.Value_I is
             V : Int;
             P : aliased Integer := Str'First;
          begin
-            V := Scan_Integer (Str, P'Access, Str'Last);
+            Scan_Integer (Str, P'Access, Str'Last, V);
             Scan_Trailing_Blanks (Str, P);
             return V;
          end;
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index 5d1140f..e0a34d9 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -38,19 +38,21 @@ generic
 
    type Uns is mod <>;
 
-   with function Scan_Raw_Unsigned
+   with procedure Scan_Raw_Unsigned
           (Str : String;
            Ptr : not null access Integer;
-           Max : Integer) return Uns;
+           Max : Integer;
+           Res : out Uns);
 
 package System.Value_I is
    pragma Preelaborate;
 
-   function Scan_Integer
+   procedure Scan_Integer
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Int;
-   --  This function scans the string starting at Str (Ptr.all) for a valid
+      Max : Integer;
+      Res : out Int);
+   --  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
    --  scanned extends no further than Str (Max). There are three cases for the
    --  return:
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index 819d132..991d4a5 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -29,18 +29,220 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with System.Val_Util; use System.Val_Util;
-
 package body System.Value_U is
 
+   --  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,
+                            Assert_And_Cut     => Ignore,
+                            Subprogram_Variant => Ignore);
+
+   --  Local lemmas
+
+   procedure Lemma_Digit_Is_Before_Last
+     (Str  : String;
+      P    : Integer;
+      From : Integer;
+      To   : Integer)
+   with Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+       and then P in From .. To
+       and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
+     Post => P /= Last_Hexa_Ghost (Str (From .. To)) + 1;
+   --  If the character at position P is a digit, P cannot be the position of
+   --  of the first non-digit in Str.
+
+   procedure Lemma_End_Of_Scan
+     (Str  : String;
+      From : Integer;
+      To   : Integer;
+      Base : Uns;
+      Acc  : Uns)
+   with Ghost,
+     Pre  => Str'Last /= Positive'Last and then From > To,
+     Post => Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+       (False, Acc);
+   --  Unfold the definition of Scan_Based_Number_Ghost on an empty string
+
+   procedure Lemma_Scan_Digit
+     (Str          : String;
+      P            : Integer;
+      Lst          : Integer;
+      Digit        : Uns;
+      Base         : Uns;
+      Old_Acc      : Uns;
+      Acc          : Uns;
+      Scan_Val     : Uns_Option;
+      Old_Overflow : Boolean;
+      Overflow     : Boolean)
+   with Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then Lst in Str'Range
+       and then P in Str'First .. Lst
+       and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+       and then Digit = Hexa_To_Unsigned_Ghost (Str (P))
+       and then Only_Hexa_Ghost (Str, P, Lst)
+       and then Base in 2 .. 16
+       and then (if Digit < Base and then Old_Acc <= Uns'Last / Base
+                 then Acc = Base * Old_Acc + Digit)
+       and then (if Digit >= Base
+                   or else Old_Acc > Uns'Last / Base
+                   or else (Old_Acc > (Uns'Last - Base + 1) / Base
+                            and then Acc < Uns'Last / Base)
+                 then Overflow
+                 else Overflow = Old_Overflow)
+       and then
+         (if not Old_Overflow then
+           Scan_Val = Scan_Based_Number_Ghost
+              (Str, P, Lst, Base, Old_Acc)),
+     Post =>
+        (if not Overflow then
+           Scan_Val = Scan_Based_Number_Ghost
+             (Str, P + 1, Lst, Base, Acc))
+       and then
+        (if Overflow then Old_Overflow or else Scan_Val.Overflow);
+   --  Unfold the definition of Scan_Based_Number_Ghost when the string starts
+   --  with a digit.
+
+   procedure Lemma_Scan_Underscore
+     (Str      : String;
+      P        : Integer;
+      From     : Integer;
+      To       : Integer;
+      Lst      : Integer;
+      Base     : Uns;
+      Acc      : Uns;
+      Scan_Val : Uns_Option;
+      Overflow : Boolean;
+      Ext      : Boolean)
+   with Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Lst <= To
+       and then P in From .. Lst + 1
+       and then P <= To
+       and then
+         (if Ext then
+            Is_Based_Format_Ghost (Str (From .. To))
+            and then Lst = Last_Hexa_Ghost (Str (From .. To))
+          else Is_Natural_Format_Ghost (Str (From .. To))
+            and then Lst = Last_Number_Ghost (Str (From .. To)))
+       and then Str (P) = '_'
+       and then
+         (if not Overflow then
+           Scan_Val = Scan_Based_Number_Ghost (Str, P, Lst, Base, Acc)),
+     Post => P + 1 <= Lst
+       and then
+         (if Ext then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+          else Str (P + 1) in '0' .. '9')
+       and then
+         (if not Overflow then
+           Scan_Val = Scan_Based_Number_Ghost (Str, P + 1, Lst, Base, Acc));
+   --  Unfold the definition of Scan_Based_Number_Ghost when the string starts
+   --  with an underscore.
+
+   -----------------------------
+   -- Local lemma null bodies --
+   -----------------------------
+
+   procedure Lemma_Digit_Is_Before_Last
+     (Str  : String;
+      P    : Integer;
+      From : Integer;
+      To   : Integer)
+   is null;
+
+   procedure Lemma_End_Of_Scan
+     (Str          : String;
+      From         : Integer;
+      To           : Integer;
+      Base         : Uns;
+      Acc          : Uns)
+   is null;
+
+   procedure Lemma_Scan_Underscore
+     (Str      : String;
+      P        : Integer;
+      From     : Integer;
+      To       : Integer;
+      Lst      : Integer;
+      Base     : Uns;
+      Acc      : Uns;
+      Scan_Val : Uns_Option;
+      Overflow : Boolean;
+      Ext      : Boolean)
+   is null;
+
+   ---------------------
+   -- Last_Hexa_Ghost --
+   ---------------------
+
+   function Last_Hexa_Ghost (Str : String) return Positive is
+   begin
+      for J in Str'Range loop
+         if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
+            return J - 1;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Str'First .. J =>
+              Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
+      end loop;
+
+      return Str'Last;
+   end Last_Hexa_Ghost;
+
+   ----------------------
+   -- Lemma_Scan_Digit --
+   ----------------------
+
+   procedure Lemma_Scan_Digit
+     (Str          : String;
+      P            : Integer;
+      Lst          : Integer;
+      Digit        : Uns;
+      Base         : Uns;
+      Old_Acc      : Uns;
+      Acc          : Uns;
+      Scan_Val     : Uns_Option;
+      Old_Overflow : Boolean;
+      Overflow     : Boolean)
+   is
+      pragma Unreferenced (Str, P, Lst, Scan_Val, Overflow, Old_Overflow);
+   begin
+      if Digit >= Base then
+         null;
+
+      elsif Old_Acc <= (Uns'Last - Base + 1) / Base then
+         pragma Assert (not Scan_Overflows_Ghost (Digit, Base, Old_Acc));
+
+      elsif Old_Acc > Uns'Last / Base then
+         null;
+
+      else
+         pragma Assert
+           ((Acc < Uns'Last / Base) =
+              Scan_Overflows_Ghost (Digit, Base, Old_Acc));
+      end if;
+   end Lemma_Scan_Digit;
+
    -----------------------
    -- Scan_Raw_Unsigned --
    -----------------------
 
-   function Scan_Raw_Unsigned
+   procedure Scan_Raw_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Uns
+      Max : Integer;
+      Res : out Uns)
    is
       P : Integer;
       --  Local copy of the pointer
@@ -63,6 +265,40 @@ package body System.Value_U is
       Digit : Uns;
       --  Digit value
 
+      Ptr_Old       : constant Integer := Ptr.all
+      with Ghost;
+      Last_Num_Init : constant Integer :=
+        Last_Number_Ghost (Str (Ptr.all .. Max))
+      with Ghost;
+      Init_Val      : constant Uns_Option :=
+        Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
+      with Ghost;
+      Starts_As_Based : constant Boolean :=
+        Last_Num_Init < Max - 1
+        and then Str (Last_Num_Init + 1) in '#' | ':'
+        and then Str (Last_Num_Init + 2) in
+        '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+      with Ghost;
+      Last_Num_Based  : constant Integer :=
+        (if Starts_As_Based
+         then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
+         else Last_Num_Init)
+      with Ghost;
+      Is_Based        : constant Boolean :=
+        Starts_As_Based
+        and then Last_Num_Based < Max
+        and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)
+      with Ghost;
+      Based_Val       : constant Uns_Option :=
+        (if Starts_As_Based and then not Init_Val.Overflow
+         then Scan_Based_Number_Ghost
+           (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+         else Init_Val)
+      with Ghost;
+      First_Exp       : constant Integer :=
+        (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1)
+      with Ghost;
+
    begin
       --  We do not tolerate strings with Str'Last = Positive'Last
 
@@ -85,9 +321,20 @@ package body System.Value_U is
          Umax10 : constant Uns := Uns'Last / 10;
          --  Numbers bigger than Umax10 overflow if multiplied by 10
 
+         Old_Uval     : Uns with Ghost;
+         Old_Overflow : Boolean with Ghost;
+
       begin
          --  Loop through decimal digits
          loop
+            pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Init + 1);
+            pragma Loop_Invariant
+              (if Overflow then Init_Val.Overflow);
+            pragma Loop_Invariant
+              (if not Overflow
+               then Init_Val = Scan_Based_Number_Ghost
+                 (Str, P, Last_Num_Init, Acc => Uval));
+
             exit when P > Max;
 
             Digit := Character'Pos (Str (P)) - Character'Pos ('0');
@@ -96,6 +343,9 @@ package body System.Value_U is
 
             if Digit > 9 then
                if Str (P) = '_' then
+                  Lemma_Scan_Underscore
+                    (Str, P, Ptr_Old, Max, Last_Num_Init, 10, Uval,
+                     Init_Val, Overflow, False);
                   Scan_Underscore (Str, P, Ptr, Max, False);
                else
                   exit;
@@ -104,6 +354,9 @@ package body System.Value_U is
             --  Accumulate result, checking for overflow
 
             else
+               Old_Uval := Uval;
+               Old_Overflow := Overflow;
+
                if Uval <= Umax then
                   Uval := 10 * Uval + Digit;
 
@@ -118,11 +371,22 @@ package body System.Value_U is
                   end if;
                end if;
 
+               Lemma_Scan_Digit
+                 (Str, P, Last_Num_Init, Digit, 10, Old_Uval, Uval, Init_Val,
+                  Old_Overflow, Overflow);
+
                P := P + 1;
             end if;
          end loop;
+         pragma Assert (P = Last_Num_Init + 1);
+         pragma Assert (Init_Val.Overflow = Overflow);
       end;
 
+      pragma Assert_And_Cut
+        (P = Last_Num_Init + 1
+         and then Overflow = Init_Val.Overflow
+         and then (if not Overflow then Init_Val.Value = Uval));
+
       Ptr.all := P;
 
       --  Deal with based case. We recognize either the standard '#' or the
@@ -153,10 +417,18 @@ package body System.Value_U is
             UmaxB : constant Uns := Uns'Last / Base;
             --  Numbers bigger than UmaxB overflow if multiplied by base
 
+            Old_Uval     : Uns with Ghost;
+            Old_Overflow : Boolean with Ghost;
+
          begin
+            pragma Assert
+              (if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
+               then Is_Based_Format_Ghost (Str (P .. Max)));
+
             --  Loop to scan out based integer value
 
             loop
+
                --  We require a digit at this stage
 
                if Str (P) in '0' .. '9' then
@@ -177,9 +449,32 @@ package body System.Value_U is
 
                else
                   Uval := Base;
+                  Base := 10;
+                  pragma Assert (Ptr.all = Last_Num_Init + 1);
+                  pragma Assert (if not Overflow then Uval = Init_Val.Value);
                   exit;
                end if;
 
+               Lemma_Digit_Is_Before_Last (Str, P, Last_Num_Init + 2, Max);
+
+               pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based);
+               pragma Loop_Invariant
+                 (Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+                  and then Digit = Hexa_To_Unsigned_Ghost (Str (P)));
+               pragma Loop_Invariant
+                 (if Overflow'Loop_Entry then Overflow);
+               pragma Loop_Invariant
+                 (if Overflow then
+                    Overflow'Loop_Entry or else Based_Val.Overflow);
+               pragma Loop_Invariant
+                 (if not Overflow
+                  then Based_Val = Scan_Based_Number_Ghost
+                    (Str, P, Last_Num_Based, Base, Uval));
+               pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1);
+
+               Old_Uval := Uval;
+               Old_Overflow := Overflow;
+
                --  If digit is too large, just signal overflow and continue.
                --  The idea here is to keep scanning as long as the input is
                --  syntactically valid, even if we have detected overflow
@@ -203,6 +498,10 @@ package body System.Value_U is
                   end if;
                end if;
 
+               Lemma_Scan_Digit
+                 (Str, P, Last_Num_Based, Digit, Base, Old_Uval, Uval,
+                  Based_Val, Old_Overflow, Overflow);
+
                --  If at end of string with no base char, not a based number
                --  but we signal Constraint_Error and set the pointer past
                --  the end of the field, since this is what the ACVC tests
@@ -219,23 +518,62 @@ package body System.Value_U is
 
                if Str (P) = Base_Char then
                   Ptr.all := P + 1;
+                  pragma Assert (Ptr.all = Last_Num_Based + 2);
+                  Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval);
+                  pragma Assert (if not Overflow then Uval = Based_Val.Value);
                   exit;
 
                --  Deal with underscore
 
                elsif Str (P) = '_' then
+                  Lemma_Scan_Underscore
+                    (Str, P, Last_Num_Init + 2, Max, Last_Num_Based, Base,
+                     Uval, Based_Val, Overflow, True);
                   Scan_Underscore (Str, P, Ptr, Max, True);
+                  pragma Assert
+                    (if not Overflow
+                     then Based_Val = Scan_Based_Number_Ghost
+                       (Str, P, Last_Num_Based, Base, Uval));
                end if;
-
             end loop;
          end;
+         pragma Assert
+           (if Starts_As_Based then P = Last_Num_Based + 1
+            else P = Last_Num_Init + 2);
+         pragma Assert
+           (Overflow =
+              (Init_Val.Overflow
+               or else Init_Val.Value not in 2 .. 16
+               or else (Starts_As_Based and then Based_Val.Overflow)));
       end if;
 
+      pragma Assert_And_Cut
+        (Overflow =
+           (Init_Val.Overflow
+            or else
+              (Last_Num_Init < Max - 1
+               and then Str (Last_Num_Init + 1) in '#' | ':'
+               and then Init_Val.Value not in 2 .. 16)
+            or else (Starts_As_Based and then Based_Val.Overflow))
+         and then
+           (if not Overflow then
+                (if Is_Based then Uval = Based_Val.Value
+                 else Uval = Init_Val.Value))
+         and then Ptr.all = First_Exp
+         and then Base in 2 .. 16
+         and then
+           (if not Overflow then
+                (if Is_Based then Base = Init_Val.Value else Base = 10)));
+
       --  Come here with scanned unsigned value in Uval. The only remaining
       --  required step is to deal with exponent if one is present.
 
       Scan_Exponent (Str, Ptr, Max, Expon);
 
+      pragma Assert
+        (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
+         then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max)));
+
       if Expon /= 0 and then Uval /= 0 then
 
          --  For non-zero value, scale by exponent value. No need to do this
@@ -246,8 +584,24 @@ package body System.Value_U is
             UmaxB : constant Uns := Uns'Last / Base;
             --  Numbers bigger than UmaxB overflow if multiplied by base
 
+            Res_Val : constant Uns_Option :=
+              Exponent_Unsigned_Ghost (Uval, Expon, Base)
+            with Ghost;
          begin
             for J in 1 .. Expon loop
+               pragma Loop_Invariant
+                 (if Overflow'Loop_Entry then Overflow);
+               pragma Loop_Invariant
+                 (if Overflow
+                  then Overflow'Loop_Entry or else Res_Val.Overflow);
+               pragma Loop_Invariant
+                 (if not Overflow
+                  then Res_Val = Exponent_Unsigned_Ghost
+                    (Uval, Expon - J + 1, Base));
+
+               pragma Assert
+                 ((Uval > UmaxB) = Scan_Overflows_Ghost (0, Base, Uval));
+
                if Uval > UmaxB then
                   Overflow := True;
                   exit;
@@ -255,15 +609,45 @@ package body System.Value_U is
 
                Uval := Uval * Base;
             end loop;
+            pragma Assert
+              (Overflow = (Init_Val.Overflow
+               or else
+                 (Last_Num_Init < Max - 1
+                  and then Str (Last_Num_Init + 1) in '#' | ':'
+                  and then Init_Val.Value not in 2 .. 16)
+               or else (Starts_As_Based and then Based_Val.Overflow)
+               or else Res_Val.Overflow));
+            pragma Assert
+              (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
+            pragma Assert
+              (Exponent_Unsigned_Ghost (Uval, 0, Base) = (False, Uval));
+            pragma Assert
+              (if not Overflow then Uval = Res_Val.Value);
+            pragma Assert
+              (if not Overflow then
+                  Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
          end;
       end if;
+      pragma Assert
+        (if Expon = 0 or else Uval = 0 then
+            Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
+      pragma Assert
+        (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
+      pragma Assert
+        (if not Overflow then
+            Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
 
-      --  Return result, dealing with sign and overflow
+      --  Return result, dealing with overflow
 
       if Overflow then
          Bad_Value (Str);
+         pragma Annotate
+           (GNATprove, Intentional,
+            "call to nonreturning subprogram might be executed",
+            "it is expected that Constraint_Error is raised in case of"
+            & " overflow");
       else
-         return Uval;
+         Res := Uval;
       end if;
    end Scan_Raw_Unsigned;
 
@@ -271,23 +655,30 @@ package body System.Value_U is
    -- Scan_Unsigned --
    -------------------
 
-   function Scan_Unsigned
+   procedure Scan_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Uns
+      Max : Integer;
+      Res : out Uns)
    is
       Start : Positive;
       --  Save location of first non-blank character
 
    begin
+      pragma Warnings
+        (Off,
+         """Start"" is set by ""Scan_Plus_Sign"" but not used after the call");
       Scan_Plus_Sign (Str, Ptr, Max, Start);
+      pragma Warnings
+        (On,
+         """Start"" is set by ""Scan_Plus_Sign"" but not used after the call");
 
       if Str (Ptr.all) not in '0' .. '9' then
          Ptr.all := Start;
          Bad_Value (Str);
       end if;
 
-      return Scan_Raw_Unsigned (Str, Ptr, Max);
+      Scan_Raw_Unsigned (Str, Ptr, Max, Res);
    end Scan_Unsigned;
 
    --------------------
@@ -313,9 +704,32 @@ package body System.Value_U is
          declare
             V : Uns;
             P : aliased Integer := Str'First;
+
+            Non_Blank : constant Positive := First_Non_Space_Ghost
+              (Str, Str'First, Str'Last)
+            with Ghost;
+            Fst_Num   : constant Positive :=
+              (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank)
+            with Ghost;
          begin
-            V := Scan_Unsigned (Str, P'Access, Str'Last);
+            pragma Assert
+              (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+
+            declare
+               P_Acc : constant not null access Integer := P'Access;
+            begin
+               Scan_Unsigned (Str, P_Acc, Str'Last, V);
+            end;
+
+            pragma Assert
+              (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+            pragma Assert
+              (V = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
+
             Scan_Trailing_Blanks (Str, P);
+
+            pragma Assert
+              (Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), V));
             return V;
          end;
       end if;
diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads
index 269eb24..b0e3b1e 100644
--- a/gcc/ada/libgnat/s-valueu.ads
+++ b/gcc/ada/libgnat/s-valueu.ads
@@ -32,6 +32,22 @@
 --  This package contains routines 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);
+pragma Warnings (Off, "postcondition does not mention function result");
+--  True postconditions are used to avoid inlining for GNATprove
+
+with System.Val_Util; use System.Val_Util;
+
 generic
 
    type Uns is mod <>;
@@ -39,10 +55,314 @@ generic
 package System.Value_U is
    pragma Preelaborate;
 
-   function Scan_Raw_Unsigned
+   type Uns_Option (Overflow : Boolean := False) is record
+      case Overflow is
+         when True =>
+            null;
+         when False =>
+            Value : Uns := 0;
+      end case;
+   end record with Ghost;
+
+   function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
+   is
+      (for all J in From .. To =>
+          Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+   with
+     Ghost,
+     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+   --  Ghost function that returns True if S has only hexadecimal characters
+   --  from index From to index To.
+
+   function Last_Hexa_Ghost (Str : String) return Positive
+   with
+     Ghost,
+     Pre  => Str /= ""
+       and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
+     Post => Last_Hexa_Ghost'Result in Str'Range
+       and then (if Last_Hexa_Ghost'Result < Str'Last then
+                   Str (Last_Hexa_Ghost'Result + 1) not in
+                     '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+       and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
+   --  Ghost function that returns the index of the last character in S that
+   --  is either an hexadecimal digit or an underscore, which necessarily
+   --  exists given the precondition on Str.
+
+   function Is_Based_Format_Ghost (Str : String) return Boolean
+   is
+     (Str /= ""
+        and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+        and then
+        (declare
+           L : constant Positive := Last_Hexa_Ghost (Str);
+         begin
+           Str (L) /= '_'
+             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
+   --  based number, consisting in a sequence of hexadecimal digits possibly
+   --  separated by single underscores. It may be followed by other characters.
+
+   function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
+     (case X is
+         when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
+         when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
+         when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
+         when others     => raise Program_Error)
+   with
+     Ghost,
+     Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+   --  Ghost function that computes the value corresponding to an hexadecimal
+   --  digit.
+
+   function Scan_Overflows_Ghost
+     (Digit : Uns;
+      Base  : Uns;
+      Acc   : Uns) return Boolean
+   is
+     (Digit >= Base
+      or else Acc > Uns'Last / Base
+      or else Uns'Last - Digit < Base * Acc)
+   with Ghost;
+   --  Ghost function which returns True if Digit + Base * Acc overflows or
+   --  Digit is greater than Base, as this is used by the algorithm for the
+   --  test of overflow.
+
+   function Scan_Based_Number_Ghost
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0) return Uns_Option
+   with
+     Ghost,
+     Subprogram_Variant => (Increases => From),
+     Pre  => Str'Last /= Positive'Last
+         and then
+           (From > To or else (From >= Str'First and then To <= Str'Last))
+         and then Only_Hexa_Ghost (Str, From, To);
+   --  Ghost function that recursively computes the based number in Str,
+   --  assuming Acc has been scanned already and scanning continues at index
+   --  From.
+
+   function Exponent_Unsigned_Ghost
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10) return Uns_Option
+   with
+     Ghost,
+     Subprogram_Variant => (Decreases => Exp);
+   --  Ghost function that recursively computes Value * Base ** Exp
+
+   function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
+     (Is_Natural_Format_Ghost (Str)
+      and then
+        (declare
+           Last_Num_Init   : constant Integer := Last_Number_Ghost (Str);
+           Starts_As_Based : constant Boolean :=
+             Last_Num_Init < Str'Last - 1
+             and then Str (Last_Num_Init + 1) in '#' | ':'
+             and then Str (Last_Num_Init + 2) in
+               '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+           Last_Num_Based  : constant Integer :=
+             (if Starts_As_Based
+              then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+              else Last_Num_Init);
+           Is_Based        : constant Boolean :=
+             Starts_As_Based
+             and then Last_Num_Based < Str'Last
+             and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+           First_Exp       : constant Integer :=
+             (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+         begin
+           (if Starts_As_Based then
+              Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+              and then Last_Num_Based < Str'Last)
+            and then Is_Opt_Exponent_Format_Ghost
+              (Str (First_Exp .. Str'Last))))
+   with
+     Ghost,
+     Pre  => Str'Last /= Positive'Last,
+     Post => True;
+   --  Ghost function that determines if Str has the correct format for an
+   --  unsigned number without a sign character.
+   --  It is a natural number in base 10, optionally followed by a based
+   --  number surrounded by delimiters # or :, optionally followed by an
+   --  exponent part.
+
+   function Raw_Unsigned_Overflows_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Boolean
+   is
+     (declare
+        Last_Num_Init   : constant Integer :=
+          Last_Number_Ghost (Str (From .. To));
+        Init_Val        : constant Uns_Option :=
+          Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+        Starts_As_Based : constant Boolean :=
+          Last_Num_Init < To - 1
+          and then Str (Last_Num_Init + 1) in '#' | ':'
+          and then Str (Last_Num_Init + 2) in
+          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+        Last_Num_Based  : constant Integer :=
+          (if Starts_As_Based
+           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+           else Last_Num_Init);
+        Is_Based        : constant Boolean :=
+          Starts_As_Based
+          and then Last_Num_Based < To
+          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+        Based_Val       : constant Uns_Option :=
+          (if Starts_As_Based and then not Init_Val.Overflow
+           then Scan_Based_Number_Ghost
+             (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+           else Init_Val);
+        First_Exp       : constant Integer :=
+          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+        Expon           : constant Natural :=
+          (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+           then Scan_Exponent_Ghost (Str (First_Exp .. To))
+           else 0);
+      begin
+        Init_Val.Overflow
+        or else
+          (Last_Num_Init < To - 1
+           and then Str (Last_Num_Init + 1) in '#' | ':'
+           and then Init_Val.Value not in 2 .. 16)
+        or else
+          (Starts_As_Based
+           and then Based_Val.Overflow)
+        or else
+          (Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+           and then
+             (declare
+                Base  : constant Uns :=
+                  (if Is_Based then Init_Val.Value else 10);
+                Value : constant Uns :=
+                  (if Is_Based then Based_Val.Value else Init_Val.Value);
+              begin
+                Exponent_Unsigned_Ghost
+                  (Value, Expon, Base).Overflow)))
+   with
+     Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9',
+     Post => True;
+   --  Ghost function that determines if the computation of the unsigned number
+   --  represented by Str will overflow. The computation overflows if either:
+   --    * The computation of the decimal part overflows,
+   --    * The decimal part is followed by a valid delimiter for a based
+   --      part, and the number corresponding to the base is not a valid base,
+   --    * The computation of the based part overflows, or
+   --    * There is an exponent and the computation of the exponentiation
+   --      overflows.
+
+   function Scan_Raw_Unsigned_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Uns
+   is
+     (declare
+        Last_Num_Init   : constant Integer :=
+          Last_Number_Ghost (Str (From .. To));
+        Init_Val        : constant Uns_Option :=
+          Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+        Starts_As_Based : constant Boolean :=
+          Last_Num_Init < To - 1
+          and then Str (Last_Num_Init + 1) in '#' | ':'
+          and then Str (Last_Num_Init + 2) in
+          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+        Last_Num_Based  : constant Integer :=
+          (if Starts_As_Based
+           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+           else Last_Num_Init);
+        Is_Based        : constant Boolean :=
+          Starts_As_Based
+          and then Last_Num_Based < To
+          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+        Based_Val       : constant Uns_Option :=
+          (if Starts_As_Based and then not Init_Val.Overflow
+           then Scan_Based_Number_Ghost
+             (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+           else Init_Val);
+        First_Exp       : constant Integer :=
+          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+        Expon           : constant Natural :=
+          (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+           then Scan_Exponent_Ghost (Str (First_Exp .. To))
+           else 0);
+        Base            : constant Uns :=
+          (if Is_Based then Init_Val.Value else 10);
+        Value           : constant Uns :=
+          (if Is_Based then Based_Val.Value else Init_Val.Value);
+      begin
+        Exponent_Unsigned_Ghost (Value, Expon, Base).Value)
+   with
+     Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9'
+       and then not Raw_Unsigned_Overflows_Ghost (Str, From, To),
+     Post => True;
+   --  Ghost function that scans an unsigned number without a sign character
+
+   function Raw_Unsigned_Last_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Positive
+   is
+     (declare
+        Last_Num_Init   : constant Integer :=
+          Last_Number_Ghost (Str (From .. To));
+        Starts_As_Based : constant Boolean :=
+          Last_Num_Init < To - 1
+          and then Str (Last_Num_Init + 1) in '#' | ':'
+          and then Str (Last_Num_Init + 2) in
+          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+        Last_Num_Based  : constant Integer :=
+          (if Starts_As_Based
+           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+           else Last_Num_Init);
+        Is_Based        : constant Boolean :=
+          Starts_As_Based
+          and then Last_Num_Based < To
+          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+        First_Exp       : constant Integer :=
+          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+      begin
+        (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+         then First_Exp
+         elsif Str (First_Exp + 1) in '-' | '+' then
+           Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
+         else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
+   with
+     Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9',
+     Post => Raw_Unsigned_Last_Ghost'Result in From .. To + 1;
+   --  Ghost function that returns the position of the cursor once an unsigned
+   --  number has been seen.
+
+   procedure Scan_Raw_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Uns;
+      Max : Integer;
+      Res : out Uns)
+   with Pre => Str'Last /= Positive'Last
+     and then Ptr.all in Str'Range
+     and then Max in Ptr.all .. Str'Last
+     and then Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)),
+     Post => not Raw_Unsigned_Overflows_Ghost (Str, Ptr.all'Old, Max)
+     and Res = Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max)
+     and Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max);
+
    --  This function scans the string starting at Str (Ptr.all) for a valid
    --  integer according to the syntax described in (RM 3.5(43)). The substring
    --  scanned extends no further than Str (Max).  Note: this does not scan
@@ -106,26 +426,158 @@ package System.Value_U is
    --  Note: if Str is empty, 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.
+   --  ??? This is not the case. We will read Str (Ptr.all) without checking
+   --  and increase Ptr.all by one.
    --
    --  Note: this routine should not be called with Str'Last = Positive'Last.
    --  If this occurs Program_Error is raised with a message noting that this
    --  case is not supported. Most such cases are eliminated by the caller.
 
-   function Scan_Unsigned
+   procedure Scan_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Uns;
+      Max : Integer;
+      Res : out Uns)
+   with Pre => Str'Last /= Positive'Last
+     and then Ptr.all in Str'Range
+     and then Max in Ptr.all .. Str'Last
+     and then not Only_Space_Ghost (Str, Ptr.all, Max)
+     and then
+       (declare
+          Non_Blank : constant Positive :=
+            First_Non_Space_Ghost (Str, Ptr.all, Max);
+          Fst_Num   : constant Positive :=
+            (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+        begin
+          Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))),
+     Post =>
+       (declare
+          Non_Blank : constant Positive :=
+            First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
+          Fst_Num   : constant Positive :=
+            (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+        begin
+          not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
+          and then Res = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)
+          and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+
    --  Same as Scan_Raw_Unsigned, except scans optional leading
    --  blanks, and an optional leading plus sign.
    --
    --  Note: if a minus sign is present, Constraint_Error will be raised.
    --  Note: trailing blanks are not scanned.
 
+   function Slide_To_1 (Str : String) return String
+   with Ghost,
+       Post =>
+         Only_Space_Ghost (Str, Str'First, Str'Last) =
+         (for all J in Str'First .. Str'Last =>
+            Slide_To_1'Result (J - Str'First + 1) = ' ');
+   --  Slides Str so that it starts at 1
+
+   function Slide_If_Necessary (Str : String) return String is
+     (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
+   with Ghost,
+       Post =>
+         Only_Space_Ghost (Str, Str'First, Str'Last) =
+         Only_Space_Ghost (Slide_If_Necessary'Result,
+                           Slide_If_Necessary'Result'First,
+                           Slide_If_Necessary'Result'Last);
+   --  If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+   function Is_Unsigned_Ghost (Str : String) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+      begin
+        Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+          and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
+          and then Only_Space_Ghost
+             (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
+   with Ghost,
+       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+       and then Str'Last /= Positive'Last,
+       Post => True;
+   --  Ghost function that determines if Str has the correct format for an
+   --  unsigned number, consisting in some blank characters, an optional
+   --  + sign, a raw unsigned number which does not overflow and then some
+   --  more blank characters.
+
+   function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+      begin
+        Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
+   with Ghost,
+       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+       and then Str'Last /= Positive'Last
+       and then Is_Unsigned_Ghost (Str),
+       Post => True;
+   --  Ghost function that returns True if Val is the value corresponding to
+   --  the unsigned number represented by Str.
+
    function Value_Unsigned
-     (Str : String) return Uns;
+     (Str : String) return Uns
+   with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+     and then Str'Length /= Positive'Last
+     and then Is_Unsigned_Ghost (Slide_If_Necessary (Str)),
+     Post =>
+         Is_Value_Unsigned_Ghost
+           (Slide_If_Necessary (Str), Value_Unsigned'Result),
+     Subprogram_Variant => (Decreases => Str'First);
    --  Used in computing X'Value (Str) where X is a modular integer type whose
    --  modulus does not exceed the range of System.Unsigned_Types.Unsigned. Str
    --  is the string argument of the attribute. Constraint_Error is raised if
    --  the string is malformed, or if the value is out of range.
 
+private
+
+   -----------------------------
+   -- Exponent_Unsigned_Ghost --
+   -----------------------------
+
+   function Exponent_Unsigned_Ghost
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10) return Uns_Option
+   is
+      (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
+       elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
+       else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
+
+   -----------------------------
+   -- Scan_Based_Number_Ghost --
+   -----------------------------
+
+   function Scan_Based_Number_Ghost
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0) return Uns_Option
+   is
+      (if From > To then (Overflow => False, Value => Acc)
+       elsif Str (From) = '_'
+       then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
+       elsif Scan_Overflows_Ghost
+         (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+       then (Overflow => True)
+       else Scan_Based_Number_Ghost
+         (Str, From + 1, To, Base,
+          Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
+
+   ----------------
+   -- Slide_To_1 --
+   ----------------
+
+   function Slide_To_1 (Str : String) return String is
+      (declare
+         Res : constant String (1 .. Str'Length) := Str;
+       begin
+         Res);
+
 end System.Value_U;
diff --git a/gcc/ada/libgnat/s-valuns.ads b/gcc/ada/libgnat/s-valuns.ads
index 2a65753..23f73ed 100644
--- a/gcc/ada/libgnat/s-valuns.ads
+++ b/gcc/ada/libgnat/s-valuns.ads
@@ -32,26 +32,40 @@
 --  This package contains routines 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;
 
-package System.Val_Uns is
+package System.Val_Uns with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Unsigned is Unsigned_Types.Unsigned;
 
    package Impl is new Value_U (Unsigned);
 
-   function Scan_Raw_Unsigned
+   procedure Scan_Raw_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Unsigned
+      Max : Integer;
+      Res : out Unsigned)
      renames Impl.Scan_Raw_Unsigned;
 
-   function Scan_Unsigned
+   procedure Scan_Unsigned
      (Str : String;
       Ptr : not null access Integer;
-      Max : Integer) return Unsigned
+      Max : Integer;
+      Res : out Unsigned)
      renames Impl.Scan_Unsigned;
 
    function Value_Unsigned
diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb
index 1a27dbe..4da585a 100644
--- a/gcc/ada/libgnat/s-valuti.adb
+++ b/gcc/ada/libgnat/s-valuti.adb
@@ -66,14 +66,17 @@ is
    -- First_Non_Space_Ghost --
    ---------------------------
 
-   function First_Non_Space_Ghost (S : String) return Positive is
+   function First_Non_Space_Ghost
+     (S        : String;
+      From, To : Integer) return Positive
+   is
    begin
-      for J in S'Range loop
+      for J in From .. To loop
          if S (J) /= ' ' then
             return J;
          end if;
 
-         pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' ');
+         pragma Loop_Invariant (for all K in From .. J => S (K) = ' ');
       end loop;
 
       raise Program_Error;
@@ -172,6 +175,9 @@ is
          Exp := 0;
          return;
       end if;
+      pragma Annotate
+        (CodePeer, False_Positive, "test always false",
+         "the slice might be empty or not start with an 'e'");
 
       --  We have an E/e, see if sign follows
 
@@ -222,7 +228,6 @@ is
          pragma Assert (Is_Natural_Format_Ghost (Rest));
 
          loop
-            pragma Assert (Str (P) = Rest (P));
             pragma Assert (Str (P) in '0' .. '9');
 
             if X < (Integer'Last / 10) then
@@ -230,17 +235,11 @@ is
             end if;
 
             pragma Loop_Invariant (X >= 0);
-            pragma Loop_Invariant (P in P'Loop_Entry .. Last);
+            pragma Loop_Invariant (P in Rest'First .. Last);
             pragma Loop_Invariant (Str (P) in '0' .. '9');
             pragma Loop_Invariant
-              (Scan_Natural_Ghost (Rest, P'Loop_Entry, 0)
-               = (if P = Max
-                    or else Rest (P + 1) not in '0' .. '9' | '_'
-                    or else X >= Integer'Last / 10
-                  then
-                    X
-                  else
-                    Scan_Natural_Ghost (Rest, P + 1, X)));
+              (Scan_Natural_Ghost (Rest, Rest'First, 0)
+               = Scan_Natural_Ghost (Rest, P + 1, X));
 
             P := P + 1;
 
@@ -252,6 +251,8 @@ is
                exit when Str (P) not in '0' .. '9';
             end if;
          end loop;
+
+         pragma Assert (P = Last + 1);
       end;
 
       if M then
@@ -298,7 +299,7 @@ is
 
       Start := P;
 
-      pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+      pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
 
       --  Skip past an initial plus sign
 
@@ -354,7 +355,7 @@ is
 
       Start := P;
 
-      pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
+      pragma Assert (Start = 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 e974251..5c0f2a5 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -41,6 +41,8 @@ pragma Assertion_Policy (Pre            => Ignore,
                          Post           => Ignore,
                          Contract_Cases => Ignore,
                          Ghost          => Ignore);
+pragma Warnings (Off, "postcondition does not mention function result");
+--  True postconditions are used to avoid inlining for GNATprove
 
 with System.Case_Util;
 
@@ -59,18 +61,23 @@ is
       (for all J in From .. To => S (J) = ' ')
    with
      Ghost,
-     Pre => From > To or else (From >= S'First and then To <= S'Last);
+     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) return Positive
+   function First_Non_Space_Ghost
+     (S        : String;
+      From, To : Integer) return Positive
    with
      Ghost,
-     Pre  => not Only_Space_Ghost (S, S'First, S'Last),
-     Post => First_Non_Space_Ghost'Result in S'Range
+     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, S'First, First_Non_Space_Ghost'Result - 1);
+         (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.
 
@@ -117,14 +124,14 @@ is
        and then
          (declare
             F : constant Positive :=
-              First_Non_Space_Ghost (Str (Ptr.all .. Max));
+              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));
+            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)
@@ -162,14 +169,14 @@ is
        and then
          (declare
             F : constant Positive :=
-              First_Non_Space_Ghost (Str (Ptr.all .. Max));
+              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));
+            First_Non_Space_Ghost (Str, Ptr.all'Old, Max);
         begin
           Ptr.all = (if Str (F) = '+' then F + 1 else F)
             and then Start = F);
@@ -195,7 +202,7 @@ is
        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 S.
+   --  precondition on Str.
 
    function Is_Natural_Format_Ghost (Str : String) return Boolean is
      (Str /= ""
@@ -215,7 +222,7 @@ is
 
    function Starts_As_Exponent_Format_Ghost
      (Str  : String;
-      Real : Boolean) return Boolean
+      Real : Boolean := False) return Boolean
    is
      (Str'Length > 1
       and then Str (Str'First) in 'E' | 'e'
@@ -242,7 +249,7 @@ is
 
    function Is_Opt_Exponent_Format_Ghost
      (Str  : String;
-      Real : Boolean) return Boolean
+      Real : Boolean := False) return Boolean
    is
      (not Starts_As_Exponent_Format_Ghost (Str, Real)
       or else
@@ -265,13 +272,35 @@ is
    with
      Ghost,
      Subprogram_Variant => (Increases => P),
-     Pre => Is_Natural_Format_Ghost (Str)
-       and then P in Str'First .. Last_Number_Ghost (Str)
-       and then Acc < Integer'Last / 10;
+     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;
@@ -286,17 +315,11 @@ is
          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
-          (declare
-             Plus_Sign  : constant Boolean := Str (Ptr.all'Old + 1) = '+';
-             Minus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '-';
-             Sign       : constant Boolean := Plus_Sign or Minus_Sign;
-             Start      : constant Natural :=
-               (if Sign then Ptr.all'Old + 2 else Ptr.all'Old + 1);
-             Value      : constant Natural :=
-               Scan_Natural_Ghost (Str (Start .. Max), Start, 0);
-           begin
-             Exp = (if Minus_Sign then -Value else Value))
+        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
@@ -340,7 +363,7 @@ is
             Str (P + 1) in '0' .. '9'),
      Post =>
        P = P'Old + 1
-         and then Ptr.all = Ptr.all;
+         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
@@ -365,19 +388,20 @@ private
       Acc : Natural)
       return Natural
    is
-     (if Str (P) = '_' then
+     (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 + (Character'Pos (Str (P)) - Character'Pos ('0'));
+             Acc * 10 +
+               (Integer'(Character'Pos (Str (P))) -
+                  Integer'(Character'Pos ('0')));
          begin
-           (if P = Str'Last
-              or else Str (P + 1) not in '0' .. '9' | '_'
-              or else Shift_Acc >= Integer'Last / 10
-            then
-              Shift_Acc
-            else
-              Scan_Natural_Ghost (Str, P + 1, Shift_Acc))));
+           Scan_Natural_Ghost (Str, P + 1, Shift_Acc)));
 
 end System.Val_Util;