projects / test_jj.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ed722ed) | patch
[Ada] Proof of runtime unit for non-binary modular exponentiation
authorYannick Moy <moy@adacore.com>
Thu, 2 Dec 2021 14:42:32 +0000 (15:42 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 6 Jan 2022 17:11:30 +0000 (17:11 +0000)
commit07793a58d0702ade3d7300c19be65cf1bb1504d2
tree74f2de43404d924f07eaeb9d355c7c9ea14cb980tree | snapshot
parented722edd2f4accad60744b95426dba3fc9ca084ccommit | diff
[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 diff | blob | history
gcc/ada/libgnat/s-expmod.ads diff | blob | history