| commit | cf1cee3fadc0febaa130f8931ce87e8b0317633b | |
| author | Yannick Moy <moy@adacore.com> | |
| Wed, 22 Feb 2023 13:36:09 +0000 (22 13:36 +0000) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Tue, 23 May 2023 07:59:05 +0000 (23 09:59 +0200) | ||
| tree | a17f06be3e664e4ebe25fe6b87ecfdec2d05847b | treesnapshot (tar.gz zip) |
| parent | b64aaf4d81916f5570ddf2414747f3152e8b9f84 | commitdiff |
ada: Facilitate proof of Interfaces.C.To_Ada
Nightly runs of GNATprove fail on proof of the assertion following
the loop. Add a loop invariant to facilitate that proof.
gcc/ada/
* libgnat/i-c.adb (To_Ada): Add loop invariant.
Nightly runs of GNATprove fail on proof of the assertion following
the loop. Add a loop invariant to facilitate that proof.
gcc/ada/
* libgnat/i-c.adb (To_Ada): Add loop invariant.
| gcc/ada/libgnat/i-c.adb | diffblobblamehistory |