diff options
author | Claire Dross <dross@adacore.com> | 2022-05-24 16:37:18 +0200 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-07-04 07:45:52 +0000 |
commit | 2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c (patch) | |
tree | 7bfa28c0de0803e768ceb56af274cc7c9542b779 | |
parent | 82b63eb0f30333b3c59e8f37c4007cb6fd3fe0f9 (diff) | |
download | gcc-2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c.zip gcc-2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c.tar.gz gcc-2e9b2ab3b5bf6e4a0bdabfeb7358206b18253e3c.tar.bz2 |
[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.
-rw-r--r-- | gcc/ada/doc/gnat_rm/the_gnat_library.rst | 40 | ||||
-rw-r--r-- | 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 72ec5e6..85044f3 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 13cff21..a893912 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} |