diff options
| author | Yannick Moy <moy@adacore.com> | 2023-02-22 13:36:09 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-23 09:59:05 +0200 |
| commit | cf1cee3fadc0febaa130f8931ce87e8b0317633b (patch) | |
| tree | a17f06be3e664e4ebe25fe6b87ecfdec2d05847b /gcc/ada/usage.adb | |
| parent | b64aaf4d81916f5570ddf2414747f3152e8b9f84 (diff) | |
| download | gcc-cf1cee3fadc0febaa130f8931ce87e8b0317633b.zip gcc-cf1cee3fadc0febaa130f8931ce87e8b0317633b.tar.gz gcc-cf1cee3fadc0febaa130f8931ce87e8b0317633b.tar.bz2 | |
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.
Diffstat (limited to 'gcc/ada/usage.adb')
0 files changed, 0 insertions, 0 deletions