From: Yannick Moy <moy@adacore.com>
Date: Mon, 16 Jan 2023 10:32:49 +0000 (+0000)
Subject: ada: Recover proof of Interfaces.C for termination
X-Git-Tag: basepoints/gcc-15~9292
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=75fb45f0692270efa1a89590e0d7dd0688101e8b;p=thirdparty%2Fgcc.git

ada: Recover proof of Interfaces.C for termination

GNATprove reports possible non-terminating loops in functions
marked as terminating. Add loop variants to prove loop termination.

gcc/ada/

	* libgnat/i-c.adb: Add loop variants. Remove useless
	initialization.
---

diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb
index 4cfccf41b1c1..9236189fc152 100644
--- a/gcc/ada/libgnat/i-c.adb
+++ b/gcc/ada/libgnat/i-c.adb
@@ -186,7 +186,7 @@ is
      (Item     : char_array;
       Trim_Nul : Boolean := True) return String
    is
-      Count : Natural := 0;
+      Count : Natural;
       From  : size_t;
 
    begin
@@ -200,6 +200,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                  Item (J) /= nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -257,6 +258,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                 Item (J) /= nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -333,6 +335,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                  Item (J) /= wide_nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -390,6 +393,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                 Item (J) /= wide_nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -466,6 +470,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                  Item (J) /= char16_nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -523,6 +528,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                 Item (J) /= char16_nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -599,6 +605,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                  Item (J) /= char32_nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;
@@ -656,6 +663,7 @@ is
             pragma Loop_Invariant
               (for all J in Item'First .. From when J /= From =>
                 Item (J) /= char32_nul);
+            pragma Loop_Variant (Increases => From);
 
             if From > Item'Last then
                raise Terminator_Error;