[gcc r12-3817] [Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not

[gcc r12-3817] [Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:490a987e05da85710ca68f4f30948ec904d745e9

commit r12-3817-g490a987e05da85710ca68f4f30948ec904d745e9
Author: Yannick Moy <moy@adacore.com>
Date:   Mon Jul 26 16:56:27 2021 +0200

    [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:
---
 gcc/ada/libgnat/a-strunb.ads | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
index 13c7612116c..77d8a59ca48 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;