diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -88,6 +88,23 @@ package body Atree is
       Table_Increment      => Alloc.Node_Offsets_Increment,
       Table_Name           => "Orig_Nodes");
 
+   ------------------
+   -- Parent Stack --
+   ------------------
+
+   --  A separate table is used to traverse trees. It passes the parent field
+   --  of each node to the called process subprogram. It is defined global to
+   --  avoid adding performance overhead if allocated each time the traversal
+   --  functions are invoked.
+
+   package Parents_Stack is new Table.Table
+     (Table_Component_Type => Node_Id,
+      Table_Index_Type     => Nat,
+      Table_Low_Bound      => 1,
+      Table_Initial        => 256,
+      Table_Increment      => 100,
+      Table_Name           => "Parents_Stack");
+
    --------------------------
    -- Paren_Count Handling --
    --------------------------
@@ -135,6 +152,20 @@ package body Atree is
    --  Fix up parent pointers for the children of Fix_Node after a copy,
    --  setting them to Fix_Node when they pointed to Ref_Node.
 
+   generic
+      with function Process
+        (Parent_Node : Node_Id;
+         Node        : Node_Id) return Traverse_Result is <>;
+   function Internal_Traverse_With_Parent
+     (Node : Node_Id) return Traverse_Final_Result;
+   pragma Inline (Internal_Traverse_With_Parent);
+   --  Internal function that provides a functionality similar to Traverse_Func
+   --  but extended to pass the Parent node to the called Process subprogram;
+   --  delegates to Traverse_Func_With_Parent the initialization of the stack
+   --  data structure which stores the parent nodes (cf. Parents_Stack).
+   --  ??? Could we factorize the common code of Internal_Traverse_Func and
+   --  Traverse_Func?
+
    procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id);
    --  Mark arbitrary node or entity N as Ghost when it is created within a
    --  Ghost region.
@@ -2322,6 +2353,167 @@ package body Atree is
       return Size_In_Slots (N) - N_Head;
    end Size_In_Slots_Dynamic;
 
