[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.

1 files changed, 43 insertions, 1 deletions

diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads
index 37dde92..9b95437 100644
--- a/gcc/ada/libgnat/a-cfinve.ads
+++ b/gcc/ada/libgnat/a-cfinve.ads
@@ -311,6 +311,48 @@ is
                 Right    => Model (Container),
                 Position => Index);
 
+   function At_End (E : access constant Vector) return access constant Vector
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function At_End
+     (E : access constant Element_Type) return access constant Element_Type
+   is (E)
+   with Ghost,
+     Annotate => (GNATprove, At_End_Borrow);
+
+   function Constant_Reference
+     (Container : aliased Vector;
+      Index     : Index_Type) return not null access constant Element_Type
+   with
+     Global => null,
+     Pre    => Index in First_Index (Container) .. Last_Index (Container),
+     Post   =>
+         Constant_Reference'Result.all = Element (Model (Container), Index);
+
+   function Reference
+     (Container : not null access Vector;
+      Index     : Index_Type) return not null access Element_Type
+   with
+     Global => null,
+     Pre    =>
+      Index in First_Index (Container.all) .. Last_Index (Container.all),
+     Post   =>
+      Length (Container.all) = Length (At_End (Container).all)
+
+         --  Container will have Result.all at index Index
+
+         and At_End (Reference'Result).all =
+           Element (Model (At_End (Container).all), Index)
+
+         --  All other elements are preserved
+
+         and M.Equal_Except
+               (Left     => Model (Container.all),
+                Right    => Model (At_End (Container).all),
+                Position => Index);
+
    procedure Insert
      (Container : in out Vector;
       Before    : Extended_Index;
@@ -909,7 +951,7 @@ private
    use Holders;
 
    subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
-   type Elements_Array is array (Array_Index range <>) of Holder;
+   type Elements_Array is array (Array_Index range <>) of aliased Holder;
    function "=" (L, R : Elements_Array) return Boolean is abstract;
 
    type Elements_Array_Ptr is access all Elements_Array;