[multiple changes]

2011-08-02  Yannick Moy  <moy@adacore.com>

	* errout.adb, errout.ads (Check_Formal_Restriction): move procedure
	from here...
	* restrict.adb, restrict.ads (Check_Formal_Restriction): ...to here
	* sem_aggr.adb, sem_ch5.adb, sem_util.adb:
	Add with/use clauses to make Check_Formal_Restriction visible

2011-08-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb (Check_Generic_Actuals): handle properly actual
	in-parameters when type of the generic formal is private in the generic
	spec and non-private in the body.

2011-08-02  Claire Dross  <dross@adacore.com>

	* a-cfdlli.adb, a-cfdlli.ads, a-cfhase.adb, a-cfhase.ads, a-cfhama.adb,
	a-cfhama.ads, a-cforse.adb, a-cforse.ads, a-cforma.adb, a-cforma.ads,
	a-cofove.adb, a-cofove.ads: New files implementing formal containers.
	* impunit.adb, Makefile.rtl: Take new files into account.

From-SVN: r177102

gcc/ada/ChangeLog

-2011-08-02  Vincent Celier  <celier@adacore.com>
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* errout.adb, errout.ads (Check_Formal_Restriction): move procedure
+	from here...
+	* restrict.adb, restrict.ads (Check_Formal_Restriction): ...to here
+	* sem_aggr.adb, sem_ch5.adb, sem_util.adb:
+	Add with/use clauses to make Check_Formal_Restriction visible
+
+2011-08-02  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch12.adb (Check_Generic_Actuals): handle properly actual
+	in-parameters when type of the generic formal is private in the generic
+	spec and non-private in the body.
+
+2011-08-02  Claire Dross  <dross@adacore.com>
 
-	* prj-nmsc.adb (Check_Library_Attributes): For virtual library project,
-	inherit library kind.
+	* a-cfdlli.adb, a-cfdlli.ads, a-cfhase.adb, a-cfhase.ads, a-cfhama.adb,
+	a-cfhama.ads, a-cforse.adb, a-cforse.ads, a-cforma.adb, a-cforma.ads,
+	a-cofove.adb, a-cofove.ads: New files implementing formal containers.
+	* impunit.adb, Makefile.rtl: Take new files into account.
 
 2011-08-02  Robert Dewar  <dewar@adacore.com>
 

gcc/ada/Makefile.rtl

@@ -92,6 +92,11 @@ GNATRTL_NONTASKING_OBJS= \
   a-cbdlli$(objext) \
   a-cborma$(objext) \
   a-cdlili$(objext) \
+  a-cfhama$(objext) \
+  a-cfhase$(objext) \
+  a-cforse$(objext) \
+  a-cfdlli$(objext) \
+  a-cforma$(objext) \
   a-cgaaso$(objext) \
   a-cgarso$(objext) \
   a-cgcaso$(objext) \
@@ -123,6 +128,7 @@ GNATRTL_NONTASKING_OBJS= \
   a-contai$(objext) \
   a-convec$(objext) \
   a-cobove$(objext) \
+  a-cofove$(objext) \
   a-coorma$(objext) \
   a-coormu$(objext) \
   a-coorse$(objext) \

gcc/ada/a-cfdlli.ads

