* [Ada] Fix proof of runtime unit System.Wid_*
@ 2022-09-02 7:53 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-02 7:53 UTC (permalink / raw)
To: gcc-patches; +Cc: Claire Dross
[-- Attachment #1: Type: text/plain, Size: 247 bytes --]
Regain the proof of System.Wid_* after changes in provers and Why3.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-widthu.adb (Lemma_Euclidean): Lemma to prove the
relation between the quotient/remainder of a division.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1450 bytes --]
diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb
--- 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);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-02 7:53 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-02 7:53 [Ada] Fix proof of runtime unit System.Wid_* Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).