ada: Update proof of runtime units

Following changes in GNATprove, proofs need to be amended.

gcc/ada/

	* libgnat/s-aridou.adb (Lemma_Div_Pow2): Add assertion.
	* libgnat/s-arit32.adb (Lemma_Abs_Div_Commutation): Simplify.
	* libgnat/s-expmod.adb (Lemma_Exp_Mod): Add assertions.
	(Lemma_Euclidean_Mod): Add body to lemma.
	(Lemma_Mult_Mod): Add assertion.
	* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Modify assertion.
	* libgnat/s-vauspe.ads (Raw_Unsigned_Last_Ghost): Add
	postcondition.
	* libgnat/s-widthi.adb: Use more precise types.

6 files changed, 31 insertions, 45 deletions

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index dbf0f42cd49..041478538a7 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -1543,7 +1543,7 @@ is
          Div2 : constant Double_Uns := Double_Uns'(2);
          Left : constant Double_Uns := X / Div1 / Div2;
          R2   : constant Double_Uns := X / Div1 - Left * Div2;
-         pragma Assert (R2 < Div2);
+         pragma Assert (R2 <= Div2 - 1);
          R1   : constant Double_Uns := X - X / Div1 * Div1;
          pragma Assert (R1 < Div1);
       begin
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
index bd316c1bc20..219523b00f2 100644
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -195,12 +195,6 @@ is
        or else (X >= Big_0 and then Y <= Big_0),
      Post => X * Y <= Big_0;
 
-   procedure Lemma_Neg_Div (X, Y : Big_Integer)
-   with
-     Ghost,
-     Pre  => Y /= 0,
-     Post => X / Y = (-X) / (-Y);
-
    procedure Lemma_Neg_Rem (X, Y : Big_Integer)
    with
      Ghost,
@@ -223,6 +217,7 @@ is
    -----------------------------
 
    procedure Lemma_Abs_Commutation (X : Int32) is null;
+   procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is null;
    procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null;
    procedure Lemma_Div_Commutation (X, Y : Uns64) is null;
    procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null;
@@ -235,22 +230,6 @@ is
    procedure Lemma_Rem_Commutation (X, Y : Uns64) is null;
 
    -------------------------------
-   -- Lemma_Abs_Div_Commutation --
-   -------------------------------
-
-   procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is
-   begin
-      if Y < 0 then
-         if X < 0 then
-            pragma Assert (abs (X / Y) = abs (X / (-Y)));
-         else
-            Lemma_Neg_Div (X, Y);
-            pragma Assert (abs (X / Y) = abs ((-X) / (-Y)));
-         end if;
-      end if;
-   end Lemma_Abs_Div_Commutation;
-
-   -------------------------------
    -- Lemma_Abs_Rem_Commutation --
    -------------------------------
 
@@ -277,16 +256,6 @@ is
       pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32);
    end Lemma_Hi_Lo;
 
-   -------------------
-   -- Lemma_Neg_Div --
-   -------------------
-
-   procedure Lemma_Neg_Div (X, Y : Big_Integer) is
-   begin
-      pragma Assert ((-X) / (-Y) = -(X / (-Y)));
-      pragma Assert (X / (-Y) = -(X / Y));
-   end Lemma_Neg_Div;
-
    -----------------
    -- Raise_Error --
    -----------------
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb
index 0682589d352..aa6e9b4c361 100644
--- a/gcc/ada/libgnat/s-expmod.adb
+++ b/gcc/ada/libgnat/s-expmod.adb
@@ -109,9 +109,21 @@ is
 
       procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) with
         Pre  => F /= 0,
-        Post => (Q * F + R) mod F = R mod F;
+        Post => (Q * F + R) mod F = R mod F,
+        Subprogram_Variant => (Decreases => Q);
 
-      procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is null;
+      -------------------------
+      -- Lemma_Euclidean_Mod --
+      -------------------------
+
+      procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is
+      begin
+         if Q > 0 then
+            Lemma_Euclidean_Mod (Q - 1, F, R);
+         end if;
+      end Lemma_Euclidean_Mod;
+
+      --  Local variables
 
       Left  : constant Big_Natural := (X + Y) mod B;
       Right : constant Big_Natural := ((X mod B) + (Y mod B)) mod B;
@@ -164,6 +176,9 @@ is
             Lemma_Mod_Mod (A, B);
             Lemma_Exp_Mod (A, Exp - 1, B);
             Lemma_Mult_Mod (A, A ** (Exp - 1), B);
+            pragma Assert
+              ((A mod B) * (A mod B) ** (Exp - 1) = (A mod B) ** Exp);
+            pragma Assert (A * A ** (Exp - 1) = A ** Exp);
             pragma Assert (Left = Right);
          end;
       end if;
@@ -190,6 +205,7 @@ is
             pragma Assert (Left = Right);
          else
             pragma Assert (Y mod B = 0);
+            pragma Assert (Y / B * B = Y);
             pragma Assert ((X * Y) mod B = (X * Y) - (X * Y) / B * B);
             pragma Assert
               ((X * Y) mod B = (X * Y) - (X * (Y / B) * B) / B * B);
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index bc6ed1ca669..062ad33b1e9 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -483,12 +483,12 @@ package body System.Value_U is
       pragma Assert
         (By
            (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max),
-            (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
-             then Ptr.all = First_Exp
-             elsif Str (First_Exp + 1) in '-' | '+' then
-                Ptr.all = Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1
-             else Ptr.all =
-                Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1)));
+            Ptr.all =
+              (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
+               then First_Exp
+               elsif Str (First_Exp + 1) in '-' | '+' then
+                 Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1
+               else Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1)));
       pragma Assert
         (if not Overflow
          then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) =
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads
index 25a095b57a0..117769d20cb 100644
--- a/gcc/ada/libgnat/s-vauspe.ads
+++ b/gcc/ada/libgnat/s-vauspe.ads
@@ -492,7 +492,8 @@ is
      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 Str (From) in '0' .. '9',
+     Post => Raw_Unsigned_Last_Ghost'Result >= From;
    --  Ghost function that returns the position of the cursor once an unsigned
    --  number has been seen.
 
diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb
index bdd1bfb303e..7f04e22ae7f 100644
--- a/gcc/ada/libgnat/s-widthi.adb
+++ b/gcc/ada/libgnat/s-widthi.adb
@@ -166,9 +166,9 @@ begin
       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;
+         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);