[gcc r13-1426] [Ada] Update the documentation of functional containers

[gcc r13-1426] [Ada] Update the documentation of functional containers

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c

commit r13-1426-g2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c
Author: Claire Dross <dross@adacore.com>
Date:   Tue May 24 16:37:18 2022 +0200

    [Ada] Update the documentation of functional containers
    
    Functional containers are now controlled. Update the documentation
    accordingly.
    
    gcc/ada/
    
            * doc/gnat_rm/the_gnat_library.rst: Functional vectors, sets,
            and maps are now controlled.
            * gnat_rm.texi: Regenerate.

Diff:
---
 gcc/ada/doc/gnat_rm/the_gnat_library.rst | 40 +++++++++++++++-----------------
 gcc/ada/gnat_rm.texi                     | 40 +++++++++++++++-----------------
 2 files changed, 38 insertions(+), 42 deletions(-)

diff --git a/gcc/ada/doc/gnat_rm/the_gnat_library.rst b/gcc/ada/doc/gnat_rm/the_gnat_library.rst
index 72ec5e62687..85044f341d0 100644
--- a/gcc/ada/doc/gnat_rm/the_gnat_library.rst
+++ b/gcc/ada/doc/gnat_rm/the_gnat_library.rst
@@ -285,17 +285,16 @@ specification of this unit is compatible with SPARK 2014.
 .. index:: Functional sets
 
 This child of ``Ada.Containers`` defines immutable sets. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
 
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 .. _`Ada.Containers.Functional_Maps_(a-cofuma.ads)`:
 
@@ -307,17 +306,16 @@ specification of this unit is compatible with SPARK 2014.
 .. index:: Functional maps
 
 This child of ``Ada.Containers`` defines immutable maps. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
-
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
+
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 .. _`Ada.Containers.Bounded_Holders_(a-coboho.ads)`:
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 13cff21288f..a8939121f79 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -23520,17 +23520,16 @@ specification of this unit is compatible with SPARK 2014.
 @geindex Functional sets
 
 This child of @code{Ada.Containers} defines immutable sets. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
 
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 @node Ada Containers Functional_Maps a-cofuma ads,Ada Containers Bounded_Holders a-coboho ads,Ada Containers Functional_Sets a-cofuse ads,The GNAT Library
 @anchor{gnat_rm/the_gnat_library ada-containers-functional-maps-a-cofuma-ads}@anchor{2f4}@anchor{gnat_rm/the_gnat_library id16}@anchor{2f5}
@@ -23542,17 +23541,16 @@ specification of this unit is compatible with SPARK 2014.
 @geindex Functional maps
 
 This child of @code{Ada.Containers} defines immutable maps. These containers are
-unbounded and may contain indefinite elements. Furthermore, to be usable in
-every context, they are neither controlled nor limited. As they are functional,
-that is, no primitives are provided which would allow modifying an existing
-container, these containers can still be used safely.
-
-Their API features functions creating new containers from existing ones.
-As a consequence, these containers are highly inefficient. They are also
-memory consuming, as the allocated memory is not reclaimed when the container
-is no longer referenced. Thus, they should in general be used in ghost code
-and annotations, so that they can be removed from the final executable. The
-specification of this unit is compatible with SPARK 2014.
+unbounded and may contain indefinite elements. Their API features functions
+creating new containers from existing ones. To remain reasonably efficient,
+their implementation involves sharing between data-structures. As they are
+functional, that is, no primitives are provided which would allow modifying an
+existing container, these containers can still be used safely.
+
+These containers are controlled so that the allocated memory can be reclaimed
+when the container is no longer referenced. Thus, they cannot directly be used
+in contexts where controlled types are not supported.
+The specification of this unit is compatible with SPARK 2014.
 
 @node Ada Containers Bounded_Holders a-coboho ads,Ada Command_Line Environment a-colien ads,Ada Containers Functional_Maps a-cofuma ads,The GNAT Library
 @anchor{gnat_rm/the_gnat_library ada-containers-bounded-holders-a-coboho-ads}@anchor{2f6}@anchor{gnat_rm/the_gnat_library id17}@anchor{2f7}