projects / test_jj.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e7da31b) | patch
[Ada] Proof of runtime units for binary modular exponentiation
authorYannick Moy <moy@adacore.com>
Thu, 2 Dec 2021 09:55:04 +0000 (10:55 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 6 Jan 2022 17:11:30 +0000 (17:11 +0000)
commited722edd2f4accad60744b95426dba3fc9ca084c
tree733e41b40bb62b6d799d646a4d73cd001e4e144ftree | snapshot
parente7da31ba2030b85ff0d15a0c4aac3318cb66b64acommit | diff
[Ada] Proof of runtime units for binary modular exponentiation

gcc/ada/

* libgnat/s-explllu.ads: Mark in SPARK.
* libgnat/s-expllu.ads: Mark in SPARK.
* libgnat/s-exponu.adb: Add loop invariants and needed
assertions.
* libgnat/s-exponu.ads: Add functional contract.
* libgnat/s-expuns.ads: Mark in SPARK.
gcc/ada/libgnat/s-explllu.ads diff | blob | history
gcc/ada/libgnat/s-expllu.ads diff | blob | history
gcc/ada/libgnat/s-exponu.adb diff | blob | history
gcc/ada/libgnat/s-exponu.ads diff | blob | history
gcc/ada/libgnat/s-expuns.ads diff | blob | history