| commit | 07793a58d0702ade3d7300c19be65cf1bb1504d2 | |
| author | Yannick Moy <moy@adacore.com> | |
| Thu, 2 Dec 2021 14:42:32 +0000 (2 15:42 +0100) | ||
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | |
| Thu, 6 Jan 2022 17:11:30 +0000 (6 17:11 +0000) | ||
| tree | 74f2de43404d924f07eaeb9d355c7c9ea14cb980 | treesnapshot (tar.gz zip) |
| parent | ed722edd2f4accad60744b95426dba3fc9ca084c | commitdiff |
[Ada] Proof of runtime unit for non-binary modular exponentiation
gcc/ada/
* libgnat/s-expmod.adb: Mark in SPARK. Add ghost code for proof.
* libgnat/s-expmod.ads: Mark in SPARK. Add ghost specifications.
gcc/ada/
* libgnat/s-expmod.adb: Mark in SPARK. Add ghost code for proof.
* libgnat/s-expmod.ads: Mark in SPARK. Add ghost specifications.
| gcc/ada/libgnat/s-expmod.adb | diffblobblamehistory | |
| gcc/ada/libgnat/s-expmod.ads | diffblobblamehistory |