+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                 ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS                --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2010, 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 Ada.Streams;
+with Ada.Containers; use Ada.Containers;
+
+generic
+   type Element_Type is private;
+
+   with function "=" (Left, Right : Element_Type)
+                      return Boolean is <>;
+
+package Ada.Containers.Formal_Doubly_Linked_Lists is
+   pragma Pure;
+
+   type List (Capacity : Count_Type) is tagged private;
+   --  pragma Preelaborable_Initialization (List);
+
+   type Cursor is private;
+   pragma Preelaborable_Initialization (Cursor);
+
+   Empty_List : constant List;
+
+   No_Element : constant Cursor;
+
+   function "=" (Left, Right : List) return Boolean;
+
+   function Length (Container : List) return Count_Type;
+
+   function Is_Empty (Container : List) return Boolean;
+
+   procedure Clear (Container : in out List);
+
+   procedure Assign (Target : in out List; Source : List);
+
+   function Copy (Source : List; Capacity : Count_Type := 0) return List;
+
+   function Element (Container : List; Position : Cursor) return Element_Type;
+
+   procedure Replace_Element
+     (Container : in out List;
+      Position  : Cursor;
+      New_Item  : Element_Type);
+
+   procedure Query_Element
+     (Container : List; Position : Cursor;
+      Process   : not null access procedure (Element : Element_Type));
+
+   procedure Update_Element
+     (Container : in out List;
+      Position  : Cursor;
+      Process   : not null access procedure (Element : in out Element_Type));
+
+   procedure Move (Target : in out List; Source : in out List);
+
+   procedure Insert
+     (Container : in out List;
+      Before    : Cursor;
+      New_Item  : Element_Type;
+      Count     : Count_Type := 1);
+
+   procedure Insert
+     (Container : in out List;
+      Before    : Cursor;
+      New_Item  : Element_Type;
+      Position  : out Cursor;
+      Count     : Count_Type := 1);
+
+   procedure Insert
+     (Container : in out List;
+      Before    : Cursor;
+      Position  : out Cursor;
+      Count     : Count_Type := 1);
+
+   procedure Prepend
+     (Container : in out List;
+      New_Item  : Element_Type;
+      Count     : Count_Type := 1);
+
+   procedure Append
+     (Container : in out List;
+      New_Item  : Element_Type;
+      Count     : Count_Type := 1);
+
+   procedure Delete
+     (Container : in out List;
+      Position  : in out Cursor;
+      Count     : Count_Type := 1);
+
+   procedure Delete_First
+     (Container : in out List;
+      Count     : Count_Type := 1);
+
+   procedure Delete_Last
+     (Container : in out List;
+      Count     : Count_Type := 1);
+
+   procedure Reverse_Elements (Container : in out List);
+
+   procedure Swap
+     (Container : in out List;
+      I, J      : Cursor);
+
+   procedure Swap_Links
+     (Container : in out List;
+      I, J      : Cursor);
+
+   procedure Splice
+     (Target : in out List;
+      Before : Cursor;
+      Source : in out List);
+
+   procedure Splice
+     (Target   : in out List;
+      Before   : Cursor;
+      Source   : in out List;
+      Position : in out Cursor);
+
+   procedure Splice
+     (Container : in out List;
+      Before    : Cursor;
+      Position  : Cursor);
+
+   function First (Container : List) return Cursor;
+
+   function First_Element (Container : List) return Element_Type;
+
+   function Last (Container : List) return Cursor;
+
+   function Last_Element (Container : List) return Element_Type;
+
+   function Next (Container : List; Position : Cursor) return Cursor;
+
+   procedure Next (Container : List; Position : in out Cursor);
+
+   function Previous (Container : List; Position : Cursor) return Cursor;
+
+   procedure Previous (Container : List; Position : in out Cursor);
+
+   function Find
+     (Container : List;
+      Item      : Element_Type;
+      Position  : Cursor := No_Element) return Cursor;
+
+   function Reverse_Find
+     (Container : List;
+      Item      : Element_Type;
+      Position  : Cursor := No_Element) return Cursor;
+
+   function Contains
+     (Container : List;
+      Item      : Element_Type) return Boolean;
+
+   function Has_Element (Container : List; Position : Cursor) return Boolean;
+
+   procedure Iterate
+     (Container : List;
+      Process   :
+      not null access procedure (Container : List; Position : Cursor));
+
+   procedure Reverse_Iterate
+     (Container : List;
+      Process   :
+      not null access procedure (Container : List; Position : Cursor));
+
+   generic
+      with function "<" (Left, Right : Element_Type) return Boolean is <>;
+   package Generic_Sorting is
+
+      function Is_Sorted (Container : List) return Boolean;
+
+      procedure Sort (Container : in out List);
+
+      procedure Merge (Target, Source : in out List);
+
+   end Generic_Sorting;
+
+   function Strict_Equal (Left, Right : List) return Boolean;
+
+   function Left (Container : List; Position : Cursor) return List;
+
+   function Right (Container : List; Position : Cursor) return List;
+
+private
+
+   type Node_Type is record
+      Prev    : Count_Type'Base := -1;
+      Next    : Count_Type;
+      Element : Element_Type;
+   end record;
+   function "=" (L, R : Node_Type) return Boolean is abstract;
+
+   type Node_Array is array (Count_Type range <>) of Node_Type;
+   function "=" (L, R : Node_Array) return Boolean is abstract;
+
+   type List_Access is access all List;
+   for List_Access'Storage_Size use 0;
+
+   type Kind is (Plain, Part);
+
+   type Plain_List (Capacity : Count_Type) is record
+      Nodes  : Node_Array (1 .. Capacity) := (others => <>);
+      Free   : Count_Type'Base := -1;
+      Busy   : Natural := 0;
+      Lock   : Natural := 0;
+   end record;
+
+   type PList_Access is access Plain_List;
+
+   type Part_List is record
+      LLength : Count_Type := 0;
+      LFirst  : Count_Type := 0;
+      LLast   : Count_Type := 0;
+   end record;
+
+   type List (Capacity : Count_Type) is tagged record
+      K      : Kind := Plain;
+      Length : Count_Type := 0;
+      First  : Count_Type := 0;
+      Last   : Count_Type := 0;
+      Part   : Part_List;
+      Plain  : PList_Access := new Plain_List'(Capacity, others => <>);
+   end record;
+
+   use Ada.Streams;
+
+   procedure Read
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : out List);
+
+   for List'Read use Read;
+
+   procedure Write
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : List);
+
+   for List'Write use Write;
+
+   type Cursor is
+      record
+         Node      : Count_Type := 0;
+      end record;
+
+   procedure Read
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : out Cursor);
+
+   for Cursor'Read use Read;
+
+   procedure Write
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : Cursor);
+
+   for Cursor'Write use Write;
+
+   Empty_List : constant List := (0, others => <>);
+
+   No_Element : constant Cursor := (Node => 0);
+
+end Ada.Containers.Formal_Doubly_Linked_Lists;

gcc/ada/a-cfhama.ads

