diff options
| author | Yannick Moy <moy@adacore.com> | 2021-12-02 10:55:04 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-06 17:11:30 +0000 |
| commit | ed722edd2f4accad60744b95426dba3fc9ca084c (patch) | |
| tree | 733e41b40bb62b6d799d646a4d73cd001e4e144f /gcc/ada/contracts.adb | |
| parent | e7da31ba2030b85ff0d15a0c4aac3318cb66b64a (diff) | |
| download | gcc-ed722edd2f4accad60744b95426dba3fc9ca084c.zip gcc-ed722edd2f4accad60744b95426dba3fc9ca084c.tar.gz gcc-ed722edd2f4accad60744b95426dba3fc9ca084c.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/contracts.adb')
0 files changed, 0 insertions, 0 deletions