diff mbox series

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

Message ID 20230523080828.1873797-1-poulhies@adacore.com
State Unresolved
Headers
Series [COMMITTED] ada: Facilitate proof of Interfaces.C.To_Ada |

Checks

Context Check Description
snail/gcc-patch-check warning Git am fail log

Commit Message

Marc Poulhiès May 23, 2023, 8:08 a.m. UTC 
  From: Yannick Moy <moy@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 mbox series

Patch

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