mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-03 05:10:26 +08:00
Code Issues Packages Projects Releases Wiki Activity

[multiple changes]

Browse Source 
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.

From-SVN: r216967
This commit is contained in:
Arnaud Charlet 2014-10-31 12:37:44 +01:00
parent 527f5eb67a
commit 4a68b7c4d5
11 changed files with 1009 additions and 1420 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
gcc/ada/ChangeLog
View File

@ -1,3 +1,28 @@
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

2
gcc/ada/Makefile.rtl
View File

@ -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) \

295
gcc/ada/a-cfinve.adb Normal file
View File

@ -0,0 +1,295 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- A D A . C O N T A I N E R S
-- . F O R M A L _ I N D E F I N I T E _ V E C T O R S --
-- --
-- B o d y --
-- --
-- Copyright (C) 2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
package body Ada.Containers.Formal_Indefinite_Vectors is
function H (New_Item : Element_Type) return Holder renames To_Holder;
function E (Container : Holder) return Element_Type renames Get;
---------
-- "=" --
---------
function "=" (Left, Right : Vector) return Boolean is
(Left.V = Right.V);
------------
-- Append --
------------
procedure Append (Container : in out Vector; New_Item : Vector) is
begin
Append (Container.V, New_Item.V);
end Append;
procedure Append
(Container : in out Vector;
New_Item : Element_Type)
is
begin
Append (Container.V, H (New_Item));
end Append;
------------
-- Assign --
------------
procedure Assign (Target : in out Vector; Source : Vector) is
begin
Assign (Target.V, Source.V);
end Assign;
--------------
-- Capacity --
--------------
function Capacity (Container : Vector) return Capacity_Range is
(Capacity (Container.V));
-----------
-- Clear --
-----------
procedure Clear (Container : in out Vector) is
begin
Clear (Container.V);
end Clear;
--------------
-- Contains --
--------------
function Contains
(Container : Vector;
Item : Element_Type) return Boolean is
(Contains (Container.V, H (Item)));
----------
-- Copy --
----------
function Copy
(Source : Vector;
Capacity : Capacity_Range := 0) return Vector is
(Capacity, V => Copy (Source.V, Capacity));
---------------------
-- Current_To_Last --
---------------------
function Current_To_Last
(Container : Vector;
Current : Index_Type) return Vector is
begin
return (Length (Container), Current_To_Last (Container.V, Current));
end Current_To_Last;
-----------------
-- Delete_Last --
-----------------
procedure Delete_Last
(Container : in out Vector)
is
begin
Delete_Last (Container.V);
end Delete_Last;
-------------
-- Element --
-------------
function Element
(Container : Vector;
Index : Index_Type) return Element_Type is
(E (Element (Container.V, Index)));
----------------
-- Find_Index --
----------------
function Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index is
(Find_Index (Container.V, H (Item), Index));
-------------------
-- First_Element --
-------------------
function First_Element (Container : Vector) return Element_Type is
(E (First_Element (Container.V)));
-----------------
-- First_Index --
-----------------
function First_Index (Container : Vector) return Index_Type is
(First_Index (Container.V));
-----------------------
-- First_To_Previous --
-----------------------
function First_To_Previous
(Container : Vector;
Current : Index_Type) return Vector is
begin
return (Length (Container), First_To_Previous (Container.V, Current));
end First_To_Previous;
---------------------
-- Generic_Sorting --
---------------------
package body Generic_Sorting is
function "<" (X, Y : Holder) return Boolean is (E (X) < E (Y));
package Def_Sorting is new Def.Generic_Sorting ("<");
use Def_Sorting;
---------------
-- Is_Sorted --
---------------
function Is_Sorted (Container : Vector) return Boolean is
(Is_Sorted (Container.V));
----------
-- Sort --
----------
procedure Sort (Container : in out Vector) is
begin
Sort (Container.V);
end Sort;
end Generic_Sorting;
-----------------
-- Has_Element --
-----------------
function Has_Element
(Container : Vector; Position : Extended_Index) return Boolean is
(Has_Element (Container.V, Position));
--------------
-- Is_Empty --
--------------
function Is_Empty (Container : Vector) return Boolean is
(Is_Empty (Container.V));
------------------
-- Last_Element --
------------------
function Last_Element (Container : Vector) return Element_Type is
(E (Last_Element (Container.V)));
----------------
-- Last_Index --
----------------
function Last_Index (Container : Vector) return Extended_Index is
(Last_Index (Container.V));
------------
-- Length --
------------
function Length (Container : Vector) return Capacity_Range is
(Length (Container.V));
---------------------
-- Replace_Element --
---------------------
procedure Replace_Element
(Container : in out Vector;
Index : Index_Type;
New_Item : Element_Type)
is
begin
Replace_Element (Container.V, Index, H (New_Item));
end Replace_Element;
----------------------
-- Reserve_Capacity --
----------------------
procedure Reserve_Capacity
(Container : in out Vector;
Capacity : Capacity_Range)
is
begin
Reserve_Capacity (Container.V, Capacity);
end Reserve_Capacity;
----------------------
-- Reverse_Elements --
----------------------
procedure Reverse_Elements (Container : in out Vector) is
begin
Reverse_Elements (Container.V);
end Reverse_Elements;
------------------------
-- Reverse_Find_Index --
------------------------
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index is
(Reverse_Find_Index (Container.V, H (Item), Index));
----------
-- Swap --
----------
procedure Swap (Container : in out Vector; I, J : Index_Type) is
begin
Swap (Container.V, I, J);
end Swap;
---------------
-- To_Vector --
---------------
function To_Vector
(New_Item : Element_Type;
Length : Capacity_Range) return Vector is
begin
return (Length, To_Vector (H (New_Item), Length));
end To_Vector;
end Ada.Containers.Formal_Indefinite_Vectors;

