diff mbox series

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

Message ID 20211025150918.GA346629@adacore.com
State Committed
Commit a3a6a0a50af2dd257682289703b721ba1b7863ca
Headers
Series [Ada] Global contracts on expression functions in Ada.Strings.Superbounded |

Commit Message

Pierre-Marie de Rodat Oct. 25, 2021, 3:09 p.m. UTC 
  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.
diff mbox series

Patch

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;