| commit | af28783eb43e0b64c40e919103d024e8edf795a0 | |
| author | Yannick Moy <moy@adacore.com> | |
| Mon, 29 Nov 2021 15:21:40 +0000 (29 16:21 +0100) | ||
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | |
| Wed, 5 Jan 2022 11:32:35 +0000 (5 11:32 +0000) | ||
| tree | 1e0962ec4919071d2977d5e37640bde31ea3b060 | treesnapshot (tar.gz zip) |
| parent | 8ec9fd41cfe7956b2c25d4539a9b5941a5d5f4cd | commitdiff |
[Ada] Proof of runtime units for integer exponentiation (checks off)
gcc/ada/
* libgnat/s-exnint.ads: Mark in SPARK. Adapt to change to
package.
* libgnat/s-exnlli.ads: Likewise.
* libgnat/s-exnllli.ads: Likewise.
* libgnat/s-exponn.adb: Add lemmas and ghost code. Secial case
value zero as Left or Right to simplify proof.
* libgnat/s-exponn.ads: Transform the generic function into a
generic package with a function inside. Add a functional
contract.
gcc/ada/
* libgnat/s-exnint.ads: Mark in SPARK. Adapt to change to
package.
* libgnat/s-exnlli.ads: Likewise.
* libgnat/s-exnllli.ads: Likewise.
* libgnat/s-exponn.adb: Add lemmas and ghost code. Secial case
value zero as Left or Right to simplify proof.
* libgnat/s-exponn.ads: Transform the generic function into a
generic package with a function inside. Add a functional
contract.