[Ada] Add Reference and Constant_Reference functions to formal containers

gcc/ada/

	* libgnat/a-cfdlli.ads, libgnat/a-cfdlli.adb
	libgnat/a-cfinve.ads, libgnat/a-cfinve.adb,
	libgnat/a-cofove.ads, libgnat/a-cofove.adb,
	libgnat/a-coboho.ads, libgnat/a-coboho.adb (Constant_Reference):
	Get a read-only access to an element of the container.
	(At_End): Ghost functions used to express pledges in the
	postcondition of Reference.
	(Reference): Get a read-write access to an element of the
	container.
	* libgnat/a-cfhama.ads, libgnat/a-cfhama.adb,
	libgnat/a-cforma.ads, libgnat/a-cforma.adb: The full view of the
	Map type is no longer a tagged type, but a wrapper over this
	tagged type. This is to avoid issues with dispatching result in
	At_End functions.
	(Constant_Reference): Get a read-only access to an element of
	the container.
	(At_End): Ghost functions used to express pledges in the
	postcondition of Reference.
	(Reference): Get a read-write access to an element of the
	container.

	* libgnat/a-cfhase.ads, libgnat/a-cfhase.adb,
	libgnat/a-cforse.ads, libgnat/a-cforse.adb: The full view of the
	Map type is no longer a tagged type, but a wrapper over this
	tagged type.
	(Constant_Reference): Get a read-only access to an element of
	the container.
	* libgnat/a-cofuse.ads, libgnat/a-cofuve.ads (Copy_Element):
	Expression function used to cause SPARK to make sure
	Element_Type is copiable.
	* libgnat/a-cofuma.ads (Copy_Key): Expression function used to
	cause SPARK to make sure Key_Type is copiable.
	(Copy_Element): Expression function used to cause SPARK to make
	sure Element_Type is copiable.

0 files changed, 0 insertions, 0 deletions