[Ada] New and updated library units for efficient and formal vectors

[Arnaud Charlet <charlet at adacore dot com>]

A new unit Ada.Containers.Formal_Indefinite_Vectors is introduced, which
defines vectors possibly holding indefinite elements, such as classwide
objects. The API of this new unit is based on the existing unit
Ada.Containers.Formal_Vectors which has been simplified in favor of
efficiency and provability. Both units can be used from client code in
SPARK and the simplification of the API is conducing to better automatic
proof of client code with GNATprove. Both units define a vector type that
can now be defined as bounded (with a maximal size fixed at declaration)
or not (in which case dynamic allocation is used to grow the vector when
the maximum size has been reached).

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-10-31  Yannick Moy  <moy@adacore.com>

	* Makefile.rtl, gnat_rm.texi, impunit.adb: Add mention of new library
	files.
	* a-cfinve.adb, a-cfinve.ads: New unit for formal indefinite
	vectors, suitable for use in client SPARK code, also more
	efficient than the standard vectors.
	* a-coboho.adb, a-coboho.ads New unit for bounded holders, that
	are used to define formal indefinite vectors in terms of formal
	definite ones.
	* a-cofove.adb, a-cofove.ads: Simplification of the API of formal
	definite vectors, similar to the API of the new indefinite ones. A
	new formal parameter of the generic unit called Bounded allows
	to define growable vectors that use dynamic allocation.

Attachment: difs
Description: Text document