diff options
| author | Yannick Moy <moy@adacore.com> | 2022-04-08 15:24:49 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-18 08:41:08 +0000 |
| commit | c6c9b82bc17e957c621bfb58e33801f956c7c31c (patch) | |
| tree | ea0dac41b2513219767f914c701fda45f064dfb6 /gcc/fortran/openmp.cc | |
| parent | 6f8f9d1bcf55187cb81ef7b0ef1e23db1bc0d440 (diff) | |
| download | gcc-c6c9b82bc17e957c621bfb58e33801f956c7c31c.zip gcc-c6c9b82bc17e957c621bfb58e33801f956c7c31c.tar.gz gcc-c6c9b82bc17e957c621bfb58e33801f956c7c31c.tar.bz2 | |
[Ada] Adapt proof of double arithmetic runtime unit
After changes in Why3 and generation of VCs, ghost code needs to be
adapted for proofs to remain automatic.
gcc/ada/
* libgnat/s-aridou.adb (Big3): Change return type.
(Lemma_Mult_Non_Negative, Lemma_Mult_Non_Positive): Reorder
alphabetically.
(Lemma_Concat_Definition, Lemma_Double_Big_2xxsingle): New
lemmas.
(Double_Divide, Scaled_Divide): Add assertions.
Diffstat (limited to 'gcc/fortran/openmp.cc')
0 files changed, 0 insertions, 0 deletions