projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b7630f) | patch
[Ada] Adapt proof of runtime unit s-arit32
authorYannick Moy <moy@adacore.com>
Wed, 20 Apr 2022 09:39:11 +0000 (09:39 +0000)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 30 May 2022 08:29:01 +0000 (08:29 +0000)
commit1ea22318caf52a98b32f8ef4e155376e7751db4b
tree0695039fc78b5643e05c9ead47ad0bb6b271d11ftree | snapshot
parent5b7630f2f266346173eb2172a9a96e925010afc5commit | diff
[Ada] Adapt proof of runtime unit s-arit32

After changes in GNATprove, adapt proof. Simply move an assertion up
before it is first needed here.

gcc/ada/

* libgnat/s-arit32.adb (Scaled_Divide32): Move assertion up.
gcc/ada/libgnat/s-arit32.adb diff | blob | history
Domain: System / Toolchain;