diff options
| author | Yannick Moy <moy@adacore.com> | 2022-03-11 11:54:53 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-16 08:42:05 +0000 |
| commit | c1e007985fef1389ba09f5b558aa4e7b9f03783f (patch) | |
| tree | 0408821c5adb45336166e7c286e30a14a12a48eb /gcc | |
| parent | 9eb55045f8d22919c47b38809afbcad7ad9a38d5 (diff) | |
| download | gcc-c1e007985fef1389ba09f5b558aa4e7b9f03783f.zip gcc-c1e007985fef1389ba09f5b558aa4e7b9f03783f.tar.gz gcc-c1e007985fef1389ba09f5b558aa4e7b9f03783f.tar.bz2 | |
[Ada] Fix proof of double arithmetic units
Proof of an assertion is not automatic anymore. Add two assertions
before it to guide the prover.
gcc/ada/
* libgnat/s-aridou.adb (Double_Divide): Add intermediate
assertions.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-aridou.adb | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index ffb6f4ca..08cbed7 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -941,11 +941,13 @@ is else T2 := Yhi * Zlo; pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo))); + pragma Assert (Big_0 = Big (Double_Uns'(Ylo * Zhi))); end if; else T2 := Ylo * Zhi; pragma Assert (Big (T2) = Big (Double_Uns'(Ylo * Zhi))); + pragma Assert (Big_0 = Big (Double_Uns'(Yhi * Zlo))); end if; T1 := Ylo * Zlo; |