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.

diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb
index 9236189fc1529957fdcf4dda695324ebcefb8469..63aa2a2d53bbeccc442fa9053078256b2c669da0 100644 (file)
--- 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