From: Yannick Moy <m...@adacore.com>
String-manipulating functions should always terminate. Add justification
for the termination of Mapping function parameter, and loop variants
where needed. This is needed for GNATprove to prove termination.
gcc/ada/
* libgnat/a-strbou.ads: Add justifications for Mapping.
* libgnat/a-strfix.adb: Same.
* libgnat/a-strfix.ads: Same.
* libgnat/a-strsea.adb: Same.
* libgnat/a-strsea.ads: Same.
* libgnat/a-strsup.adb: Same and add loop variants.
* libgnat/a-strsup.ads: Same and add specification of termination.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/a-strbou.ads | 6 ++++++
gcc/ada/libgnat/a-strfix.adb | 12 ++++++++++++
gcc/ada/libgnat/a-strfix.ads | 6 ++++++
gcc/ada/libgnat/a-strsea.adb | 18 ++++++++++++++++++
gcc/ada/libgnat/a-strsea.ads | 3 +++
gcc/ada/libgnat/a-strsup.adb | 14 ++++++++++++++
gcc/ada/libgnat/a-strsup.ads | 7 +++++++
7 files changed, 66 insertions(+)
diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index 0ada7872572..1e4a366c5fe 100644
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -1341,6 +1341,9 @@ package Ada.Strings.Bounded with SPARK_Mode is
(for all K in 1 .. Length (Source) =>
Element (Translate'Result, K) = Mapping (Element (Source, K))),
Global => null;
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
procedure Translate
(Source : in out Bounded_String;
@@ -1352,6 +1355,9 @@ package Ada.Strings.Bounded with SPARK_Mode is
(for all K in 1 .. Length (Source) =>
Element (Source, K) = Mapping (Element (Source'Old, K))),
Global => null;
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
---------------------------------------
-- String Transformation Subprograms --
diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb
index 7e8ac1cd0d3..ace705d2e8a 100644
--- a/gcc/ada/libgnat/a-strfix.adb
+++ b/gcc/ada/libgnat/a-strfix.adb
@@ -773,12 +773,18 @@ package body Ada.Strings.Fixed with SPARK_Mode is
do
for J in Source'Range loop
Result (J - (Source'First - 1)) := Mapping.all (Source (J));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
pragma Loop_Invariant
(for all K in Source'First .. J =>
Result (K - (Source'First - 1))'Initialized);
pragma Loop_Invariant
(for all K in Source'First .. J =>
Result (K - (Source'First - 1)) = Mapping (Source (K)));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
end return;
end Translate;
@@ -791,9 +797,15 @@ package body Ada.Strings.Fixed with SPARK_Mode is
begin
for J in Source'Range loop
Source (J) := Mapping.all (Source (J));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
pragma Loop_Invariant
(for all K in Source'First .. J =>
Source (K) = Mapping (Source'Loop_Entry (K)));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
end Translate;
diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index dee64ab9e0e..0838d59d5f7 100644
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -754,6 +754,9 @@ package Ada.Strings.Fixed with SPARK_Mode is
= Mapping (Source (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
function Translate
(Source : String;
@@ -796,6 +799,9 @@ package Ada.Strings.Fixed with SPARK_Mode is
(for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
procedure Translate
(Source : in out String;
diff --git a/gcc/ada/libgnat/a-strsea.adb b/gcc/ada/libgnat/a-strsea.adb
index ef3584382eb..7c1e2fac1af 100644
--- a/gcc/ada/libgnat/a-strsea.adb
+++ b/gcc/ada/libgnat/a-strsea.adb
@@ -185,6 +185,9 @@ package body Ada.Strings.Search with SPARK_Mode is
Ind := Ind + 1;
for K in Pattern'Range loop
if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
goto Cont;
end if;
@@ -192,6 +195,9 @@ package body Ada.Strings.Search with SPARK_Mode is
pragma Loop_Invariant
(for all J in Pattern'First .. K =>
Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
pragma Assert (Match (Source, Pattern, Mapping, Ind));
@@ -489,12 +495,18 @@ package body Ada.Strings.Search with SPARK_Mode is
if Pattern (K) /= Mapping.all
(Source (Ind + (K - Pattern'First)))
then
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
goto Cont1;
end if;
pragma Loop_Invariant
(for all J in Pattern'First .. K =>
Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
pragma Assert (Match (Source, Pattern, Mapping, Ind));
@@ -515,12 +527,18 @@ package body Ada.Strings.Search with SPARK_Mode is
if Pattern (K) /= Mapping.all
(Source (Ind + (K - Pattern'First)))
then
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
goto Cont2;
end if;
pragma Loop_Invariant
(for all J in Pattern'First .. K =>
Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
return Ind;
diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads
index 2c24e1a6983..5651bdcdf3c 100644
--- a/gcc/ada/libgnat/a-strsea.ads
+++ b/gcc/ada/libgnat/a-strsea.ads
@@ -74,6 +74,9 @@ package Ada.Strings.Search with SPARK_Mode is
and then Source'Length > 0
and then From in Source'First .. Source'Last - (Pattern'Length - 1),
Global => null;
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
function Match
(Source : String;
diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index dd7b0322b76..70aa4f8bcf3 100644
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -1570,6 +1570,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
(for all K in 1 .. Indx =>
Result.Data (K) =
Item (Item'First + (K - 1) mod Ilen));
+ pragma Loop_Variant (Increases => Indx);
end loop;
Result.Data (Indx + 1 .. Max_Length) := Super_String_Data
@@ -1609,6 +1610,7 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
(for all K in Indx + 1 .. Max_Length =>
Result.Data (K) =
Item (Item'Last - (Max_Length - K) mod Ilen));
+ pragma Loop_Variant (Decreases => Indx);
end loop;
Result.Data (1 .. Indx) :=
@@ -1845,10 +1847,16 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
begin
for J in 1 .. Source.Current_Length loop
Result.Data (J) := Mapping.all (Source.Data (J));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
pragma Loop_Invariant
(for all K in 1 .. J =>
Result.Data (K) = Mapping (Source.Data (K)));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
Result.Current_Length := Source.Current_Length;
@@ -1862,9 +1870,15 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
begin
for J in 1 .. Source.Current_Length loop
Source.Data (J) := Mapping.all (Source.Data (J));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
pragma Loop_Invariant
(for all K in 1 .. J =>
Source.Data (K) = Mapping (Source'Loop_Entry.Data (K)));
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
end loop;
end Super_Translate;
diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads
index 14e78e44ee5..7a8a2bac996 100644
--- a/gcc/ada/libgnat/a-strsup.ads
+++ b/gcc/ada/libgnat/a-strsup.ads
@@ -53,6 +53,7 @@ with Ada.Strings.Text_Buffers;
package Ada.Strings.Superbounded with SPARK_Mode is
pragma Preelaborate;
+ pragma Annotate (GNATprove, Always_Return, Superbounded);
-- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
-- derived from Super_String, with the constraint of the maximum length.
@@ -1406,6 +1407,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is
Super_Element (Super_Translate'Result, K) =
Mapping (Super_Element (Source, K))),
Global => null;
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
procedure Super_Translate
(Source : in out Super_String;
@@ -1418,6 +1422,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is
Super_Element (Source, K) =
Mapping (Super_Element (Source'Old, K))),
Global => null;
+ pragma Annotate (GNATprove, False_Positive,
+ "call via access-to-subprogram",
+ "function Mapping must always terminate");
---------------------------------------
-- String Transformation Subprograms --
--
2.40.0
