* [Ada] Add loop variants to Ada.Strings.Search and Ada.Strings.Maps
@ 2022-09-02 7:53 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-02 7:53 UTC (permalink / raw)
To: gcc-patches; +Cc: Claire Dross
[-- Attachment #1: Type: text/plain, Size: 226 bytes --]
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 2435 bytes --]
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;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-02 7:53 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-02 7:53 [Ada] Add loop variants to Ada.Strings.Search and Ada.Strings.Maps Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).