+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--    A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ M A P S     --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2010, 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 Ada.Containers.Hash_Tables;
+private with Ada.Streams;
+with Ada.Containers; use Ada.Containers;
+
+generic
+   type Key_Type is private;
+   type Element_Type is private;
+
+   with function Hash (Key : Key_Type) return Hash_Type;
+   with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Formal_Hashed_Maps is
+   pragma Pure;
+
+   type Map (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
+   --  pragma Preelaborable_Initialization (Map);
+
+   type Cursor is private;
+   pragma Preelaborable_Initialization (Cursor);
+
+   Empty_Map : constant Map;
+
+   No_Element : constant Cursor;
+
+   function "=" (Left, Right : Map) return Boolean;
+
+   function Capacity (Container : Map) return Count_Type;
+
+   procedure Reserve_Capacity
+     (Container : in out Map;
+      Capacity  : Count_Type);
+
+   function Length (Container : Map) return Count_Type;
+
+   function Is_Empty (Container : Map) return Boolean;
+
+   --  ??? what does clear do to active elements?
+   procedure Clear (Container : in out Map);
+
+   procedure Assign (Target : in out Map; Source : Map);
+
+   --  ???
+   --  capacity=0 means use container.length as cap of tgt
+   --  modulos=0 means use default_modulous(container.length)
+   function Copy (Source   : Map;
+                  Capacity : Count_Type := 0) return Map;
+
+   function Key (Container : Map; Position : Cursor) return Key_Type;
+
+   function Element (Container : Map; Position : Cursor) return Element_Type;
+
+   procedure Replace_Element
+     (Container : in out Map;
+      Position  : Cursor;
+      New_Item  : Element_Type);
+
+   procedure Query_Element
+     (Container : in out Map;
+      Position  : Cursor;
+      Process   : not null access
+        procedure (Key : Key_Type; Element : Element_Type));
+
+   procedure Update_Element
+     (Container : in out Map;
+      Position  : Cursor;
+      Process   : not null access
+        procedure (Key : Key_Type; Element : in out Element_Type));
+
+   procedure Move (Target : in out Map; Source : in out Map);
+
+   procedure Insert
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type;
+      Position  : out Cursor;
+      Inserted  : out Boolean);
+
+   procedure Insert
+     (Container : in out Map;
+      Key       : Key_Type;
+      Position  : out Cursor;
+      Inserted  : out Boolean);
+
+   procedure Insert
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type);
+
+   procedure Include
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type);
+
+   procedure Replace
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type);
+
+   procedure Exclude (Container : in out Map; Key : Key_Type);
+
+   procedure Delete (Container : in out Map; Key : Key_Type);
+
+   procedure Delete (Container : in out Map; Position : in out Cursor);
+
+   function First (Container : Map) return Cursor;
+
+   function Next (Container : Map; Position : Cursor) return Cursor;
+
+   procedure Next (Container : Map; Position : in out Cursor);
+
+   function Find (Container : Map; Key : Key_Type) return Cursor;
+
+   function Contains (Container : Map; Key : Key_Type) return Boolean;
+
+   function Element (Container : Map; Key : Key_Type) return Element_Type;
+
+   function Has_Element (Container : Map; Position : Cursor) return Boolean;
+
+   function Equivalent_Keys
+     (Left   : Map;
+      CLeft  : Cursor;
+      Right  : Map;
+      CRight : Cursor) return Boolean;
+
+   function Equivalent_Keys
+     (Left  : Map;
+      CLeft : Cursor;
+      Right : Key_Type) return Boolean;
+
+   function Equivalent_Keys
+     (Left   : Key_Type;
+      Right  : Map;
+      CRight : Cursor) return Boolean;
+
+   procedure Iterate
+     (Container : Map;
+      Process   :
+        not null access procedure (Container : Map; Position : Cursor));
+
+   function Default_Modulus (Capacity : Count_Type) return Hash_Type;
+
+   function Strict_Equal (Left, Right : Map) return Boolean;
+
+   function Left (Container : Map; Position : Cursor) return Map;
+
+   function Right (Container : Map; Position : Cursor) return Map;
+
+   function Overlap (Left, Right : Map) return Boolean;
+
+private
+   --  pragma Inline ("=");
+   pragma Inline (Length);
+   pragma Inline (Is_Empty);
+   pragma Inline (Clear);
+   pragma Inline (Key);
+   pragma Inline (Element);
+   --  pragma Inline (Move);  ???
+   pragma Inline (Contains);
+   pragma Inline (Capacity);
+   --  pragma Inline (Reserve_Capacity);  ???
+   pragma Inline (Has_Element);
+   pragma Inline (Equivalent_Keys);
+   pragma Inline (Next);
+
+   type Node_Type is record
+      Key         : Key_Type;
+      Element     : Element_Type;
+      Next        : Count_Type;
+      Has_Element : Boolean := False;
+   end record;
+
+   package HT_Types is new
+     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types
+     (Node_Type);
+
+   type HT_Access is access all HT_Types.Hash_Table_Type;
+
+   type Kind is (Plain, Part);
+
+   type Map (Capacity : Count_Type; Modulus : Hash_Type) is tagged record
+      HT     : HT_Access := new HT_Types.Hash_Table_Type (Capacity, Modulus);
+      K      : Kind := Plain;
+      Length : Count_Type := 0;
+      First  : Count_Type := 0;
+      Last   : Count_Type := 0;
+   end record;
+
+   use HT_Types;
+   use Ada.Streams;
+
+   procedure Write
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : Map);
+
+   for Map'Write use Write;
+
+   procedure Read
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : out Map);
+
+   for Map'Read use Read;
+
+   type Map_Access is access all Map;
+   for Map_Access'Storage_Size use 0;
+
+   type Cursor is
+      record
+         Node      : Count_Type;
+      end record;
+
+   procedure Read
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : out Cursor);
+
+   for Cursor'Read use Read;
+
+   procedure Write
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : Cursor);
+
+   for Cursor'Write use Write;
+
+   Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
+
+   No_Element : constant Cursor := (Node => 0);
+
+end Ada.Containers.Formal_Hashed_Maps;

gcc/ada/a-cfhase.ads