249
gcc/ada/a-cfinve.ads Normal file
View File

@ -0,0 +1,249 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- A D A . C O N T A I N E R S
-- . F O R M A L _ I N D E F I N I T E _ V E C T O R S --
-- --
-- S p e c --
-- --
-- Copyright (C) 2014, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
-- Similar to Ada.Containers.Formal_Vectors. The main difference is that
-- Element_Type may be indefinite (but not an unconstrained array). In
-- addition, this is simplified by removing less-used functionality.
with Ada.Containers.Bounded_Holders;
with Ada.Containers.Formal_Vectors;
generic
type Index_Type is range <>;
type Element_Type (<>) is private;
Max_Size_In_Storage_Elements : Natural :=
Element_Type'Max_Size_In_Storage_Elements;
-- This has the same meaning as in Ada.Containers.Bounded_Holders, with the
-- same restrictions.
with function "=" (Left, Right : Element_Type) return Boolean is <>;
Bounded : Boolean := True;
-- If True, the containers are bounded; the initial capacity is the maximum
-- size, and heap allocation will be avoided. If False, the containers can
-- grow via heap allocation.
package Ada.Containers.Formal_Indefinite_Vectors is
pragma Annotate (GNATprove, External_Axiomatization);
subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 ..
Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
No_Index : constant Extended_Index := Extended_Index'First;
subtype Capacity_Range is
Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
type Vector (Capacity : Capacity_Range) is limited private with
Default_Initial_Condition;
function Empty_Vector return Vector;
function "=" (Left, Right : Vector) return Boolean with
Global => null;
function To_Vector
(New_Item : Element_Type;
Length : Capacity_Range) return Vector
with
Global => null;
function Capacity (Container : Vector) return Capacity_Range with
Global => null;
procedure Reserve_Capacity
(Container : in out Vector;
Capacity : Capacity_Range)
with
Global => null,
Pre => (if Bounded then Capacity <= Container.Capacity);
function Length (Container : Vector) return Capacity_Range with
Global => null;
function Is_Empty (Container : Vector) return Boolean with
Global => null;
procedure Clear (Container : in out Vector) with
Global => null;
-- Note that this reclaims storage in the unbounded case. You need to call
-- this before a container goes out of scope in order to avoid storage
-- leaks.
procedure Assign (Target : in out Vector; Source : Vector) with
Global => null,
Pre => (if Bounded then Length (Source) <= Target.Capacity);
function Copy
(Source : Vector;
Capacity : Capacity_Range := 0) return Vector
with
Global => null,
Pre => (if Bounded then Length (Source) <= Capacity);
function Element
(Container : Vector;
Index : Index_Type) return Element_Type
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container);
procedure Replace_Element
(Container : in out Vector;
Index : Index_Type;
New_Item : Element_Type)
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container);
procedure Append
(Container : in out Vector;
New_Item : Vector)
with
Global => null,
Pre => (if Bounded then
Length (Container) + Length (New_Item) <= Container.Capacity);
procedure Append
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null,
Pre => (if Bounded then
Length (Container) < Container.Capacity);
procedure Delete_Last
(Container : in out Vector)
with
Global => null;
procedure Reverse_Elements (Container : in out Vector) with
Global => null;
procedure Swap (Container : in out Vector; I, J : Index_Type) with
Global => null,
Pre => I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container);
function First_Index (Container : Vector) return Index_Type with
Global => null;
function First_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container);
function Last_Index (Container : Vector) return Extended_Index with
Global => null;
function Last_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container);
function Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index
with
Global => null;
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index
with
Global => null;
function Contains
(Container : Vector;
Item : Element_Type) return Boolean
with
Global => null;
function Has_Element
(Container : Vector; Position : Extended_Index) return Boolean with
Global => null;
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting is
function Is_Sorted (Container : Vector) return Boolean with
Global => null;
procedure Sort (Container : in out Vector) with
Global => null;
end Generic_Sorting;
function First_To_Previous
(Container : Vector;
Current : Index_Type) return Vector
with
Global => null;
function Current_To_Last
(Container : Vector;
Current : Index_Type) return Vector
with
Global => null;
private
pragma Inline (First_Index);
pragma Inline (Last_Index);
pragma Inline (Element);
pragma Inline (First_Element);
pragma Inline (Last_Element);
pragma Inline (Replace_Element);
pragma Inline (Contains);
-- The implementation method is to instantiate Bounded_Holders to get a
-- definite type for Element_Type, and then use that Holder type to
-- instantiate Formal_Vectors. All the operations are just wrappers.
package Holders is new Bounded_Holders
(Element_Type, Max_Size_In_Storage_Elements, "=");
use Holders;
package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
use Def;
-- ????Assert that Def subtypes have the same range.
type Vector (Capacity : Capacity_Range) is limited record
V : Def.Vector (Capacity);
end record;
function Empty_Vector return Vector is
((Capacity => 0, V => Def.Empty_Vector));
end Ada.Containers.Formal_Indefinite_Vectors;

