1 files changed, 0 insertions, 131 deletions
diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb
index 9595790..c66d662 100644
--- a/gcc/ada/libgnat/s-widthi.adb
+++ b/gcc/ada/libgnat/s-widthi.adb
@@ -29,109 +29,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-
 function System.Width_I (Lo, Hi : Int) return Natural 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);
-
-   -----------------------
-   -- Local Subprograms --
-   -----------------------
-
-   package Signed_Conversion is new Signed_Conversions (Int => Int);
-
-   function Big (Arg : Int) return Big_Integer renames
-     Signed_Conversion.To_Big_Integer;
-
-   --  Maximum value of exponent for 10 that fits in Uns'Base
-   function Max_Log10 return Natural is
-     (case Int'Base'Size is
-        when 8   => 2,
-        when 16  => 4,
-        when 32  => 9,
-        when 64  => 19,
-        when 128 => 38,
-        when others => raise Program_Error)
-   with Ghost;
-
-   ------------------
-   -- Local Lemmas --
-   ------------------
-
-   procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
-   with
-     Ghost,
-     Pre  => A <= B,
-     Post => A * C <= B * C;
-
-   procedure Lemma_Div_Commutation (X, Y : Int)
-   with
-     Ghost,
-     Pre  => X >= 0 and Y > 0,
-     Post => Big (X) / Big (Y) = Big (X / Y);
-
-   procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive)
-   with
-     Ghost,
-     Post => X / Y / Z = X / (Y * Z);
-
-   ----------------------
-   -- Lemma_Lower_Mult --
-   ----------------------
-
-   procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
-
-   ---------------------------
-   -- Lemma_Div_Commutation --
-   ---------------------------
-
-   procedure Lemma_Div_Commutation (X, Y : Int) is null;
-
-   ---------------------
-   -- Lemma_Div_Twice --
-   ---------------------
-
-   procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
-      XY  : constant Big_Natural := X / Y;
-      YZ  : constant Big_Natural := Y * Z;
-      XYZ : constant Big_Natural := X / Y / Z;
-      R   : constant Big_Natural := (XY rem Z) * Y + (X rem Y);
-   begin
-      pragma Assert (X = XY * Y + (X rem Y));
-      pragma Assert (XY = XY / Z * Z + (XY rem Z));
-      pragma Assert (X = XYZ * YZ + R);
-      pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y);
-      pragma Assert (R <= YZ - 1);
-      pragma Assert (X / YZ = (XYZ * YZ + R) / YZ);
-      pragma Assert (X / YZ = XYZ + R / YZ);
-   end Lemma_Div_Twice;
-
-   --  Local variables
-
    W : Natural;
    T : Int;
-
-   --  Local ghost variables
-
-   Max_W  : constant Natural := Max_Log10 with Ghost;
-   Big_10 : constant Big_Integer := Big (10) with Ghost;
-
-   Pow    : Big_Integer := 1 with Ghost;
-   T_Init : constant Int :=
-     Int'Max (abs Int'Max (Lo, Int'First + 1),
-              abs Int'Max (Hi, Int'First + 1))
-     with Ghost;
-
---  Start of processing for System.Width_I
-
 begin
    if Lo > Hi then
       return 0;
@@ -151,41 +51,10 @@ begin
       --  Increase value if more digits required
 
       while T >= 10 loop
-         Lemma_Div_Commutation (T, 10);
-         Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10);
-
          T := T / 10;
          W := W + 1;
-         Pow := Pow * 10;
-
-         pragma Loop_Invariant (T >= 0);
-         pragma Loop_Invariant (W in 3 .. Max_W + 3);
-         pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
-         pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
-         pragma Loop_Variant (Decreases => T);
       end loop;
 
-      declare
-         F : constant Big_Positive := Big_10 ** (W - 2) with Ghost;
-         Q : constant Big_Natural := Big (T_Init) / F with Ghost;
-         R : constant Big_Natural := Big (T_Init) rem F with Ghost;
-      begin
-         pragma Assert (Q < Big_10);
-         pragma Assert (Big (T_Init) = Q * F + R);
-         Lemma_Lower_Mult (Q, Big (9), F);
-         pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
-         pragma Assert (Big (T_Init) < Big_10 * F);
-         pragma Assert (Big_10 * F = Big_10 ** (W - 1));
-      end;
-
-      --  This is an expression of the functional postcondition for Width_I,
-      --  which cannot be expressed readily as a postcondition as this would
-      --  require making the instantiation Signed_Conversion and function Big
-      --  available from the spec.
-
-      pragma Assert (Big (Int'Max (Lo, Int'First + 1)) < Big_10 ** (W - 1));
-      pragma Assert (Big (Int'Max (Hi, Int'First + 1)) < Big_10 ** (W - 1));
-
       return W;
    end if;