diff options
| author | Yannick Moy <moy@adacore.com> | 2022-04-04 17:38:57 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-18 08:41:04 +0000 |
| commit | 3c63f73051458b24298eb82ddd109bbc6a453464 (patch) | |
| tree | d631f84ab206cb131d325cce839787f38cf4024b /gcc/fortran | |
| parent | 5b0e8d6937f7857e3dc7486a989e0c72d478c1ed (diff) | |
| download | gcc-3c63f73051458b24298eb82ddd109bbc6a453464.zip gcc-3c63f73051458b24298eb82ddd109bbc6a453464.tar.gz gcc-3c63f73051458b24298eb82ddd109bbc6a453464.tar.bz2 | |
[Ada] Fix proof of runtime units
Update to latest version of Why3 caused some proof regressions.
Fix the proof by changing ghost code.
gcc/ada/
* libgnat/s-imagei.adb (Set_Digits): Add assertion.
* libgnat/s-imgboo.adb (Image_Boolean): Add assertions.
* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertion.
Diffstat (limited to 'gcc/fortran')
0 files changed, 0 insertions, 0 deletions