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 <m...@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.
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 216956)
+++ gnat_rm.texi (working copy)
@@ -542,6 +542,8 @@
* Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)::
* Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)::
* Ada.Containers.Formal_Vectors (a-cofove.ads)::
+* Ada.Containers.Formal_Indefinite_Vectors (a-cfinve.ads)::
+* Ada.Containers.Bounded_Holders (a-coboho.ads)::
* Ada.Command_Line.Environment (a-colien.ads)::
* Ada.Command_Line.Remove (a-colire.ads)::
* Ada.Command_Line.Response_File (a-clrefi.ads)::
@@ -5165,6 +5167,10 @@
enumeration type not marked with pragma @code{Ordered} will be considered
as unordered, and will generate warnings for inappropriate uses.
+Note that generic types are not considered ordered or unordered (since the
+template can be instantiated for both cases), so we never generate warnings
+for the case of generic enumerated types.
+
For additional information please refer to the description of the
@option{-gnatw.u} switch in the @value{EDITION} User's Guide.
@@ -19022,6 +19028,8 @@
* Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)::
* Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)::
* Ada.Containers.Formal_Vectors (a-cofove.ads)::
+* Ada.Containers.Formal_Indefinite_Vectors (a-cfinve.ads)::
+* Ada.Containers.Bounded_Holders (a-coboho.ads)::
* Ada.Command_Line.Environment (a-colien.ads)::
* Ada.Command_Line.Remove (a-colire.ads)::
* Ada.Command_Line.Response_File (a-clrefi.ads)::
@@ -19325,6 +19333,31 @@
efficient version than the one defined in the standard. In particular it
does not have the complex overhead required to detect cursor tampering.
+@node Ada.Containers.Formal_Indefinite_Vectors (a-cfinve.ads)
+@section @code{Ada.Containers.Formal_Indefinite_Vectors} (@file{a-cfinve.ads})
+@cindex @code{Ada.Containers.Formal_Indefinite_Vectors} (@file{a-cfinve.ads})
+@cindex Formal container for vectors
+
+@noindent
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for vectors of indefinite elements, meant to
+facilitate formal verification of code using such containers. The
+specification of this unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
+
+@node Ada.Containers.Bounded_Holders (a-coboho.ads)
+@section @code{Ada.Containers.Bounded_Holders} (@file{a-coboho.ads})
+@cindex @code{Ada.Containers.Bounded_Holders} (@file{a-coboho.ads})
+@cindex Formal container for vectors
+
+@noindent
+This child of @code{Ada.Containers} defines a modified version of
+Indefinite_Holders that avoids heap allocation.
+
@node Ada.Command_Line.Environment (a-colien.ads)
@section @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
@cindex @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
Index: impunit.adb
===================================================================
--- impunit.adb (revision 216925)
+++ impunit.adb (working copy)
@@ -581,6 +581,8 @@
-- GNAT Defined Additions to Ada 2012 --
----------------------------------------
+ ("a-cfinve", F), -- Ada.Containers.Formal_Indefinite_Vectors
+ ("a-coboho", F), -- Ada.Containers.Bounded_Holders
("a-cofove", F), -- Ada.Containers.Formal_Vectors
("a-cfdlli", F), -- Ada.Containers.Formal_Doubly_Linked_Lists
("a-cforse", F), -- Ada.Containers.Formal_Ordered_Sets
Index: a-coboho.adb
===================================================================
--- a-coboho.adb (revision 0)
+++ a-coboho.adb (revision 0)
@@ -0,0 +1,89 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- A D A . C O N T A I N E R S . B O U N D E D _ H O L D E R S --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2014, Free Software Foundation, Inc. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+with Unchecked_Conversion;
+with Ada.Assertions; use Ada.Assertions;
+
+package body Ada.Containers.Bounded_Holders is
+
+ function Size_In_Storage_Elements (Element : Element_Type) return Natural is
+ (Element'Size / System.Storage_Unit)
+ with Pre =>
+ (Element'Size mod System.Storage_Unit = 0 or else
+ raise Assertion_Error with "Size must be a multiple of Storage_Unit")
+ and then
+ (Element'Size / System.Storage_Unit <= Max_Size_In_Storage_Elements
+ or else raise Assertion_Error with "Size is too big");
+ -- This returns the size of Element in storage units. It raises an
+ -- exception if the size is not a multiple of Storage_Unit, or if the size
+ -- is too big.
+
+ function Cast is new
+ Unchecked_Conversion (System.Address, Element_Access);
+
+ ---------
+ -- "=" --
+ ---------
+
+ function "=" (Left, Right : Holder) return Boolean is
+ begin
+ return Get (Left) = Get (Right);
+ end "=";
+
+ -------------
+ -- Element --
+ -------------
+
+ function Get (Container : Holder) return Element_Type is
+ begin
+ return Cast (Container'Address).all;
+ end Get;
+
+ ---------------------
+ -- Replace_Element --
+ ---------------------
+
+ procedure Set (Container : in out Holder; New_Item : Element_Type) is
+ Storage : Storage_Array
+ (1 .. Size_In_Storage_Elements (New_Item)) with
+ Address => New_Item'Address;
+ begin
+ Container.Data (Storage'Range) := Storage;
+ end Set;
+
+ ---------------
+ -- To_Holder --
+ ---------------
+
+ function To_Holder (New_Item : Element_Type) return Holder is
+ begin
+ return Result : Holder do
+ Set (Result, New_Item);
+ end return;
+ end To_Holder;
+
+end Ada.Containers.Bounded_Holders;
Index: a-coboho.ads
===================================================================
--- a-coboho.ads (revision 0)
+++ a-coboho.ads (revision 0)
@@ -0,0 +1,102 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- A D A . C O N T A I N E R S . B O U N D E D _ H O L D E R S --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2014, Free Software Foundation, Inc. --
+-- --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contents of the part following the private keyword. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+private with System;
+
+generic
+ type Element_Type (<>) is private;
+ Max_Size_In_Storage_Elements : Natural :=
+ Element_Type'Max_Size_In_Storage_Elements;
+ with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Bounded_Holders is
+ -- This package is patterned after Ada.Containers.Indefinite_Holders. It is
+ -- used to treat indefinite subtypes as definite, but without using heap
+ -- allocation. For example, you might like to say:
+ --
+ -- type A is array (...) of T'Class; -- illegal
+ --
+ -- Instead, you can instantiate this package with Element_Type => T'Class,
+ -- and say:
+ --
+ -- type A is array (...) of Holder;
+ --
+ -- Each object of type Holder is allocated Max_Size_In_Storage_Elements
+ -- bytes. If you try to create a holder from an object of type Element_Type
+ -- that is too big, an exception is raised. This applies to To_Holder and
+ -- Replace_Element. If you pass an Element_Type object that is smaller than
+ -- Max_Size_In_Storage_Elements, it works fine, but some space is wasted.
+ --
+ -- Element_Type must not be an unconstrained array type. It can be a
+ -- class-wide type or a type with non-defaulted discriminants.
+ --
+ -- The 'Size of each Element_Type object must be a multiple of
+ -- System.Storage_Unit; e.g. creating Holders from 5-bit objects won't
+ -- work.
+
+ type Holder is private;
+
+ function "=" (Left, Right : Holder) return Boolean;
+
+ function To_Holder (New_Item : Element_Type) return Holder;
+ function "+" (New_Item : Element_Type) return Holder renames To_Holder;
+
+ function Get (Container : Holder) return Element_Type;
+
+ procedure Set (Container : in out Holder; New_Item : Element_Type);
+
+private
+
+ -- The implementation uses low-level tricks (Address clauses and unchecked
+ -- conversions of access types) to treat the elements as storage arrays.
+
+ pragma Assert (Element_Type'Alignment <= Standard'Maximum_Alignment);
+ -- This prevents elements with a user-specified Alignment that is too big
+
+ type Storage_Element is mod System.Storage_Unit;
+ type Storage_Array is array (Positive range <>) of Storage_Element;
+ type Holder is record
+ Data : Storage_Array (1 .. Max_Size_In_Storage_Elements);
+ end record
+ with Alignment => Standard'Maximum_Alignment;
+ -- We would like to say "Alignment => Element_Type'Alignment", but that
+ -- is illegal because it's not static, so we use the maximum possible
+ -- (default) alignment instead.
+
+ type Element_Access is access all Element_Type;
+ pragma Assert (Element_Access'Size = Standard'Address_Size,
+ "cannot instantiate with an array type");
+ -- If Element_Access is a fat pointer, Element_Type must be an
+ -- unconstrained array, which is not allowed. Arrays won't work, because
+ -- the 'Address of an array points to the first element, thus losing the
+ -- bounds.
+
+end Ada.Containers.Bounded_Holders;
Index: a-cfinve.adb
===================================================================
--- a-cfinve.adb (revision 0)
+++ a-cfinve.adb (revision 0)
@@ -0,0 +1,295 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- A D A . C O N T A I N E R S
+-- . F O R M A L _ I N D E F I N I T E _ V E C T O R S --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2014, Free Software Foundation, Inc. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+package body Ada.Containers.Formal_Indefinite_Vectors is
+
+ function H (New_Item : Element_Type) return Holder renames To_Holder;
+ function E (Container : Holder) return Element_Type renames Get;
+
+ ---------
+ -- "=" --
+ ---------
+
+ function "=" (Left, Right : Vector) return Boolean is
+ (Left.V = Right.V);
+
+ ------------
+ -- Append --
+ ------------
+
+ procedure Append (Container : in out Vector; New_Item : Vector) is
+ begin
+ Append (Container.V, New_Item.V);
+ end Append;
+
+ procedure Append
+ (Container : in out Vector;
+ New_Item : Element_Type)
+ is
+ begin
+ Append (Container.V, H (New_Item));
+ end Append;
+
+ ------------
+ -- Assign --
+ ------------
+
+ procedure Assign (Target : in out Vector; Source : Vector) is
+ begin
+ Assign (Target.V, Source.V);
+ end Assign;
+
+ --------------
+ -- Capacity --
+ --------------
+
+ function Capacity (Container : Vector) return Capacity_Range is
+ (Capacity (Container.V));
+
+ -----------
+ -- Clear --
+ -----------
+
+ procedure Clear (Container : in out Vector) is
+ begin
+ Clear (Container.V);
+ end Clear;
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (Container : Vector;
+ Item : Element_Type) return Boolean is
+ (Contains (Container.V, H (Item)));
+
+ ----------
+ -- Copy --
+ ----------
+
+ function Copy
+ (Source : Vector;
+ Capacity : Capacity_Range := 0) return Vector is
+ (Capacity, V => Copy (Source.V, Capacity));
+
+ ---------------------
+ -- Current_To_Last --
+ ---------------------
+
+ function Current_To_Last
+ (Container : Vector;
+ Current : Index_Type) return Vector is
+ begin
+ return (Length (Container), Current_To_Last (Container.V, Current));
+ end Current_To_Last;
+
+ -----------------
+ -- Delete_Last --
+ -----------------
+
+ procedure Delete_Last
+ (Container : in out Vector)
+ is
+ begin
+ Delete_Last (Container.V);
+ end Delete_Last;
+
+ -------------
+ -- Element --
+ -------------
+
+ function Element
+ (Container : Vector;
+ Index : Index_Type) return Element_Type is
+ (E (Element (Container.V, Index)));
+
+ ----------------
+ -- Find_Index --
+ ----------------
+
+ function Find_Index
+ (Container : Vector;
+ Item : Element_Type;
+ Index : Index_Type := Index_Type'First) return Extended_Index is
+ (Find_Index (Container.V, H (Item), Index));
+
+ -------------------
+ -- First_Element --
+ -------------------
+
+ function First_Element (Container : Vector) return Element_Type is
+ (E (First_Element (Container.V)));
+
+ -----------------
+ -- First_Index --
+ -----------------
+
+ function First_Index (Container : Vector) return Index_Type is
+ (First_Index (Container.V));
+
+ -----------------------
+ -- First_To_Previous --
+ -----------------------
+
+ function First_To_Previous
+ (Container : Vector;
+ Current : Index_Type) return Vector is
+ begin
+ return (Length (Container), First_To_Previous (Container.V, Current));
+ end First_To_Previous;
+
+ ---------------------
+ -- Generic_Sorting --
+ ---------------------
+
+ package body Generic_Sorting is
+
+ function "<" (X, Y : Holder) return Boolean is (E (X) < E (Y));
+ package Def_Sorting is new Def.Generic_Sorting ("<");
+ use Def_Sorting;
+
+ ---------------
+ -- Is_Sorted --
+ ---------------
+
+ function Is_Sorted (Container : Vector) return Boolean is
+ (Is_Sorted (Container.V));
+
+ ----------
+ -- Sort --
+ ----------
+
+ procedure Sort (Container : in out Vector) is
+ begin
+ Sort (Container.V);
+ end Sort;
+
+ end Generic_Sorting;
+
+ -----------------
+ -- Has_Element --
+ -----------------
+
+ function Has_Element
+ (Container : Vector; Position : Extended_Index) return Boolean is
+ (Has_Element (Container.V, Position));
+
+ --------------
+ -- Is_Empty --
+ --------------
+
+ function Is_Empty (Container : Vector) return Boolean is
+ (Is_Empty (Container.V));
+
+ ------------------
+ -- Last_Element --
+ ------------------
+
+ function Last_Element (Container : Vector) return Element_Type is
+ (E (Last_Element (Container.V)));
+
+ ----------------
+ -- Last_Index --
+ ----------------
+
+ function Last_Index (Container : Vector) return Extended_Index is
+ (Last_Index (Container.V));
+
+ ------------
+ -- Length --
+ ------------
+
+ function Length (Container : Vector) return Capacity_Range is
+ (Length (Container.V));
+
+ ---------------------
+ -- Replace_Element --
+ ---------------------
+
+ procedure Replace_Element
+ (Container : in out Vector;
+ Index : Index_Type;
+ New_Item : Element_Type)
+ is
+ begin
+ Replace_Element (Container.V, Index, H (New_Item));
+ end Replace_Element;
+
+ ----------------------
+ -- Reserve_Capacity --
+ ----------------------
+
+ procedure Reserve_Capacity
+ (Container : in out Vector;
+ Capacity : Capacity_Range)
+ is
+ begin
+ Reserve_Capacity (Container.V, Capacity);
+ end Reserve_Capacity;
+
+ ----------------------
+ -- Reverse_Elements --
+ ----------------------
+
+ procedure Reverse_Elements (Container : in out Vector) is
+ begin
+ Reverse_Elements (Container.V);
+ end Reverse_Elements;
+
+ ------------------------
+ -- Reverse_Find_Index --
+ ------------------------
+
+ function Reverse_Find_Index
+ (Container : Vector;
+ Item : Element_Type;
+ Index : Index_Type := Index_Type'Last) return Extended_Index is
+ (Reverse_Find_Index (Container.V, H (Item), Index));
+
+ ----------
+ -- Swap --
+ ----------
+
+ procedure Swap (Container : in out Vector; I, J : Index_Type) is
+ begin
+ Swap (Container.V, I, J);
+ end Swap;
+
+ ---------------
+ -- To_Vector --
+ ---------------
+
+ function To_Vector
+ (New_Item : Element_Type;
+ Length : Capacity_Range) return Vector is
+ begin
+ return (Length, To_Vector (H (New_Item), Length));
+ end To_Vector;
+
+end Ada.Containers.Formal_Indefinite_Vectors;
Index: a-cfinve.ads
===================================================================
--- a-cfinve.ads (revision 0)
+++ a-cfinve.ads (revision 0)
@@ -0,0 +1,249 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- A D A . C O N T A I N E R S
+-- . F O R M A L _ I N D E F I N I T E _ V E C T O R S --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2014, Free Software Foundation, Inc. --
+-- --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contents of the part following the private keyword. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+-- Similar to Ada.Containers.Formal_Vectors. The main difference is that
+-- Element_Type may be indefinite (but not an unconstrained array). In
+-- addition, this is simplified by removing less-used functionality.
+
+with Ada.Containers.Bounded_Holders;
+with Ada.Containers.Formal_Vectors;
+
+generic
+ type Index_Type is range <>;
+ type Element_Type (<>) is private;
+ Max_Size_In_Storage_Elements : Natural :=
+ Element_Type'Max_Size_In_Storage_Elements;
+ -- This has the same meaning as in Ada.Containers.Bounded_Holders, with the
+ -- same restrictions.
+
+ with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+ Bounded : Boolean := True;
+ -- If True, the containers are bounded; the initial capacity is the maximum
+ -- size, and heap allocation will be avoided. If False, the containers can
+ -- grow via heap allocation.
+
+package Ada.Containers.Formal_Indefinite_Vectors is
+ pragma Annotate (GNATprove, External_Axiomatization);
+
+ subtype Extended_Index is Index_Type'Base
+ range Index_Type'First - 1 ..
+ Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
+
+ No_Index : constant Extended_Index := Extended_Index'First;
+
+ subtype Capacity_Range is
+ Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
+
+ type Vector (Capacity : Capacity_Range) is limited private with
+ Default_Initial_Condition;
+
+ function Empty_Vector return Vector;
+
+ function "=" (Left, Right : Vector) return Boolean with
+ Global => null;
+
+ function To_Vector
+ (New_Item : Element_Type;
+ Length : Capacity_Range) return Vector
+ with
+ Global => null;
+
+ function Capacity (Container : Vector) return Capacity_Range with
+ Global => null;
+
+ procedure Reserve_Capacity
+ (Container : in out Vector;
+ Capacity : Capacity_Range)
+ with
+ Global => null,
+ Pre => (if Bounded then Capacity <= Container.Capacity);
+
+ function Length (Container : Vector) return Capacity_Range with
+ Global => null;
+
+ function Is_Empty (Container : Vector) return Boolean with
+ Global => null;
+
+ procedure Clear (Container : in out Vector) with
+ Global => null;
+ -- Note that this reclaims storage in the unbounded case. You need to call
+ -- this before a container goes out of scope in order to avoid storage
+ -- leaks.
+
+ procedure Assign (Target : in out Vector; Source : Vector) with
+ Global => null,
+ Pre => (if Bounded then Length (Source) <= Target.Capacity);
+
+ function Copy
+ (Source : Vector;
+ Capacity : Capacity_Range := 0) return Vector
+ with
+ Global => null,
+ Pre => (if Bounded then Length (Source) <= Capacity);
+
+ function Element
+ (Container : Vector;
+ Index : Index_Type) return Element_Type
+ with
+ Global => null,
+ Pre => Index in First_Index (Container) .. Last_Index (Container);
+
+ procedure Replace_Element
+ (Container : in out Vector;
+ Index : Index_Type;
+ New_Item : Element_Type)
+ with
+ Global => null,
+ Pre => Index in First_Index (Container) .. Last_Index (Container);
+
+ procedure Append
+ (Container : in out Vector;
+ New_Item : Vector)
+ with
+ Global => null,
+ Pre => (if Bounded then
+ Length (Container) + Length (New_Item) <= Container.Capacity);
+
+ procedure Append
+ (Container : in out Vector;
+ New_Item : Element_Type)
+ with
+ Global => null,
+ Pre => (if Bounded then
+ Length (Container) < Container.Capacity);
+
+ procedure Delete_Last
+ (Container : in out Vector)
+ with
+ Global => null;
+
+ procedure Reverse_Elements (Container : in out Vector) with
+ Global => null;
+
+ procedure Swap (Container : in out Vector; I, J : Index_Type) with
+ Global => null,
+ Pre => I in First_Index (Container) .. Last_Index (Container)
+ and then J in First_Index (Container) .. Last_Index (Container);
+
+ function First_Index (Container : Vector) return Index_Type with
+ Global => null;
+
+ function First_Element (Container : Vector) return Element_Type with
+ Global => null,
+ Pre => not Is_Empty (Container);
+
+ function Last_Index (Container : Vector) return Extended_Index with
+ Global => null;
+
+ function Last_Element (Container : Vector) return Element_Type with
+ Global => null,
+ Pre => not Is_Empty (Container);
+
+ function Find_Index
+ (Container : Vector;
+ Item : Element_Type;
+ Index : Index_Type := Index_Type'First) return Extended_Index
+ with
+ Global => null;
+
+ function Reverse_Find_Index
+ (Container : Vector;
+ Item : Element_Type;
+ Index : Index_Type := Index_Type'Last) return Extended_Index
+ with
+ Global => null;
+
+ function Contains
+ (Container : Vector;
+ Item : Element_Type) return Boolean
+ with
+ Global => null;
+
+ function Has_Element
+ (Container : Vector; Position : Extended_Index) return Boolean with
+ Global => null;
+
+ generic
+ with function "<" (Left, Right : Element_Type) return Boolean is <>;
+ package Generic_Sorting is
+
+ function Is_Sorted (Container : Vector) return Boolean with
+ Global => null;
+
+ procedure Sort (Container : in out Vector) with
+ Global => null;
+
+ end Generic_Sorting;
+
+ function First_To_Previous
+ (Container : Vector;
+ Current : Index_Type) return Vector
+ with
+ Global => null;
+ function Current_To_Last
+ (Container : Vector;
+ Current : Index_Type) return Vector
+ with
+ Global => null;
+
+private
+
+ pragma Inline (First_Index);
+ pragma Inline (Last_Index);
+ pragma Inline (Element);
+ pragma Inline (First_Element);
+ pragma Inline (Last_Element);
+ pragma Inline (Replace_Element);
+ pragma Inline (Contains);
+
+ -- The implementation method is to instantiate Bounded_Holders to get a
+ -- definite type for Element_Type, and then use that Holder type to
+ -- instantiate Formal_Vectors. All the operations are just wrappers.
+
+ package Holders is new Bounded_Holders
+ (Element_Type, Max_Size_In_Storage_Elements, "=");
+ use Holders;
+
+ package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
+ use Def;
+
+ -- ????Assert that Def subtypes have the same range.
+
+ type Vector (Capacity : Capacity_Range) is limited record
+ V : Def.Vector (Capacity);
+ end record;
+
+ function Empty_Vector return Vector is
+ ((Capacity => 0, V => Def.Empty_Vector));
+
+end Ada.Containers.Formal_Indefinite_Vectors;
Index: Makefile.rtl
===================================================================
--- Makefile.rtl (revision 216925)
+++ Makefile.rtl (working copy)
@@ -110,6 +110,7 @@
a-cfdlli$(objext) \
a-cfhama$(objext) \
a-cfhase$(objext) \
+ a-cfinve$(objext) \
a-cforma$(objext) \
a-cforse$(objext) \
a-cgaaso$(objext) \
@@ -134,6 +135,7 @@
a-ciormu$(objext) \
a-ciorse$(objext) \
a-clrefi$(objext) \
+ a-coboho$(objext) \
a-cobove$(objext) \
a-cofove$(objext) \
a-cogeso$(objext) \
Index: a-cofove.adb
===================================================================
--- a-cofove.adb (revision 216925)
+++ a-cofove.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -26,156 +26,33 @@
------------------------------------------------------------------------------
with Ada.Containers.Generic_Array_Sort;
+with Unchecked_Deallocation;
with System; use type System.Address;
package body Ada.Containers.Formal_Vectors is
+ Growth_Factor : constant := 2;
+ -- When growing a container, multiply current capacity by this. Doubling
+ -- leads to amortized linear-time copying.
+
type Int is range System.Min_Int .. System.Max_Int;
type UInt is mod System.Max_Binary_Modulus;
- function Get_Element
- (Container : Vector;
- Position : Count_Type) return Element_Type;
+ type Elements_Array_Ptr_Const is access constant Elements_Array;
- procedure Insert_Space
- (Container : in out Vector;
- Before : Extended_Index;
- Count : Count_Type := 1);
+ procedure Free is
+ new Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
- ---------
- -- "&" --
- ---------
+ function Elems (Container : in out Vector) return Elements_Array_Ptr;
+ function Elemsc
+ (Container : Vector) return Elements_Array_Ptr_Const;
+ -- Returns a pointer to the Elements array currently in use -- either
+ -- Container.Elements_Ptr or a pointer to Container.Elements.
- function "&" (Left, Right : Vector) return Vector is
- LN : constant Count_Type := Length (Left);
- RN : constant Count_Type := Length (Right);
+ function Get_Element
+ (Container : Vector;
+ Position : Capacity_Range) return Element_Type;
- begin
- if LN = 0 then
- if RN = 0 then
- return Empty_Vector;
- end if;
-
- declare
- E : constant Elements_Array (1 .. Length (Right)) :=
- Right.Elements (1 .. RN);
- begin
- return (Length (Right), E, Last => Right.Last, others => <>);
- end;
- end if;
-
- if RN = 0 then
- declare
- E : constant Elements_Array (1 .. Length (Left)) :=
- Left.Elements (1 .. LN);
- begin
- return (Length (Left), E, Last => Left.Last, others => <>);
- end;
- end if;
-
- declare
- N : constant Int'Base := Int (LN) + Int (RN);
- Last_As_Int : Int'Base;
-
- begin
- if Int (No_Index) > Int'Last - N then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- Last_As_Int := Int (No_Index) + N;
-
- if Last_As_Int > Int (Index_Type'Last) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- -- TODO: should check whether length > max capacity (cnt_t'last) ???
-
- declare
- Last : constant Index_Type := Index_Type (Last_As_Int);
-
- LE : constant Elements_Array (1 .. LN) := Left.Elements (1 .. LN);
- RE : Elements_Array renames Right.Elements (1 .. RN);
-
- Capacity : constant Count_Type := Length (Left) + Length (Right);
-
- begin
- return (Capacity, LE & RE, Last => Last, others => <>);
- end;
- end;
- end "&";
-
- function "&" (Left : Vector; Right : Element_Type) return Vector is
- LN : constant Count_Type := Length (Left);
- Last_As_Int : Int'Base;
-
- begin
- if LN = 0 then
- return (1, (1 .. 1 => Right), Index_Type'First, others => <>);
- end if;
-
- if Int (Index_Type'First) > Int'Last - Int (LN) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- Last_As_Int := Int (Index_Type'First) + Int (LN);
-
- if Last_As_Int > Int (Index_Type'Last) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- declare
- Last : constant Index_Type := Index_Type (Last_As_Int);
- LE : constant Elements_Array (1 .. LN) := Left.Elements (1 .. LN);
-
- Capacity : constant Count_Type := Length (Left) + 1;
-
- begin
- return (Capacity, LE & Right, Last => Last, others => <>);
- end;
- end "&";
-
- function "&" (Left : Element_Type; Right : Vector) return Vector is
- RN : constant Count_Type := Length (Right);
- Last_As_Int : Int'Base;
-
- begin
- if RN = 0 then
- return (1, (1 .. 1 => Left),
- Index_Type'First, others => <>);
- end if;
-
- if Int (Index_Type'First) > Int'Last - Int (RN) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- Last_As_Int := Int (Index_Type'First) + Int (RN);
-
- if Last_As_Int > Int (Index_Type'Last) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- declare
- Last : constant Index_Type := Index_Type (Last_As_Int);
- RE : Elements_Array renames Right.Elements (1 .. RN);
- Capacity : constant Count_Type := 1 + Length (Right);
- begin
- return (Capacity, Left & RE, Last => Last, others => <>);
- end;
- end "&";
-
- function "&" (Left, Right : Element_Type) return Vector is
- begin
- if Index_Type'First >= Index_Type'Last then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- declare
- Last : constant Index_Type := Index_Type'First + 1;
- begin
- return (2, (Left, Right), Last => Last, others => <>);
- end;
- end "&";
-
---------
-- "=" --
---------
@@ -190,7 +67,7 @@
return False;
end if;
- for J in Count_Type range 1 .. Length (Left) loop
+ for J in 1 .. Length (Left) loop
if Get_Element (Left, J) /= Get_Element (Right, J) then
return False;
end if;
@@ -205,25 +82,24 @@
procedure Append (Container : in out Vector; New_Item : Vector) is
begin
- if Is_Empty (New_Item) then
- return;
- end if;
-
- if Container.Last = Index_Type'Last then
- raise Constraint_Error with "vector is already at its maximum length";
- end if;
-
- Insert (Container, Container.Last + 1, New_Item);
+ for X in First_Index (New_Item) .. Last_Index (New_Item) loop
+ Append (Container, Element (New_Item, X));
+ end loop;
end Append;
procedure Append
(Container : in out Vector;
- New_Item : Element_Type;
- Count : Count_Type := 1)
+ New_Item : Element_Type)
is
+ New_Length : constant UInt := UInt (Length (Container) + 1);
begin
- if Count = 0 then
- return;
+ if not Bounded and then
+ Capacity (Container) < Capacity_Range (New_Length)
+ then
+ Reserve_Capacity
+ (Container,
+ Capacity_Range'Max (Capacity (Container) * Growth_Factor,
+ Capacity_Range (New_Length)));
end if;
if Container.Last = Index_Type'Last then
@@ -232,7 +108,8 @@
-- TODO: should check whether length > max capacity (cnt_t'last) ???
- Insert (Container, Container.Last + 1, New_Item, Count);
+ Container.Last := Container.Last + 1;
+ Elems (Container) (Length (Container)) := New_Item;
end Append;
------------
@@ -240,30 +117,28 @@
------------
procedure Assign (Target : in out Vector; Source : Vector) is
- LS : constant Count_Type := Length (Source);
+ LS : constant Capacity_Range := Length (Source);
begin
if Target'Address = Source'Address then
return;
end if;
- if Target.Capacity < LS then
+ if Bounded and then Target.Capacity < LS then
raise Constraint_Error;
end if;
Clear (Target);
-
- Target.Elements (1 .. LS) := Source.Elements (1 .. LS);
- Target.Last := Source.Last;
+ Append (Target, Source);
end Assign;
--------------
-- Capacity --
--------------
- function Capacity (Container : Vector) return Count_Type is
+ function Capacity (Container : Vector) return Capacity_Range is
begin
- return Container.Elements'Length;
+ return Elemsc (Container)'Length;
end Capacity;
-----------
@@ -273,6 +148,8 @@
procedure Clear (Container : in out Vector) is
begin
Container.Last := No_Index;
+ Free (Container.Elements_Ptr);
+ -- It's OK if Container.Elements_Ptr is null
end Clear;
--------------
@@ -293,22 +170,22 @@
function Copy
(Source : Vector;
- Capacity : Count_Type := 0) return Vector
+ Capacity : Capacity_Range := 0) return Vector
is
- LS : constant Count_Type := Length (Source);
- C : Count_Type;
+ LS : constant Capacity_Range := Length (Source);
+ C : Capacity_Range;
begin
if Capacity = 0 then
C := LS;
- elsif Capacity >= LS and then Capacity in Capacity_Range then
+ elsif Capacity >= LS then
C := Capacity;
else
raise Capacity_Error;
end if;
return Target : Vector (C) do
- Target.Elements (1 .. LS) := Source.Elements (1 .. LS);
+ Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS);
Target.Last := Source.Last;
end return;
end Copy;
@@ -319,146 +196,29 @@
function Current_To_Last
(Container : Vector;
- Current : Cursor) return Vector
+ Current : Index_Type) return Vector
is
- C : Vector (Container.Capacity) := Copy (Container, Container.Capacity);
-
begin
- if Current = No_Element then
- Clear (C);
- return C;
-
- elsif not Has_Element (Container, Current) then
- raise Constraint_Error;
-
- else
- while C.Last /= Container.Last - Current.Index + 1 loop
- Delete_First (C);
+ return Result : Vector
+ (Count_Type (Container.Last - Current + 1))
+ do
+ for X in Current .. Container.Last loop
+ Append (Result, Element (Container, X));
end loop;
-
- return C;
- end if;
+ end return;
end Current_To_Last;
- ------------
- -- Delete --
- ------------
-
- procedure Delete
- (Container : in out Vector;
- Index : Extended_Index;
- Count : Count_Type := 1)
- is
- begin
- if Index < Index_Type'First then
- raise Constraint_Error with "Index is out of range (too small)";
- end if;
-
- if Index > Container.Last then
- if Index > Container.Last + 1 then
- raise Constraint_Error with "Index is out of range (too large)";
- end if;
-
- return;
- end if;
-
- if Count = 0 then
- return;
- end if;
-
- declare
- I_As_Int : constant Int := Int (Index);
- Old_Last_As_Int : constant Int := Index_Type'Pos (Container.Last);
-
- Count1 : constant Int'Base := Count_Type'Pos (Count);
- Count2 : constant Int'Base := Old_Last_As_Int - I_As_Int + 1;
- N : constant Int'Base := Int'Min (Count1, Count2);
-
- J_As_Int : constant Int'Base := I_As_Int + N;
-
- begin
- if J_As_Int > Old_Last_As_Int then
- Container.Last := Index - 1;
-
- else
- declare
- EA : Elements_Array renames Container.Elements;
-
- II : constant Int'Base := I_As_Int - Int (No_Index);
- I : constant Count_Type := Count_Type (II);
-
- JJ : constant Int'Base := J_As_Int - Int (No_Index);
- J : constant Count_Type := Count_Type (JJ);
-
- New_Last_As_Int : constant Int'Base := Old_Last_As_Int - N;
- New_Last : constant Index_Type :=
- Index_Type (New_Last_As_Int);
-
- KK : constant Int := New_Last_As_Int - Int (No_Index);
- K : constant Count_Type := Count_Type (KK);
-
- begin
- EA (I .. K) := EA (J .. Length (Container));
- Container.Last := New_Last;
- end;
- end if;
- end;
- end Delete;
-
- procedure Delete
- (Container : in out Vector;
- Position : in out Cursor;
- Count : Count_Type := 1)
- is
- begin
- if not Position.Valid then
- raise Constraint_Error with "Position cursor has no element";
- end if;
-
- if Position.Index > Container.Last then
- raise Program_Error with "Position index is out of range";
- end if;
-
- Delete (Container, Position.Index, Count);
- Position := No_Element;
- end Delete;
-
- ------------------
- -- Delete_First --
- ------------------
-
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type := 1)
- is
- begin
- if Count = 0 then
- return;
- end if;
-
- if Count >= Length (Container) then
- Clear (Container);
- return;
- end if;
-
- Delete (Container, Index_Type'First, Count);
- end Delete_First;
-
-----------------
-- Delete_Last --
-----------------
procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type := 1)
+ (Container : in out Vector)
is
+ Count : constant Capacity_Range := 1;
Index : Int'Base;
begin
- if Count = 0 then
- return;
- end if;
-
Index := Int'Base (Container.Last) - Int'Base (Count);
if Index < Index_Type'Pos (Index_Type'First) then
@@ -483,67 +243,31 @@
declare
II : constant Int'Base := Int (Index) - Int (No_Index);
- I : constant Count_Type := Count_Type (II);
+ I : constant Capacity_Range := Capacity_Range (II);
begin
return Get_Element (Container, I);
end;
end Element;
- function Element
- (Container : Vector;
- Position : Cursor) return Element_Type
- is
- Lst : constant Index_Type := Last_Index (Container);
+ --------------
+ -- Elements --
+ --------------
+ function Elems (Container : in out Vector) return Elements_Array_Ptr is
begin
- if not Position.Valid then
- raise Constraint_Error with "Position cursor has no element";
- end if;
+ return (if Container.Elements_Ptr = null
+ then Container.Elements'Unrestricted_Access
+ else Container.Elements_Ptr);
+ end Elems;
- if Position.Index > Lst then
- raise Constraint_Error with "Position cursor is out of range";
- end if;
-
- declare
- II : constant Int'Base := Int (Position.Index) - Int (No_Index);
- I : constant Count_Type := Count_Type (II);
- begin
- return Get_Element (Container, I);
- end;
- end Element;
-
- ----------
- -- Find --
- ----------
-
- function Find
- (Container : Vector;
- Item : Element_Type;
- Position : Cursor := No_Element) return Cursor
- is
- K : Count_Type;
- Last : constant Index_Type := Last_Index (Container);
-
+ function Elemsc
+ (Container : Vector) return Elements_Array_Ptr_Const is
begin
- if Position.Valid then
- if Position.Index > Last_Index (Container) then
- raise Program_Error with "Position index is out of range";
- end if;
- end if;
+ return (if Container.Elements_Ptr = null
+ then Container.Elements'Unrestricted_Access
+ else Elements_Array_Ptr_Const (Container.Elements_Ptr));
+ end Elemsc;
- K := Count_Type (Int (Position.Index) - Int (No_Index));
-
- for J in Position.Index .. Last loop
- if Get_Element (Container, K) = Item then
- return Cursor'(Index => J, others => <>);
- end if;
-
- K := K + 1;
- end loop;
-
- return No_Element;
- end Find;
-
----------------
-- Find_Index --
----------------
@@ -553,11 +277,11 @@
Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index
is
- K : Count_Type;
+ K : Capacity_Range;
Last : constant Index_Type := Last_Index (Container);
begin
- K := Count_Type (Int (Index) - Int (No_Index));
+ K := Capacity_Range (Int (Index) - Int (No_Index));
for Indx in Index .. Last loop
if Get_Element (Container, K) = Item then
return Indx;
@@ -569,19 +293,6 @@
return No_Index;
end Find_Index;
- -----------
- -- First --
- -----------
-
- function First (Container : Vector) return Cursor is
- begin
- if Is_Empty (Container) then
- return No_Element;
- end if;
-
- return (True, Index_Type'First);
- end First;
-
-------------------
-- First_Element --
-------------------
@@ -611,24 +322,16 @@
function First_To_Previous
(Container : Vector;
- Current : Cursor) return Vector
+ Current : Index_Type) return Vector
is
- C : Vector (Container.Capacity) := Copy (Container, Container.Capacity);
-
begin
- if Current = No_Element then
- return C;
-
- elsif not Has_Element (Container, Current) then
- raise Constraint_Error;
-
- else
- while C.Last /= Current.Index - 1 loop
- Delete_Last (C);
+ return Result : Vector
+ (Count_Type (Current - First_Index (Container)))
+ do
+ for X in First_Index (Container) .. Current - 1 loop
+ Append (Result, Element (Container, X));
end loop;
-
- return C;
- end if;
+ end return;
end First_To_Previous;
---------------------
@@ -650,9 +353,9 @@
end if;
declare
- L : constant Count_Type := Length (Container);
+ L : constant Capacity_Range := Length (Container);
begin
- for J in Count_Type range 1 .. L - 1 loop
+ for J in 1 .. L - 1 loop
if Get_Element (Container, J + 1) <
Get_Element (Container, J)
then
@@ -664,66 +367,6 @@
return True;
end Is_Sorted;
- -----------
- -- Merge --
- -----------
-
- procedure Merge (Target, Source : in out Vector) is
- begin
- declare
- TA : Elements_Array renames Target.Elements;
- SA : Elements_Array renames Source.Elements;
-
- I, J : Count_Type;
-
- begin
- -- ???
- -- if Target.Last < Index_Type'First then
- -- Move (Target => Target, Source => Source);
- -- return;
- -- end if;
-
- if Target'Address = Source'Address then
- return;
- end if;
-
- if Source.Last < Index_Type'First then
- return;
- end if;
-
- -- I think we're missing this check in a-convec.adb... ???
-
- I := Length (Target);
- Set_Length (Target, I + Length (Source));
-
- J := Length (Target);
- while not Is_Empty (Source) loop
- pragma Assert (Length (Source) <= 1
- or else not (SA (Length (Source)) <
- SA (Length (Source) - 1)));
-
- if I = 0 then
- TA (1 .. J) := SA (1 .. Length (Source));
- Source.Last := No_Index;
- return;
- end if;
-
- pragma Assert (I <= 1 or else not (TA (I) < TA (I - 1)));
-
- if SA (Length (Source)) < TA (I) then
- TA (J) := TA (I);
- I := I - 1;
-
- else
- TA (J) := SA (Length (Source));
- Source.Last := Source.Last - 1;
- end if;
-
- J := J - 1;
- end loop;
- end;
- end Merge;
-
----------
-- Sort --
----------
@@ -732,17 +375,18 @@
is
procedure Sort is
new Generic_Array_Sort
- (Index_Type => Count_Type,
+ (Index_Type => Capacity_Range,
Element_Type => Element_Type,
Array_Type => Elements_Array,
"<" => "<");
+ Len : constant Capacity_Range := Length (Container);
begin
if Container.Last <= Index_Type'First then
return;
end if;
- Sort (Container.Elements (1 .. Length (Container)));
+ Sort (Elems (Container) (1 .. Len));
end Sort;
end Generic_Sorting;
@@ -753,10 +397,10 @@
function Get_Element
(Container : Vector;
- Position : Count_Type) return Element_Type
+ Position : Capacity_Range) return Element_Type
is
begin
- return Container.Elements (Position);
+ return Elemsc (Container) (Position);
end Get_Element;
-----------------
@@ -764,402 +408,11 @@
-----------------
function Has_Element
- (Container : Vector;
- Position : Cursor) return Boolean
- is
+ (Container : Vector; Position : Extended_Index) return Boolean is
begin
- if not Position.Valid then
- return False;
- else
- return Position.Index <= Last_Index (Container);
- end if;
+ return Position in First_Index (Container) .. Last_Index (Container);
end Has_Element;
- ------------
- -- Insert --
- ------------
-
- procedure Insert
- (Container : in out Vector;
- Before : Extended_Index;
- New_Item : Element_Type;
- Count : Count_Type := 1)
- is
- N : constant Int := Count_Type'Pos (Count);
-
- First : constant Int := Int (Index_Type'First);
- New_Last_As_Int : Int'Base;
- New_Last : Index_Type;
- New_Length : UInt;
- Max_Length : constant UInt := UInt (Container.Capacity);
-
- begin
- if Before < Index_Type'First then
- raise Constraint_Error with
- "Before index is out of range (too small)";
- end if;
-
- if Before > Container.Last
- and then Before > Container.Last + 1
- then
- raise Constraint_Error with
- "Before index is out of range (too large)";
- end if;
-
- if Count = 0 then
- return;
- end if;
-
- declare
- Old_Last_As_Int : constant Int := Int (Container.Last);
-
- begin
- if Old_Last_As_Int > Int'Last - N then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- New_Last_As_Int := Old_Last_As_Int + N;
-
- if New_Last_As_Int > Int (Index_Type'Last) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- New_Length := UInt (New_Last_As_Int - First + Int'(1));
-
- if New_Length > Max_Length then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- New_Last := Index_Type (New_Last_As_Int);
-
- -- Resolve issue of capacity vs. max index ???
- end;
-
- declare
- EA : Elements_Array renames Container.Elements;
-
- BB : constant Int'Base := Int (Before) - Int (No_Index);
- B : constant Count_Type := Count_Type (BB);
-
- LL : constant Int'Base := New_Last_As_Int - Int (No_Index);
- L : constant Count_Type := Count_Type (LL);
-
- begin
- if Before <= Container.Last then
- declare
- II : constant Int'Base := BB + N;
- I : constant Count_Type := Count_Type (II);
- begin
- EA (I .. L) := EA (B .. Length (Container));
- EA (B .. I - 1) := (others => New_Item);
- end;
-
- else
- EA (B .. L) := (others => New_Item);
- end if;
- end;
-
- Container.Last := New_Last;
- end Insert;
-
- procedure Insert
- (Container : in out Vector;
- Before : Extended_Index;
- New_Item : Vector)
- is
- N : constant Count_Type := Length (New_Item);
-
- begin
- if Before < Index_Type'First then
- raise Constraint_Error with
- "Before index is out of range (too small)";
- end if;
-
- if Before > Container.Last
- and then Before > Container.Last + 1
- then
- raise Constraint_Error with
- "Before index is out of range (too large)";
- end if;
-
- if N = 0 then
- return;
- end if;
-
- Insert_Space (Container, Before, Count => N);
-
- declare
- Dst_Last_As_Int : constant Int'Base :=
- Int (Before) + Int (N) - 1 - Int (No_Index);
-
- Dst_Last : constant Count_Type := Count_Type (Dst_Last_As_Int);
-
- BB : constant Int'Base := Int (Before) - Int (No_Index);
- B : constant Count_Type := Count_Type (BB);
-
- begin
- if Container'Address /= New_Item'Address then
- Container.Elements (B .. Dst_Last) := New_Item.Elements (1 .. N);
- return;
- end if;
-
- declare
- Src : Elements_Array renames Container.Elements (1 .. B - 1);
-
- Index_As_Int : constant Int'Base := BB + Src'Length - 1;
-
- Index : constant Count_Type := Count_Type (Index_As_Int);
-
- Dst : Elements_Array renames Container.Elements (B .. Index);
-
- begin
- Dst := Src;
- end;
-
- if Dst_Last = Length (Container) then
- return;
- end if;
-
- declare
- Src : Elements_Array renames
- Container.Elements (Dst_Last + 1 .. Length (Container));
-
- Index_As_Int : constant Int'Base :=
- Dst_Last_As_Int - Src'Length + 1;
-
- Index : constant Count_Type := Count_Type (Index_As_Int);
-
- Dst : Elements_Array renames
- Container.Elements (Index .. Dst_Last);
-
- begin
- Dst := Src;
- end;
- end;
- end Insert;
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Vector)
- is
- Index : Index_Type'Base;
-
- begin
- if Is_Empty (New_Item) then
- return;
- end if;
-
- if not Before.Valid
- or else Before.Index > Container.Last
- then
- if Container.Last = Index_Type'Last then
- raise Constraint_Error with
- "vector is already at its maximum length";
- end if;
-
- Index := Container.Last + 1;
-
- else
- Index := Before.Index;
- end if;
-
- Insert (Container, Index, New_Item);
- end Insert;
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Vector;
- Position : out Cursor)
- is
- Index : Index_Type'Base;
-
- begin
- if Is_Empty (New_Item) then
- if not Before.Valid
- or else Before.Index > Container.Last
- then
- Position := No_Element;
- else
- Position := (True, Before.Index);
- end if;
-
- return;
- end if;
-
- if not Before.Valid
- or else Before.Index > Container.Last
- then
- if Container.Last = Index_Type'Last then
- raise Constraint_Error with
- "vector is already at its maximum length";
- end if;
-
- Index := Container.Last + 1;
-
- else
- Index := Before.Index;
- end if;
-
- Insert (Container, Index, New_Item);
-
- Position := Cursor'(True, Index);
- end Insert;
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Element_Type;
- Count : Count_Type := 1)
- is
- Index : Index_Type'Base;
-
- begin
- if Count = 0 then
- return;
- end if;
-
- if not Before.Valid
- or else Before.Index > Container.Last
- then
- if Container.Last = Index_Type'Last then
- raise Constraint_Error with
- "vector is already at its maximum length";
- end if;
-
- Index := Container.Last + 1;
-
- else
- Index := Before.Index;
- end if;
-
- Insert (Container, Index, New_Item, Count);
- end Insert;
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Element_Type;
- Position : out Cursor;
- Count : Count_Type := 1)
- is
- Index : Index_Type'Base;
-
- begin
- if Count = 0 then
- if not Before.Valid
- or else Before.Index > Container.Last
- then
- Position := No_Element;
- else
- Position := (True, Before.Index);
- end if;
-
- return;
- end if;
-
- if not Before.Valid
- or else Before.Index > Container.Last
- then
- if Container.Last = Index_Type'Last then
- raise Constraint_Error with
- "vector is already at its maximum length";
- end if;
-
- Index := Container.Last + 1;
-
- else
- Index := Before.Index;
- end if;
-
- Insert (Container, Index, New_Item, Count);
-
- Position := Cursor'(True, Index);
- end Insert;
-
- ------------------
- -- Insert_Space --
- ------------------
-
- procedure Insert_Space
- (Container : in out Vector;
- Before : Extended_Index;
- Count : Count_Type := 1)
- is
- N : constant Int := Count_Type'Pos (Count);
-
- First : constant Int := Int (Index_Type'First);
- New_Last_As_Int : Int'Base;
- New_Last : Index_Type;
- New_Length : UInt;
- Max_Length : constant UInt := UInt (Count_Type'Last);
-
- begin
- if Before < Index_Type'First then
- raise Constraint_Error with
- "Before index is out of range (too small)";
- end if;
-
- if Before > Container.Last
- and then Before > Container.Last + 1
- then
- raise Constraint_Error with
- "Before index is out of range (too large)";
- end if;
-
- if Count = 0 then
- return;
- end if;
-
- declare
- Old_Last_As_Int : constant Int := Int (Container.Last);
-
- begin
- if Old_Last_As_Int > Int'Last - N then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- New_Last_As_Int := Old_Last_As_Int + N;
-
- if New_Last_As_Int > Int (Index_Type'Last) then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- New_Length := UInt (New_Last_As_Int - First + Int'(1));
-
- if New_Length > Max_Length then
- raise Constraint_Error with "new length is out of range";
- end if;
-
- New_Last := Index_Type (New_Last_As_Int);
-
- -- Resolve issue of capacity vs. max index ???
- end;
-
- declare
- EA : Elements_Array renames Container.Elements;
-
- BB : constant Int'Base := Int (Before) - Int (No_Index);
- B : constant Count_Type := Count_Type (BB);
-
- LL : constant Int'Base := New_Last_As_Int - Int (No_Index);
- L : constant Count_Type := Count_Type (LL);
-
- begin
- if Before <= Container.Last then
- declare
- II : constant Int'Base := BB + N;
- I : constant Count_Type := Count_Type (II);
- begin
- EA (I .. L) := EA (B .. Length (Container));
- end;
- end if;
- end;
-
- Container.Last := New_Last;
- end Insert_Space;
-
--------------
-- Is_Empty --
--------------
@@ -1169,19 +422,6 @@
return Last_Index (Container) < Index_Type'First;
end Is_Empty;
- ----------
- -- Last --
- ----------
-
- function Last (Container : Vector) return Cursor is
- begin
- if Is_Empty (Container) then
- return No_Element;
- end if;
-
- return (True, Last_Index (Container));
- end Last;
-
------------------
-- Last_Element --
------------------
@@ -1208,134 +448,15 @@
-- Length --
------------
- function Length (Container : Vector) return Count_Type is
+ function Length (Container : Vector) return Capacity_Range is
L : constant Int := Int (Last_Index (Container));
F : constant Int := Int (Index_Type'First);
N : constant Int'Base := L - F + 1;
begin
- return Count_Type (N);
+ return Capacity_Range (N);
end Length;
- ----------
- -- Move --
- ----------
-
- procedure Move
- (Target : in out Vector;
- Source : in out Vector)
- is
- N : constant Count_Type := Length (Source);
-
- begin
- if Target'Address = Source'Address then
- return;
- end if;
-
- if N > Target.Capacity then
- raise Constraint_Error with -- correct exception here???
- "length of Source is greater than capacity of Target";
- end if;
-
- -- We could also write this as a loop, and incrementally
- -- copy elements from source to target.
-
- Target.Last := No_Index; -- in case array assignment files
- Target.Elements (1 .. N) := Source.Elements (1 .. N);
-
- Target.Last := Source.Last;
- Source.Last := No_Index;
- end Move;
-
- ----------
- -- Next --
- ----------
-
- function Next (Container : Vector; Position : Cursor) return Cursor is
- begin
- if not Position.Valid then
- return No_Element;
- end if;
-
- if Position.Index < Last_Index (Container) then
- return (True, Position.Index + 1);
- end if;
-
- return No_Element;
- end Next;
-
- ----------
- -- Next --
- ----------
-
- procedure Next (Container : Vector; Position : in out Cursor) is
- begin
- if not Position.Valid then
- return;
- end if;
-
- if Position.Index < Last_Index (Container) then
- Position.Index := Position.Index + 1;
- else
- Position := No_Element;
- end if;
- end Next;
-
- -------------
- -- Prepend --
- -------------
-
- procedure Prepend (Container : in out Vector; New_Item : Vector) is
- begin
- Insert (Container, Index_Type'First, New_Item);
- end Prepend;
-
- procedure Prepend
- (Container : in out Vector;
- New_Item : Element_Type;
- Count : Count_Type := 1)
- is
- begin
- Insert (Container,
- Index_Type'First,
- New_Item,
- Count);
- end Prepend;
-
- --------------
- -- Previous --
- --------------
-
- procedure Previous (Container : Vector; Position : in out Cursor) is
- begin
- if not Position.Valid then
- return;
- end if;
-
- if Position.Index > Index_Type'First
- and then Position.Index <= Last_Index (Container)
- then
- Position.Index := Position.Index - 1;
- else
- Position := No_Element;
- end if;
- end Previous;
-
- function Previous (Container : Vector; Position : Cursor) return Cursor is
- begin
- if not Position.Valid then
- return No_Element;
- end if;
-
- if Position.Index > Index_Type'First
- and then Position.Index <= Last_Index (Container)
- then
- return (True, Position.Index - 1);
- end if;
-
- return No_Element;
- end Previous;
-
---------------------
-- Replace_Element --
---------------------
@@ -1352,46 +473,38 @@
declare
II : constant Int'Base := Int (Index) - Int (No_Index);
- I : constant Count_Type := Count_Type (II);
+ I : constant Capacity_Range := Capacity_Range (II);
begin
- Container.Elements (I) := New_Item;
+ Elems (Container) (I) := New_Item;
end;
end Replace_Element;
- procedure Replace_Element
- (Container : in out Vector;
- Position : Cursor;
- New_Item : Element_Type)
- is
- begin
- if not Position.Valid then
- raise Constraint_Error with "Position cursor has no element";
- end if;
-
- if Position.Index > Container.Last then
- raise Constraint_Error with "Position cursor is out of range";
- end if;
-
- declare
- II : constant Int'Base := Int (Position.Index) - Int (No_Index);
- I : constant Count_Type := Count_Type (II);
- begin
- Container.Elements (I) := New_Item;
- end;
- end Replace_Element;
-
----------------------
-- Reserve_Capacity --
----------------------
procedure Reserve_Capacity
(Container : in out Vector;
- Capacity : Count_Type)
+ Capacity : Capacity_Range)
is
begin
- if Capacity > Container.Capacity then
- raise Constraint_Error with "Capacity is out of range";
+ if Bounded then
+ if Capacity > Container.Capacity then
+ raise Constraint_Error with "Capacity is out of range";
+ end if;
+ else
+ if Capacity > Formal_Vectors.Capacity (Container) then
+ declare
+ New_Elements : constant Elements_Array_Ptr :=
+ new Elements_Array (1 .. Capacity);
+ L : constant Capacity_Range := Length (Container);
+ begin
+ New_Elements (1 .. L) := Elemsc (Container) (1 .. L);
+ Free (Container.Elements_Ptr);
+ Container.Elements_Ptr := New_Elements;
+ end;
+ end if;
end if;
end Reserve_Capacity;
@@ -1406,8 +519,8 @@
end if;
declare
- I, J : Count_Type;
- E : Elements_Array renames Container.Elements;
+ I, J : Capacity_Range;
+ E : Elements_Array renames Elems (Container).all;
begin
I := 1;
@@ -1426,39 +539,6 @@
end;
end Reverse_Elements;
- ------------------
- -- Reverse_Find --
- ------------------
-
- function Reverse_Find
- (Container : Vector;
- Item : Element_Type;
- Position : Cursor := No_Element) return Cursor
- is
- Last : Index_Type'Base;
- K : Count_Type;
-
- begin
- if not Position.Valid
- or else Position.Index > Last_Index (Container)
- then
- Last := Last_Index (Container);
- else
- Last := Position.Index;
- end if;
-
- K := Count_Type (Int (Last) - Int (No_Index));
- for Indx in reverse Index_Type'First .. Last loop
- if Get_Element (Container, K) = Item then
- return (True, Indx);
- end if;
-
- K := K - 1;
- end loop;
-
- return No_Element;
- end Reverse_Find;
-
------------------------
-- Reverse_Find_Index --
------------------------
@@ -1469,7 +549,7 @@
Index : Index_Type := Index_Type'Last) return Extended_Index
is
Last : Index_Type'Base;
- K : Count_Type;
+ K : Capacity_Range;
begin
if Index > Last_Index (Container) then
@@ -1478,7 +558,7 @@
Last := Index;
end if;
- K := Count_Type (Int (Last) - Int (No_Index));
+ K := Capacity_Range (Int (Last) - Int (No_Index));
for Indx in reverse Index_Type'First .. Last loop
if Get_Element (Container, K) = Item then
return Indx;
@@ -1490,44 +570,6 @@
return No_Index;
end Reverse_Find_Index;
- ----------------
- -- Set_Length --
- ----------------
-
- procedure Set_Length
- (Container : in out Vector;
- New_Length : Count_Type)
- is
- begin
- if New_Length = Formal_Vectors.Length (Container) then
- return;
- end if;
-
- if New_Length > Container.Capacity then
- raise Constraint_Error; -- ???
- end if;
-
- declare
- Last_As_Int : constant Int'Base :=
- Int (Index_Type'First) + Int (New_Length) - 1;
- begin
- Container.Last := Index_Type'Base (Last_As_Int);
- end;
- end Set_Length;
-
- ------------------
- -- Strict_Equal --
- ------------------
-
- function Strict_Equal (Left, Right : Vector) return Boolean is
- begin
- -- On bounded vectors, cursors are indexes. As a consequence, two
- -- vectors always have the same cursor at the same position and
- -- Strict_Equal is simply =
-
- return Left = Right;
- end Strict_Equal;
-
----------
-- Swap --
----------
@@ -1550,8 +592,8 @@
II : constant Int'Base := Int (I) - Int (No_Index);
JJ : constant Int'Base := Int (J) - Int (No_Index);
- EI : Element_Type renames Container.Elements (Count_Type (II));
- EJ : Element_Type renames Container.Elements (Count_Type (JJ));
+ EI : Element_Type renames Elems (Container) (Capacity_Range (II));
+ EJ : Element_Type renames Elems (Container) (Capacity_Range (JJ));
EI_Copy : constant Element_Type := EI;
@@ -1561,55 +603,13 @@
end;
end Swap;
- procedure Swap (Container : in out Vector; I, J : Cursor) is
- begin
- if not I.Valid then
- raise Constraint_Error with "I cursor has no element";
- end if;
-
- if not J.Valid then
- raise Constraint_Error with "J cursor has no element";
- end if;
-
- Swap (Container, I.Index, J.Index);
- end Swap;
-
---------------
- -- To_Cursor --
- ---------------
-
- function To_Cursor
- (Container : Vector;
- Index : Extended_Index) return Cursor
- is
- begin
- if Index not in Index_Type'First .. Last_Index (Container) then
- return No_Element;
- end if;
-
- return Cursor'(True, Index);
- end To_Cursor;
-
- --------------
- -- To_Index --
- --------------
-
- function To_Index (Position : Cursor) return Extended_Index is
- begin
- if not Position.Valid then
- return No_Index;
- end if;
-
- return Position.Index;
- end To_Index;
-
- ---------------
-- To_Vector --
---------------
function To_Vector
(New_Item : Element_Type;
- Length : Count_Type) return Vector
+ Length : Capacity_Range) return Vector
is
begin
if Length = 0 then
Index: a-cofove.ads
===================================================================
--- a-cofove.ads (revision 216925)
+++ a-cofove.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2014, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
@@ -35,38 +35,19 @@
-- unit compatible with SPARK 2014. Note that the API of this unit may be
-- subject to incompatible changes as SPARK 2014 evolves.
--- The modifications are:
-
--- A parameter for the container is added to every function reading the
--- content of a container: Element, Next, Query_Element, Previous, Iterate,
--- Has_Element, Reverse_Iterate. This change is motivated by the need
--- to have cursors which are valid on different containers (typically a
--- container C and its previous version C'Old) for expressing properties,
--- which is not possible if cursors encapsulate an access to the underlying
--- container.
-
--- There are three new functions:
-
--- function Strict_Equal (Left, Right : Vector) return Boolean;
--- function First_To_Previous (Container : Vector; Current : Cursor)
--- return Vector;
--- function Current_To_Last (Container : Vector; Current : Cursor)
--- return Vector;
-
--- See detailed specifications for these subprograms
-
-with Ada.Containers;
-use Ada.Containers;
-
generic
type Index_Type is range <>;
type Element_Type is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
+ Bounded : Boolean := True;
+ -- If True, the containers are bounded; the initial capacity is the maximum
+ -- size, and heap allocation will be avoided. If False, the containers can
+ -- grow via heap allocation.
+
package Ada.Containers.Formal_Vectors is
pragma Annotate (GNATprove, External_Axiomatization);
- pragma Pure;
subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 ..
@@ -77,248 +58,95 @@
subtype Capacity_Range is
Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
- type Vector (Capacity : Capacity_Range) is private with
- Iterable => (First => First,
- Next => Next,
- Has_Element => Has_Element,
- Element => Element),
+ type Vector (Capacity : Capacity_Range) is limited private with
Default_Initial_Condition;
+ -- In the bounded case, Capacity is the capacity of the container, which
+ -- never changes. In the unbounded case, Capacity is the initial capacity
+ -- of the container, and operations such as Reserve_Capacity and Append can
+ -- increase the capacity. The capacity never shrinks, except in the case of
+ -- Clear.
+ --
+ -- Note that all objects of type Vector are constrained, including in the
+ -- unbounded case; you can't assign from one object to another if the
+ -- Capacity is different.
- type Cursor is private;
- pragma Preelaborable_Initialization (Cursor);
+ function Empty_Vector return Vector;
- Empty_Vector : constant Vector;
-
- No_Element : constant Cursor;
-
function "=" (Left, Right : Vector) return Boolean with
Global => null;
function To_Vector
(New_Item : Element_Type;
- Length : Count_Type) return Vector
+ Length : Capacity_Range) return Vector
with
Global => null;
- function "&" (Left, Right : Vector) return Vector with
- Global => null,
- Pre => Capacity_Range'Last - Length (Left) >= Length (Right);
-
- function "&" (Left : Vector; Right : Element_Type) return Vector with
- Global => null,
- Pre => Length (Left) < Capacity_Range'Last;
-
- function "&" (Left : Element_Type; Right : Vector) return Vector with
- Global => null,
- Pre => Length (Right) < Capacity_Range'Last;
-
- function "&" (Left, Right : Element_Type) return Vector with
- Global => null,
- Pre => Capacity_Range'Last >= 2;
-
- function Capacity (Container : Vector) return Count_Type with
+ function Capacity (Container : Vector) return Capacity_Range with
Global => null;
procedure Reserve_Capacity
(Container : in out Vector;
- Capacity : Count_Type)
+ Capacity : Capacity_Range)
with
Global => null,
- Pre => Capacity <= Container.Capacity;
+ Pre => (if Bounded then Capacity <= Container.Capacity);
- function Length (Container : Vector) return Count_Type with
+ function Length (Container : Vector) return Capacity_Range with
Global => null;
- procedure Set_Length
- (Container : in out Vector;
- New_Length : Count_Type)
- with
- Global => null,
- Pre => New_Length <= Length (Container);
-
function Is_Empty (Container : Vector) return Boolean with
Global => null;
procedure Clear (Container : in out Vector) with
Global => null;
+ -- Note that this reclaims storage in the unbounded case. You need to call
+ -- this before a container goes out of scope in order to avoid storage
+ -- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
procedure Assign (Target : in out Vector; Source : Vector) with
Global => null,
- Pre => Length (Source) <= Target.Capacity;
+ Pre => (if Bounded then Length (Source) <= Target.Capacity);
function Copy
(Source : Vector;
- Capacity : Count_Type := 0) return Vector
+ Capacity : Capacity_Range := 0) return Vector
with
Global => null,
- Pre => Length (Source) <= Capacity and then Capacity in Capacity_Range;
+ Pre => (if Bounded then Length (Source) <= Capacity);
- function To_Cursor
- (Container : Vector;
- Index : Extended_Index) return Cursor
- with
- Global => null;
-
- function To_Index (Position : Cursor) return Extended_Index with
- Global => null;
-
function Element
(Container : Vector;
Index : Index_Type) return Element_Type
with
Global => null,
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container);
+ Pre => Index in First_Index (Container) .. Last_Index (Container);
- function Element
- (Container : Vector;
- Position : Cursor) return Element_Type
- with
- Global => null,
- Pre => Has_Element (Container, Position);
-
procedure Replace_Element
(Container : in out Vector;
Index : Index_Type;
New_Item : Element_Type)
with
Global => null,
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container);
+ Pre => Index in First_Index (Container) .. Last_Index (Container);
- procedure Replace_Element
- (Container : in out Vector;
- Position : Cursor;
- New_Item : Element_Type)
- with
- Global => null,
- Pre => Has_Element (Container, Position);
-
- procedure Move (Target : in out Vector; Source : in out Vector) with
- Global => null,
- Pre => Length (Source) <= Target.Capacity;
-
- procedure Insert
- (Container : in out Vector;
- Before : Extended_Index;
- New_Item : Vector)
- with
- Global => null,
- Pre => First_Index (Container) <= Before
- and then Before <= Last_Index (Container) + 1
- and then Length (Container) < Container.Capacity;
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Vector)
- with
- Global => null,
- Pre => Length (Container) < Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Vector;
- Position : out Cursor)
- with
- Global => null,
- Pre => Length (Container) < Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
-
- procedure Insert
- (Container : in out Vector;
- Before : Extended_Index;
- New_Item : Element_Type;
- Count : Count_Type := 1)
- with
- Global => null,
- Pre => First_Index (Container) <= Before
- and then Before <= Last_Index (Container) + 1
- and then Length (Container) + Count <= Container.Capacity;
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Element_Type;
- Count : Count_Type := 1)
- with
- Global => null,
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
-
- procedure Insert
- (Container : in out Vector;
- Before : Cursor;
- New_Item : Element_Type;
- Position : out Cursor;
- Count : Count_Type := 1)
- with
- Global => null,
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
-
- procedure Prepend
- (Container : in out Vector;
- New_Item : Vector)
- with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
-
- procedure Prepend
- (Container : in out Vector;
- New_Item : Element_Type;
- Count : Count_Type := 1)
- with
- Global => null,
- Pre => Length (Container) + Count <= Container.Capacity;
-
procedure Append
(Container : in out Vector;
New_Item : Vector)
with
Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Pre => (if Bounded then
+ Length (Container) + Length (New_Item) <= Container.Capacity);
procedure Append
(Container : in out Vector;
- New_Item : Element_Type;
- Count : Count_Type := 1)
+ New_Item : Element_Type)
with
Global => null,
- Pre => Length (Container) + Count <= Container.Capacity;
+ Pre => (if Bounded then
+ Length (Container) < Container.Capacity);
- procedure Delete
- (Container : in out Vector;
- Index : Extended_Index;
- Count : Count_Type := 1)
- with
- Global => null,
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container) + 1;
-
- procedure Delete
- (Container : in out Vector;
- Position : in out Cursor;
- Count : Count_Type := 1)
- with
- Global => null,
- Pre => Has_Element (Container, Position);
-
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type := 1)
- with
- Global => null;
-
procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type := 1)
+ (Container : in out Vector)
with
Global => null;
@@ -327,21 +155,12 @@
procedure Swap (Container : in out Vector; I, J : Index_Type) with
Global => null,
- Pre => First_Index (Container) <= I
- and then I <= Last_Index (Container)
- and then First_Index (Container) <= J
- and then J <= Last_Index (Container);
+ Pre => I in First_Index (Container) .. Last_Index (Container)
+ and then J in First_Index (Container) .. Last_Index (Container);
- procedure Swap (Container : in out Vector; I, J : Cursor) with
- Global => null,
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
-
function First_Index (Container : Vector) return Index_Type with
Global => null;
- function First (Container : Vector) return Cursor with
- Global => null;
-
function First_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container);
@@ -349,29 +168,10 @@
function Last_Index (Container : Vector) return Extended_Index with
Global => null;
- function Last (Container : Vector) return Cursor with
- Global => null;
-
function Last_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container);
- function Next (Container : Vector; Position : Cursor) return Cursor with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
-
- procedure Next (Container : Vector; Position : in out Cursor) with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
-
- function Previous (Container : Vector; Position : Cursor) return Cursor with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
-
- procedure Previous (Container : Vector; Position : in out Cursor) with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
-
function Find_Index
(Container : Vector;
Item : Element_Type;
@@ -379,14 +179,6 @@
with
Global => null;
- function Find
- (Container : Vector;
- Item : Element_Type;
- Position : Cursor := No_Element) return Cursor
- with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
-
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
@@ -394,22 +186,14 @@
with
Global => null;
- function Reverse_Find
- (Container : Vector;
- Item : Element_Type;
- Position : Cursor := No_Element) return Cursor
- with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
-
function Contains
(Container : Vector;
Item : Element_Type) return Boolean
with
Global => null;
- function Has_Element (Container : Vector; Position : Cursor) return Boolean
- with
+ function Has_Element
+ (Container : Vector; Position : Extended_Index) return Boolean with
Global => null;
generic
@@ -422,29 +206,18 @@
procedure Sort (Container : in out Vector) with
Global => null;
- procedure Merge (Target : in out Vector; Source : in out Vector) with
- Global => null;
-
end Generic_Sorting;
- function Strict_Equal (Left, Right : Vector) return Boolean with
- Global => null;
- -- Strict_Equal returns True if the containers are physically equal, i.e.
- -- they are structurally equal (function "=" returns True) and that they
- -- have the same set of cursors.
-
function First_To_Previous
(Container : Vector;
- Current : Cursor) return Vector
+ Current : Index_Type) return Vector
with
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
+ Global => null;
function Current_To_Last
(Container : Vector;
- Current : Cursor) return Vector
+ Current : Index_Type) return Vector
with
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
+ Global => null;
-- First_To_Previous returns a container containing all elements preceding
-- Current (excluded) in Container. Current_To_Last returns a container
-- containing all elements following Current (included) in Container.
@@ -462,24 +235,33 @@
pragma Inline (Last_Element);
pragma Inline (Replace_Element);
pragma Inline (Contains);
- pragma Inline (Next);
- pragma Inline (Previous);
- type Elements_Array is array (Count_Type range <>) of Element_Type;
+ type Elements_Array is array (Capacity_Range range <>) of Element_Type;
function "=" (L, R : Elements_Array) return Boolean is abstract;
- type Vector (Capacity : Capacity_Range) is record
- Elements : Elements_Array (1 .. Capacity);
- Last : Extended_Index := No_Index;
- end record;
+ type Elements_Array_Ptr is access all Elements_Array;
- type Cursor is record
- Valid : Boolean := True;
- Index : Index_Type := Index_Type'First;
+ type Vector (Capacity : Capacity_Range) is limited record
+ -- In the bounded case, the elements are stored in Elements. In the
+ -- unbounded case, the elements are initially stored in Elements, until
+ -- we run out of room, then we switch to Elements_Ptr.
+ Elements : aliased Elements_Array (1 .. Capacity);
+ Last : Extended_Index := No_Index;
+ Elements_Ptr : Elements_Array_Ptr := null;
end record;
- Empty_Vector : constant Vector := (Capacity => 0, others => <>);
+ -- The primary reason Vector is limited is that in the unbounded case, once
+ -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
+ -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
+ -- so for example "Append (X, ...);" will modify BOTH X and Y. That would
+ -- allow SPARK to "prove" things that are false. We could fix that by
+ -- making Vector a controlled type, and override Adjust to make a deep
+ -- copy, but finalization is not allowed in SPARK.
+ --
+ -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
+ -- allowed on Vectors.
- No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
+ function Empty_Vector return Vector is
+ ((Capacity => 0, others => <>));
end Ada.Containers.Formal_Vectors;
