diff options
| author | Yannick Moy <moy@adacore.com> | 2022-04-11 15:56:01 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-19 14:05:29 +0000 |
| commit | 054cf924ac00a47301a1c49f6433f70775fe1c0d (patch) | |
| tree | c4b9ea9836b00503a8617c66309c39cdedddfecc /gcc/ada/gcc-interface | |
| parent | 88f7b07de7579251f5134b65dad406fdfda3d057 (diff) | |
| download | gcc-054cf924ac00a47301a1c49f6433f70775fe1c0d.zip gcc-054cf924ac00a47301a1c49f6433f70775fe1c0d.tar.gz gcc-054cf924ac00a47301a1c49f6433f70775fe1c0d.tar.bz2 | |
[Ada] Further 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 (Lemma_Abs_Range,
Lemma_Double_Shift_Left, Lemma_Shift_Left): New lemmas.
(Double_Divide): Add ghost code.
(Lemma_Concat_Definition, Lemma_Double_Shift_Left,
Lemma_Shift_Left, Lemma_Shift_Right): Define or complete lemmas.
(Scaled_Divide): Add ghost code.
Diffstat (limited to 'gcc/ada/gcc-interface')
0 files changed, 0 insertions, 0 deletions