+2014-10-31 Vasiliy Fofanov <fofanov@adacore.com>
+
+ * prj-conf.adb (Do_Autoconf): Refactor the code so that empty
+ Normalized_Pathname doesn't inhibit the custom Selected_Target
+ value.
+ * prj-conf.adb (Parse_Project_And_Apply_Config): Make sure that
+ Automatically_Generated is correctly set after the first call
+ to Process_Project_And_Apply_Config and not modified after the
+ second call, if any.
+
+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.
+
2014-10-31 Vincent Celier <celier@adacore.com>
* prj-conf.adb (Look_For_Project_Paths): New procedure
a-cfdlli$(objext) \
a-cfhama$(objext) \
a-cfhase$(objext) \
+ a-cfinve$(objext) \
a-cforma$(objext) \
a-cforse$(objext) \
a-cgaaso$(objext) \
a-ciormu$(objext) \
a-ciorse$(objext) \
a-clrefi$(objext) \
+ a-coboho$(objext) \
a-cobove$(objext) \
a-cofove$(objext) \
a-cogeso$(objext) \
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
-- --
-- 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- --
------------------------------------------------------------------------------
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;
-
- procedure Insert_Space
- (Container : in out Vector;
- Before : Extended_Index;
- Count : Count_Type := 1);
-
- ---------
- -- "&" --
- ---------
-
- function "&" (Left, Right : Vector) return Vector is
- LN : constant Count_Type := Length (Left);
- RN : constant Count_Type := Length (Right);
-
- 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;
+ type Elements_Array_Ptr_Const is access constant Elements_Array;
- 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 "&";
+ procedure Free is
+ new Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
- 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;
+ 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.
- declare
- Last : constant Index_Type := Index_Type'First + 1;
- begin
- return (2, (Left, Right), Last => Last, others => <>);
- end;
- end "&";
+ function Get_Element
+ (Container : Vector;
+ Position : Capacity_Range) return Element_Type;
---------
-- "=" --
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;
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
-- 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;
------------
------------
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;
-----------
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;
--------------
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;
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
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;
-
- 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);
+ return (if Container.Elements_Ptr = null
+ then Container.Elements'Unrestricted_Access
+ else Container.Elements_Ptr);
+ end Elems;
+ 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;
-
- 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;
+ return (if Container.Elements_Ptr = null
+ then Container.Elements'Unrestricted_Access
+ else Elements_Array_Ptr_Const (Container.Elements_Ptr));
+ end Elemsc;
----------------
-- Find_Index --
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;
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 --
-------------------
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;
---------------------
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
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 --
----------
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;
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;
-----------------
-----------------
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 --
- ------------
+ --------------
+ -- Is_Empty --
+ --------------
- 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);
+ function Is_Empty (Container : Vector) return Boolean is
+ begin
+ return Last_Index (Container) < Index_Type'First;
+ end Is_Empty;
- 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);
+ ------------------
+ -- Last_Element --
+ ------------------
+ function Last_Element (Container : Vector) return Element_Type is
begin
- if Before < Index_Type'First then
- raise Constraint_Error with
- "Before index is out of range (too small)";
+ if Is_Empty (Container) then
+ raise Constraint_Error with "Container is empty";
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;
+ return Get_Element (Container, Length (Container));
+ end Last_Element;
- if Count = 0 then
- return;
- end if;
+ ----------------
+ -- Last_Index --
+ ----------------
- declare
- Old_Last_As_Int : constant Int := Int (Container.Last);
+ function Last_Index (Container : Vector) return Extended_Index is
+ begin
+ return Container.Last;
+ end Last_Index;
- begin
- if Old_Last_As_Int > Int'Last - N then
- raise Constraint_Error with "new length is out of range";
- end if;
+ ------------
+ -- Length --
+ ------------
- 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 --
- --------------
-
- function Is_Empty (Container : Vector) return Boolean is
- begin
- 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 --
- ------------------
-
- function Last_Element (Container : Vector) return Element_Type is
- begin
- if Is_Empty (Container) then
- raise Constraint_Error with "Container is empty";
- end if;
-
- return Get_Element (Container, Length (Container));
- end Last_Element;
-
- ----------------
- -- Last_Index --
- ----------------
-
- function Last_Index (Container : Vector) return Extended_Index is
- begin
- return Container.Last;
- end Last_Index;
-
- ------------
- -- 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 --
---------------------
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;
- 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;
+ Elems (Container) (I) := New_Item;
end;
end Replace_Element;
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;
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;
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 --
------------------------
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
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;
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 --
----------
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;
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
-- --
-- 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 --
-- 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 ..
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;
-
- type Cursor is private;
- pragma Preelaborable_Initialization (Cursor);
-
- Empty_Vector : constant Vector;
-
- No_Element : constant Cursor;
+ -- 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.
+
+ function Empty_Vector return Vector;
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;
-
- function To_Cursor
- (Container : Vector;
- Index : Extended_Index) return Cursor
- with
- Global => null;
-
- function To_Index (Position : Cursor) return Extended_Index with
- Global => null;
+ Pre => (if Bounded then Length (Source) <= Capacity);
function Element
(Container : Vector;
Index : Index_Type) return Element_Type
with
Global => null,
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container);
-
- function Element
- (Container : Vector;
- Position : Cursor) return Element_Type
- with
- Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Index in First_Index (Container) .. Last_Index (Container);
procedure Replace_Element
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null,
- Pre => First_Index (Container) <= Index
- and then Index <= 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;
+ Pre => Index in First_Index (Container) .. Last_Index (Container);
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)
- with
- Global => null,
- Pre => Length (Container) + Count <= 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)
+ New_Item : Element_Type)
with
Global => null,
- Pre => Has_Element (Container, Position);
-
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type := 1)
- with
- Global => null;
+ Pre => (if Bounded then
+ Length (Container) < Container.Capacity);
procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type := 1)
+ (Container : in out Vector)
with
Global => null;
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);
-
- procedure Swap (Container : in out Vector; I, J : Cursor) with
- Global => null,
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
+ 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 (Container : Vector) return Cursor 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 (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;
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;
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
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.
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 => <>);
-
- No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
+ -- 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.
+
+ function Empty_Vector return Vector is
+ ((Capacity => 0, others => <>));
end Ada.Containers.Formal_Vectors;
* 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)::
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.
* 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)::
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})
-- 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
Args (3) := Conf_File_Name;
end if;
- if Normalized_Hostname = "" then
- Arg_Last := 3;
- else
- if Selected_Target'Length = 0 then
- if At_Least_One_Compiler_Command then
- Args (4) :=
- new String'("--target=all");
- else
- Args (4) :=
- new String'("--target=" & Normalized_Hostname);
- end if;
+ Arg_Last := 3;
+ if Selected_Target /= null and then
+ Selected_Target.all /= ""
+ then
+ Args (4) :=
+ new String'("--target=" & Selected_Target.all);
+ Arg_Last := 4;
+ elsif Normalized_Hostname /= "" then
+ if At_Least_One_Compiler_Command then
+ Args (4) :=
+ new String'("--target=all");
else
Args (4) :=
- new String'("--target=" & Selected_Target.all);
+ new String'("--target=" & Normalized_Hostname);
end if;
Arg_Last := 4;
then
Write_Line
("warning: " &
- "--RTS is taken into account only in auto-configuration");
+ "runtimes are taken into account only in auto-configuration");
end if;
-- Parse the configuration file
procedure Add_Directory (Dir : String);
-- Add a directory at the end of the Project Path
+ Auto_Generated : Boolean;
+
-------------------
-- Add_Directory --
-------------------
Update_Ignore_Missing_With (Env.Flags, True);
+ Automatically_Generated := False;
+ -- If in fact the config file is automatically generated,
+ -- Automatically_Generated will be set to True after invocation of
+ -- Process_Project_And_Apply_Config.
+
-- Record Target_Value and Target_Origin.
if Target_Name = "" then
Prj.Initialize (Project_Tree);
Main_Project := No_Project;
- Automatically_Generated := False;
Prj.Part.Parse
(In_Tree => Project_Node_Tree,
Env => Env,
Packages_To_Check => Packages_To_Check,
Allow_Automatic_Generation => Allow_Automatic_Generation,
- Automatically_Generated => Automatically_Generated,
+ Automatically_Generated => Auto_Generated,
Config_File_Path => Config_File_Path,
Target_Name => Target_Name,
Normalized_Hostname => Normalized_Hostname,
On_New_Tree_Loaded => On_New_Tree_Loaded,
Do_Phase_1 => Opt.Target_Origin = Specified);
+ if Auto_Generated then
+ Automatically_Generated := True;
+ end if;
+
-- Exit if there was an error. Otherwise, if Config_Try_Again is True,
-- update the project path and try again.
projects / gcc.git / commitdiff