projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b0e8d6) | patch
[Ada] Fix proof of runtime units
authorYannick Moy <moy@adacore.com>
Mon, 4 Apr 2022 15:38:57 +0000 (17:38 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 18 May 2022 08:41:04 +0000 (08:41 +0000)
commit3c63f73051458b24298eb82ddd109bbc6a453464
treed631f84ab206cb131d325cce839787f38cf4024btree | snapshot
parent5b0e8d6937f7857e3dc7486a989e0c72d478c1edcommit | diff
[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.
gcc/ada/libgnat/s-imagei.adb diff | blob | history
gcc/ada/libgnat/s-imgboo.adb diff | blob | history
gcc/ada/libgnat/s-valueu.adb diff | blob | history
Domain: System / Toolchain;