This is the mail archive of the mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

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

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

	* Makefile.rtl, gnat_rm.texi, impunit.adb: Add mention of new library
	* a-cfinve.adb, New unit for formal indefinite
	vectors, suitable for use in client SPARK code, also more
	efficient than the standard vectors.
	* a-coboho.adb, New unit for bounded holders, that
	are used to define formal indefinite vectors in terms of formal
	definite ones.
	* a-cofove.adb, 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

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]