diff options
author | Claire Dross <dross@adacore.com> | 2022-07-12 09:14:40 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-02 09:34:06 +0200 |
commit | bf52ee6a4f86cbd60770fc22ad5abce0f437762a (patch) | |
tree | 16f5c5f9b1f5e1609fc7cb753773c3d6b5a3465c /gcc | |
parent | 7c339b3b5a63bac5e5223e33cce4c9833153edbb (diff) | |
download | gcc-bf52ee6a4f86cbd60770fc22ad5abce0f437762a.zip gcc-bf52ee6a4f86cbd60770fc22ad5abce0f437762a.tar.gz gcc-bf52ee6a4f86cbd60770fc22ad5abce0f437762a.tar.bz2 |
[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.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/s-widthu.adb | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index 390942c..df5f224 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); |