+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--    A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ S E T S     --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2010, 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 Ada.Containers.Hash_Tables;
+private with Ada.Streams;
+
+with Ada.Containers;
+use Ada.Containers;
+
+generic
+   type Element_Type is private;
+
+   with function Hash (Element : Element_Type) return Hash_Type;
+
+   with function Equivalent_Elements (Left, Right : Element_Type)
+                                      return Boolean;
+
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Formal_Hashed_Sets is
+   pragma Pure;
+
+   type Set (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
+   --  pragma Preelaborable_Initialization (Set);
+
+   type Cursor is private;
+   pragma Preelaborable_Initialization (Cursor);
+
+   Empty_Set : constant Set;
+
+   No_Element : constant Cursor;
+
+   function "=" (Left, Right : Set) return Boolean;
+
+   function Equivalent_Sets (Left, Right : Set) return Boolean;
+
+   function To_Set (New_Item : Element_Type) return Set;
+
+   function Capacity (Container : Set) return Count_Type;
+
+   procedure Reserve_Capacity
+     (Container : in out Set;
+      Capacity  : Count_Type);
+
+   function Length (Container : Set) return Count_Type;
+
+   function Is_Empty (Container : Set) return Boolean;
+
+   procedure Clear (Container : in out Set);
+
+   procedure Assign (Target : in out Set; Source : Set);
+
+   function Copy (Source   : Set;
+                  Capacity : Count_Type := 0) return Set;
+
+   function Element (Container : Set; Position : Cursor) return Element_Type;
+
+   procedure Replace_Element
+     (Container : in out Set;
+      Position  : Cursor;
+      New_Item  : Element_Type);
+
+   procedure Query_Element
+     (Container : in out Set;
+      Position  : Cursor;
+      Process   : not null access procedure (Element : Element_Type));
+
+   procedure Move (Target : in out Set; Source : in out Set);
+
+   procedure Insert
+     (Container : in out Set;
+      New_Item  : Element_Type;
+      Position  : out Cursor;
+      Inserted  : out Boolean);
+
+   procedure Insert  (Container : in out Set; New_Item : Element_Type);
+
+   procedure Include (Container : in out Set; New_Item : Element_Type);
+
+   procedure Replace (Container : in out Set; New_Item : Element_Type);
+
+   procedure Exclude (Container : in out Set; Item     : Element_Type);
+
+   procedure Delete  (Container : in out Set; Item     : Element_Type);
+
+   procedure Delete (Container : in out Set; Position  : in out Cursor);
+
+   procedure Union (Target : in out Set; Source : Set);
+
+   function Union (Left, Right : Set) return Set;
+
+   function "or" (Left, Right : Set) return Set renames Union;
+
+   procedure Intersection (Target : in out Set; Source : Set);
+
+   function Intersection (Left, Right : Set) return Set;
+
+   function "and" (Left, Right : Set) return Set renames Intersection;
+
+   procedure Difference (Target : in out Set; Source : Set);
+
+   function Difference (Left, Right : Set) return Set;
+
+   function "-" (Left, Right : Set) return Set renames Difference;
+
+   procedure Symmetric_Difference (Target : in out Set; Source : Set);
+
+   function Symmetric_Difference (Left, Right : Set) return Set;
+
+   function "xor" (Left, Right : Set) return Set
+                   renames Symmetric_Difference;
+
+   function Overlap (Left, Right : Set) return Boolean;
+
+   function Is_Subset (Subset : Set; Of_Set : Set) return Boolean;
+
+   function First (Container : Set) return Cursor;
+
+   function Next (Container : Set; Position : Cursor) return Cursor;
+
+   procedure Next (Container : Set; Position : in out Cursor);
+
+   function Find
+     (Container : Set;
+      Item      : Element_Type) return Cursor;
+
+   function Contains (Container : Set; Item : Element_Type) return Boolean;
+
+   function Has_Element (Container : Set; Position : Cursor) return Boolean;
+
+   function Equivalent_Elements (Left  : Set; CLeft : Cursor;
+                                 Right : Set; CRight : Cursor) return Boolean;
+
+   function Equivalent_Elements
+     (Left  : Set; CLeft : Cursor;
+      Right : Element_Type) return Boolean;
+
+   function Equivalent_Elements
+     (Left  : Element_Type;
+      Right : Set; CRight : Cursor) return Boolean;
+
+   procedure Iterate
+     (Container : Set;
+      Process   :
+        not null access procedure (Container : Set; Position : Cursor));
+
+   function Default_Modulus (Capacity : Count_Type) return Hash_Type;
+
+   generic
+      type Key_Type (<>) is private;
+
+      with function Key (Element : Element_Type) return Key_Type;
+
+      with function Hash (Key : Key_Type) return Hash_Type;
+
+      with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+
+   package Generic_Keys is
+
+      function Key (Container : Set; Position : Cursor) return Key_Type;
+
+      function Element (Container : Set; Key : Key_Type) return Element_Type;
+
+      procedure Replace
+        (Container : in out Set;
+         Key       : Key_Type;
+         New_Item  : Element_Type);
+
+      procedure Exclude (Container : in out Set; Key : Key_Type);
+
+      procedure Delete (Container : in out Set; Key : Key_Type);
+
+      function Find (Container : Set; Key : Key_Type) return Cursor;
+
+      function Contains (Container : Set; Key : Key_Type) return Boolean;
+
+      procedure Update_Element_Preserving_Key
+        (Container : in out Set;
+         Position  : Cursor;
+         Process   : not null access
+           procedure (Element : in out Element_Type));
+
+   end Generic_Keys;
+
+   function Strict_Equal (Left, Right : Set) return Boolean;
+
+   function Left (Container : Set; Position : Cursor) return Set;
+
+   function Right (Container : Set; Position : Cursor) return Set;
+
+private
+
+   pragma Inline (Next);
+
+   type Node_Type is
+      record
+         Element     : Element_Type;
+         Next        : Count_Type;
+         Has_Element : Boolean := False;
+      end record;
+
+   package HT_Types is
+     new Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types
+     (Node_Type);
+
+   type HT_Access is access all HT_Types.Hash_Table_Type;
+
+   type Kind is (Plain, Part);
+
+   type Set (Capacity : Count_Type; Modulus : Hash_Type) is tagged record
+      HT     : HT_Access :=
+                 new HT_Types.Hash_Table_Type'(Capacity, Modulus,
+                                               others => <>);
+      K      : Kind := Plain;
+      Length : Count_Type := 0;
+      First  : Count_Type := 0;
+      Last   : Count_Type := 0;
+   end record;
+
+   use HT_Types;
+   use Ada.Streams;
+
+   type Cursor is
+      record
+         Node      : Count_Type;
+      end record;
+
+   procedure Write
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : Cursor);
+
+   for Cursor'Write use Write;
+
+   procedure Read
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : out Cursor);
+
+   for Cursor'Read use Read;
+
+   No_Element : constant Cursor := (Node => 0);
+
+   procedure Write
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : Set);
+
+   for Set'Write use Write;
+
+   procedure Read
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : out Set);
+
+   for Set'Read use Read;
+
+   Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>);
+
+end Ada.Containers.Formal_Hashed_Sets;

gcc/ada/a-cforma.ads

