1 files changed, 0 insertions, 70 deletions

diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index 2c4fe09..53790a0 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -33,16 +33,6 @@ with System.Val_Util; use System.Val_Util;
 
 package body System.Value_I is
 
-   --  Ghost code, loop invariants and assertions in this unit are meant for
-   --  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);
-
    ------------------
    -- Scan_Integer --
    ------------------
@@ -53,25 +43,6 @@ package body System.Value_I is
       Max : Integer;
       Res : out Int)
    is
-      procedure Prove_Is_Int_Of_Uns
-        (Minus : Boolean;
-         Uval  : Uns;
-         Val   : Int)
-      with Ghost,
-        Pre => Spec.Uns_Is_Valid_Int (Minus, Uval)
-          and then
-            (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
-             elsif Minus then Val = -(Int (Uval))
-             else Val = Int (Uval)),
-        Post => Spec.Is_Int_Of_Uns (Minus, Uval, Val);
-      --  Unfold the definition of Is_Int_Of_Uns
-
-      procedure Prove_Is_Int_Of_Uns
-        (Minus : Boolean;
-         Uval  : Uns;
-         Val   : Int)
-      is null;
-
       Uval : Uns;
       --  Unsigned result
 
@@ -81,15 +52,6 @@ package body System.Value_I is
       Unused_Start : Positive;
       --  Saves location of first non-blank (not used in this case)
 
-      Non_Blank : constant Positive :=
-        First_Non_Space_Ghost (Str, Ptr.all, Max)
-      with Ghost;
-
-      Fst_Num   : constant Positive :=
-        (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
-         else Non_Blank)
-      with Ghost;
-
    begin
       Scan_Sign (Str, Ptr, Max, Minus, Unused_Start);
 
@@ -99,8 +61,6 @@ package body System.Value_I is
       end if;
 
       Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
-      pragma Assert
-        (Uval = U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
 
       --  Deal with overflow cases, and also with largest negative number
 
@@ -121,11 +81,6 @@ package body System.Value_I is
       else
          Res := Int (Uval);
       end if;
-
-      Prove_Is_Int_Of_Uns
-        (Minus => Str (Non_Blank) = '-',
-         Uval  => Uval,
-         Val   => Res);
    end Scan_Integer;
 
    -------------------
@@ -141,15 +96,7 @@ package body System.Value_I is
       if Str'Last = Positive'Last then
          declare
             subtype NT is String (1 .. Str'Length);
-            procedure Prove_Is_Integer_Ghost with
-              Ghost,
-              Pre  => Str'Length < Natural'Last
-              and then not Only_Space_Ghost (Str, Str'First, Str'Last)
-              and then Spec.Is_Integer_Ghost (Spec.Slide_To_1 (Str)),
-              Post => Spec.Is_Integer_Ghost (NT (Str));
-            procedure Prove_Is_Integer_Ghost is null;
          begin
-            Prove_Is_Integer_Ghost;
             return Value_Integer (NT (Str));
          end;
 
@@ -159,31 +106,14 @@ package body System.Value_I is
          declare
             V : Int;
             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) in '+' | '-' then Non_Blank + 1
-               else Non_Blank)
-            with Ghost;
          begin
-
             declare
                P_Acc : constant not null access Integer := P'Access;
             begin
                Scan_Integer (Str, P_Acc, Str'Last, V);
             end;
 
-            pragma Assert
-              (P = U_Spec.Raw_Unsigned_Last_Ghost
-                 (Str, Fst_Num, Str'Last));
-
             Scan_Trailing_Blanks (Str, P);
-
-            pragma Assert
-              (Spec.Is_Value_Integer_Ghost (Spec.Slide_If_Necessary (Str), V));
             return V;
          end;
       end if;