exp_ch6.adb (Expand_N_Extended_Return_Statement): Use New_Copy_Tree instead of Relocate_Node as any subsequent copies of the...

2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Expand_N_Extended_Return_Statement): Use
	New_Copy_Tree instead of Relocate_Node as any subsequent copies
	of the relocated node will have mangled Parent pointers.
	* sem_util.adb (Build_NCT_Hash_Tables): Reset both hash
	tables used in conjunction with entity and itype replication.
	(Visit_Entity): Rewrite the restriction on which entities
	require duplication.  The restriction now includes all types.

2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>

	* a-cofuse.ads, a-cfdlli.ads, a-cfhase.adb, a-cfhase.ads, a-cfinve.adb,
	a-cfinve.ads, a-cforma.adb, a-cforma.ads, a-cofuma.adb, a-cofuma.ads,
	a-cfhama.adb, a-cfhama.ads, a-cforse.adb: Minor reformatting and code
	cleanups.

From-SVN: r247384

16 files changed, 368 insertions, 371 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6997493..209e16e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,22 @@
 2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* exp_ch6.adb (Expand_N_Extended_Return_Statement): Use
+	New_Copy_Tree instead of Relocate_Node as any subsequent copies
+	of the relocated node will have mangled Parent pointers.
+	* sem_util.adb (Build_NCT_Hash_Tables): Reset both hash
+	tables used in conjunction with entity and itype replication.
+	(Visit_Entity): Rewrite the restriction on which entities
+	require duplication.  The restriction now includes all types.
+
+2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* a-cofuse.ads, a-cfdlli.ads, a-cfhase.adb, a-cfhase.ads, a-cfinve.adb,
+	a-cfinve.ads, a-cforma.adb, a-cforma.ads, a-cofuma.adb, a-cofuma.ads,
+	a-cfhama.adb, a-cfhama.ads, a-cforse.adb: Minor reformatting and code
+	cleanups.
+
+2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* exp_util.adb, g-dyntab.adb, par-ch4.adb, sem_util.adb, sem_attr.adb,
 	gnat1drv.adb, exp_disp.adb, namet.adb, alloc.ads: Minor reformatting.
 
diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads
index e7b7ba7..f6638cb 100644
--- a/gcc/ada/a-cfdlli.ads
+++ b/gcc/ada/a-cfdlli.ads
@@ -1541,9 +1541,9 @@ is
            Post   =>
              M_Elements_Sorted'Result =
                (for all I in 1 .. M.Length (Container) =>
-                  (for all J in I .. M.Length (Container) =>
-                       Element (Container, I) = Element (Container, J)
-                         or Element (Container, I) < Element (Container, J)));
+                 (for all J in I .. M.Length (Container) =>
+                   Element (Container, I) = Element (Container, J)
+                     or Element (Container, I) < Element (Container, J)));
          pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
 
       end Formal_Model;
diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb
index 4351102..bf782c6 100644
--- a/gcc/ada/a-cfhama.adb
+++ b/gcc/ada/a-cfhama.adb
@@ -370,7 +370,9 @@ is
       -- Find --
       ----------
 
-      function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+      function Find
+        (Container : K.Sequence;
+         Key       : Key_Type) return Count_Type
       is
       begin
          for I in 1 .. K.Length (Container) loop
@@ -385,8 +387,9 @@ is
       -- K_Keys_Included --
       ---------------------
 
-      function K_Keys_Included (Left  : K.Sequence;
-                               Right : K.Sequence) return Boolean
+      function K_Keys_Included
+        (Left  : K.Sequence;
+         Right : K.Sequence) return Boolean
       is
       begin
          for I in 1 .. K.Length (Left) loop
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index dc60dc8..e02accc 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -126,8 +126,8 @@ is
         Global => null,
         Post =>
           (if Find'Result > 0 then
-             Find'Result <= K.Length (Container)
-               and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
+              Find'Result <= K.Length (Container)
+                and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
 
       function K_Keys_Included
         (Left  : K.Sequence;
@@ -139,9 +139,9 @@ is
         Post   =>
           K_Keys_Included'Result =
             (for all I in 1 .. K.Length (Left) =>
-               Find (Right, K.Get (Left, I)) > 0
-                 and then K.Get (Right, Find (Right, K.Get (Left, I))) =
-                     K.Get (Left, I));
+              Find (Right, K.Get (Left, I)) > 0
+                and then K.Get (Right, Find (Right, K.Get (Left, I))) =
+                         K.Get (Left, I));
 
       package P is new Ada.Containers.Functional_Maps
         (Key_Type                       => Cursor,
@@ -203,14 +203,15 @@ is
             --  It only contains keys contained in Model
 
             and (for all Key of Keys'Result =>
-                   M.Has_Key (Model (Container), Key))
+                  M.Has_Key (Model (Container), Key))
 
             --  It contains all the keys contained in Model
 
             and (for all Key of Model (Container) =>
                   (Find (Keys'Result, Key) > 0
-                     and then Equivalent_Keys
-                      (K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
+                    and then Equivalent_Keys
+                               (K.Get (Keys'Result, Find (Keys'Result, Key)),
+                                Key)))
 
             --  It has no duplicate
 
@@ -221,7 +222,8 @@ is
                   (for all J in 1 .. Length (Container) =>
                     (if Equivalent_Keys
                           (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
-                     then I = J)));
+                     then
+                        I = J)));
       pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
 
       function Positions (Container : Map) return P.Map with
@@ -246,7 +248,7 @@ is
             and then
               (for all J of Positions'Result =>
                 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
-                  then I = J)));
+                 then I = J)));
 
       procedure Lift_Abstraction_Level (Container : Map) with
         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
@@ -547,9 +549,9 @@ is
 
             --  Key is inserted in Container
 
-            and K.Get (Keys (Container),
-                       P.Get (Positions (Container), Find (Container, Key))) =
-                Key
+            and K.Get
+                  (Keys (Container),
+                   P.Get (Positions (Container), Find (Container, Key))) = Key
 
             --  Mapping from cursors to keys is preserved
 
diff --git a/gcc/ada/a-cfhase.adb b/gcc/ada/a-cfhase.adb
index f40fc2f..9b2c9a4 100644
--- a/gcc/ada/a-cfhase.adb
+++ b/gcc/ada/a-cfhase.adb
@@ -38,16 +38,13 @@ with System; use type System.Address;
 package body Ada.Containers.Formal_Hashed_Sets with
   SPARK_Mode => Off
 is
-
    -----------------------
    -- Local Subprograms --
    -----------------------
 
    --  All need comments ???
 
