diff options
| author | Yannick Moy <moy@adacore.com> | 2021-11-30 15:11:32 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-05 11:32:35 +0000 |
| commit | 3814652309edac1154ee3c7e40ff65ff861d17f3 (patch) | |
| tree | 29548a7b4dc8172b97ada4a08ec366c955150414 /gcc/ada/sem_ch3.adb | |
| parent | 1702fb6bf95de5461f896cf69832edc0e2e40cc5 (diff) | |
| download | gcc-3814652309edac1154ee3c7e40ff65ff861d17f3.zip gcc-3814652309edac1154ee3c7e40ff65ff861d17f3.tar.gz gcc-3814652309edac1154ee3c7e40ff65ff861d17f3.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/sem_ch3.adb')
0 files changed, 0 insertions, 0 deletions