1 files changed, 0 insertions, 120 deletions
diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb
index df27e50..fe51d61 100644
--- a/gcc/ada/libgnat/s-widthu.adb
+++ b/gcc/ada/libgnat/s-widthu.adb
@@ -31,110 +31,12 @@
 
 package body System.Width_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);
-
    function Width (Lo, Hi : Uns) 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 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 : Uns)
-      with
-        Ghost,
-        Pre  => 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);
-
-      procedure Lemma_Euclidian (V, Q, F, R : Big_Integer)
-      with
-        Ghost,
-        Pre  => F > 0 and then Q = V / F and then R = V rem F,
-        Post => V = Q * F + R;
-      --  Ghost lemma to prove the relation between the quotient/remainder of
-      --  division by F and the value V.
-
-      ----------------------
-      -- Lemma_Lower_Mult --
-      ----------------------
-
-      procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
-
-      ---------------------------
-      -- Lemma_Div_Commutation --
-      ---------------------------
-
-      procedure Lemma_Div_Commutation (X, Y : Uns) 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;
-
-      ---------------------
-      -- Lemma_Euclidian --
-      ---------------------
-
-      procedure Lemma_Euclidian (V, Q, F, R : Big_Integer) is null;
-
-      --  Local variables
-
       W : Natural;
       T : Uns;
-
-      --  Local ghost variables
-
-      Max_W  : constant Natural := Max_Log10 with Ghost;
-      Pow    : Big_Integer := 1 with Ghost;
-      T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost;
-
-   --  Start of processing for System.Width_U
-
    begin
       if Lo > Hi then
          return 0;
-
       else
          --  Minimum value is 2, one for space, one for digit
 
@@ -147,32 +49,10 @@ package body System.Width_U is
          --  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 (W in 3 .. Max_W + 2);
-            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_Integer := Big_10 ** (W - 2) with Ghost;
-            Q : constant Big_Integer := Big (T_Init) / F with Ghost;
-            R : constant Big_Integer := Big (T_Init) rem F with Ghost;
-         begin
-            pragma Assert (Q < Big_10);
-            Lemma_Euclidian (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;
-
          return W;
       end if;
    end Width;