ada: Add annotations for proof of termination of runtime units

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.

diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index 0ada7872572bef658bbcb0a95628e037d46c4c7c..1e4a366c5fe37eaf48e8fa9d02e66a8835bf4f4f 100644 (file)
--- 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 7e8ac1cd0d3e632ef106afa8e1867ef5799b20e7..ace705d2e8abf371d4e008502112a674843afaac 100644 (file)
--- 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 dee64ab9e0e18ece36fa1e075cc34126566b8cc4..0838d59d5f7cc1caa6669a65a9e746105b9e209f 100644 (file)
--- 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 ef3584382eb6dbf3c6e590455516bbab2b7f65e1..7c1e2fac1af57fe5394e31e74459ae42703a3a6b 100644 (file)
--- 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 2c24e1a69832cfa1b67e36f934ee0fd583659f04..5651bdcdf3cfb5e57da405384d97685f6a636abb 100644 (file)
--- 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 dd7b0322b76894b7a1b04655c913639461d42c3b..70aa4f8bcf31f91da6ac2b65b4c147639bbfe8f8 100644 (file)
--- 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 14e78e44ee53c89791d100441d3a15fc9ac256a5..7a8a2bac996ea07afc087894ddb54e45839e08a1 100644 (file)
--- 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 --