[Ada] Fix proof of runtime unit System.Wid_*

Regain the proof of System.Wid_* after changes in provers and Why3.

gcc/ada/

	* libgnat/s-widthu.adb (Lemma_Euclidean): Lemma to prove the
	relation between the quotient/remainder of a division.

diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb
index 390942c8f808c71ee3330ca8c12dded6a4250dcc..df5f224426c867e5a289815b054835070928fda3 100644 (file)
--- a/gcc/ada/libgnat/s-widthu.adb
+++ b/gcc/ada/libgnat/s-widthu.adb
@@ -73,6 +73,14 @@ package body System.Width_U is
         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 --
       ----------------------
@@ -104,6 +112,12 @@ package body System.Width_U is
          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;
@@ -152,7 +166,7 @@ package body System.Width_U is
             R : constant Big_Integer := Big (T_Init) rem F with Ghost;
          begin
             pragma Assert (Q < Big_10);
-            pragma Assert (Big (T_Init) = Q * F + R);
+            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);