+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--   A D A . C O N T A I N E R S . F O R M A L _ O R D E R E D _ M A P S    --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2010, 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 Ada.Containers.Red_Black_Trees;
+private with Ada.Streams;
+with Ada.Containers; use Ada.Containers;
+
+generic
+   type Key_Type is private;
+   type Element_Type is private;
+
+   with function "<" (Left, Right : Key_Type) return Boolean is <>;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Formal_Ordered_Maps is
+   pragma Pure;
+
+   function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+
+   type Map (Capacity : Count_Type) is tagged private;
+   --  pragma Preelaborable_Initialization (Map);
+
+   type Cursor is private;
+   pragma Preelaborable_Initialization (Cursor);
+
+   Empty_Map : constant Map;
+
+   No_Element : constant Cursor;
+
+   function "=" (Left, Right : Map) return Boolean;
+
+   function Length (Container : Map) return Count_Type;
+
+   function Is_Empty (Container : Map) return Boolean;
+
+   procedure Clear (Container : in out Map);
+
+   procedure Assign (Target : in out Map; Source : Map);
+
+   function Copy (Source : Map; Capacity : Count_Type := 0) return Map;
+
+   function Key (Container : Map; Position : Cursor) return Key_Type;
+
+   function Element (Container : Map; Position : Cursor) return Element_Type;
+
+   procedure Replace_Element
+     (Container : in out Map;
+      Position  : Cursor;
+      New_Item  : Element_Type);
+
+   procedure Query_Element
+     (Container : in out Map;
+      Position  : Cursor;
+      Process   : not null access
+        procedure (Key : Key_Type; Element : Element_Type));
+
+   procedure Update_Element
+     (Container : in out Map;
+      Position  : Cursor;
+      Process   : not null access
+        procedure (Key : Key_Type; Element : in out Element_Type));
+
+   procedure Move (Target : in out Map; Source : in out Map);
+
+   procedure Insert
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type;
+      Position  : out Cursor;
+      Inserted  : out Boolean);
+
+   procedure Insert
+     (Container : in out Map;
+      Key       : Key_Type;
+      Position  : out Cursor;
+      Inserted  : out Boolean);
+
+   procedure Insert
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type);
+
+   procedure Include
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type);
+
+   procedure Replace
+     (Container : in out Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type);
+
+   procedure Exclude (Container : in out Map; Key : Key_Type);
+
+   procedure Delete (Container : in out Map; Key : Key_Type);
+
+   procedure Delete (Container : in out Map; Position : in out Cursor);
+
+   procedure Delete_First (Container : in out Map);
+
+   procedure Delete_Last (Container : in out Map);
+
+   function First (Container : Map) return Cursor;
+
+   function First_Element (Container : Map) return Element_Type;
+
+   function First_Key (Container : Map) return Key_Type;
+
+   function Last (Container : Map) return Cursor;
+
+   function Last_Element (Container : Map) return Element_Type;
+
+   function Last_Key (Container : Map) return Key_Type;
+
+   function Next (Container : Map; Position : Cursor) return Cursor;
+
+   procedure Next (Container : Map; Position : in out Cursor);
+
+   function Previous (Container : Map; Position : Cursor) return Cursor;
+
+   procedure Previous (Container : Map; Position : in out Cursor);
+
+   function Find (Container : Map; Key : Key_Type) return Cursor;
+
+   function Element (Container : Map; Key : Key_Type) return Element_Type;
+
+   function Floor (Container : Map; Key : Key_Type) return Cursor;
+
+   function Ceiling (Container : Map; Key : Key_Type) return Cursor;
+
+   function Contains (Container : Map; Key : Key_Type) return Boolean;
+
+   function Has_Element (Container : Map; Position : Cursor) return Boolean;
+
+   procedure Iterate
+     (Container : Map;
+      Process   :
+        not null access procedure (Container : Map; Position : Cursor));
+
+   procedure Reverse_Iterate
+     (Container : Map;
+      Process   :
+        not null access procedure (Container : Map; Position : Cursor));
+
+   function Strict_Equal (Left, Right : Map) return Boolean;
+
+   function Left (Container : Map; Position : Cursor) return Map;
+
+   function Right (Container : Map; Position : Cursor) return Map;
+
+   function Overlap (Left, Right : Map) return Boolean;
+
+private
+
+   pragma Inline (Next);
+   pragma Inline (Previous);
+
+   subtype Node_Access is Count_Type;
+
+   use Red_Black_Trees;
+
+   type Node_Type is record
+      Has_Element : Boolean := False;
+      Parent  : Node_Access;
+      Left    : Node_Access;
+      Right   : Node_Access;
+      Color   : Red_Black_Trees.Color_Type := Red;
+      Key     : Key_Type;
+      Element : Element_Type;
+   end record;
+
+   type Kind is (Plain, Part);
+
+   package Tree_Types is
+     new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
+
+   type Tree_Type_Access is access all Tree_Types.Tree_Type;
+
+   type Map (Capacity : Count_Type) is tagged record
+      Tree   : Tree_Type_Access := new Tree_Types.Tree_Type (Capacity);
+      K      : Kind := Plain;
+      Length : Count_Type := 0;
+      First  : Count_Type := 0;
+      Last   : Count_Type := 0;
+   end record;
+
+   use Ada.Streams;
+
+   type Map_Access is access all Map;
+   for Map_Access'Storage_Size use 0;
+
+   type Cursor is record
+      Node      : Node_Access;
+   end record;
+
+   procedure Write
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : Cursor);
+
+   for Cursor'Write use Write;
+
+   procedure Read
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : out Cursor);
+
+   for Cursor'Read use Read;
+
+   No_Element : constant Cursor := (Node => 0);
+
+   procedure Write
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : Map);
+
+   for Map'Write use Write;
+
+   procedure Read
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : out Map);
+
+   for Map'Read use Read;
+
+   Empty_Map : constant Map := (Capacity => 0, others => <>);
+
+end Ada.Containers.Formal_Ordered_Maps;

gcc/ada/a-cforse.ads

