From 3a4c933f593c89295b966f789cba9ad5a6dad28a Mon Sep 17 00:00:00 2001
From: Claire Dross <dross@adacore.com>
Date: Tue, 12 Jul 2022 13:21:40 +0200
Subject: [PATCH] [Ada] Add loop variants to Ada.Strings.Search and
 Ada.Strings.Maps

Add loop variants to verify that loops terminate in string handling.

gcc/ada/

	* libgnat/a-strmap.adb: Add variants to simple and while loops.
	* libgnat/a-strsea.adb: Idem.
---
 gcc/ada/libgnat/a-strmap.adb | 4 ++++
 gcc/ada/libgnat/a-strsea.adb | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/gcc/ada/libgnat/a-strmap.adb b/gcc/ada/libgnat/a-strmap.adb
index 77780f93f0c7..e092db046caa 100644
--- a/gcc/ada/libgnat/a-strmap.adb
+++ b/gcc/ada/libgnat/a-strmap.adb
@@ -290,6 +290,7 @@ is
          loop
             pragma Loop_Invariant
               (Seq1 (Seq1'First .. J) = Seq2 (Seq2'First .. J));
+            pragma Loop_Variant (Increases => J);
 
             if J = Positive'Last then
                return;
@@ -440,6 +441,7 @@ is
               (Character'Pos (C) >= Character'Pos (C'Loop_Entry));
             pragma Loop_Invariant
               (for all Char in C'Loop_Entry .. C => not Set (Char));
+            pragma Loop_Variant (Increases => C);
             exit when C = Character'Last;
             C := Character'Succ (C);
          end loop;
@@ -457,6 +459,7 @@ is
             pragma Loop_Invariant
               (for all Char in C'Loop_Entry .. C =>
                  (if Char /= C then Set (Char)));
+            pragma Loop_Variant (Increases => C);
             exit when not Set (C) or else C = Character'Last;
             C := Character'Succ (C);
          end loop;
@@ -491,6 +494,7 @@ is
          pragma Loop_Invariant
            (for all Span of Max_Ranges (1 .. Range_Num) =>
               (for all Char in Span.Low .. Span.High => Set (Char)));
+         pragma Loop_Variant (Increases => Range_Num);
       end loop;
 
       return Max_Ranges (1 .. Range_Num);
diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb
index 71a415fbc15c..652c79716fed 100644
--- a/gcc/ada/libgnat/a-strsea.adb
+++ b/gcc/ada/libgnat/a-strsea.adb
@@ -113,6 +113,7 @@ package body Ada.Strings.Search with SPARK_Mode is
 
             pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
             pragma Loop_Invariant (Ind >= Source'First);
+            pragma Loop_Variant (Increases => Ind);
          end loop;
 
       --  Mapped case
@@ -142,6 +143,7 @@ package body Ada.Strings.Search with SPARK_Mode is
             null;
             pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
             pragma Loop_Invariant (Ind >= Source'First);
+            pragma Loop_Variant (Increases => Ind);
          end loop;
       end if;
 
@@ -200,6 +202,7 @@ package body Ada.Strings.Search with SPARK_Mode is
          null;
          pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
          pragma Loop_Invariant (Ind >= Source'First);
+         pragma Loop_Variant (Increases => Ind);
       end loop;
 
       return Num;
-- 
2.47.2