-   procedure Difference
-     (Left, Right : Set;
-      Target      : in out Set);
+   procedure Difference (Left : Set; Right : Set; Target : in out Set);
 
    function Equivalent_Keys
      (Key  : Element_Type;
@@ -68,10 +65,10 @@ is
    pragma Inline (Hash_Node);
 
    procedure Insert
-     (Container       : in out Set;
-      New_Item : Element_Type;
-      Node     : out Count_Type;
-      Inserted : out Boolean);
+     (Container : in out Set;
+      New_Item  : Element_Type;
+      Node      : out Count_Type;
+      Inserted  : out Boolean);
 
    procedure Intersection
      (Left   : Set;
@@ -136,10 +133,13 @@ is
       begin
          Node  := First (Left).Node;
          while Node /= 0 loop
-            ENode := Find (Container => Right,
-                           Item      => Left.Nodes (Node).Element).Node;
-            if ENode = 0 or else
-              Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
+            ENode :=
+              Find
+                (Container => Right,
+                 Item      => Left.Nodes (Node).Element).Node;
+
+            if ENode = 0
+              or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
             then
                return False;
             end if;
@@ -148,9 +148,7 @@ is
          end loop;
 
          return True;
-
       end;
-
    end "=";
 
    ------------
@@ -228,11 +226,11 @@ is
       Capacity : Count_Type := 0) return Set
    is
       C      : constant Count_Type :=
-        Count_Type'Max (Capacity, Source.Capacity);
+                 Count_Type'Max (Capacity, Source.Capacity);
+      Cu     : Cursor;
       H      : Hash_Type;
       N      : Count_Type;
       Target : Set (C, Source.Modulus);
-      Cu     : Cursor;
 
    begin
       if 0 < Capacity and then Capacity < Source.Capacity then
@@ -276,10 +274,7 @@ is
    -- Delete --
    ------------
 
-   procedure Delete
-     (Container : in out Set;
-      Item      : Element_Type)
-   is
+   procedure Delete (Container : in out Set; Item : Element_Type) is
       X : Count_Type;
 
    begin
@@ -292,10 +287,7 @@ is
       Free (Container, X);
    end Delete;
 
-   procedure Delete
-     (Container : in out Set;
-      Position  : in out Cursor)
-   is
+   procedure Delete (Container : in out Set; Position : in out Cursor) is
    begin
       if not Has_Element (Container, Position) then
          raise Constraint_Error with "Position cursor has no element";
@@ -313,11 +305,11 @@ is
    -- Difference --
    ----------------
 
-   procedure Difference
-     (Target : in out Set;
-      Source : Set)
-   is
-      Tgt_Node, Src_Node, Src_Last, Src_Length : Count_Type;
+   procedure Difference (Target : in out Set; Source : Set) is
+      Src_Last   : Count_Type;
+      Src_Length : Count_Type;
+      Src_Node   : Count_Type;
+      Tgt_Node   : Count_Type;
 
       TN : Nodes_Type renames Target.Nodes;
       SN : Nodes_Type renames Source.Nodes;
@@ -369,10 +361,7 @@ is
       end loop;
    end Difference;
 
-   procedure Difference
-     (Left, Right : Set;
-      Target      : in out Set)
-   is
+   procedure Difference (Left : Set; Right : Set; Target : in out Set) is
       procedure Process (L_Node : Count_Type);
 
       procedure Iterate is
@@ -383,9 +372,10 @@ is
       -------------
 
       procedure Process (L_Node : Count_Type) is
+         B : Boolean;
          E : Element_Type renames Left.Nodes (L_Node).Element;
          X : Count_Type;
-         B : Boolean;
+
       begin
          if Find (Right, E).Node = 0 then
             Insert (Target, E, X, B);
@@ -399,7 +389,7 @@ is
       Iterate (Left);
    end Difference;
 
-   function Difference (Left, Right : Set) return Set is
+   function Difference (Left : Set; Right : Set) return Set is
       C : Count_Type;
       H : Hash_Type;
 
@@ -437,8 +427,8 @@ is
          raise Constraint_Error with "Position cursor equals No_Element";
       end if;
 
-      pragma Assert (Vet (Container, Position),
-                     "bad cursor in function Element");
+      pragma Assert
+        (Vet (Container, Position), "bad cursor in function Element");
 
       return Container.Nodes (Position.Node).Element;
    end Element;
@@ -466,7 +456,7 @@ is
          L_Node : Node_Type) return Boolean
       is
          R_Index : constant Hash_Type :=
-           Element_Keys.Index (R_HT, L_Node.Element);
+                     Element_Keys.Index (R_HT, L_Node.Element);
          R_Node  : Count_Type := R_HT.Buckets (R_Index);
          RN      : Nodes_Type renames R_HT.Nodes;
 
@@ -508,10 +498,7 @@ is
    -- Exclude --
    -------------
 
-   procedure Exclude
-     (Container : in out Set;
-      Item      : Element_Type)
-   is
+   procedure Exclude (Container : in out Set; Item : Element_Type) is
       X : Count_Type;
    begin
       Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
@@ -771,10 +758,7 @@ is
    -- Free --
    ----------
 
-   procedure Free
-     (HT : in out Set;
-      X  : Count_Type)
-   is
+   procedure Free (HT : in out Set; X : Count_Type) is
    begin
       HT.Nodes (X).Has_Element := False;
       HT_Ops.Free (HT, X);
@@ -784,10 +768,7 @@ is
    -- Generic_Allocate --
    ----------------------
 
-   procedure Generic_Allocate
-     (HT   : in out Set;
-      Node : out Count_Type)
-   is
+   procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
       procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
    begin
       Allocate (HT, Node);
@@ -809,14 +790,13 @@ is
       -- Local Instantiations --
       --------------------------
 
-      package Key_Keys is
-        new Hash_Tables.Generic_Bounded_Keys
-          (HT_Types        => HT_Types,
-           Next            => Next,
-           Set_Next        => Set_Next,
-           Key_Type        => Key_Type,
-           Hash            => Hash,
-           Equivalent_Keys => Equivalent_Key_Node);
+      package Key_Keys is new Hash_Tables.Generic_Bounded_Keys
+        (HT_Types        => HT_Types,
+         Next            => Next,
+         Set_Next        => Set_Next,
+         Key_Type        => Key_Type,
+         Hash            => Hash,
+         Equivalent_Keys => Equivalent_Key_Node);
 
       --------------
       -- Contains --
@@ -834,10 +814,7 @@ is
       -- Delete --
       ------------
 