+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--   A D A . C O N T A I N E R S . F O R M A L _ O R D E R E D _ S E T S    --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2010, 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 Ada.Containers.Red_Black_Trees;
+private with Ada.Streams;
+
+with Ada.Containers;
+use Ada.Containers;
+
+generic
+   type Element_Type is private;
+
+   with function "<" (Left, Right : Element_Type) return Boolean is <>;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Formal_Ordered_Sets is
+   pragma Pure;
+
+   function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
+
+   type Set (Capacity : Count_Type) is tagged private;
+   --  pragma Preelaborable_Initialization (Set);
+
+   type Cursor is private;
+   pragma Preelaborable_Initialization (Cursor);
+
+   Empty_Set : constant Set;
+
+   No_Element : constant Cursor;
+
+   function "=" (Left, Right : Set) return Boolean;
+
+   function Equivalent_Sets (Left, Right : Set) return Boolean;
+
+   function To_Set (New_Item : Element_Type) return Set;
+
+   function Length (Container : Set) return Count_Type;
+
+   function Is_Empty (Container : Set) return Boolean;
+
+   procedure Clear (Container : in out Set);
+
+   procedure Assign (Target : in out Set; Source : Set);
+
+   function Copy (Source : Set; Capacity : Count_Type := 0) return Set;
+
+   function Element (Container : Set; Position : Cursor) return Element_Type;
+
+   procedure Replace_Element
+     (Container : in out Set;
+      Position  : Cursor;
+      New_Item  : Element_Type);
+
+   procedure Query_Element
+     (Container : in out Set;
+      Position  : Cursor;
+      Process   : not null access procedure (Element : Element_Type));
+
+   procedure Move (Target : in out Set; Source : in out Set);
+
+   procedure Insert
+     (Container : in out Set;
+      New_Item  : Element_Type;
+      Position  : out Cursor;
+      Inserted  : out Boolean);
+
+   procedure Insert
+     (Container : in out Set;
+      New_Item  : Element_Type);
+
+   procedure Include
+     (Container : in out Set;
+      New_Item  : Element_Type);
+
+   procedure Replace
+     (Container : in out Set;
+      New_Item  : Element_Type);
+
+   procedure Exclude
+     (Container : in out Set;
+      Item      : Element_Type);
+
+   procedure Delete
+     (Container : in out Set;
+      Item      : Element_Type);
+
+   procedure Delete
+     (Container : in out Set;
+      Position  : in out Cursor);
+
+   procedure Delete_First (Container : in out Set);
+
+   procedure Delete_Last (Container : in out Set);
+
+   procedure Union (Target : in out Set; Source : Set);
+
+   function Union (Left, Right : Set) return Set;
+
+   function "or" (Left, Right : Set) return Set renames Union;
+
+   procedure Intersection (Target : in out Set; Source : Set);
+
+   function Intersection (Left, Right : Set) return Set;
+
+   function "and" (Left, Right : Set) return Set renames Intersection;
+
+   procedure Difference (Target : in out Set; Source : Set);
+
+   function Difference (Left, Right : Set) return Set;
+
+   function "-" (Left, Right : Set) return Set renames Difference;
+
+   procedure Symmetric_Difference (Target : in out Set; Source : Set);
+
+   function Symmetric_Difference (Left, Right : Set) return Set;
+
+   function "xor" (Left, Right : Set) return Set renames Symmetric_Difference;
+
+   function Overlap (Left, Right : Set) return Boolean;
+
+   function Is_Subset (Subset : Set; Of_Set : Set) return Boolean;
+
+   function First (Container : Set) return Cursor;
+
+   function First_Element (Container : Set) return Element_Type;
+
+   function Last (Container : Set) return Cursor;
+
+   function Last_Element (Container : Set) return Element_Type;
+
+   function Next (Container : Set; Position : Cursor) return Cursor;
+
+   procedure Next (Container : Set; Position : in out Cursor);
+
+   function Previous (Container : Set; Position : Cursor) return Cursor;
+
+   procedure Previous (Container : Set; Position : in out Cursor);
+
+   function Find (Container : Set; Item : Element_Type) return Cursor;
+
+   function Floor (Container : Set; Item : Element_Type) return Cursor;
+
+   function Ceiling (Container : Set; Item : Element_Type) return Cursor;
+
+   function Contains (Container : Set; Item : Element_Type) return Boolean;
+
+   function Has_Element (Container : Set; Position : Cursor) return Boolean;
+
+   procedure Iterate
+     (Container : Set;
+      Process   :
+        not null access procedure (Container : Set; Position : Cursor));
+
+   procedure Reverse_Iterate
+     (Container : Set;
+      Process   :
+        not null access procedure (Container : Set; Position : Cursor));
+
+   generic
+      type Key_Type (<>) is private;
+
+      with function Key (Element : Element_Type) return Key_Type;
+
+      with function "<" (Left, Right : Key_Type) return Boolean is <>;
+
+   package Generic_Keys is
+
+      function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+
+      function Key (Container : Set; Position : Cursor) return Key_Type;
+
+      function Element (Container : Set; Key : Key_Type) return Element_Type;
+
+      procedure Replace
+        (Container : in out Set;
+         Key       : Key_Type;
+         New_Item  : Element_Type);
+
+      procedure Exclude (Container : in out Set; Key : Key_Type);
+
+      procedure Delete (Container : in out Set; Key : Key_Type);
+
+      function Find (Container : Set; Key : Key_Type) return Cursor;
+
+      function Floor (Container : Set; Key : Key_Type) return Cursor;
+
+      function Ceiling (Container : Set; Key : Key_Type) return Cursor;
+
+      function Contains (Container : Set; Key : Key_Type) return Boolean;
+
+      procedure Update_Element_Preserving_Key
+        (Container : in out Set;
+         Position  : Cursor;
+         Process   : not null access
+           procedure (Element : in out Element_Type));
+
+   end Generic_Keys;
+
+   function Strict_Equal (Left, Right : Set) return Boolean;
+
+   function Left (Container : Set; Position : Cursor) return Set;
+
+   function Right (Container : Set; Position : Cursor) return Set;
+
+private
+
+   pragma Inline (Next);
+   pragma Inline (Previous);
+
+   type Node_Type is record
+      Has_Element : Boolean := False;
+      Parent  : Count_Type;
+      Left    : Count_Type;
+      Right   : Count_Type;
+      Color   : Red_Black_Trees.Color_Type;
+      Element : Element_Type;
+   end record;
+
+   type Kind is (Plain, Part);
+
+   package Tree_Types is
+     new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
+
+   type Tree_Type_Access is access all Tree_Types.Tree_Type;
+
+   type Set (Capacity : Count_Type) is tagged record
+      Tree   : Tree_Type_Access := new Tree_Types.Tree_Type (Capacity);
+      K      : Kind := Plain;
+      Length : Count_Type := 0;
+      First  : Count_Type := 0;
+      Last   : Count_Type := 0;
+   end record;
+
+   use Red_Black_Trees;
+   use Ada.Streams;
+
+   type Set_Access is access all Set;
+   for Set_Access'Storage_Size use 0;
+
+   type Cursor is record
+      Node      : Count_Type;
+   end record;
+
+   procedure Write
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : Cursor);
+
+   for Cursor'Write use Write;
+
+   procedure Read
+     (Stream : not null access Root_Stream_Type'Class;
+      Item   : out Cursor);
+
+   for Cursor'Read use Read;
+
+   No_Element : constant Cursor := (Node => 0);
+
+   procedure Write
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : Set);
+
+   for Set'Write use Write;
+
+   procedure Read
+     (Stream    : not null access Root_Stream_Type'Class;
+      Container : out Set);
+
+   for Set'Read use Read;
+
+   Empty_Set : constant Set :=
+                 (Capacity => 0, others => <>);
+
+end Ada.Containers.Formal_Ordered_Sets;

