Reference and Constant_Reference functions are added to all formal containers types, returning an access to an element in the container. This takes avantage of pointer support in SPARK.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
patch.diff.gz
Description: application/gzip
