diff mbox series

[COMMITTED] ada: Recover proof of Interfaces.C for termination

Message ID 20230515094425.1408943-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Recover proof of Interfaces.C for termination |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès May 15, 2023, 9:44 a.m. UTC 
  From: Yannick Moy <moy@adacore.com>

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.

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

---
 gcc/ada/libgnat/i-c.adb | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb
index 4cfccf41b1c..9236189fc15 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;