gcc/ada/errout.adb

@@ -224,19 +224,6 @@ package body Errout is
       end if;
    end Change_Error_Text;
 
-   ------------------------------
-   -- Check_Formal_Restriction --
-   ------------------------------
-
-   procedure Check_Formal_Restriction (Msg : String; N : Node_Id) is
-   begin
-      if Formal_Verification_Mode
-        and then Comes_From_Source (Original_Node (N))
-      then
-         Error_Msg_F ("|~~" & Msg, N);
-      end if;
-   end Check_Formal_Restriction;
-
    ------------------------
    -- Compilation_Errors --
    ------------------------

gcc/ada/errout.ads

@@ -740,13 +740,6 @@ package Errout is
    --  the given text. This text may contain insertion characters in the
    --  usual manner, and need not be the same length as the original text.
 
-   procedure Check_Formal_Restriction (Msg : String; N : Node_Id);
-   --  Provides a wrappper on Error_Msg_F which prepends the special characters
-   --  "|~~" (error not serious, language prepended) provided:
-   --  * the current mode is formal verification.
-   --  * the node N comes originally from source.
-   --  Otherwise, does nothing.
-
    function First_Node (C : Node_Id) return Node_Id;
    --  Given a construct C, finds the first node in the construct, i.e. the
    --  one with the lowest Sloc value. This is useful in placing error msgs.

gcc/ada/impunit.adb

@@ -512,7 +512,13 @@ package body Impunit is
      "a-cborse",    -- Ada.Containers.Bounded_Ordered_Sets
      "a-cborma",    -- Ada.Containers.Bounded_Ordered_Maps
      "a-cbhase",    -- Ada.Containers.Bounded_Hashed_Sets
-     "a-cbhama");   -- Ada.Containers.Bounded_Hashed_Maps
+     "a-cbhama",    -- Ada.Containers.Bounded_Hashed_Maps
+     "a-cofove",    -- Ada.Containers.Formal_Vectors
+     "a-cfdlli",    -- Ada.Containers.Formal_Doubly_Linked_Lists
+     "a-cforse",    -- Ada.Containers.Formal_Ordered_Sets
+     "a-cforma",    -- Ada.Containers.Formal_Ordered_Maps
+     "a-cfhase",    -- Ada.Containers.Formal_Hashed_Sets
+     "a-cfhama");   -- Ada.Containers.Formal_Hashed_Maps
 
    -----------------------
    -- Alternative Units --

gcc/ada/restrict.adb

@@ -105,6 +105,19 @@ package body Restrict is
       Check_Restriction (No_Elaboration_Code, N);
    end Check_Elaboration_Code_Allowed;
 
+   ------------------------------
+   -- Check_Formal_Restriction --
+   ------------------------------
+
+   procedure Check_Formal_Restriction (Msg : String; N : Node_Id) is
+   begin
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+      then
+         Error_Msg_F ("|~~" & Msg, N);
+      end if;
+   end Check_Formal_Restriction;
+
    -----------------------------------------
    -- Check_Implicit_Dynamic_Code_Allowed --
    -----------------------------------------

gcc/ada/restrict.ads

@@ -219,6 +219,12 @@ package Restrict is
    --  an elaboration routine. If elaboration code is not allowed, an error
    --  message is posted on the node given as argument.
 
+   procedure Check_Formal_Restriction (Msg : String; N : Node_Id);
+   --  Provides a wrappper on Error_Msg_F which prepends the special characters
+   --  "|~~" (error not serious, language prepended) provided the current mode
+   --  is formal verification and the node N comes originally from source.
+   --  Otherwise, does nothing.
+
    procedure Check_Implicit_Dynamic_Code_Allowed (N : Node_Id);
    --  Tests to see if dynamic code generation (dynamically generated
    --  trampolines, in particular) is allowed by the current restrictions

gcc/ada/sem_aggr.adb

@@ -40,6 +40,7 @@ with Namet.Sp; use Namet.Sp;
 with Nmake;    use Nmake;
 with Nlists;   use Nlists;
 with Opt;      use Opt;
+with Restrict; use Restrict;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Cat;  use Sem_Cat;
@@ -1098,10 +1099,11 @@ package body Sem_Aggr is
       end if;
 
       --  An unqualified aggregate is restricted in SPARK or ALFA to:
-      --  * an 'aggregate item' inside an aggregate for a multi-dimensional
-      --    array.
-      --  * an expression being assigned to an unconstrained array, but only
-      --    if the aggregate specifies a value for OTHERS only.
+
+      --    An aggregate item inside an aggregate for a multi-dimensional array
+
+      --    An expression being assigned to an unconstrained array, but only if
+      --    the aggregate specifies a value for OTHERS only.
 
       if Nkind (Parent (N)) /= N_Qualified_Expression then
          if Is_Array_Type (Etype (N)) then