-      procedure Delete
-        (Container : in out Set;
-         Key       : Key_Type)
-      is
+      procedure Delete (Container : in out Set; Key : Key_Type) is
          X : Count_Type;
 
       begin
@@ -884,10 +861,7 @@ is
       -- Exclude --
       -------------
 
-      procedure Exclude
-        (Container : in out Set;
-         Key       : Key_Type)
-      is
+      procedure Exclude (Container : in out Set; Key : Key_Type) is
          X : Count_Type;
       begin
          Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
@@ -930,6 +904,7 @@ is
                   return False;
                end if;
             end loop;
+
             return True;
          end M_Included_Except;
 
@@ -942,8 +917,7 @@ is
       function Key (Container : Set; Position : Cursor) return Key_Type is
       begin
          if not Has_Element (Container, Position) then
-            raise Constraint_Error with
-              "Position cursor has no element";
+            raise Constraint_Error with "Position cursor has no element";
          end if;
 
          pragma Assert
@@ -969,8 +943,7 @@ is
 
       begin
          if Node = 0 then
-            raise Constraint_Error with
-              "attempt to replace key not in set";
+            raise Constraint_Error with "attempt to replace key not in set";
          end if;
 
          Replace_Element (Container, Node, New_Item);
@@ -1006,12 +979,9 @@ is
    -- Include --
    -------------
 
-   procedure Include
-     (Container : in out Set;
-      New_Item  : Element_Type)
-   is
-      Position : Cursor;
+   procedure Include (Container : in out Set; New_Item : Element_Type) is
       Inserted : Boolean;
+      Position : Cursor;
 
    begin
       Insert (Container, New_Item, Position, Inserted);
@@ -1035,12 +1005,9 @@ is
       Insert (Container, New_Item, Position.Node, Inserted);
    end Insert;
 
-   procedure Insert
-     (Container : in out Set;
-      New_Item  : Element_Type)
-   is
-      Position : Cursor;
+   procedure Insert (Container : in out Set; New_Item : Element_Type) is
       Inserted : Boolean;
+      Position : Cursor;
 
    begin
       Insert (Container, New_Item, Position, Inserted);
@@ -1099,10 +1066,7 @@ is
    -- Intersection --
    ------------------
 
-   procedure Intersection
-     (Target : in out Set;
-      Source : Set)
-   is
+   procedure Intersection (Target : in out Set; Source : Set) is
       Tgt_Node : Count_Type;
       TN       : Nodes_Type renames Target.Nodes;
 
@@ -1133,11 +1097,7 @@ is
       end loop;
    end Intersection;
 
-   procedure Intersection
-     (Left   : Set;
-      Right  : Set;
-      Target : in out Set)
-   is
+   procedure Intersection (Left : Set; Right : Set; Target : in out Set) is
       procedure Process (L_Node : Count_Type);
 
       procedure Iterate is
@@ -1165,7 +1125,7 @@ is
       Iterate (Left);
    end Intersection;
 
-   function Intersection (Left, Right : Set) return Set is
+   function Intersection (Left : Set; Right : Set) return Set is
       C : Count_Type;
       H : Hash_Type;
 
@@ -1179,7 +1139,7 @@ is
 
       return S : Set (C, H) do
          if Length (Left) /= 0 and Length (Right) /= 0 then
-               Intersection (Left, Right, Target => S);
+            Intersection (Left, Right, Target => S);
          end if;
       end return;
    end Intersection;
@@ -1301,8 +1261,7 @@ is
       end if;
 
       if not Has_Element (Container, Position) then
-         raise Constraint_Error
-           with "Position has no element";
+         raise Constraint_Error with "Position has no element";
       end if;
 
       pragma Assert (Vet (Container, Position), "bad cursor in Next");
@@ -1353,16 +1312,12 @@ is
    -- Replace --
    -------------
 
-   procedure Replace
-     (Container : in out Set;
-      New_Item  : Element_Type)
-   is
+   procedure Replace (Container : in out Set; New_Item : Element_Type) is
       Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
 
    begin
       if Node = 0 then
-         raise Constraint_Error with
-           "attempt to replace element not in set";
+         raise Constraint_Error with "attempt to replace element not in set";
       end if;
 
       Container.Nodes (Node).Element := New_Item;
@@ -1379,12 +1334,11 @@ is
    is
    begin
       if not Has_Element (Container, Position) then
-         raise Constraint_Error with
-           "Position cursor equals No_Element";
+         raise Constraint_Error with "Position cursor equals No_Element";
       end if;
 
-      pragma Assert (Vet (Container, Position),
-                     "bad cursor in Replace_Element");
+      pragma Assert
+        (Vet (Container, Position), "bad cursor in Replace_Element");
 
       Replace_Element (Container, Position.Node, New_Item);
    end Replace_Element;
@@ -1425,10 +1379,7 @@ is
    -- Symmetric_Difference --
    --------------------------
 
-   procedure Symmetric_Difference
-     (Target : in out Set;
-      Source : Set)
-   is
+   procedure Symmetric_Difference (Target : in out Set; Source : Set) is
       procedure Process (Source_Node : Count_Type);
       pragma Inline (Process);
 
@@ -1439,9 +1390,10 @@ is
       -------------
 
       procedure Process (Source_Node : Count_Type) is
+         B : Boolean;
          N : Node_Type renames Source.Nodes (Source_Node);
          X : Count_Type;
-         B : Boolean;
+
       begin
          if Is_In (Target, N) then
             Delete (Target, N.Element);
@@ -1467,7 +1419,7 @@ is
       Iterate (Source);
    end Symmetric_Difference;
 
-   function Symmetric_Difference (Left, Right : Set) return Set is
+   function Symmetric_Difference (Left : Set; Right : Set) return Set is
       C : Count_Type;
       H : Hash_Type;
 
@@ -1512,10 +1464,7 @@ is
    -- Union --
    -----------
 
-   procedure Union
-     (Target : in out Set;
-      Source : Set)
-   is
+   procedure Union (Target : in out Set; Source : Set) is
       procedure Process (Src_Node : Count_Type);
 
       procedure Iterate is
@@ -1536,7 +1485,7 @@ is
          Insert (Target, E, X, B);
       end Process;
 
-      --  Start of processing for Union
+   --  Start of processing for Union
 
    begin
       if Target'Address = Source'Address then
@@ -1546,7 +1495,7 @@ is
       Iterate (Source);
    end Union;
 
-   function Union (Left, Right : Set) return Set is
+   function Union (Left : Set; Right : Set) return Set is
       C : Count_Type;
       H : Hash_Type;
 
diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index 0f2be85..fd3d007 100644
--- a/gcc/ada/a-cfhase.ads
+++ b/gcc/ada/a-cfhase.ads
@@ -55,8 +55,10 @@ generic
 
    with function Hash (Element : Element_Type) return Hash_Type;
 
-   with function Equivalent_Elements (Left, Right : Element_Type)
-                                      return Boolean is "=";
+   with function Equivalent_Elements
+     (Left  : Element_Type;
+      Right : Element_Type) return Boolean is "=";
+
 package Ada.Containers.Formal_Hashed_Sets with
   SPARK_Mode
 is
@@ -122,8 +124,9 @@ is
         Global => null,
         Post =>
           (if Find'Result > 0 then
-             Find'Result <= E.Length (Container)
-               and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
+              Find'Result <= E.Length (Container)
+                and Equivalent_Elements
+                      (Item, E.Get (Container, Find'Result)));
 
       function E_Elements_Included
         (Left  : E.Sequence;
@@ -135,9 +138,9 @@ is
         Post   =>
           E_Elements_Included'Result =
             (for all I in 1 .. E.Length (Left) =>
-               Find (Right, E.Get (Left, I)) > 0
-                 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
-                     E.Get (Left, I));
+              Find (Right, E.Get (Left, I)) > 0
+                and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+                         E.Get (Left, I));
       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 
       function E_Elements_Included
@@ -152,9 +155,9 @@ is
           E_Elements_Included'Result =
             (for all I in 1 .. E.Length (Left) =>
               (if M.Contains (Model, E.Get (Left, I)) then
-                 Find (Right, E.Get (Left, I)) > 0
-                   and then E.Get (Right, Find (Right, E.Get (Left, I))) =
-                       E.Get (Left, I)));
+                  Find (Right, E.Get (Left, I)) > 0
+                    and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+                             E.Get (Left, I)));
       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 
       function E_Elements_Included
@@ -171,13 +174,14 @@ is
           E_Elements_Included'Result =
             (for all I in 1 .. E.Length (Container) =>
               (if M.Contains (Model, E.Get (Container, I)) then
-                 Find (Left, E.Get (Container, I)) > 0
-                   and then E.Get (Left, Find (Left, E.Get (Container, I))) =
-                       E.Get (Container, I)
+                  Find (Left, E.Get (Container, I)) > 0
+                    and then E.Get (Left, Find (Left, E.Get (Container, I))) =
+                             E.Get (Container, I)
                else
-                 Find (Right, E.Get (Container, I)) > 0
-                   and then E.Get (Right, Find (Right, E.Get (Container, I))) =
-                       E.Get (Container, I)));
+                  Find (Right, E.Get (Container, I)) > 0
+                    and then E.Get
+                               (Right, Find (Right, E.Get (Container, I))) =
+                             E.Get (Container, I)));
       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 
       package P is new Ada.Containers.Functional_Maps
@@ -241,8 +245,8 @@ is
 
                and (for all C of P_Left =>
                      (if C /= Position then
-                        E.Get (E_Left, P.Get (P_Left, C)) =
-                        E.Get (E_Right, P.Get (P_Right, C)))));
+                         E.Get (E_Left, P.Get (P_Left, C)) =
+                         E.Get (E_Right, P.Get (P_Right, C)))));
 
       function Model (Container : Set) return M.Set with
       --  The high-level model of a set is a set of elements. Neither cursors
@@ -266,15 +270,16 @@ is
             --  It only contains keys contained in Model
 
             and (for all Item of Elements'Result =>
-                   M.Contains (Model (Container), Item))
+                  M.Contains (Model (Container), Item))
 
             --  It contains all the elements contained in Model
 
             and (for all Item of Model (Container) =>
                   (Find (Elements'Result, Item) > 0
-                     and then Equivalent_Elements
-                      (E.Get (Elements'Result, Find (Elements'Result, Item)),
-                       Item)))
+                    and then Equivalent_Elements
+                               (E.Get (Elements'Result,
+                                       Find (Elements'Result, Item)),
+                                Item)))
 
             --  It has no duplicate
 
@@ -311,7 +316,7 @@ is
             and then
               (for all J of Positions'Result =>
                 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
-                  then I = J)));
+                 then I = J)));
 
       procedure Lift_Abstraction_Level (Container : Set) with
         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
@@ -343,13 +348,13 @@ is
    function "=" (Left, Right : Set) return Boolean with
      Global => null,
      Post   =>
-       "="'Result =
-         (Length (Left) = Length (Right)
-            and E_Elements_Included (Elements (Left), Elements (Right)))
+         "="'Result =
+           (Length (Left) = Length (Right)
+             and E_Elements_Included (Elements (Left), Elements (Right)))
        and
          "="'Result =
            (E_Elements_Included (Elements (Left), Elements (Right))
-              and E_Elements_Included (Elements (Right), Elements (Left)));
+             and E_Elements_Included (Elements (Right), Elements (Left)));
 
    function Equivalent_Sets (Left, Right : Set) return Boolean with
      Global => null,
@@ -378,12 +383,10 @@ is
 
          --  Actual elements are preserved
 
