[COMMITTED] ada: Facilitate proof of Interfaces.C.To_Ada

[Marc Poulhiès via Gcc-patches]

From: Yannick Moy <m...@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/i-c.adb | 1 +
 1 file changed, 1 insertion(+)

diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb
index 9236189fc15..63aa2a2d53b 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
-- 
2.40.0