diff options
| author | Yannick Moy <moy@adacore.com> | 2022-02-02 12:52:36 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-11 08:53:20 +0000 |
| commit | 4c533da21d6298cdf9eb11df7353b8c8684c7756 (patch) | |
| tree | 0cba4d9c9160c50c696a2fdd16edc525479e8bab /gcc | |
| parent | a58f70c30c4900bb9024681e0b86e85d96cac2e7 (diff) | |
| download | gcc-4c533da21d6298cdf9eb11df7353b8c8684c7756.zip gcc-4c533da21d6298cdf9eb11df7353b8c8684c7756.tar.gz gcc-4c533da21d6298cdf9eb11df7353b8c8684c7756.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 0fefb6b..ffb6f4ca 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)); |