-         and
-           E_Elements_Included
-             (Elements (Container), Elements (Container)'Old)
-         and
-           E_Elements_Included
-             (Elements (Container)'Old, Elements (Container));
+         and E_Elements_Included
+              (Elements (Container), Elements (Container)'Old)
+         and E_Elements_Included
+              (Elements (Container)'Old, Elements (Container));
 
    function Is_Empty (Container : Set) return Boolean with
      Global => null,
@@ -402,10 +405,8 @@ is
 
          --  Actual elements are preserved
 
-         and
-           E_Elements_Included (Elements (Target), Elements (Source))
-         and
-           E_Elements_Included (Elements (Source), Elements (Target));
+         and E_Elements_Included (Elements (Target), Elements (Source))
+         and E_Elements_Included (Elements (Source), Elements (Target));
 
    function Copy
      (Source   : Set;
@@ -482,10 +483,8 @@ is
 
          --  Actual elements are preserved
 
-         and
-           E_Elements_Included (Elements (Target), Elements (Source)'Old)
-         and
-           E_Elements_Included (Elements (Source)'Old, Elements (Target));
+         and E_Elements_Included (Elements (Target), Elements (Source)'Old)
+         and E_Elements_Included (Elements (Source)'Old, Elements (Target));
 
    procedure Insert
      (Container : in out Set;
@@ -769,27 +768,25 @@ is
 
          --  Elements of Target come from either Source or Target
 
-         and
-           M.Included_In_Union
-             (Model (Target), Model (Source), Model (Target)'Old)
+         and M.Included_In_Union
+               (Model (Target), Model (Source), Model (Target)'Old)
 
          --  Actual value of elements come from either Left or Right
 
-         and
-           E_Elements_Included
-             (Elements (Target),
-              Model (Target)'Old,
-              Elements (Target)'Old,
-              Elements (Source))
-         and
-           E_Elements_Included
-             (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
-         and
-           E_Elements_Included
-             (Elements (Source),
-              Model (Target)'Old,
-              Elements (Source),
-              Elements (Target))
+         and E_Elements_Included
+               (Elements (Target),
+                Model (Target)'Old,
+                Elements (Target)'Old,
+                Elements (Source))
+
+         and E_Elements_Included
+               (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
+
+         and E_Elements_Included
+               (Elements (Source),
+                Model (Target)'Old,
+                Elements (Source),
+                Elements (Target))
 
          --  Mapping from cursors of Target to elements is preserved
 
@@ -820,21 +817,20 @@ is
 
          --  Actual value of elements come from either Left or Right
 
-         and
-           E_Elements_Included
-             (Elements (Union'Result),
-              Model (Left),
-              Elements (Left),
-              Elements (Right))
-         and
-           E_Elements_Included
-             (Elements (Left), Model (Left), Elements (Union'Result))
-         and
-           E_Elements_Included
-             (Elements (Right),
-              Model (Left),
-              Elements (Right),
-              Elements (Union'Result));
+         and E_Elements_Included
+               (Elements (Union'Result),
+                Model (Left),
+                Elements (Left),
+                Elements (Right))
+
+         and E_Elements_Included
+               (Elements (Left), Model (Left), Elements (Union'Result))
+
+         and E_Elements_Included
+               (Elements (Right),
+                Model (Left),
+                Elements (Right),
+                Elements (Union'Result));
 
    function "or" (Left, Right : Set) return Set renames Union;
 
@@ -854,16 +850,14 @@ is
 
          --  Elements both in Source and Target are in the intersection
 
-         and
-           M.Includes_Intersection
-             (Model (Target), Model (Source), Model (Target)'Old)
+         and M.Includes_Intersection
+               (Model (Target), Model (Source), Model (Target)'Old)
 
          --  Actual value of elements of Target is preserved
 
          and E_Elements_Included (Elements (Target), Elements (Target)'Old)
-         and
-           E_Elements_Included
-             (Elements (Target)'Old, Model (Source), Elements (Target))
+         and E_Elements_Included
+               (Elements (Target)'Old, Model (Source), Elements (Target))
 
          --  Mapping from cursors of Target to elements is preserved
 
@@ -886,18 +880,17 @@ is
 
          --  Elements both in Left and Right are in the result of Intersection
 
-         and
-           M.Includes_Intersection
-             (Model (Intersection'Result), Model (Left), Model (Right))
+         and M.Includes_Intersection
+               (Model (Intersection'Result), Model (Left), Model (Right))
 
          --  Actual value of elements come from Left
 
-         and
-           E_Elements_Included
-             (Elements (Intersection'Result), Elements (Left))
-         and
-           E_Elements_Included
-             (Elements (Left), Model (Right), Elements (Intersection'Result));
+         and E_Elements_Included
+               (Elements (Intersection'Result), Elements (Left))
+
+         and E_Elements_Included
+               (Elements (Left), Model (Right),
+                Elements (Intersection'Result));
 
    function "and" (Left, Right : Set) return Set renames Intersection;
 
@@ -917,16 +910,14 @@ is
 
          --  Elements in Target but not in Source are in the difference
 
-         and
-           M.Included_In_Union
-             (Model (Target)'Old, Model (Target), Model (Source))
+         and M.Included_In_Union
+               (Model (Target)'Old, Model (Target), Model (Source))
 
          --  Actual value of elements of Target is preserved
 
          and E_Elements_Included (Elements (Target), Elements (Target)'Old)
-         and
-           E_Elements_Included
-             (Elements (Target)'Old, Model (Target), Elements (Target))
+         and E_Elements_Included
+               (Elements (Target)'Old, Model (Target), Elements (Target))
 
          --  Mapping from cursors of Target to elements is preserved
 
@@ -952,19 +943,18 @@ is
 
          --  Elements in Left but not in Right are in the difference
 
-         and
-           M.Included_In_Union
-             (Model (Left), Model (Difference'Result), Model (Right))
+         and M.Included_In_Union
+               (Model (Left), Model (Difference'Result), Model (Right))
 
          --  Actual value of elements come from Left
 
-         and
-           E_Elements_Included (Elements (Difference'Result), Elements (Left))
-         and
-           E_Elements_Included
-             (Elements (Left),
-              Model (Difference'Result),
-              Elements (Difference'Result));
+         and E_Elements_Included
+               (Elements (Difference'Result), Elements (Left))
+
+         and E_Elements_Included
+               (Elements (Left),
+                Model (Difference'Result),
+                Elements (Difference'Result));
 
    function "-" (Left, Right : Set) return Set renames Difference;
 
@@ -984,30 +974,27 @@ is
 
          --  Elements in Target but not in Source are in the difference
 
-         and
-           M.Included_In_Union
-             (Model (Target)'Old, Model (Target), Model (Source))
+         and M.Included_In_Union
+               (Model (Target)'Old, Model (Target), Model (Source))
 
          --  Elements in Source but not in Target are in the difference
 
-         and
-           M.Included_In_Union
-             (Model (Source), Model (Target), Model (Target)'Old)
+         and M.Included_In_Union
+               (Model (Source), Model (Target), Model (Target)'Old)
 
          --  Actual value of elements come from either Left or Right
 
-         and
-           E_Elements_Included
-             (Elements (Target),
-              Model (Target)'Old,
-              Elements (Target)'Old,
-              Elements (Source))
-         and
-           E_Elements_Included
-             (Elements (Target)'Old, Model (Target), Elements (Target))
-         and
-           E_Elements_Included
-             (Elements (Source), Model (Target), Elements (Target));
+         and E_Elements_Included
+               (Elements (Target),
+                Model (Target)'Old,
+                Elements (Target)'Old,
+                Elements (Source))
+
+         and E_Elements_Included
+               (Elements (Target)'Old, Model (Target), Elements (Target))
+
+         and E_Elements_Included
+               (Elements (Source), Model (Target), Elements (Target));
 
    function Symmetric_Difference (Left, Right : Set) return Set with
      Global => null,
@@ -1019,40 +1006,42 @@ is
 
          --  Elements of the difference were not both in Left and Right
 
-         and
-           M.Not_In_Both
-             (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
+         and M.Not_In_Both
+               (Model (Symmetric_Difference'Result),
+                Model (Left),
+                Model (Right))
 
          --  Elements in Left but not in Right are in the difference
 
-         and
-           M.Included_In_Union
-             (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
+         and M.Included_In_Union
+               (Model (Left),
+                Model (Symmetric_Difference'Result),
+                Model (Right))
 
          --  Elements in Right but not in Left are in the difference
 
-         and
-           M.Included_In_Union
-             (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
+         and M.Included_In_Union
+               (Model (Right),
+                Model (Symmetric_Difference'Result),
+                Model (Left))
 
          --  Actual value of elements come from either Left or Right
 
-         and
-           E_Elements_Included
-             (Elements (Symmetric_Difference'Result),
-              Model (Left),
-              Elements (Left),
-              Elements (Right))
-         and
-           E_Elements_Included
-             (Elements (Left),
-              Model (Symmetric_Difference'Result),
-              Elements (Symmetric_Difference'Result))
-         and
-           E_Elements_Included
-             (Elements (Right),
-              Model (Symmetric_Difference'Result),
-              Elements (Symmetric_Difference'Result));
+         and E_Elements_Included
+               (Elements (Symmetric_Difference'Result),
+                Model (Left),
+                Elements (Left),
+                Elements (Right))
+
+         and E_Elements_Included
+               (Elements (Left),
+                Model (Symmetric_Difference'Result),
+                Elements (Symmetric_Difference'Result))
+
+         and E_Elements_Included
+               (Elements (Right),
+                Model (Symmetric_Difference'Result),
+                Elements (Symmetric_Difference'Result));
 
    function "xor" (Left, Right : Set) return Set
      renames Symmetric_Difference;
@@ -1167,8 +1156,8 @@ is
              Post   =>
                M_Included_Except'Result =
                  (for all E of Left =>
-                    Contains (Right, E)
-                      or Equivalent_Keys (Generic_Keys.Key (E), Key));
+                   Contains (Right, E)
+                     or Equivalent_Keys (Generic_Keys.Key (E), Key));
 
       end Formal_Model;
       use Formal_Model;
@@ -1309,16 +1298,15 @@ is
 
                --  The key designated by the result of Find is Key
 
-               and
-                 Equivalent_Keys
-                   (Generic_Keys.Key (Container, Find'Result), Key));
+               and Equivalent_Keys
+                     (Generic_Keys.Key (Container, Find'Result), Key));
 
       function Contains (Container : Set; Key : Key_Type) return Boolean with
         Global => null,
         Post   =>
           Contains'Result =
             (for some E of Model (Container) =>
-                Equivalent_Keys (Key, Generic_Keys.Key (E)));
+              Equivalent_Keys (Key, Generic_Keys.Key (E)));
 
    end Generic_Keys;
 
diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb
index 4cb3227..8a9d11d 100644
--- a/gcc/ada/a-cfinve.adb
+++ b/gcc/ada/a-cfinve.adb
@@ -705,12 +705,11 @@ is
          function "<" (Left : Holder; Right : Holder) return Boolean is
            (E (Left) < E (Right));
 
-         procedure Sort is
-           new Generic_Array_Sort
-                 (Index_Type   => Array_Index,
-                  Element_Type => Holder,
-                  Array_Type   => Elements_Array,
-                  "<"          => "<");
+         procedure Sort is new Generic_Array_Sort
+           (Index_Type   => Array_Index,
+            Element_Type => Holder,
+            Array_Type   => Elements_Array,
+            "<"          => "<");
 
          Len : constant Capacity_Range := Length (Container);
 
@@ -1065,8 +1064,9 @@ is
       then
          Reserve_Capacity
            (Container,
-            Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor,
-                                Capacity_Range (New_Length)));
+            Capacity_Range'Max
+              (Current_Capacity (Container) * Growth_Factor,
+               Capacity_Range (New_Length)));
       end if;
 
       declare
@@ -1348,10 +1348,10 @@ is
       --  hence we also know that
       --    Index - Index_Type'First >= 0
 
-      --  The issue is that even though 0 is guaranteed to be a value in
-      --  the type Index_Type'Base, there's no guarantee that the difference
-      --  is a value in that type. To prevent overflow we use the wider
-      --  of Count_Type'Base and Index_Type'Base to perform intermediate
+      --  The issue is that even though 0 is guaranteed to be a value in the
+      --  type Index_Type'Base, there's no guarantee that the difference is a
+      --  value in that type. To prevent overflow we use the wider of
+      --  Count_Type'Base and Index_Type'Base to perform intermediate
       --  calculations.
 
       if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
@@ -1362,8 +1362,8 @@ is
                      Count_Type'Base (Index_Type'First);
       end if;
 
-      --  The array index subtype for all container element arrays
-      --  always starts with 1.
+      --  The array index subtype for all container element arrays always
+      --  starts with 1.
 
       return 1 + Offset;
    end To_Array_Index;
diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads
index e1bc30c..a7799e5 100644
--- a/gcc/ada/a-cfinve.ads
+++ b/gcc/ada/a-cfinve.ads
@@ -830,9 +830,9 @@ is
            Post   =>
              M_Elements_Sorted'Result =
                (for all I in Index_Type'First .. M.Last (Container) =>
-                  (for all J in I .. M.Last (Container) =>
-                       Element (Container, I) = Element (Container, J)
-                         or Element (Container, I) < Element (Container, J)));
+                 (for all J in I .. M.Last (Container) =>
+                   Element (Container, I) = Element (Container, J)
+                     or Element (Container, I) < Element (Container, J)));
          pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
 
       end Formal_Model;
diff --git a/gcc/ada/a-cforma.adb b/gcc/ada/a-cforma.adb
index a7dc514..5967973 100644
--- a/gcc/ada/a-cforma.adb
+++ b/gcc/ada/a-cforma.adb
@@ -518,7 +518,9 @@ is
       -- Find --
       ----------
 
-      function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+      function Find
+        (Container : K.Sequence;
+         Key       : Key_Type) return Count_Type
       is
       begin
          for I in 1 .. K.Length (Container) loop
@@ -634,9 +636,12 @@ is
          --  for their postconditions.
 
          while Position /= 0 loop
-            R := M.Add (Container => R,
-                        New_Key   => Container.Nodes (Position).Key,
-                        New_Item  => Container.Nodes (Position).Element);
+            R :=
+              M.Add
+                (Container => R,
+                 New_Key   => Container.Nodes (Position).Key,
+                 New_Item  => Container.Nodes (Position).Element);
+
             Position := Tree_Operations.Next (Container, Position);
          end loop;
 
diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 6b0597e..ed4e872 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -159,16 +159,16 @@ is
         Pre    => Position - 1 <= K.Length (Container),
         Post   =>
           K_Is_Find'Result =
+             ((if Position > 0 then
+                  K_Bigger_Than_Range (Container, 1, Position - 1, Key))
 
-            ((if Position > 0 then
-                K_Bigger_Than_Range (Container, 1, Position - 1, Key))
-
-             and (if Position < K.Length (Container) then
-                    K_Smaller_Than_Range
-                      (Container,
-                       Position + 1,
-                       K.Length (Container),
-                       Key)));
+            and
+              (if Position < K.Length (Container) then
+                  K_Smaller_Than_Range
+                    (Container,
+                     Position + 1,
+                     K.Length (Container),
+                     Key)));
       pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find);
 
       function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
@@ -178,8 +178,8 @@ is
         Global => null,
         Post =>
           (if Find'Result > 0 then
-             Find'Result <= K.Length (Container)
-               and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
+              Find'Result <= K.Length (Container)
+                and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
 
       package P is new Ada.Containers.Functional_Maps
         (Key_Type                       => Cursor,
@@ -246,20 +246,21 @@ is
             --  It only contains keys contained in Model
 
             and (for all Key of Keys'Result =>
-                   M.Has_Key (Model (Container), Key))
+                  M.Has_Key (Model (Container), Key))
 
             --  It contains all the keys contained in Model
 
             and (for all Key of Model (Container) =>
                   (Find (Keys'Result, Key) > 0
-                     and then Equivalent_Keys
-                      (K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
+                    and then Equivalent_Keys
+                               (K.Get (Keys'Result, Find (Keys'Result, Key)),
+                                Key)))
 
             --  It is sorted in increasing order
 
             and (for all I in 1 .. Length (Container) =>
                   Find (Keys'Result, K.Get (Keys'Result, I)) = I
-                  and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I));
+                    and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I));
       pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
 
       function Positions (Container : Map) return P.Map with
@@ -284,7 +285,7 @@ is
             and then
               (for all J of Positions'Result =>
                 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
-                  then I = J)));
+                 then I = J)));
 
       procedure Lift_Abstraction_Level (Container : Map) with
         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
@@ -942,7 +943,7 @@ is
      Contract_Cases =>
        (Position = No_Element
           or else P.Get (Positions (Container), Position) = 1
-         =>
+        =>
           Position = No_Element,
 
         others =>
@@ -983,6 +984,7 @@ is
      Contract_Cases =>
        (Length (Container) = 0 or else Key < First_Key (Container) =>
           Floor'Result = No_Element,
+
         others =>
           Has_Element (Container, Floor'Result)
             and not (Key < K.Get (Keys (Container),
@@ -999,9 +1001,9 @@ is
           Ceiling'Result = No_Element,
         others =>
           Has_Element (Container, Ceiling'Result)
-            and
-              not (K.Get (Keys (Container),
-                          P.Get (Positions (Container), Ceiling'Result)) < Key)
+            and not (K.Get
+                       (Keys (Container),
+                        P.Get (Positions (Container), Ceiling'Result)) < Key)
             and K_Is_Find
                   (Keys (Container),
                    Key,
diff --git a/gcc/ada/a-cforse.adb b/gcc/ada/a-cforse.adb
index 47e863b..b386c52 100644
--- a/gcc/ada/a-cforse.adb
+++ b/gcc/ada/a-cforse.adb
@@ -608,6 +608,7 @@ is
                return False;
             end if;
          end loop;
+
          return True;
       end E_Bigger_Than_Range;
 
@@ -700,6 +701,7 @@ is
                end if;
             end loop;
          end if;
+
          return True;
       end E_Is_Find;
 
@@ -719,6 +721,7 @@ is
                return False;
             end if;
          end loop;
+
          return True;
       end E_Smaller_Than_Range;
 
@@ -736,6 +739,7 @@ is
                return I;
             end if;
          end loop;
+
          return 0;
       end Find;
 
diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb
index 487aff4..93a38b5 100644
--- a/gcc/ada/a-cofuma.adb
+++ b/gcc/ada/a-cofuma.adb
@@ -152,8 +152,11 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
    -- Has_Witness --
    -----------------
 
-   function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
-   is (Witness in 1 .. Length (Container.Keys));
+   function Has_Witness
+     (Container : Map;
+      Witness   : Count_Type) return Boolean
+   is
+     (Witness in 1 .. Length (Container.Keys));
 
    --------------
    -- Is_Empty --
@@ -265,7 +268,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
    -- W_Get --
    -----------
 
-   function W_Get (Container : Map; Witness : Count_Type) return Element_Type
+   function W_Get
+     (Container : Map;
+      Witness   : Count_Type) return Element_Type
    is
      (Get (Container.Elements, Witness));
 
diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads
index ea44dcf..f98bfe7 100644
--- a/gcc/ada/a-cofuma.ads
+++ b/gcc/ada/a-cofuma.ads
@@ -35,9 +35,11 @@ private with Ada.Containers.Functional_Base;
 generic
    type Key_Type (<>) is private;
    type Element_Type (<>)  is private;
+
    with function Equivalent_Keys
      (Left  : Key_Type;
       Right : Key_Type) return Boolean is "=";
+
    Enable_Handling_Of_Equivalence : Boolean := True;
    --  This constant should only be set to False when no particular handling
    --  of equivalence over keys is needed, that is, Equivalent_Keys defines a
@@ -77,7 +79,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
           --  Has_Key returns the same result on all equivalent keys
 
           (if (for some K of Container => Equivalent_Keys (K, Key)) then
-             Has_Key'Result));
+              Has_Key'Result));
 
    function Get (Container : Map; Key : Key_Type) return Element_Type with
    --  Return the element associated with Key in Container
@@ -90,8 +92,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
           --  Get returns the same result on all equivalent keys
 
           Get'Result = W_Get (Container, Witness (Container, Key))
-          and (for all K of Container =>
-                 (Equivalent_Keys (K, Key) =
+            and (for all K of Container =>
+                  (Equivalent_Keys (K, Key) =
                     (Witness (Container, Key) = Witness (Container, K)))));
 
    function Length (Container : Map) return Count_Type with
diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads
index 87165d7..5eafbc4 100644
--- a/gcc/ada/a-cofuse.ads
+++ b/gcc/ada/a-cofuse.ads
@@ -34,9 +34,11 @@ private with Ada.Containers.Functional_Base;
 
 generic
    type Element_Type (<>) is private;
+
    with function Equivalent_Elements
      (Left  : Element_Type;
       Right : Element_Type) return Boolean is "=";
+
    Enable_Handling_Of_Equivalence : Boolean := True;
    --  This constant should only be set to False when no particular handling
    --  of equivalence over elements is needed, that is, Equivalent_Elements
@@ -75,7 +77,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
           --  Contains returns the same result on all equivalent elements
 
           (if (for some E of Container => Equivalent_Elements (E, Item)) then
-             Contains'Result));
+              Contains'Result));
 
    function Length (Container : Set) return Count_Type with
      Global => null;
@@ -89,8 +91,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
    --  Set inclusion
 
      Global => null,
-     Post   => "<="'Result = (for all Item of Left => Contains (Right, Item))
-       and (if "<="'Result then Length (Left) <= Length (Right));
+     Post   => "<="'Result = (for all Item of Left => Contains (Right, Item));
 
    function "=" (Left : Set; Right : Set) return Boolean with
    --  Extensional equality over sets
@@ -187,7 +188,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
 
      Global => null,
      Post   =>
-       Num_Overlaps'Result = Length (Intersection (Left, Right));
+       Num_Overlaps'Result = Length (Intersection (Left, Right))
+         and (if Left <= Right then Num_Overlaps'Result = Length (Left)
+              else Num_Overlaps'Result < Length (Left))
+         and (if Right <= Left then Num_Overlaps'Result = Length (Right)
+              else Num_Overlaps'Result < Length (Right))
+         and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right);
 
    ----------------------------
    -- Construction Functions --
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index fe47352..36f4360 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -4798,7 +4798,7 @@ package body Exp_Ch6 is
                   Init_Assignment :=
                     Make_Assignment_Statement (Loc,
                       Name       => New_Occurrence_Of (Ret_Obj_Id, Loc),
-                      Expression => Relocate_Node (Ret_Obj_Expr));
+                      Expression => New_Copy_Tree (Ret_Obj_Expr));
 
                   Set_Etype (Name (Init_Assignment), Etype (Ret_Obj_Id));
                   Set_Assignment_OK (Name (Init_Assignment));
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 8b1f9c0..92b3307 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -17003,7 +17003,7 @@ package body Sem_Util is
 
    package NCT_Itype_Assoc is new Simple_HTable (
      Header_Num => NCT_Header_Num,
-     Element    => Entity_Id,
+     Element    => Node_Or_Entity_Id,
      No_Element => Empty,
      Key        => Entity_Id,
      Hash       => New_Copy_Hash,
@@ -17114,37 +17114,45 @@ package body Sem_Util is
       ---------------------------
 
       procedure Build_NCT_Hash_Tables is
-         Elmt : Elmt_Id;
-         Ent  : Entity_Id;
+         Assoc : Entity_Id;
+         Elmt  : Elmt_Id;
+         Key   : Entity_Id;
+         Value : Entity_Id;
 
       begin
          if No (Map) then
             return;
          end if;
 
+         --  Clear both hash tables associated with entry replication since
+         --  multiple calls to New_Copy_Tree could cause multiple collisions
+         --  and produce long linked lists in individual buckets.
+
+         NCT_Assoc.Reset;
+         NCT_Itype_Assoc.Reset;
+
          Elmt := First_Elmt (Map);
          while Present (Elmt) loop
-            Ent := Node (Elmt);
 
-            --  Get new entity, and associate old and new
+            --  Extract a (key, value) pair from the map
 
+            Key := Node (Elmt);
             Next_Elmt (Elmt);
-            NCT_Assoc.Set (Ent, Node (Elmt));
+            Value := Node (Elmt);
 
-            if Is_Type (Ent) then
-               declare
-                  Anode : constant Entity_Id :=
-                            Associated_Node_For_Itype (Ent);
+            --  Add the pair in the association hash table
 
-               begin
-                  --  Enter the link between the associated node of the old
-                  --  Itype and the new Itype, for updating later when node
-                  --  is copied.
+            NCT_Assoc.Set (Key, Value);
 
-                  if Present (Anode) then
-                     NCT_Itype_Assoc.Set (Anode, Node (Elmt));
-                  end if;
-               end;
+            --  Add a link between the associated node of the old Itype and the
+            --  new Itype, for updating later when node is copied.
+
+            if Is_Type (Key) then
+               Assoc := Associated_Node_For_Itype (Key);
+
+               if Present (Assoc) then
+                  NCT_Itype_Assoc.Set (Assoc, Value);
+               end if;
             end if;
 
             Next_Elmt (Elmt);
@@ -17540,23 +17548,29 @@ package body Sem_Util is
          pragma Assert (not Is_Itype (Old_Entity));
          pragma Assert (Nkind (Old_Entity) in N_Entity);
 
-         --  Restrict entity creation to declarations of constants, variables
-         --  and subtypes. There is no need to duplicate entities declared in
-         --  inner scopes.
+         --  Do not duplicate an entity when it is declared within an inner
+         --  scope enclosed by an expression with actions.
 
-         if (not Ekind_In (Old_Entity, E_Constant, E_Variable)
-              and then Nkind (Parent (Old_Entity)) /= N_Subtype_Declaration)
-           or else EWA_Inner_Scope_Level > 0
-         then
+         if EWA_Inner_Scope_Level > 0 then
+            return;
+
+         --  Entity duplication is currently performed only for objects and
+         --  types. Relaxing this restriction leads to a performance penalty.
+
+         elsif Ekind_In (Old_Entity, E_Constant, E_Variable) then
+            null;
+
+         elsif Is_Type (Old_Entity) then
+            null;
+
+         else
             return;
          end if;
 
          New_E := New_Copy (Old_Entity);
 
-         --  The new entity has all the attributes of the old one, and we
-         --  just copy the contents of the entity. However, the back-end
-         --  needs different names for debugging purposes, so we create a
-         --  new internal name for it in all cases.
+         --  The new entity has all the attributes of the old one, however it
+         --  requires a new name for debugging purposes.
 
          Set_Chars (New_E, New_Internal_Name ('T'));
 
@@ -17830,8 +17844,8 @@ package body Sem_Util is
             while Present (New_E) loop
 
                --  Skip entities that were not created in the first phase
-               --  (that is, old entities specified by the caller in the
-               --  set of mappings to be applied to the tree).
+               --  (that is, old entities specified by the caller in the set of
+               --  mappings to be applied to the tree).
 
                if Is_Itype (New_E)
                  or else No (Map)