From: Yannick Moy <moy@adacore.com>
Date: Mon, 26 Jul 2021 14:56:27 +0000 (+0200)
Subject: [Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not
X-Git-Tag: basepoints/gcc-13~4496
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=490a987e05da85710ca68f4f30948ec904d745e9;p=thirdparty%2Fgcc.git

[Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not

gcc/ada/

	* libgnat/a-strunb.ads: Mark package in SPARK with private part
	not in SPARK.
	(Free): Mark not in SPARK.
---

diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
index 13c7612116c8..77d8a59ca482 100644
--- a/gcc/ada/libgnat/a-strunb.ads
+++ b/gcc/ada/libgnat/a-strunb.ads
@@ -53,6 +53,7 @@ private with Ada.Strings.Text_Buffers;
 --  and selector operations are provided.
 
 package Ada.Strings.Unbounded with
+  SPARK_Mode,
   Initial_Condition => Length (Null_Unbounded_String) = 0
 is
    pragma Preelaborate;
@@ -73,7 +74,7 @@ is
    --  Provides a (nonprivate) access type for explicit processing of
    --  unbounded-length strings.
 
-   procedure Free (X : in out String_Access);
+   procedure Free (X : in out String_Access) with SPARK_Mode => Off;
    --  Performs an unchecked deallocation of an object of type String_Access
 
    --------------------------------------------------------
@@ -732,6 +733,8 @@ is
    --  strings applied to the string represented by Source's original value.
 
 private
+   pragma SPARK_Mode (Off);  --  Controlled types are not in SPARK
+
    pragma Inline (Length);
 
    package AF renames Ada.Finalization;