From 4a68b7c4d594e082b32da7e76a7cd7a472abb5de Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 31 Oct 2014 12:37:44 +0100 Subject: [PATCH] [multiple changes] 2014-10-31 Vasiliy Fofanov * 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 * 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. From-SVN: r216967 --- gcc/ada/ChangeLog | 25 + gcc/ada/Makefile.rtl | 2 + gcc/ada/a-cfinve.adb | 295 ++++++++++ gcc/ada/a-cfinve.ads | 249 ++++++++ gcc/ada/a-coboho.adb | 89 +++ gcc/ada/a-coboho.ads | 102 ++++ gcc/ada/a-cofove.adb | 1278 +++++------------------------------------- gcc/ada/a-cofove.ads | 352 +++--------- gcc/ada/gnat_rm.texi | 33 ++ gcc/ada/impunit.adb | 2 + gcc/ada/prj-conf.adb | 40 +- 11 files changed, 1028 insertions(+), 1439 deletions(-) create mode 100644 gcc/ada/a-cfinve.adb create mode 100644 gcc/ada/a-cfinve.ads create mode 100644 gcc/ada/a-coboho.adb create mode 100644 gcc/ada/a-coboho.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9e76cbb5f68..7081458aca4 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,28 @@ +2014-10-31 Vasiliy Fofanov + + * 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 + + * 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 * prj-conf.adb (Look_For_Project_Paths): New procedure diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl index cfab8cf350a..ce59a64cfc2 100644 --- a/gcc/ada/Makefile.rtl +++ b/gcc/ada/Makefile.rtl @@ -110,6 +110,7 @@ GNATRTL_NONTASKING_OBJS= \ 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 @@ GNATRTL_NONTASKING_OBJS= \ a-ciormu$(objext) \ a-ciorse$(objext) \ a-clrefi$(objext) \ + a-coboho$(objext) \ a-cobove$(objext) \ a-cofove$(objext) \ a-cogeso$(objext) \ diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb new file mode 100644 index 00000000000..793b5c3922f --- /dev/null +++ b/gcc/ada/a-cfinve.adb @@ -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 -- +-- . -- +------------------------------------------------------------------------------ + +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; diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads new file mode 100644 index 00000000000..19cc166f268 --- /dev/null +++ b/gcc/ada/a-cfinve.ads @@ -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 -- +-- . -- +------------------------------------------------------------------------------ + +-- 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; diff --git a/gcc/ada/a-coboho.adb b/gcc/ada/a-coboho.adb new file mode 100644 index 00000000000..23beaea9b37 --- /dev/null +++ b/gcc/ada/a-coboho.adb @@ -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 -- +-- . -- +------------------------------------------------------------------------------ + +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; diff --git a/gcc/ada/a-coboho.ads b/gcc/ada/a-coboho.ads new file mode 100644 index 00000000000..244c4d41fe9 --- /dev/null +++ b/gcc/ada/a-coboho.ads @@ -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 -- +-- . -- +------------------------------------------------------------------------------ + +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; diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb index a12f8c243df..42d61f4e0e4 100644 --- a/gcc/ada/a-cofove.adb +++ b/gcc/ada/a-cofove.adb @@ -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,155 +26,32 @@ ------------------------------------------------------------------------------ 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; --------- -- "=" -- @@ -190,7 +67,7 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is -- 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 @@ package body Ada.Containers.Formal_Vectors is ------------ 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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,66 +243,30 @@ package body Ada.Containers.Formal_Vectors is 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 -- @@ -553,11 +277,11 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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,578 +408,55 @@ package body Ada.Containers.Formal_Vectors is ----------------- 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 -- --------------------- @@ -1352,32 +473,10 @@ package body Ada.Containers.Formal_Vectors is 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; @@ -1387,11 +486,25 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 @@ package body Ada.Containers.Formal_Vectors is 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 diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index f5b9b64347b..cff122a8954 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -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,105 +58,68 @@ package Ada.Containers.Formal_Vectors is 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; @@ -183,142 +127,26 @@ package Ada.Containers.Formal_Vectors is 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; @@ -327,21 +155,12 @@ package Ada.Containers.Formal_Vectors is 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); @@ -349,29 +168,10 @@ package Ada.Containers.Formal_Vectors is 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 @@ package Ada.Containers.Formal_Vectors is 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 @@ package Ada.Containers.Formal_Vectors is 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 @@ package Ada.Containers.Formal_Vectors is 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 @@ private 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; diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index e7bd8bf489c..e0f6b3fcf3b 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -542,6 +542,8 @@ The GNAT Library * 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 @@ subranges) for unordered types. If this switch is used, then any 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 @@ of GNAT, and will generate a warning message. * 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 @@ 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.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}) diff --git a/gcc/ada/impunit.adb b/gcc/ada/impunit.adb index 49baf1651c2..ca53594fa7c 100644 --- a/gcc/ada/impunit.adb +++ b/gcc/ada/impunit.adb @@ -581,6 +581,8 @@ package body Impunit is -- 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 diff --git a/gcc/ada/prj-conf.adb b/gcc/ada/prj-conf.adb index fe6cb60b381..8d4e3d46d91 100644 --- a/gcc/ada/prj-conf.adb +++ b/gcc/ada/prj-conf.adb @@ -1101,21 +1101,21 @@ package body Prj.Conf is 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; @@ -1496,7 +1496,7 @@ package body Prj.Conf is 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 @@ -1610,6 +1610,8 @@ package body Prj.Conf is procedure Add_Directory (Dir : String); -- Add a directory at the end of the Project Path + Auto_Generated : Boolean; + ------------------- -- Add_Directory -- ------------------- @@ -1630,6 +1632,11 @@ package body Prj.Conf is 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 @@ -1647,7 +1654,6 @@ package body Prj.Conf is Prj.Initialize (Project_Tree); Main_Project := No_Project; - Automatically_Generated := False; Prj.Part.Parse (In_Tree => Project_Node_Tree, @@ -1728,7 +1734,7 @@ package body Prj.Conf is 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, @@ -1736,6 +1742,10 @@ package body Prj.Conf is 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. -- 2.30.2