public inbox for gcc-cvs@sourceware.org help / color / mirror / Atom feed
From: Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-305] [Ada] Adapt proof of System.Arith_Double after update of Z3 Date: Wed, 11 May 2022 08:55:54 +0000 (GMT) [thread overview] Message-ID: <20220511085554.9E90A3835413@sourceware.org> (raw) https://gcc.gnu.org/g:4c533da21d6298cdf9eb11df7353b8c8684c7756 commit r13-305-g4c533da21d6298cdf9eb11df7353b8c8684c7756 Author: Yannick Moy <moy@adacore.com> Date: Wed Feb 2 12:52:36 2022 +0100 [Ada] Adapt proof of System.Arith_Double after update of Z3 Update to version 4.8.14 of prover Z3 requires minor adjustments of the ghost code to add necessary intermediate assertions that drive the automatic proof. gcc/ada/ * libgnat/s-aridou.adb (Double_Divide, Scaled_Divide): Add intermediate assertions. Diff: --- gcc/ada/libgnat/s-aridou.adb | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 0fefb6bd945..ffb6f4ca269 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -924,6 +924,8 @@ is else Q := 0; + pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Yhi)); + pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Zhi)); pragma Assert (Big (Double_Uns'(Yhi * Zhi)) >= 1); if Yhi > 1 or else Zhi > 1 then pragma Assert (Big (Double_Uns'(Yhi * Zhi)) > 1); @@ -938,10 +940,12 @@ is return; else T2 := Yhi * Zlo; + pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo))); end if; else T2 := Ylo * Zhi; + pragma Assert (Big (T2) = Big (Double_Uns'(Ylo * Zhi))); end if; T1 := Ylo * Zlo; @@ -1527,10 +1531,14 @@ is Raise_Error; else T2 := Xhi * Ylo; + pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + + Big (Double_Uns'(Xlo * Yhi))); end if; elsif Yhi /= 0 then T2 := Xlo * Yhi; + pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + + Big (Double_Uns'(Xlo * Yhi))); else -- Yhi = Xhi = 0 T2 := 0; @@ -1544,7 +1552,7 @@ is pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi))); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Xhi * Ylo)), - Big (Double_Uns'(Xlo * Yhi))); + Big (Double_Uns'(Xlo * Yhi))); pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1)); Lemma_Add_Commutation (T2, Hi (T1)); pragma Assert @@ -2575,7 +2583,13 @@ is Big (Double_Uns (Qd (J))) - 1, Big (Double_Uns (Qd (J) - 1)), 0); - Qd (J) := Qd (J) - 1; + declare + Prev : constant Single_Uns := Qd (J) - 1 with Ghost; + begin + Qd (J) := Qd (J) - 1; + + pragma Assert (Qd (J) = Prev); + end; pragma Assert (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
reply other threads:[~2022-05-11 8:55 UTC|newest] Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20220511085554.9E90A3835413@sourceware.org \ --to=pmderodat@gcc.gnu.org \ --cc=gcc-cvs@gcc.gnu.org \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
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).