[Ada] Proof of runtime units for integer exponentiation (checks on)
authorYannick Moy <moy@adacore.com>
Tue, 30 Nov 2021 14:11:32 +0000 (15:11 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 5 Jan 2022 11:32:35 +0000 (11:32 +0000)
commit3814652309edac1154ee3c7e40ff65ff861d17f3
tree29548a7b4dc8172b97ada4a08ec366c955150414
parent1702fb6bf95de5461f896cf69832edc0e2e40cc5
[Ada] Proof of runtime units for integer exponentiation (checks on)

gcc/ada/

* libgnat/s-expint.ads: Mark in SPARK. Adapt to change to
package.
* libgnat/s-explli.ads: Likewise.
* libgnat/s-expllli.ads: Likewise.
* libgnat/s-expont.adb: Add lemmas and ghost code.
* libgnat/s-expont.ads: Add functional contract.
gcc/ada/libgnat/s-expint.ads
gcc/ada/libgnat/s-explli.ads
gcc/ada/libgnat/s-expllli.ads
gcc/ada/libgnat/s-expont.adb
gcc/ada/libgnat/s-expont.ads