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 | |
| 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.
| -rw-r--r-- | gcc/ada/libgnat/i-c.adb | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb index 9236189..63aa2a2 100644 --- a/gcc/ada/libgnat/i-c.adb +++ b/gcc/ada/libgnat/i-c.adb @@ -605,6 +605,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char32_nul); + pragma Loop_Invariant (From <= Item'First + C_Length_Ghost (Item)); pragma Loop_Variant (Increases => From); if From > Item'Last then |