From: Piotr Trojanek <trojanek@adacore.com>
Date: Wed, 28 Jul 2021 13:16:09 +0000 (+0200)
Subject: [Ada] Remove Initializes contracts from Ada.Strings.Bounded
X-Git-Tag: basepoints/gcc-13~4465
X-Git-Url: http://git.ipfire.org/gitweb.cgi?a=commitdiff_plain;h=e2b2f629da02f9b2549db7297133166f721953ae;p=thirdparty%2Fgcc.git

[Ada] Remove Initializes contracts from Ada.Strings.Bounded

gcc/ada/

	* libgnat/a-strbou.ads (Generic_Bounded_Length): Remove explicit
	Initializes contract.
---

diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index cc24f707e5f8..31c1cc97093e 100644
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -45,8 +45,6 @@ package Ada.Strings.Bounded with SPARK_Mode is
       --  Maximum length of a Bounded_String
 
    package Generic_Bounded_Length with SPARK_Mode,
-     Initializes       => (Null_Bounded_String => Max,
-                           Max_Length          => Max),
      Initial_Condition => Length (Null_Bounded_String) = 0,
      Abstract_State    => null
    is