From: Claire Dross <dross@adacore.com>
Date: Tue, 12 Jul 2022 07:14:40 +0000 (+0200)
Subject: [Ada] Fix proof of runtime unit System.Wid_*
X-Git-Tag: basepoints/gcc-14~4841
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=bf52ee6a4f86cbd60770fc22ad5abce0f437762a;p=thirdparty%2Fgcc.git

[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 390942c8f808..df5f224426c8 100644
--- 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);