89
gcc/ada/a-coboho.adb Normal file
View File

@ -0,0 +1,89 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- A D A . C O N T A I N E R S . B O U N D E D _ H O L D E R S --
-- --
-- B o d y --
-- --
-- Copyright (C) 2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
with Unchecked_Conversion;
with Ada.Assertions; use Ada.Assertions;
package body Ada.Containers.Bounded_Holders is
function Size_In_Storage_Elements (Element : Element_Type) return Natural is
(Element'Size / System.Storage_Unit)
with Pre =>
(Element'Size mod System.Storage_Unit = 0 or else
raise Assertion_Error with "Size must be a multiple of Storage_Unit")
and then
(Element'Size / System.Storage_Unit <= Max_Size_In_Storage_Elements
or else raise Assertion_Error with "Size is too big");
-- This returns the size of Element in storage units. It raises an
-- exception if the size is not a multiple of Storage_Unit, or if the size
-- is too big.
function Cast is new
Unchecked_Conversion (System.Address, Element_Access);
---------
-- "=" --
---------
function "=" (Left, Right : Holder) return Boolean is
begin
return Get (Left) = Get (Right);
end "=";
-------------
-- Element --
-------------
function Get (Container : Holder) return Element_Type is
begin
return Cast (Container'Address).all;
end Get;
---------------------
-- Replace_Element --
---------------------
procedure Set (Container : in out Holder; New_Item : Element_Type) is
Storage : Storage_Array
(1 .. Size_In_Storage_Elements (New_Item)) with
Address => New_Item'Address;
begin
Container.Data (Storage'Range) := Storage;
end Set;
---------------
-- To_Holder --
---------------
function To_Holder (New_Item : Element_Type) return Holder is
begin
return Result : Holder do
Set (Result, New_Item);
end return;
end To_Holder;
end Ada.Containers.Bounded_Holders;

102
gcc/ada/a-coboho.ads Normal file
View File

@ -0,0 +1,102 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- A D A . C O N T A I N E R S . B O U N D E D _ H O L D E R S --
-- --
-- S p e c --
-- --
-- Copyright (C) 2014, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
private with System;
generic
type Element_Type (<>) is private;
Max_Size_In_Storage_Elements : Natural :=
Element_Type'Max_Size_In_Storage_Elements;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Bounded_Holders is
-- This package is patterned after Ada.Containers.Indefinite_Holders. It is
-- used to treat indefinite subtypes as definite, but without using heap
-- allocation. For example, you might like to say:
--
-- type A is array (...) of T'Class; -- illegal
--
-- Instead, you can instantiate this package with Element_Type => T'Class,
-- and say:
--
-- type A is array (...) of Holder;
--
-- Each object of type Holder is allocated Max_Size_In_Storage_Elements
-- bytes. If you try to create a holder from an object of type Element_Type
-- that is too big, an exception is raised. This applies to To_Holder and
-- Replace_Element. If you pass an Element_Type object that is smaller than
-- Max_Size_In_Storage_Elements, it works fine, but some space is wasted.
--
-- Element_Type must not be an unconstrained array type. It can be a
-- class-wide type or a type with non-defaulted discriminants.
--
-- The 'Size of each Element_Type object must be a multiple of
-- System.Storage_Unit; e.g. creating Holders from 5-bit objects won't
-- work.
type Holder is private;
function "=" (Left, Right : Holder) return Boolean;
function To_Holder (New_Item : Element_Type) return Holder;
function "+" (New_Item : Element_Type) return Holder renames To_Holder;
function Get (Container : Holder) return Element_Type;
procedure Set (Container : in out Holder; New_Item : Element_Type);
private
-- The implementation uses low-level tricks (Address clauses and unchecked
-- conversions of access types) to treat the elements as storage arrays.
pragma Assert (Element_Type'Alignment <= Standard'Maximum_Alignment);
-- This prevents elements with a user-specified Alignment that is too big
type Storage_Element is mod System.Storage_Unit;
type Storage_Array is array (Positive range <>) of Storage_Element;
type Holder is record
Data : Storage_Array (1 .. Max_Size_In_Storage_Elements);
end record
with Alignment => Standard'Maximum_Alignment;
-- We would like to say "Alignment => Element_Type'Alignment", but that
-- is illegal because it's not static, so we use the maximum possible
-- (default) alignment instead.
type Element_Access is access all Element_Type;
pragma Assert (Element_Access'Size = Standard'Address_Size,
"cannot instantiate with an array type");
-- If Element_Access is a fat pointer, Element_Type must be an
-- unconstrained array, which is not allowed. Arrays won't work, because
-- the 'Address of an array points to the first element, thus losing the
-- bounds.
end Ada.Containers.Bounded_Holders;

1230
gcc/ada/a-cofove.adb
View File

File diff suppressed because it is too large Load Diff

362
gcc/ada/a-cofove.ads
View File

@ -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;
-- In the bounded case, Capacity is the capacity of the container, which
-- never changes. In the unbounded case, Capacity is the initial capacity
-- of the container, and operations such as Reserve_Capacity and Append can
-- increase the capacity. The capacity never shrinks, except in the case of
-- Clear.
--
-- Note that all objects of type Vector are constrained, including in the
-- unbounded case; you can't assign from one object to another if the
-- Capacity is different.
type Cursor is private;
pragma Preelaborable_Initialization (Cursor);
Empty_Vector : constant Vector;
No_Element : constant Cursor;
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);
Pre => Index in First_Index (Container) .. Last_Index (Container);
procedure Replace_Element
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;
Position : Cursor;
New_Item : Element_Type)
with
Global => null,
Pre => Has_Element (Container, Position);
procedure Move (Target : in out Vector; Source : in out Vector) with
Global => null,
Pre => Length (Source) <= Target.Capacity;
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Vector)
with
Global => null,
Pre => First_Index (Container) <= Before
and then Before <= Last_Index (Container) + 1
and then Length (Container) < Container.Capacity;
procedure Insert
(Container : in out Vector;
Before : Cursor;
New_Item : Vector)
with
Global => null,
Pre => Length (Container) < Container.Capacity
and then (Has_Element (Container, Before)
or else Before = No_Element);
procedure Insert
(Container : in out Vector;
Before : Cursor;
New_Item : Vector;
Position : out Cursor)
with
Global => null,
Pre => Length (Container) < Container.Capacity
and then (Has_Element (Container, Before)
or else Before = No_Element);
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Element_Type;
Count : Count_Type := 1)
with
Global => null,
Pre => First_Index (Container) <= Before
and then Before <= Last_Index (Container) + 1
and then Length (Container) + Count <= Container.Capacity;
procedure Insert
(Container : in out Vector;
Before : Cursor;
New_Item : Element_Type;
Count : Count_Type := 1)
with
Global => null,
Pre => Length (Container) + Count <= Container.Capacity
and then (Has_Element (Container, Before)
or else Before = No_Element);
procedure Insert
(Container : in out Vector;
Before : Cursor;
New_Item : Element_Type;
Position : out Cursor;
Count : Count_Type := 1)
with
Global => null,
Pre => Length (Container) + Count <= Container.Capacity
and then (Has_Element (Container, Before)
or else Before = No_Element);
procedure Prepend
(Container : in out Vector;
New_Item : Vector)
with
Global => null,
Pre => Length (Container) < Container.Capacity;
procedure Prepend
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type := 1)
with
Global => null,
Pre => Length (Container) + Count <= Container.Capacity;
procedure Append
(Container : in out Vector;
New_Item : Vector)
with
Global => null,
Pre => Length (Container) < Container.Capacity;
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)
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;
type Elements_Array_Ptr is access all Elements_Array;
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;
type Cursor is record
Valid : Boolean := True;
Index : Index_Type := Index_Type'First;
end record;
-- 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.
Empty_Vector : constant Vector := (Capacity => 0, others => <>);
No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
function Empty_Vector return Vector is
((Capacity => 0, others => <>));
end Ada.Containers.Formal_Vectors;

33
gcc/ada/gnat_rm.texi
View File

@ -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})

2
gcc/ada/impunit.adb
View File

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

40
gcc/ada/prj-conf.adb
View File

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