projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9eb5504) | patch
[Ada] Fix proof of double arithmetic units
authorYannick Moy <moy@adacore.com>
Fri, 11 Mar 2022 10:54:53 +0000 (11:54 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 16 May 2022 08:42:05 +0000 (08:42 +0000)
commitc1e007985fef1389ba09f5b558aa4e7b9f03783f
tree0408821c5adb45336166e7c286e30a14a12a48ebtree | snapshot
parent9eb55045f8d22919c47b38809afbcad7ad9a38d5commit | diff
[Ada] Fix proof of double arithmetic units

Proof of an assertion is not automatic anymore. Add two assertions
before it to guide the prover.

gcc/ada/

* libgnat/s-aridou.adb (Double_Divide): Add intermediate
assertions.
gcc/ada/libgnat/s-aridou.adb diff | blob | history
Domain: System / Toolchain;