[Ada] Global contracts on expression functions in Ada.Strings.Superbounded

[Ada] Global contracts on expression functions in Ada.Strings.Superbounded

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 268 bytes --]

For consistency, add Global => null contracts also to expression
functions in the Ada.Strings.Superbounded package.

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

gcc/ada/

	* libgnat/a-strsup.ads (Super_Length, Super_Element,
	Super_Slice): Add Global contracts.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1453 bytes --]

diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads
--- a/gcc/ada/libgnat/a-strsup.ads
+++ b/gcc/ada/libgnat/a-strsup.ads
@@ -76,7 +76,8 @@ package Ada.Strings.Superbounded with SPARK_Mode is
    --  that they can be renamed in Ada.Strings.Bounded.Generic_Bounded_Length.
 
    function Super_Length (Source : Super_String) return Natural
-   is (Source.Current_Length);
+   is (Source.Current_Length)
+   with Global => null;
 
    --------------------------------------------------------
    -- Conversion, Concatenation, and Selection Functions --
@@ -620,7 +621,8 @@ package Ada.Strings.Superbounded with SPARK_Mode is
    is (if Index <= Source.Current_Length
        then Source.Data (Index)
        else raise Index_Error)
-   with Pre => Index <= Super_Length (Source);
+   with Pre    => Index <= Super_Length (Source),
+        Global => null;
 
    procedure Super_Replace_Element
      (Source : in out Super_String;
@@ -649,8 +651,9 @@ package Ada.Strings.Superbounded with SPARK_Mode is
           --  get the null string in accordance with normal Ada slice rules.
 
           String (Source.Data (Low .. High)))
-   with Pre => Low - 1 <= Super_Length (Source)
-                 and then High <= Super_Length (Source);
+   with Pre    => Low - 1 <= Super_Length (Source)
+                    and then High <= Super_Length (Source),
+        Global => null;
 
    function Super_Slice
      (Source : Super_String;