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/d | |
| 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/d')
0 files changed, 0 insertions, 0 deletions