+   -----------------------------------
+   -- Internal_Traverse_With_Parent --
+   -----------------------------------
+
+   function Internal_Traverse_With_Parent
+      (Node : Node_Id) return Traverse_Final_Result
+   is
+      Tail_Recursion_Counter : Natural := 0;
+
+      procedure Pop_Parents;
+      --  Pop enclosing nodes of tail recursion plus the current parent.
+
+      function Traverse_Field (Fld : Union_Id) return Traverse_Final_Result;
+      --  Fld is one of the Traversed fields of Nod, which is necessarily a
+      --  Node_Id or List_Id. It is traversed, and the result is the result of
+      --  this traversal.
+
+      -----------------
+      -- Pop_Parents --
+      -----------------
+
+      procedure Pop_Parents is
+      begin
+         --  Pop the enclosing nodes of the tail recursion
+
+         for J in 1 .. Tail_Recursion_Counter loop
+            Parents_Stack.Decrement_Last;
+         end loop;
+
+         --  Pop the current node
+
+         pragma Assert (Parents_Stack.Table (Parents_Stack.Last) = Node);
+         Parents_Stack.Decrement_Last;
+      end Pop_Parents;
+
+      --------------------
+      -- Traverse_Field --
+      --------------------
+
+      function Traverse_Field (Fld : Union_Id) return Traverse_Final_Result is
+      begin
+         if Fld /= Union_Id (Empty) then
+
+            --  Descendant is a node
+
+            if Fld in Node_Range then
+               return Internal_Traverse_With_Parent (Node_Id (Fld));
+
+            --  Descendant is a list
+
+            elsif Fld in List_Range then
+               declare
+                  Elmt : Node_Id := First (List_Id (Fld));
+               begin
+                  while Present (Elmt) loop
+                     if Internal_Traverse_With_Parent (Elmt) = Abandon then
+                        return Abandon;
+                     end if;
+
+                     Next (Elmt);
+                  end loop;
+               end;
+
+            else
+               raise Program_Error;
+            end if;
+         end if;
+
+         return OK;
+      end Traverse_Field;
+
+      --  Local variables
+
+      Parent_Node : Node_Id := Parents_Stack.Table (Parents_Stack.Last);
+      Cur_Node    : Node_Id := Node;
+
+   --  Start of processing for Internal_Traverse_With_Parent
+
+   begin
+      --  If the last field is a node, we eliminate the tail recursion by
+      --  jumping back to this label. This is because concatenations are
+      --  sometimes deeply nested, as in X1&X2&...&Xn. Gen_IL ensures that the
+      --  Left_Opnd field of N_Op_Concat comes last in Traversed_Fields, so the
+      --  tail recursion is eliminated in that case. This trick prevents us
+      --  from running out of stack memory in that case. We don't bother
+      --  eliminating the tail recursion if the last field is a list.
+
+      <<Tail_Recurse>>
+
+      Parents_Stack.Append (Cur_Node);
+
+      case Process (Parent_Node, Cur_Node) is
+         when Abandon =>
+            Pop_Parents;
+            return Abandon;
+
+         when Skip =>
+            Pop_Parents;
+            return OK;
+
+         when OK =>
+            null;
+
+         when OK_Orig =>
+            Cur_Node := Original_Node (Cur_Node);
+      end case;
+
+      --  Check for empty Traversed_Fields before entering loop below, so the
+      --  tail recursive step won't go past the end.
+
+      declare
+         Cur_Field : Offset_Array_Index := Traversed_Offset_Array'First;
+         Offsets : Traversed_Offset_Array renames
+           Traversed_Fields (Nkind (Cur_Node));
+
+      begin
+         if Offsets (Traversed_Offset_Array'First) /= No_Field_Offset then
+            while Offsets (Cur_Field + 1) /= No_Field_Offset loop
+               declare
+                  F : constant Union_Id :=
+                    Get_Node_Field_Union (Cur_Node, Offsets (Cur_Field));
+
+               begin
+                  if Traverse_Field (F) = Abandon then
+                     Pop_Parents;
+                     return Abandon;
+                  end if;
+               end;
+
+               Cur_Field := Cur_Field + 1;
+            end loop;
+
+            declare
+               F : constant Union_Id :=
+                 Get_Node_Field_Union (Cur_Node, Offsets (Cur_Field));
+
+            begin
+               if F not in Node_Range then
+                  if Traverse_Field (F) = Abandon then
+                     Pop_Parents;
+                     return Abandon;
+                  end if;
+
+               elsif F /= Empty_List_Or_Node then
+                  --  Here is the tail recursion step, we reset Cur_Node and
+                  --  jump back to the start of the procedure, which has the
+                  --  same semantic effect as a call.
+
+                  Tail_Recursion_Counter := Tail_Recursion_Counter + 1;
+                  Parent_Node := Cur_Node;
+                  Cur_Node := Node_Id (F);
+                  goto Tail_Recurse;
+               end if;
+            end;
+         end if;
+      end;
+
+      Pop_Parents;
+      return OK;
+   end Internal_Traverse_With_Parent;
+
    -------------------
    -- Traverse_Func --
    -------------------
@@ -2454,6 +2646,32 @@ package body Atree is
       return OK;
    end Traverse_Func;
 
+   -------------------------------
+   -- Traverse_Func_With_Parent --
+   -------------------------------
+
+   function Traverse_Func_With_Parent
+     (Node : Node_Id) return Traverse_Final_Result
+   is
+      function Traverse is new Internal_Traverse_With_Parent (Process);
+      Result : Traverse_Final_Result;
+   begin
+      --  Ensure that the Parents stack is not currently in use; required since
+      --  it is global and hence a tree traversal with parents must be finished
+      --  before the next tree traversal with parents starts.
+
+      pragma Assert (Parents_Stack.Last = 0);
+      Parents_Stack.Set_Last (0);
+
+      Parents_Stack.Append (Parent (Node));
+      Result := Traverse (Node);
+      Parents_Stack.Decrement_Last;
+
+      pragma Assert (Parents_Stack.Last = 0);
+
+      return Result;
+   end Traverse_Func_With_Parent;
+
    -------------------
    -- Traverse_Proc --
    -------------------
@@ -2466,6 +2684,18 @@ package body Atree is
       Discard := Traverse (Node);
    end Traverse_Proc;
 
+   -------------------------------
+   -- Traverse_Proc_With_Parent --
+   -------------------------------
+
+   procedure Traverse_Proc_With_Parent (Node : Node_Id) is
+      function Traverse is new Traverse_Func_With_Parent (Process);
+      Discard : Traverse_Final_Result;
+      pragma Warnings (Off, Discard);
+   begin
+      Discard := Traverse (Node);
+   end Traverse_Proc_With_Parent;
+
    ------------
    -- Unlock --
    ------------


diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads
--- a/gcc/ada/atree.ads
+++ b/gcc/ada/atree.ads
@@ -409,6 +409,16 @@ package Atree is
    --  by a call to Process returning Abandon, otherwise it is OK (meaning that
    --  all calls to process returned either OK, OK_Orig, or Skip).
 
+   generic
+      with function Process
+        (Parent_Node : Node_Id;
+         Node        : Node_Id) return Traverse_Result is <>;
+   function Traverse_Func_With_Parent
+     (Node : Node_Id) return Traverse_Final_Result;
+   pragma Inline (Traverse_Func_With_Parent);
+   --  Same as Traverse_Func except that the called function Process receives
+   --  also the Parent_Node of Node.
+
    generic
       with function Process (N : Node_Id) return Traverse_Result is <>;
    procedure Traverse_Proc (Node : Node_Id);
@@ -416,6 +426,15 @@ package Atree is
    --  This is the same as Traverse_Func except that no result is returned,
    --  i.e. Traverse_Func is called and the result is simply discarded.
 
+   generic
+      with function Process
+        (Parent_Node : Node_Id;
+         Node        : Node_Id) return Traverse_Result is <>;
+   procedure Traverse_Proc_With_Parent (Node : Node_Id);
+   pragma Inline (Traverse_Proc_With_Parent);
+   --  Same as Traverse_Proc except that the called function Process receives
+   --  also the Parent_Node of Node.
+
    ---------------------------
    -- Node Access Functions --
    ---------------------------


diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -4323,9 +4323,55 @@ package body Contracts is
          -----------------------------------------
 
          procedure Restore_Original_Selected_Component is
+            Restored_Nodes_List : Elist_Id := No_Elist;
+
+            procedure Fix_Parents (N : Node_Id);
+            --  Traverse the subtree of N fixing the Parent field of all the
+            --  nodes.
 
             function Restore_Node (N : Node_Id) return Traverse_Result;
-            --  Process a single node
+            --  Process dispatching calls to functions whose original node was
+            --  a selected component, and replace them with their original
+            --  node. Restored nodes are stored in the Restored_Nodes_List
+            --  to fix the parent fields of their subtrees in a separate
+            --  tree traversal.
+
+            -----------------
+            -- Fix_Parents --
+            -----------------
+
+            procedure Fix_Parents (N : Node_Id) is
+
+               function Fix_Parent
+                 (Parent_Node : Node_Id;
+                  Node        : Node_Id) return Traverse_Result;
+               --  Process a single node
+
+               ----------------
+               -- Fix_Parent --
+               ----------------
+
+               function Fix_Parent
+                 (Parent_Node : Node_Id;
+                  Node        : Node_Id) return Traverse_Result
+               is
+                  Par : constant Node_Id := Parent (Node);
+
+               begin
+                  if Par /= Parent_Node then
+                     pragma Assert (not Is_List_Member (Node));
+                     Set_Parent (Node, Parent_Node);
+                  end if;
+
+                  return OK;
+               end Fix_Parent;
+
+               procedure Fix_Parents is
+                  new Traverse_Proc_With_Parent (Fix_Parent);
+
+            begin
+               Fix_Parents (N);
+            end Fix_Parents;
 
             ------------------
             -- Restore_Node --
@@ -4340,13 +4386,11 @@ package body Contracts is
                   Rewrite (N, Original_Node (N));
                   Set_Original_Node (N, N);
 
-                  --  Restore decoration of its child nodes; required to ensure
-                  --  proper copies of this subtree (if required) by subsequent
-                  --  calls to New_Copy_Tree (since otherwise these child nodes
-                  --  are not duplicated).
+                  --  Save the restored node in the Restored_Nodes_List to fix
+                  --  the parent fields of their subtrees in a separate tree
+                  --  traversal.
 
-                  Set_Parent (Prefix (N), N);
-                  Set_Parent (Selector_Name (N), N);
+                  Append_New_Elmt (N, Restored_Nodes_List);
                end if;
 
                return OK;
@@ -4354,8 +4398,29 @@ package body Contracts is
 
             procedure Restore_Nodes is new Traverse_Proc (Restore_Node);
 
+         --  Start of processing for Restore_Original_Selected_Component
+
          begin
             Restore_Nodes (Expr);
+
+            --  After restoring the original node we must fix the decoration
+            --  of the Parent attribute to ensure tree consistency; required
+            --  because when the class-wide condition is inherited, calls to
+            --  New_Copy_Tree will perform copies of this subtree, and formal
+            --  occurrences with wrong Parent field cannot be mapped to the
+            --  new formals.
+
+            if Present (Restored_Nodes_List) then
+               declare
+                  Elmt : Elmt_Id := First_Elmt (Restored_Nodes_List);
+
+               begin
+                  while Present (Elmt) loop
+                     Fix_Parents (Node (Elmt));
+                     Next_Elmt (Elmt);
+                  end loop;
+               end;
+            end if;
          end Restore_Original_Selected_Component;
 
       --  Start of processing for Preanalyze_Condition
@@ -4428,11 +4493,60 @@ package body Contracts is
            (Par_Subp : Entity_Id;
             Subp     : Entity_Id) return Node_Id
          is
+            function Check_Condition (Expr : Node_Id) return Boolean;
+            --  Used in assertion to check that Expr has no reference to the
+            --  formals of Par_Subp.
+
+            ---------------------
+            -- Check_Condition --
+            ---------------------
+
+            function Check_Condition (Expr : Node_Id) return Boolean is
+               Par_Formal_Id : Entity_Id;
+
+               function Check_Entity (N : Node_Id) return Traverse_Result;
+               --  Check occurrence of Par_Formal_Id
+
+               ------------------
+               -- Check_Entity --
+               ------------------
+
+               function Check_Entity (N : Node_Id) return Traverse_Result is
+               begin
+                  if Nkind (N) = N_Identifier
+                    and then Present (Entity (N))
+                    and then Entity (N) = Par_Formal_Id
+                  then
+                     return Abandon;
+                  end if;
+
+                  return OK;
+               end Check_Entity;
+
+               function Check_Expression is new Traverse_Func (Check_Entity);
+
+            --  Start of processing for Check_Condition
+
+            begin
+               Par_Formal_Id := First_Formal (Par_Subp);
+
+               while Present (Par_Formal_Id) loop
+                  if Check_Expression (Expr) = Abandon then
+                     return False;
+                  end if;
+
+                  Next_Formal (Par_Formal_Id);
+               end loop;
+
+               return True;
+            end Check_Condition;
+
+            --  Local variables
+
             Assoc_List     : constant Elist_Id := New_Elmt_List;
             Par_Formal_Id  : Entity_Id := First_Formal (Par_Subp);
             Subp_Formal_Id : Entity_Id := First_Formal (Subp);
-
-         --  Start of processing for Inherit_Condition
+            New_Condition  : Node_Id;
 
          begin
             while Present (Par_Formal_Id) loop
@@ -4443,9 +4557,25 @@ package body Contracts is
                Next_Formal (Subp_Formal_Id);
             end loop;
 
-            return New_Copy_Tree
-                     (Source => Class_Condition (Kind, Par_Subp),
-                      Map    => Assoc_List);
+            --  Check that Parent field of all the nodes have their correct
+            --  decoration; required because otherwise mapped nodes with
+            --  wrong Parent field are left unmodified in the copied tree
+            --  and cause reporting wrong errors at later stages.
+
+            pragma Assert
+              (Check_Parents (Class_Condition (Kind, Par_Subp), Assoc_List));
+
+            New_Condition :=
+              New_Copy_Tree
+                (Source => Class_Condition (Kind, Par_Subp),
+                 Map    => Assoc_List);
+
+            --  Ensure that the inherited condition has no reference to the
+            --  formals of the parent subprogram.
+
+            pragma Assert (Check_Condition (New_Condition));
+
+            return New_Condition;
          end Inherit_Condition;
 
          ----------------------


diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4443,6 +4443,44 @@ package body Sem_Util is
       end if;
    end Check_Nonvolatile_Function_Profile;
 
+   -------------------
+   -- Check_Parents --
+   -------------------
+
+   function Check_Parents (N : Node_Id; List : Elist_Id) return Boolean is
+
+      function Check_Node
+        (Parent_Node : Node_Id;
+         N           : Node_Id) return Traverse_Result;
+      --  Process a single node.
+
+      ----------------
+      -- Check_Node --
+      ----------------
+
+      function Check_Node
+        (Parent_Node : Node_Id;
+         N           : Node_Id) return Traverse_Result is
+      begin
+         if Nkind (N) = N_Identifier
+           and then Parent (N) /= Parent_Node
+           and then Present (Entity (N))
+           and then Contains (List, Entity (N))
+         then
+            return Abandon;
+         end if;
+
+         return OK;
+      end Check_Node;
+
+      function Traverse is new Traverse_Func_With_Parent (Check_Node);
+
+   --  Start of processing for Check_Parents
+
+   begin
+      return Traverse (N) = OK;
+   end Check_Parents;
+
    -----------------------------
    -- Check_Part_Of_Reference --
    -----------------------------


diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -448,6 +448,10 @@ package Sem_Util is
    --  Verify that the profile of nonvolatile function Func_Id does not contain
    --  effectively volatile parameters or return type for reading.
 
+   function Check_Parents (N : Node_Id; List : Elist_Id) return Boolean;
+   --  Return True if all the occurrences of subtree N referencing entities in
+   --  the given List have the right value in their Parent field.
+
    procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
    --  Verify the legality of reference Ref to variable Var_Id when the
    --  variable is a constituent of a single protected/task type.


