From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 622A3385E021; Mon, 4 Jul 2022 07:50:12 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 622A3385E021 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-1426] [Ada] Update the documentation of functional containers X-Act-Checkin: gcc X-Git-Author: Claire Dross X-Git-Refname: refs/heads/master X-Git-Oldrev: 82b63eb0f30333b3c59e8f37c4007cb6fd3fe0f9 X-Git-Newrev: 2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c Message-Id: <20220704075012.622A3385E021@sourceware.org> Date: Mon, 4 Jul 2022 07:50:12 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 04 Jul 2022 07:50:12 -0000 https://gcc.gnu.org/g:2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c commit r13-1426-g2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c Author: Claire Dross 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}