diff mbox series

[Ada] Add loop variants to Ada.Strings.Search and Ada.Strings.Maps

Message ID 20220902075326.GA1121061@poulhies-Precision-5550
State New, archived
Headers
Series [Ada] Add loop variants to Ada.Strings.Search and Ada.Strings.Maps |

Commit Message

Marc Poulhiès Sept. 2, 2022, 7:53 a.m. UTC 
  Add loop variants to verify that loops terminate in string handling.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/a-strmap.adb: Add variants to simple and while loops.
	* libgnat/a-strsea.adb: Idem.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/a-strmap.adb b/gcc/ada/libgnat/a-strmap.adb
--- 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
--- 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;