diff options
| author | Claire Dross <dross@adacore.com> | 2022-07-12 09:14:40 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-02 09:34:06 +0200 |
| commit | bf52ee6a4f86cbd60770fc22ad5abce0f437762a (patch) | |
| tree | 16f5c5f9b1f5e1609fc7cb753773c3d6b5a3465c /gcc/gcc.cc | |
| parent | 7c339b3b5a63bac5e5223e33cce4c9833153edbb (diff) | |
| download | gcc-bf52ee6a4f86cbd60770fc22ad5abce0f437762a.zip gcc-bf52ee6a4f86cbd60770fc22ad5abce0f437762a.tar.gz gcc-bf52ee6a4f86cbd60770fc22ad5abce0f437762a.tar.bz2 | |
[Ada] Fix proof of runtime unit System.Wid_*
Regain the proof of System.Wid_* after changes in provers and Why3.
gcc/ada/
* libgnat/s-widthu.adb (Lemma_Euclidean): Lemma to prove the
relation between the quotient/remainder of a division.
Diffstat (limited to 'gcc/gcc.cc')
0 files changed, 0 insertions, 0 deletions