diff options
| author | Claire Dross <dross@adacore.com> | 2022-07-12 11:34:31 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-02 09:34:06 +0200 |
| commit | e973ea0151a1551947fcdcadaeb9406789324b06 (patch) | |
| tree | 6ecc4ac659c302648e363988a210fed016cab833 /gcc/gcc.cc | |
| parent | bf52ee6a4f86cbd60770fc22ad5abce0f437762a (diff) | |
| download | gcc-e973ea0151a1551947fcdcadaeb9406789324b06.zip gcc-e973ea0151a1551947fcdcadaeb9406789324b06.tar.gz gcc-e973ea0151a1551947fcdcadaeb9406789324b06.tar.bz2 | |
[Ada] Fix proof of runtime unit System.Exp_Mod
Regain the proof of System.Exp_Mod after changes in provers and Why3.
gcc/ada/
* libgnat/s-expmod.adb (Lemma_Add_Mod): Add new lemma to factor
out a complex sub-proof.
(Exp_Modular): Add assertion to help proof.
Diffstat (limited to 'gcc/gcc.cc')
0 files changed, 0 insertions, 0 deletions