diff options
| author | Yannick Moy <moy@adacore.com> | 2021-12-02 15:42:32 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-01-06 17:11:30 +0000 |
| commit | 07793a58d0702ade3d7300c19be65cf1bb1504d2 (patch) | |
| tree | 74f2de43404d924f07eaeb9d355c7c9ea14cb980 /gcc/go | |
| parent | ed722edd2f4accad60744b95426dba3fc9ca084c (diff) | |
| download | gcc-07793a58d0702ade3d7300c19be65cf1bb1504d2.zip gcc-07793a58d0702ade3d7300c19be65cf1bb1504d2.tar.gz gcc-07793a58d0702ade3d7300c19be65cf1bb1504d2.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/go')
0 files changed, 0 insertions, 0 deletions