@@ -1114,7 +1116,7 @@ package body Sem_Aggr is
                end if;
 
                --  The following check is disabled until a proper place is
-               --  found where the type of the parent node can be inspected.
+               --  found where the type of the parent node can be inspected???
 
 --              elsif not (Nkind (Parent (N)) = N_Aggregate
 --                         and then Is_Array_Type (Etype (Parent (N)))
@@ -1130,10 +1132,12 @@ package body Sem_Aggr is
             Check_Formal_Restriction
               ("record aggregate should be qualified", N);
 
-            --  The type of aggregate is neither array nor record, so an error
-            --  must have occurred during resolution. Do not report an
-            --  additional message here.
+         --  The type of aggregate is neither array nor record, so an error
+         --  must have occurred during resolution. Do not report an additional
+         --  message here.
 
+         else
+            null;
          end if;
       end if;
 
@@ -1145,8 +1149,7 @@ package body Sem_Aggr is
       if Raises_Constraint_Error (N) then
          Aggr_Subtyp := Etype (N);
          Rewrite (N,
-           Make_Raise_Constraint_Error (Loc,
-             Reason => CE_Range_Check_Failed));
+           Make_Raise_Constraint_Error (Loc, Reason => CE_Range_Check_Failed));
          Set_Raises_Constraint_Error (N);
          Set_Etype (N, Aggr_Subtyp);
          Set_Analyzed (N);
@@ -3112,9 +3115,9 @@ package body Sem_Aggr is
 
    begin
       --  A record aggregate is restricted in SPARK or ALFA:
-      --  * each named association can have only a single choice.
-      --  * OTHERS cannot be used.
-      --  * positional and named associations cannot be mixed.
+      --    Each named association can have only a single choice.
+      --    OTHERS cannot be used.
+      --    Positional and named associations cannot be mixed.
 
       if Present (Component_Associations (N))
         and then Present (First (Component_Associations (N)))
@@ -3128,19 +3131,21 @@ package body Sem_Aggr is
 
          declare
             Assoc : Node_Id;
+
          begin
             Assoc := First (Component_Associations (N));
-
             while Present (Assoc) loop
                if List_Length (Choices (Assoc)) > 1 then
                   Check_Formal_Restriction
                     ("component association in record aggregate must "
                      & "contain a single choice", Assoc);
                end if;
+
                if Nkind (First (Choices (Assoc))) = N_Others_Choice then
                   Check_Formal_Restriction
                     ("record aggregate cannot contain OTHERS", Assoc);
                end if;
+
                Assoc := Next (Assoc);
             end loop;
          end;

gcc/ada/sem_ch12.adb

@@ -4966,6 +4966,7 @@ package body Sem_Ch12 is
             else
                Check_Private_View (Subtype_Indication (Parent (E)));
             end if;
+
             Set_Is_Generic_Actual_Type (E, True);
             Set_Is_Hidden (E, False);
             Set_Is_Potentially_Use_Visible (E,
@@ -5054,6 +5055,63 @@ package body Sem_Ch12 is
             Set_Is_Hidden (E, False);
          end if;
 
+         if Ekind (E) = E_Constant then
+
+            --  If the type of the actual is a private type declared in the
+            --  enclosing scope of the generic unit, the body of the generic
+            --  sees the full view of the type (because it has to appear in
+            --  the corresponding package body). If the type is private now,
+            --  exchange views to restore the proper visiblity in the instance.
+
+            declare
+               Typ          : constant Entity_Id := Base_Type (Etype (E));
+               --  The type of the actual
+
+               Gen_Id       : Entity_Id;
+               --  The generic unit
+
+               Parent_Scope : Entity_Id;
+               --  The enclosing scope of the generic unit
+
+            begin
+               if Is_Wrapper_Package (Instance) then
+                  Gen_Id :=
+                     Generic_Parent
+                       (Specification
+                         (Unit_Declaration_Node
+                           (Related_Instance (Instance))));
+               else
+                  Gen_Id :=
+                    Generic_Parent
+                      (Specification (Unit_Declaration_Node (Instance)));
+               end if;
+
+               Parent_Scope := Scope (Gen_Id);
+
+               --  The exchange is only needed if the generic is defined
+               --  within a package which is not a common ancestor of the
+               --  scope of the instance, and is not already in scope.
+
+               if Is_Private_Type (Typ)
+                 and then Scope (Typ) = Parent_Scope
+                 and then Scope (Instance) /= Parent_Scope
+                 and then Ekind (Parent_Scope) = E_Package
+                 and then not Is_Child_Unit (Gen_Id)
+               then
+                  Switch_View (Typ);
+
+                  --  If the type of the entity is a subtype, it may also
+                  --  have to be made visible, together with the base type
+                  --  of its full view, after exchange.
+
+                  if Is_Private_Type (Etype (E)) then
+                     Switch_View (Etype (E));
+                     Switch_View (Base_Type (Etype (E)));
+                  end if;
+               end if;
+            end;
+         end if;
+
          Next_Entity (E);
       end loop;
    end Check_Generic_Actuals;

gcc/ada/sem_ch5.adb

@@ -36,6 +36,7 @@ with Namet;    use Namet;
 with Nlists;   use Nlists;
 with Nmake;    use Nmake;
 with Opt;      use Opt;
+with Restrict; use Restrict;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
@@ -1860,8 +1861,9 @@ package body Sem_Ch5 is
                --  SPARK or ALFA.
 
                if Nkind (DS) = N_Range then
-                  Check_Formal_Restriction ("loop parameter specification "
-                                            & "must include subtype mark", N);
+                  Check_Formal_Restriction
+                    ("loop parameter specification must include subtype mark",
+                     N);
                end if;
 
                --  Now analyze the subtype definition. If it is a range, create

gcc/ada/sem_util.adb

@@ -40,6 +40,7 @@ with Lib.Xref; use Lib.Xref;
 with Nlists;   use Nlists;
 with Output;   use Output;
 with Opt;      use Opt;
+with Restrict; use Restrict;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;