diff options
| author | Yannick Moy <moy@adacore.com> | 2022-07-11 15:00:46 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-02 09:34:06 +0200 |
| commit | 7c339b3b5a63bac5e5223e33cce4c9833153edbb (patch) | |
| tree | 1ee1568c1a5589695d0d6dbab3e38b587c753938 /gcc/gcc.cc | |
| parent | 66643a9fe96e66914f074bee84d1fc30915afcb5 (diff) | |
| download | gcc-7c339b3b5a63bac5e5223e33cce4c9833153edbb.zip gcc-7c339b3b5a63bac5e5223e33cce4c9833153edbb.tar.gz gcc-7c339b3b5a63bac5e5223e33cce4c9833153edbb.tar.bz2 | |
[Ada] Recover proof of Scaled_Divide in System.Arith_64
Proof of Scaled_Divide was impacted by changes in provers and Why3.
Recover it partially, leaving some unproved basic inferences to be
further investigated.
gcc/ada/
* libgnat/s-aridou.adb: Add or rework ghost code.
* libgnat/s-aridou.ads: Add Big_Positive subtype.
Diffstat (limited to 'gcc/gcc.cc')
0 files changed, 0 insertions, 0 deletions