From bf52ee6a4f86cbd60770fc22ad5abce0f437762a Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Tue, 12 Jul 2022 09:14:40 +0200 Subject: [PATCH] [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. --- gcc/ada/libgnat/s-widthu.adb | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) 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); -- 2.47.2