From: Claire Dross Date: Tue, 24 May 2022 14:37:18 +0000 (+0200) Subject: [Ada] Update the documentation of functional containers X-Git-Tag: basepoints/gcc-14~5781 X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c;p=thirdparty%2Fgcc.git [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 --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}