From: Yannick Moy <moy@adacore.com>
Date: Wed, 22 Feb 2023 13:36:09 +0000 (+0000)
Subject: ada: Facilitate proof of Interfaces.C.To_Ada
X-Git-Tag: basepoints/gcc-15~9036
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=cf1cee3fadc0febaa130f8931ce87e8b0317633b;p=thirdparty%2Fgcc.git

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 9236189fc152..63aa2a2d53bb 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