diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 7387ffe634734eb13748b26f4d0ca0bf4ec8f9f7..29557eca54f0be543f2fb16f17ece20239b1a1fe 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -2198,12 +2198,24 @@ package body Contracts is
          Result  : Entity_Id)
       is
          Loc       : constant Source_Ptr := Sloc (Body_Decl);
+         Last_Decl : Node_Id;
          Params    : List_Id := No_List;
          Proc_Bod  : Node_Id;
          Proc_Decl : Node_Id;
          Proc_Id   : Entity_Id;
          Proc_Spec : Node_Id;
 
+         --  Extra declarations needed to handle interactions between
+         --  postconditions and finalization.
+
+         Postcond_Enabled_Decl : Node_Id;
+         Return_Success_Decl   : Node_Id;
+         Result_Obj_Decl       : Node_Id;
+         Result_Obj_Type_Decl  : Node_Id;
+         Result_Obj_Type       : Entity_Id;
+
+      --  Start of processing for Build_Postconditions_Procedure
+
       begin
          --  Nothing to do if there are no actions to check on exit
 
@@ -2211,6 +2223,29 @@ package body Contracts is
             return;
          end if;
 
+         --  Otherwise, we generate the postcondition procedure and add
+         --  associated objects and conditions used to coordinate postcondition
+         --  evaluation with finalization.
+
+         --  Generate:
+         --
+         --    procedure _postconditions (Return_Exp : Result_Typ);
+         --
+         --    --  Result_Obj_Type created when Result_Type is non-elementary
+         --    [type Result_Obj_Type is access all Result_Typ;]
+         --
+         --    Result_Obj : Result_Obj_Type;
+         --
+         --    Postcond_Enabled            : Boolean := True;
+         --    Return_Success_For_Postcond : Boolean := False;
+         --
+         --    procedure _postconditions (Return_Exp : Result_Typ) is
+         --    begin
+         --       if Postcond_Enabled and then Return_Success_For_Postcond then
+         --          [stmts];
+         --       end if;
+         --    end;
+
          Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
          Set_Debug_Info_Needed   (Proc_Id);
          Set_Postconditions_Proc (Subp_Id, Proc_Id);
@@ -2248,12 +2283,14 @@ package body Contracts is
          --  body. This ensures that the body will not cause any premature
          --  freezing, as it may mention types:
 
+         --  Generate:
+         --
          --    procedure Proc (Obj : Array_Typ) is
          --       procedure _postconditions is
          --       begin
          --          ... Obj ...
          --       end _postconditions;
-
+         --
          --       subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
          --    begin
 
@@ -2265,12 +2302,121 @@ package body Contracts is
          Insert_Before_First_Source_Declaration
            (Proc_Decl, Declarations (Body_Decl));
          Analyze (Proc_Decl);
+         Last_Decl := Proc_Decl;
+
+         --  When Result is present (e.g. the postcondition checks apply to a
+         --  function) we make a local object to capture the result, so, if
+         --  needed, we can call the generated postconditions procedure during
+         --  finalization instead of at the point of return.
+
+         --  Note: The placement of the following declarations before the
+         --  declaration of the body of the postconditions, but after the
+         --  declaration of the postconditions spec is deliberate and required
+         --  since other code within the expander expects them to be located
+         --  here. Perhaps when more space is available in the tree this will
+         --  no longer be necessary ???
+
+         if Present (Result) then
+            --  Elementary result types mean a copy is cheap and preferred over
+            --  using pointers.
+
+            if Is_Elementary_Type (Etype (Result)) then
+               Result_Obj_Type := Etype (Result);
+
+            --  Otherwise, we create a named access type to capture the result
+
+            --  Generate:
+            --
+            --  type Result_Obj_Type is access all [Result_Type];
+
+            else
+               Result_Obj_Type := Make_Temporary (Loc, 'R');
+
+               Result_Obj_Type_Decl :=
+                 Make_Full_Type_Declaration (Loc,
+                   Defining_Identifier => Result_Obj_Type,
+                   Type_Definition     =>
+                     Make_Access_To_Object_Definition (Loc,
+                       All_Present        => True,
+                       Subtype_Indication => New_Occurrence_Of
+                                               (Etype (Result), Loc)));
+               Insert_After_And_Analyze (Proc_Decl, Result_Obj_Type_Decl);
+               Last_Decl := Result_Obj_Type_Decl;
+            end if;
+
+            --  Create the result obj declaration
+
+            --  Generate:
+            --
+            --  Result_Object_For_Postcond : Result_Obj_Type;
+
+            Result_Obj_Decl :=
+              Make_Object_Declaration (Loc,
+                Defining_Identifier =>
+                  Make_Defining_Identifier
+                    (Loc, Name_uResult_Object_For_Postcond),
+                Object_Definition   =>
+                  New_Occurrence_Of
+                    (Result_Obj_Type, Loc));
+            Set_No_Initialization (Result_Obj_Decl);
+            Insert_After_And_Analyze (Last_Decl, Result_Obj_Decl);
+            Last_Decl := Result_Obj_Decl;
+         end if;
+
+         --  Build the Postcond_Enabled flag used to delay evaluation of
+         --  postconditions until finalization has been performed when cleanup
+         --  actions are present.
+
+         --  Generate:
+         --
+         --    Postcond_Enabled : Boolean := True;
+
+         Postcond_Enabled_Decl :=
+           Make_Object_Declaration (Loc,
+             Defining_Identifier =>
+               Make_Defining_Identifier
+                 (Loc, Name_uPostcond_Enabled),
+             Object_Definition   => New_Occurrence_Of (Standard_Boolean, Loc),
+             Expression          => New_Occurrence_Of (Standard_True, Loc));
+         Insert_After_And_Analyze (Last_Decl, Postcond_Enabled_Decl);
+         Last_Decl := Postcond_Enabled_Decl;
+
+         --  Create a flag to indicate that return has been reached
+
+         --  This is necessary for deciding whether to execute _postconditions
+         --  during finalization.
+
+         --  Generate:
+         --
+         --    Return_Success_For_Postcond : Boolean := False;
+
+         Return_Success_Decl :=
+           Make_Object_Declaration (Loc,
+             Defining_Identifier =>
+               Make_Defining_Identifier
+                 (Loc, Name_uReturn_Success_For_Postcond),
+             Object_Definition   => New_Occurrence_Of (Standard_Boolean, Loc),
+             Expression          => New_Occurrence_Of (Standard_False, Loc));
+         Insert_After_And_Analyze (Last_Decl, Return_Success_Decl);
+         Last_Decl := Return_Success_Decl;
 
          --  Set an explicit End_Label to override the sloc of the implicit
          --  RETURN statement, and prevent it from inheriting the sloc of one
          --  the postconditions: this would cause confusing debug info to be
          --  produced, interfering with coverage-analysis tools.
 
+         --  Also, wrap the postcondition checks in a conditional which can be
+         --  used to delay their evaluation when clean-up actions are present.
+
+         --  Generate:
+         --
+         --    procedure _postconditions is
+         --    begin
+         --       if Postcond_Enabled and then Return_Success_For_Postcond then
+         --          [Stmts];
+         --       end if;
+         --    end;
+
          Proc_Bod :=
            Make_Subprogram_Body (Loc,
              Specification              =>
@@ -2278,10 +2424,22 @@ package body Contracts is
              Declarations               => Empty_List,
              Handled_Statement_Sequence =>
                Make_Handled_Sequence_Of_Statements (Loc,
-                 Statements => Stmts,
-                 End_Label  => Make_Identifier (Loc, Chars (Proc_Id))));
+                 End_Label  => Make_Identifier (Loc, Chars (Proc_Id)),
+                 Statements => New_List (
+                   Make_If_Statement (Loc,
+                     Condition      =>
+                       Make_And_Then (Loc,
+                         Left_Opnd  =>
+                           New_Occurrence_Of
+                             (Defining_Identifier
+                               (Postcond_Enabled_Decl), Loc),
+                         Right_Opnd =>
+                           New_Occurrence_Of
+                             (Defining_Identifier
+                               (Return_Success_Decl), Loc)),
+                      Then_Statements => Stmts))));
+         Insert_After_And_Analyze (Last_Decl, Proc_Bod);
 
-         Insert_After_And_Analyze (Proc_Decl, Proc_Bod);
       end Build_Postconditions_Procedure;
 
       ----------------------------
@@ -3280,6 +3438,81 @@ package body Contracts is
       Freeze_Contracts;
    end Freeze_Previous_Contracts;
 
+   --------------------------
+   -- Get_Postcond_Enabled --
+   --------------------------
+
+   function Get_Postcond_Enabled (Subp : Entity_Id) return Node_Id is
+      Decl : Node_Id;
+   begin
+      Decl :=
+        Next (Unit_Declaration_Node (Postconditions_Proc (Subp)));
+      while Present (Decl) loop
+
+         if Nkind (Decl) = N_Object_Declaration
+          and then Chars (Defining_Identifier (Decl))
+                     = Name_uPostcond_Enabled
+         then
+            return Defining_Identifier (Decl);
+         end if;
+
+         Next (Decl);
+      end loop;
+
+      return Empty;
+   end Get_Postcond_Enabled;
+
+   ------------------------------------
+   -- Get_Result_Object_For_Postcond --
+   ------------------------------------
+
+   function Get_Result_Object_For_Postcond
+     (Subp : Entity_Id) return Node_Id
+   is
+      Decl : Node_Id;
+   begin
+      Decl :=
+        Next (Unit_Declaration_Node (Postconditions_Proc (Subp)));
+      while Present (Decl) loop
+
+         if Nkind (Decl) = N_Object_Declaration
+           and then Chars (Defining_Identifier (Decl))
+                      = Name_uResult_Object_For_Postcond
+         then
+            return Defining_Identifier (Decl);
+         end if;
+
+         Next (Decl);
+      end loop;
+
+      return Empty;
+   end Get_Result_Object_For_Postcond;
+
+   -------------------------------------
+   -- Get_Return_Success_For_Postcond --
+   -------------------------------------
+
+   function Get_Return_Success_For_Postcond (Subp : Entity_Id) return Node_Id
+   is
+      Decl : Node_Id;
+   begin
+      Decl :=
+        Next (Unit_Declaration_Node (Postconditions_Proc (Subp)));
+      while Present (Decl) loop
+
+         if Nkind (Decl) = N_Object_Declaration
+          and then Chars (Defining_Identifier (Decl))
+                     = Name_uReturn_Success_For_Postcond
+         then
+            return Defining_Identifier (Decl);
+         end if;
+
+         Next (Decl);
+      end loop;
+
+      return Empty;
+   end Get_Return_Success_For_Postcond;
+
    ---------------------------------
    -- Inherit_Subprogram_Contract --
    ---------------------------------
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 4782ef59cb2c78fc95a9e225343886eb69d32e13..b8a12ffd58ab13de509e72f33e4fd41a2d84bbc3 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -188,6 +188,21 @@ package Contracts is
    --  denoted by Body_Decl. In addition, freeze the contract of the nearest
    --  enclosing package body.
 
+   function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id;
+   --  Get the defining identifier for a subprogram's Postcond_Enabled
+   --  object created during the expansion of the subprogram's postconditions.
+
+   function Get_Result_Object_For_Postcond (Subp : Entity_Id) return Entity_Id;
+   --  Get the defining identifier for a subprogram's
+   --  Result_Object_For_Postcond object created during the expansion of the
+   --  subprogram's postconditions.
+
+   function Get_Return_Success_For_Postcond
+     (Subp : Entity_Id) return Entity_Id;
+   --  Get the defining identifier for a subprogram's
+   --  Return_Success_For_Postcond object created during the expansion of the
+   --  subprogram's postconditions.
+
    procedure Inherit_Subprogram_Contract
      (Subp      : Entity_Id;
       From_Subp : Entity_Id);
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 8949703f8d7a5bfaccd8924dfdd05f68025c3c52..8c401ca0c6a6cf5f3acd3e117ef1f333381ce896 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -6802,7 +6802,9 @@ package body Einfo is
 
    procedure Set_Stores_Attribute_Old_Prefix (Id : E; V : B := True) is
    begin
-      pragma Assert (Ekind (Id) = E_Constant);
+      pragma Assert (Is_Type (Id)
+                      or else (Ekind (Id) in E_Constant
+                                           | E_Variable));
       Set_Flag270 (Id, V);
    end Set_Stores_Attribute_Old_Prefix;
 
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 360ce7ce85588cd11be3ce0c46248434c661ae6d..cc0c815186ee1dd119db10bb259c390f63b10cf1 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -4503,8 +4503,8 @@ package Einfo is
 --       stored discriminants for the record (sub)type.
 
 --    Stores_Attribute_Old_Prefix (Flag270)
---       Defined in constants. Set when the constant has been generated to save
---       the value of attribute 'Old's prefix.
+--       Defined in constants, variables, and types which are created during
+--       expansion in order to save the value of attribute 'Old's prefix.
 
 --    Strict_Alignment (Flag145) [implementation base type only]
 --       Defined in all type entities. Indicates that the type is by-reference
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 0a5fbccec820ee515b618c9ff0d18428ed8ee4f7..afe7e8ba63e1f19d26250be30fe7892f5e0a12fc 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -6246,9 +6246,24 @@ package body Exp_Ch6 is
             --  Call the _Postconditions procedure if the related subprogram
             --  has contract assertions that need to be verified on exit.
 
+            --  Also, mark the successful return to signal that postconditions
+            --  need to be evaluated when finalization occurs.
+
             if Ekind (Spec_Id) = E_Procedure
               and then Present (Postconditions_Proc (Spec_Id))
             then
+               --  Generate:
+               --
+               --    Return_Success_For_Postcond := True;
+               --    _postconditions;
+
+               Insert_Action (Stmt,
+                 Make_Assignment_Statement (Loc,
+                   Name       =>
+                     New_Occurrence_Of
+                      (Get_Return_Success_For_Postcond (Spec_Id), Loc),
+                   Expression => New_Occurrence_Of (Standard_True, Loc)));
+
                Insert_Action (Stmt,
                  Make_Procedure_Call_Statement (Loc,
                    Name =>
@@ -6676,9 +6691,24 @@ package body Exp_Ch6 is
       --  Call the _Postconditions procedure if the related subprogram has
       --  contract assertions that need to be verified on exit.
 
+      --  Also, mark the successful return to signal that postconditions need
+      --  to be evaluated when finalization occurs.
+
       if Ekind (Scope_Id) in E_Entry | E_Entry_Family | E_Procedure
         and then Present (Postconditions_Proc (Scope_Id))
       then
+         --  Generate:
+         --
+         --    Return_Success_For_Postcond := True;
+         --    _postconditions;
+
+         Insert_Action (N,
+           Make_Assignment_Statement (Loc,
+             Name       =>
+               New_Occurrence_Of
+                (Get_Return_Success_For_Postcond (Scope_Id), Loc),
+             Expression => New_Occurrence_Of (Standard_True, Loc)));
+
          Insert_Action (N,
            Make_Procedure_Call_Statement (Loc,
              Name => New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc)));
@@ -7565,6 +7595,41 @@ package body Exp_Ch6 is
 
          Force_Evaluation (Exp, Mode => Strict);
 
+         --  Save the return value or a pointer to the return value since we
+         --  may need to call postconditions after finalization when cleanup
+         --  actions are present.
+
+         --  Generate:
+         --
+         --    Result_Object_For_Postcond := [Exp]'Unrestricted_Access;
+
+         Insert_Action (Exp,
+           Make_Assignment_Statement (Loc,
+             Name       =>
+               New_Occurrence_Of
+                (Get_Result_Object_For_Postcond (Scope_Id), Loc),
+             Expression =>
+               (if Is_Elementary_Type (Etype (R_Type)) then
+                   New_Copy_Tree (Exp)
+                else
+                   Make_Attribute_Reference (Loc,
+                     Attribute_Name => Name_Unrestricted_Access,
+                     Prefix         => New_Copy_Tree (Exp)))));
+
+         --  Mark the successful return to signal that postconditions need to
+         --  be evaluated when finalization occurs.
+
+         --  Generate:
+         --
+         --    Return_Success_For_Postcond := True;
+
+         Insert_Action (Exp,
+           Make_Assignment_Statement (Loc,
+             Name       =>
+               New_Occurrence_Of
+                (Get_Return_Success_For_Postcond (Scope_Id), Loc),
+             Expression => New_Occurrence_Of (Standard_True, Loc)));
+
          --  Generate call to _Postconditions
 
          Insert_Action (Exp,
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 64de40c6a04dfa787c215bbb534f11f73e8f9e5a..43920993ff997cf2943aca2db1a928a1918f2943 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -27,42 +27,43 @@
 --    - controlled types
 --    - transient scopes
 
-with Atree;    use Atree;
-with Debug;    use Debug;
-with Einfo;    use Einfo;
-with Elists;   use Elists;
-with Errout;   use Errout;
-with Exp_Ch6;  use Exp_Ch6;
-with Exp_Ch9;  use Exp_Ch9;
-with Exp_Ch11; use Exp_Ch11;
-with Exp_Dbug; use Exp_Dbug;
-with Exp_Dist; use Exp_Dist;
-with Exp_Disp; use Exp_Disp;
-with Exp_Prag; use Exp_Prag;
-with Exp_Tss;  use Exp_Tss;
-with Exp_Util; use Exp_Util;
-with Freeze;   use Freeze;
-with Lib;      use Lib;
-with Nlists;   use Nlists;
-with Nmake;    use Nmake;
-with Opt;      use Opt;
-with Output;   use Output;
-with Restrict; use Restrict;
-with Rident;   use Rident;
-with Rtsfind;  use Rtsfind;
-with Sinfo;    use Sinfo;
-with Sem;      use Sem;
-with Sem_Aux;  use Sem_Aux;
-with Sem_Ch3;  use Sem_Ch3;
-with Sem_Ch7;  use Sem_Ch7;
-with Sem_Ch8;  use Sem_Ch8;
-with Sem_Res;  use Sem_Res;
-with Sem_Util; use Sem_Util;
-with Snames;   use Snames;
-with Stand;    use Stand;
-with Tbuild;   use Tbuild;
-with Ttypes;   use Ttypes;
-with Uintp;    use Uintp;
+with Atree;     use Atree;
+with Contracts; use Contracts;
+with Debug;     use Debug;
+with Einfo;     use Einfo;
+with Elists;    use Elists;
+with Errout;    use Errout;
+with Exp_Ch6;   use Exp_Ch6;
+with Exp_Ch9;   use Exp_Ch9;
+with Exp_Ch11;  use Exp_Ch11;
+with Exp_Dbug;  use Exp_Dbug;
+with Exp_Dist;  use Exp_Dist;
+with Exp_Disp;  use Exp_Disp;
+with Exp_Prag;  use Exp_Prag;
+with Exp_Tss;   use Exp_Tss;
+with Exp_Util;  use Exp_Util;
+with Freeze;    use Freeze;
+with Lib;       use Lib;
+with Nlists;    use Nlists;
+with Nmake;     use Nmake;
+with Opt;       use Opt;
+with Output;    use Output;
+with Restrict;  use Restrict;
+with Rident;    use Rident;
+with Rtsfind;   use Rtsfind;
+with Sinfo;     use Sinfo;
+with Sem;       use Sem;
+with Sem_Aux;   use Sem_Aux;
+with Sem_Ch3;   use Sem_Ch3;
+with Sem_Ch7;   use Sem_Ch7;
+with Sem_Ch8;   use Sem_Ch8;
+with Sem_Res;   use Sem_Res;
+with Sem_Util;  use Sem_Util;
+with Snames;    use Snames;
+with Stand;     use Stand;
+with Tbuild;    use Tbuild;
+with Ttypes;    use Ttypes;
+with Uintp;     use Uintp;
 
 package body Exp_Ch7 is
 
@@ -339,6 +340,17 @@ package body Exp_Ch7 is
    --  such as for task termination. Fin_Id is the finalizer declaration
    --  entity.
 
+   procedure Build_Finalizer_Helper
+     (N                 : Node_Id;
+      Clean_Stmts       : List_Id;
+      Mark_Id           : Entity_Id;
+      Top_Decls         : List_Id;
+      Defer_Abort       : Boolean;
+      Fin_Id            : out Entity_Id;
+      Finalize_Old_Only : Boolean);
+   --  An internal routine which does all of the heavy lifting on behalf of
+   --  Build_Finalizer.
+
    procedure Build_Finalizer_Call (N : Node_Id; Fin_Id : Entity_Id);
    --  N is a construct which contains a handled sequence of statements, Fin_Id
    --  is the entity of a finalizer. Create an At_End handler which covers the
@@ -1397,20 +1409,32 @@ package body Exp_Ch7 is
          else
             Append_Freeze_Actions (Ptr_Typ, Actions);
          end if;
+
+         Analyze_List (Actions);
+
+         --  When the type the finalization master is being generated for was
+         --  created to store a 'Old object, then mark it as such so its
+         --  finalization can be delayed until after postconditions have been
+         --  checked.
+
+         if Stores_Attribute_Old_Prefix (Ptr_Typ) then
+            Set_Stores_Attribute_Old_Prefix (Fin_Mas_Id);
+         end if;
       end;
    end Build_Finalization_Master;
 
-   ---------------------
-   -- Build_Finalizer --
-   ---------------------
+   ----------------------------
+   -- Build_Finalizer_Helper --
+   ----------------------------
 
-   procedure Build_Finalizer
+   procedure Build_Finalizer_Helper
      (N                 : Node_Id;
       Clean_Stmts       : List_Id;
       Mark_Id           : Entity_Id;
       Top_Decls         : List_Id;
       Defer_Abort       : Boolean;
-      Fin_Id            : out Entity_Id)
+      Fin_Id            : out Entity_Id;
+      Finalize_Old_Only : Boolean)
    is
       Acts_As_Clean    : constant Boolean :=
                            Present (Mark_Id)
@@ -1746,9 +1770,20 @@ package body Exp_Ch7 is
          --  The default name is _finalizer
 
          else
-            Fin_Id :=
-              Make_Defining_Identifier (Loc,
-                Chars => New_External_Name (Name_uFinalizer));
+            --  Generation of a finalization procedure exclusively for 'Old
+            --  interally generated constants requires different name since
+            --  there will need to be multiple finalization routines in the
+            --  same scope. See Build_Finalizer for details.
+
+            if Finalize_Old_Only then
+               Fin_Id :=
+                 Make_Defining_Identifier (Loc,
+                   Chars => New_External_Name (Name_uFinalizer_Old));
+            else
+               Fin_Id :=
+                 Make_Defining_Identifier (Loc,
+                   Chars => New_External_Name (Name_uFinalizer));
+            end if;
 
             --  The visibility semantics of AT_END handlers force a strange
             --  separation of spec and body for stack-related finalizers:
@@ -2051,8 +2086,26 @@ package body Exp_Ch7 is
 
             pragma Assert (Present (Spec_Decls));
 
-            Append_To (Spec_Decls, Fin_Spec);
-            Analyze (Fin_Spec);
+            --  It maybe possible that we are finalizing 'Old objects which
+            --  exist in the spec declarations. When this is the case the
+            --  Finalizer_Insert_Node will come before the end of the
+            --  Spec_Decls. So, to mitigate this, we insert the finalizer spec
+            --  earlier at the Finalizer_Insert_Nod instead of appending to the
+            --  end of Spec_Decls to prevent its body appearing before its
+            --  corresponding spec.
+
+            if Present (Finalizer_Insert_Nod)
+              and then List_Containing (Finalizer_Insert_Nod) = Spec_Decls
+            then
+               Insert_After_And_Analyze (Finalizer_Insert_Nod, Fin_Spec);
+               Finalizer_Insert_Nod := Fin_Spec;
+
+            --  Otherwise, Finalizer_Insert_Nod is not in Spec_Decls
+
+            else
+               Append_To (Spec_Decls, Fin_Spec);
+               Analyze (Fin_Spec);
+            end if;
 
             --  When the finalizer acts solely as a cleanup routine, the body
             --  is inserted right after the spec.
@@ -2194,9 +2247,26 @@ package body Exp_Ch7 is
 
          Decl := Last_Non_Pragma (Decls);
          while Present (Decl) loop
+            --  Depending on the value of flag Finalize_Old_Only we determine
+            --  which objects get finalized as part of the current finalizer
+            --  being built.
+
+            --  When True, only temporaries capturing the value of attribute
+            --  'Old are finalized and all other cases are ignored.
+
+            --  When False, temporary objects used to capture the value of 'Old
+            --  are ignored and all others are considered.
+
+            if Finalize_Old_Only
+                 xor (Nkind (Decl) = N_Object_Declaration
+                       and then Stores_Attribute_Old_Prefix
+                                  (Defining_Identifier (Decl)))
+            then
+               null;
+
             --  Library-level tagged types
 
-            if Nkind (Decl) = N_Full_Type_Declaration then
+            elsif Nkind (Decl) = N_Full_Type_Declaration then
                Typ := Defining_Identifier (Decl);
 
                --  Ignored Ghost types do not need any cleanup actions because
@@ -3409,7 +3479,7 @@ package body Exp_Ch7 is
                New_Occurrence_Of (DT_Ptr, Loc))));
       end Process_Tagged_Type_Declaration;
 
-   --  Start of processing for Build_Finalizer
+   --  Start of processing for Build_Finalizer_Helper
 
    begin
       Fin_Id := Empty;
@@ -3559,7 +3629,7 @@ package body Exp_Ch7 is
       if Acts_As_Clean or else Has_Ctrl_Objs or else Has_Tagged_Types then
          Create_Finalizer;
       end if;
-   end Build_Finalizer;
+   end Build_Finalizer_Helper;
 
    --------------------------
    -- Build_Finalizer_Call --
@@ -3642,6 +3712,468 @@ package body Exp_Ch7 is
       Expand_At_End_Handler (HSS, Empty);
    end Build_Finalizer_Call;
 
+   ---------------------
+   -- Build_Finalizer --
+   ---------------------
+
+   procedure Build_Finalizer
+     (N           : Node_Id;
+      Clean_Stmts : List_Id;
+      Mark_Id     : Entity_Id;
+      Top_Decls   : List_Id;
+      Defer_Abort : Boolean;
+      Fin_Id      : out Entity_Id)
+   is
+      Def_Ent : constant Entity_Id  := Unique_Defining_Entity (N);
+      Loc     : constant Source_Ptr := Sloc (N);
+
+      --  Declarations used for the creation of _finalization_controller
+
+      Fin_Old_Id           : Entity_Id := Empty;
+      Fin_Controller_Id    : Entity_Id := Empty;
+      Fin_Controller_Decls : List_Id;
+      Fin_Controller_Stmts : List_Id;
+      Fin_Controller_Body  : Node_Id   := Empty;
+      Fin_Controller_Spec  : Node_Id   := Empty;
+      Postconditions_Call  : Node_Id   := Empty;
+
+      --  Defining identifiers for local objects used to store exception info
+
+      Raised_Post_Exception_Id         : Entity_Id := Empty;
+      Raised_Finalization_Exception_Id : Entity_Id := Empty;
+      Saved_Exception_Id               : Entity_Id := Empty;
+
+   --  Start of processing for Build_Finalizer
+
+   begin
+      --  Create the general finalization routine
+
+      Build_Finalizer_Helper
+        (N                 => N,
+         Clean_Stmts       => Clean_Stmts,
+         Mark_Id           => Mark_Id,
+         Top_Decls         => Top_Decls,
+         Defer_Abort       => Defer_Abort,
+         Fin_Id            => Fin_Id,
+         Finalize_Old_Only => False);
+
+      --  When postconditions are present, expansion gets much more complicated
+      --  due to both the fact that they must be called after finalization and
+      --  that finalization of 'Old objects must occur after the postconditions
+      --  get checked.
+
+      --  Additionally, exceptions between general finalization and 'Old
+      --  finalization must be propagated correctly and exceptions which happen
+      --  during _postconditions need to be saved and reraised after
+      --  finalization of 'Old objects.
+
+      --  Generate:
+      --
+      --    Postcond_Enabled := False;
+      --
+      --    procedure _finalization_controller is
+      --
+      --       --  Exception capturing and tracking
+      --
+      --       Saved_Exception               : Exception_Occurrence;
+      --       Raised_Post_Exception         : Boolean := False;
+      --       Raised_Finalization_Exception : Boolean := False;
+      --
+      --    --  Start of processing for _finalization_controller
+      --
+      --    begin
+      --       --  Perform general finalization
+      --
+      --       begin
+      --          _finalizer;
+      --       exception
+      --          when others =>
+      --             --  Save the exception
+      --
+      --             Raised_Finalization_Exception := True;
+      --             Save_Occurrence
+      --               (Saved_Exception, Get_Current_Excep.all);
+      --       end;
+      --
+      --       --  Perform postcondition checks after general finalization, but
+      --       --  before finalization of 'Old related objects.
+      --
+      --       if not Raised_Finalization_Exception then
+      --          begin
+      --             --  Re-enable postconditions and check them
+      --
+      --             Postcond_Enabled := True;
+      --             _postconditions [(Result_Obj_For_Postcond[.all])];
+      --          exception
+      --             when others =>
+      --                --  Save the exception
+      --
+      --                Raised_Post_Exception := True;
+      --                Save_Occurrence
+      --                  (Saved_Exception, Get_Current_Excep.all);
+      --          end;
+      --       end if;
+      --
+      --       --  Finally finalize 'Old related objects
+      --
+      --       begin
+      --          _finalizer_old;
+      --       exception
+      --          when others =>
+      --             --  Reraise the previous finalization error if there is
+      --             --  one.
+      --
+      --             if Raised_Finalization_Exception then
+      --                Reraise_Occurrence (Saved_Exception);
+      --             end if;
+      --
+      --             --  Otherwise, reraise the current one
+      --
+      --             raise;
+      --       end;
+      --
+      --       --  Reraise any saved exception
+      --
+      --       if Raised_Finalization_Exception
+      --            or else Raised_Post_Exception
+      --       then
+      --          Reraise_Occurrence (Saved_Exception);
+      --       end if;
+      --    end _finalization_controller;
+
+      if Nkind (N) = N_Subprogram_Body
+        and then Present (Postconditions_Proc (Def_Ent))
+      then
+         Fin_Controller_Stmts := New_List;
+         Fin_Controller_Decls := New_List;
+
+         --  Build the 'Old finalizer
+
+         Build_Finalizer_Helper
+           (N                 => N,
+            Clean_Stmts       => Empty_List,
+            Mark_Id           => Mark_Id,
+            Top_Decls         => Top_Decls,
+            Defer_Abort       => Defer_Abort,
+            Fin_Id            => Fin_Old_Id,
+            Finalize_Old_Only => True);
+
+         --  Create local declarations for _finalization_controller needed for
+         --  saving exceptions.
+         --
+         --  Generate:
+         --
+         --    Saved_Exception               : Exception_Occurrence;
+         --    Raised_Post_Exception         : Boolean := False;
+         --    Raised_Finalization_Exception : Boolean := False;
+
+         Saved_Exception_Id               := Make_Temporary (Loc, 'S');
+         Raised_Post_Exception_Id         := Make_Temporary (Loc, 'P');
+         Raised_Finalization_Exception_Id := Make_Temporary (Loc, 'F');
+
+         Append_List_To (Fin_Controller_Decls, New_List (
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Saved_Exception_Id,
+             Object_Definition   =>
+               New_Occurrence_Of (RTE (RE_Exception_Occurrence), Loc)),
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Raised_Post_Exception_Id,
+             Object_Definition   => New_Occurrence_Of (Standard_Boolean, Loc),
+             Expression          => New_Occurrence_Of (Standard_False, Loc)),
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Raised_Finalization_Exception_Id,
+             Object_Definition   => New_Occurrence_Of (Standard_Boolean, Loc),
+             Expression          => New_Occurrence_Of (Standard_False, Loc))));
+
+         --  Call _finalizer and save any exceptions which occur
+
+         --  Generate:
+         --
+         --    begin
+         --       _finalizer;
+         --    exception
+         --       when others =>
+         --          Raised_Finalization_Exception := True;
+         --          Save_Occurrence
+         --            (Saved_Exception, Get_Current_Excep.all);
+         --    end;
+
+         if Present (Fin_Id) then
+            Append_To (Fin_Controller_Stmts,
+              Make_Block_Statement (Loc,
+                Handled_Statement_Sequence =>
+                  Make_Handled_Sequence_Of_Statements (Loc,
+                    Statements         => New_List (
+                      Make_Procedure_Call_Statement (Loc,
+                        Name => New_Occurrence_Of (Fin_Id, Loc))),
+                    Exception_Handlers => New_List (
+                      Make_Exception_Handler (Loc,
+                        Exception_Choices => New_List (
+                          Make_Others_Choice (Loc)),
+                        Statements        => New_List (
+                          Make_Assignment_Statement (Loc,
+                            Name       =>
+                              New_Occurrence_Of
+                                (Raised_Finalization_Exception_Id, Loc),
+                            Expression =>
+                              New_Occurrence_Of (Standard_True, Loc)),
+                          Make_Procedure_Call_Statement (Loc,
+                             Name                   =>
+                               New_Occurrence_Of
+                                 (RTE (RE_Save_Occurrence), Loc),
+                             Parameter_Associations => New_List (
+                               New_Occurrence_Of
+                                 (Saved_Exception_Id, Loc),
+                               Make_Explicit_Dereference (Loc,
+                                 Prefix =>
+                                   Make_Function_Call (Loc,
+                                     Name =>
+                                       Make_Explicit_Dereference (Loc,
+                                         Prefix =>
+                                           New_Occurrence_Of
+                                             (RTE (RE_Get_Current_Excep),
+                                              Loc))))))))))));
+         end if;
+
+         --  Create the call to postconditions based on the kind of the current
+         --  subprogram, and the type of the Result_Obj_For_Postcond.
+
+         --  Generate:
+         --
+         --    _postconditions (Result_Obj_For_Postcond[.all]);
+         --
+         --   or
+         --
+         --    _postconditions;
+
+         if Ekind (Def_Ent) = E_Procedure then
+            Postconditions_Call :=
+              Make_Procedure_Call_Statement (Loc,
+                Name =>
+                  New_Occurrence_Of
+                    (Postconditions_Proc (Def_Ent), Loc));
+         else
+            Postconditions_Call :=
+              Make_Procedure_Call_Statement (Loc,
+                Name                   =>
+                  New_Occurrence_Of
+                    (Postconditions_Proc (Def_Ent), Loc),
+                Parameter_Associations => New_List (
+                  (if Is_Elementary_Type (Etype (Def_Ent)) then
+                      New_Occurrence_Of
+                        (Get_Result_Object_For_Postcond
+                          (Def_Ent), Loc)
+                   else
+                      Make_Explicit_Dereference (Loc,
+                        New_Occurrence_Of
+                          (Get_Result_Object_For_Postcond
+                            (Def_Ent), Loc)))));
+         end if;
+
+         --  Call _postconditions when no general finalization exceptions have
+         --  occured taking care to enable the postconditions and save any
+         --  exception occurrences.
+
+         --  Generate:
+         --
+         --    if not Raised_Finalization_Exception then
+         --       begin
+         --          Postcond_Enabled := True;
+         --          _postconditions [(Result_Obj_For_Postcond[.all])];
+         --       exception
+         --          when others =>
+         --             Raised_Post_Exception := True;
+         --             Save_Occurrence
+         --               (Saved_Exception, Get_Current_Excep.all);
+         --       end;
+         --    end if;
+
+         Append_To (Fin_Controller_Stmts,
+           Make_If_Statement (Loc,
+             Condition       =>
+               Make_Op_Not (Loc,
+                 Right_Opnd =>
+                   New_Occurrence_Of
+                     (Raised_Finalization_Exception_Id, Loc)),
+             Then_Statements => New_List (
+               Make_Block_Statement (Loc,
+                 Handled_Statement_Sequence =>
+                   Make_Handled_Sequence_Of_Statements (Loc,
+                     Statements         => New_List (
+                       Make_Assignment_Statement (Loc,
+                         Name       =>
+                           New_Occurrence_Of
+                             (Get_Postcond_Enabled (Def_Ent), Loc),
+                         Expression =>
+                            New_Occurrence_Of
+                              (Standard_True, Loc)),
+                       Postconditions_Call),
+                     Exception_Handlers => New_List (
+                       Make_Exception_Handler (Loc,
+                         Exception_Choices => New_List (
+                           Make_Others_Choice (Loc)),
+                         Statements        => New_List (
+                           Make_Assignment_Statement (Loc,
+                             Name       =>
+                               New_Occurrence_Of
+                                 (Raised_Post_Exception_Id, Loc),
+                             Expression =>
+                               New_Occurrence_Of (Standard_True, Loc)),
+                           Make_Procedure_Call_Statement (Loc,
+                              Name                   =>
+                                New_Occurrence_Of
+                                  (RTE (RE_Save_Occurrence), Loc),
+                              Parameter_Associations => New_List (
+                                New_Occurrence_Of
+                                  (Saved_Exception_Id, Loc),
+                                Make_Explicit_Dereference (Loc,
+                                  Prefix =>
+                                    Make_Function_Call (Loc,
+                                      Name =>
+                                        Make_Explicit_Dereference (Loc,
+                                          Prefix =>
+                                            New_Occurrence_Of
+                                              (RTE (RE_Get_Current_Excep),
+                                               Loc))))))))))))));
+
+         --  Call _finalizer_old and reraise any exception that occurred during
+         --  initial finalization within the exception handler. Otherwise,
+         --  propagate the current exception.
+
+         --  Generate:
+         --
+         --    begin
+         --       _finalizer_old;
+         --    exception
+         --       when others =>
+         --          if Raised_Finalization_Exception then
+         --             Reraise_Occurrence (Saved_Exception);
+         --          end if;
+         --          raise;
+         --    end;
+
+         if Present (Fin_Old_Id) then
+            Append_To (Fin_Controller_Stmts,
+              Make_Block_Statement (Loc,
+                Handled_Statement_Sequence =>
+                  Make_Handled_Sequence_Of_Statements (Loc,
+                    Statements         => New_List (
+                      Make_Procedure_Call_Statement (Loc,
+                        Name => New_Occurrence_Of (Fin_Old_Id, Loc))),
+                    Exception_Handlers => New_List (
+                      Make_Exception_Handler (Loc,
+                        Exception_Choices => New_List (
+                          Make_Others_Choice (Loc)),
+                        Statements        => New_List (
+                          Make_If_Statement (Loc,
+                            Condition       =>
+                              New_Occurrence_Of
+                                (Raised_Finalization_Exception_Id, Loc),
+                            Then_Statements => New_List (
+                              Make_Procedure_Call_Statement (Loc,
+                                Name                   =>
+                                  New_Occurrence_Of
+                                    (RTE (RE_Reraise_Occurrence), Loc),
+                                Parameter_Associations => New_List (
+                                  New_Occurrence_Of
+                                    (Saved_Exception_Id, Loc))))),
+                          Make_Raise_Statement (Loc)))))));
+         end if;
+
+         --  Once finalization is complete reraise any pending exceptions
+
+         --  Generate:
+         --
+         --    if Raised_Post_Exception
+         --      or else Raised_Finalization_Exception
+         --    then
+         --       Reraise_Occurrence (Saved_Exception);
+         --    end if;
+
+         Append_To (Fin_Controller_Stmts,
+           Make_If_Statement (Loc,
+             Condition       =>
+               Make_Or_Else (Loc,
+                 Left_Opnd  =>
+                   New_Occurrence_Of
+                     (Raised_Post_Exception_Id, Loc),
+                 Right_Opnd =>
+                   New_Occurrence_Of
+                     (Raised_Finalization_Exception_Id, Loc)),
+             Then_Statements => New_List (
+               Make_Procedure_Call_Statement (Loc,
+                 Name            =>
+                   New_Occurrence_Of (RTE (RE_Reraise_Occurrence), Loc),
+                 Parameter_Associations => New_List (
+                   New_Occurrence_Of
+                     (Saved_Exception_Id, Loc))))));
+
+         --  Make the finalization controller subprogram body and declaration.
+
+         --  Generate:
+         --    procedure _finalization_controller;
+         --
+         --    procedure _finalization_controller is
+         --    begin
+         --       [Fin_Controller_Stmts];
+         --    end;
+
+         Fin_Controller_Id :=
+           Make_Defining_Identifier (Loc,
+             Chars => New_External_Name (Name_uFinalization_Controller));
+
+         Fin_Controller_Spec :=
+           Make_Subprogram_Declaration (Loc,
+             Specification =>
+               Make_Procedure_Specification (Loc,
+                 Defining_Unit_Name => Fin_Controller_Id));
+
+         Fin_Controller_Body :=
+           Make_Subprogram_Body (Loc,
+             Specification              =>
+               Make_Procedure_Specification (Loc,
+                 Defining_Unit_Name =>
+                   Make_Defining_Identifier (Loc, Chars (Fin_Controller_Id))),
+             Declarations               => Fin_Controller_Decls,
+             Handled_Statement_Sequence =>
+               Make_Handled_Sequence_Of_Statements (Loc,
+                 Statements => Fin_Controller_Stmts));
+
+         --  Disable _postconditions calls which get generated before return
+         --  statements to delay their evaluation until after finalization.
+
+         --  This is done by way of the local Postcond_Enabled object which is
+         --  initially assigned to True - we then create an assignment within
+         --  the subprogram's declaration to make it False and assign it back
+         --  to True before _postconditions is called within
+         --  _finalization_controller.
+
+         --  Generate:
+         --
+         --    Postcond_Enable := False;
+
+         Append_To (Top_Decls,
+           Make_Assignment_Statement (Loc,
+             Name       =>
+               New_Occurrence_Of
+                 (Get_Postcond_Enabled (Def_Ent), Loc),
+             Expression =>
+               New_Occurrence_Of
+                 (Standard_False, Loc)));
+
+         --  Add the subprogram to the list of declarations an analyze it
+
+         Append_To (Top_Decls, Fin_Controller_Spec);
+         Analyze (Fin_Controller_Spec);
+         Insert_After (Fin_Controller_Spec, Fin_Controller_Body);
+         Analyze (Fin_Controller_Body, Suppress => All_Checks);
+
+         --  Return the finalization controller as the result Fin_Id
+
+         Fin_Id := Fin_Controller_Id;
+      end if;
+   end Build_Finalizer;
+
    ---------------------
    -- Build_Late_Proc --
    ---------------------
@@ -4806,6 +5338,12 @@ package body Exp_Ch7 is
                                  Nkind (N) = N_Block_Statement
                                    and then Present (Cleanup_Actions (N));
 
+      Has_Postcondition      : constant Boolean :=
+                                 Nkind (N) = N_Subprogram_Body
+                                   and then Present
+                                              (Postconditions_Proc
+                                                (Unique_Defining_Entity (N)));
+
       Actions_Required       : constant Boolean :=
                                  Requires_Cleanup_Actions (N, True)
                                    or else Is_Asynchronous_Call
@@ -5020,6 +5558,34 @@ package body Exp_Ch7 is
             end;
          end if;
 
+         --  Move the _postconditions subprogram declaration and its associated
+         --  objects into the declarations section so that it is callable
+         --  within _postconditions.
+
+         if Has_Postcondition then
+            declare
+               Decl      : Node_Id;
+               Prev_Decl : Node_Id;
+
+            begin
+               Decl :=
+                 Prev (Subprogram_Body
+                        (Postconditions_Proc (Current_Subprogram)));
+               while Present (Decl) loop
+                  Prev_Decl := Prev (Decl);
+
+                  Remove (Decl);
+                  Prepend_To (New_Decls, Decl);
+
+                  exit when Nkind (Decl) = N_Subprogram_Declaration
+                              and then Chars (Corresponding_Body (Decl))
+                                         = Name_uPostconditions;
+
+                  Decl := Prev_Decl;
+               end loop;
+            end;
+         end if;
+
          --  Ensure the presence of a declaration list in order to successfully
          --  append all original statements to it.
 
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 9a227c693d7f3074bd12f4cfd94bc38b457e8338..d616fb6d901b5de2a18600fe17b418c3e1ad5583 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -1581,6 +1581,12 @@ package body Exp_Prag is
                       Expression => Pref));
                end if;
 
+               --  Mark the temporary as coming from a 'Old reference
+
+               if Present (Temp) then
+                  Set_Stores_Attribute_Old_Prefix (Temp);
+               end if;
+
                --  Ensure that the prefix is valid
 
                if Validity_Checks_On and then Validity_Check_Operands then
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 9aff0f591938297f2bde93e239ffd9bd0534fe3d..29c11cd397c13fec36e8879ecfb8b52056d6b278 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2490,13 +2490,11 @@ package body Sem_Ch6 is
          Result : Entity_Id := Empty;
 
       begin
-         --  Loop outward through the Scope_Stack, skipping blocks, loops,
-         --  and postconditions.
+         --  Loop outward through the Scope_Stack, skipping blocks, and loops
 
          for J in reverse 0 .. Scope_Stack.Last loop
             Result := Scope_Stack.Table (J).Entity;
-            exit when Ekind (Result) not in E_Block | E_Loop
-              and then Chars (Result) /= Name_uPostconditions;
+            exit when Ekind (Result) not in E_Block | E_Loop;
          end loop;
 
          pragma Assert (Present (Result));
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index b093808113a173cbbb25ba249a46ce48b8b799af..1a2d2a2d125ab841b1ea3e2576c9bd2433b6b4ba 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -30651,8 +30651,10 @@ package body Sem_Prag is
       --  The pragma appears inside the statements of a subprogram body. This
       --  placement is the result of subprogram contract expansion.
 
-      elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then
-         return Parent (Context);
+      elsif Is_Statement (Context)
+        and then Present (Enclosing_HSS (Context))
+      then
+         return Parent (Enclosing_HSS (Context));
 
       --  The pragma appears inside the declarative part of a package body
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index c695cbc5266b6f77139d395b976245a49368a5a4..bb078d285736e28e646c9c45355e6f43848d028f 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7931,6 +7931,34 @@ package body Sem_Util is
       return Empty;
    end Enclosing_Generic_Unit;
 
+   -------------------
+   -- Enclosing_HSS --
+   -------------------
+
+   function Enclosing_HSS (Stmt : Node_Id) return Node_Id is
+      Par : Node_Id;
+   begin
+      pragma Assert (Is_Statement (Stmt));
+
+      Par := Parent (Stmt);
+      while Present (Par) loop
+
+         if Nkind (Par) = N_Handled_Sequence_Of_Statements then
+            return Par;
+
+         --  Prevent the search from going too far
+
+         elsif Is_Body_Or_Package_Declaration (Par) then
+            return Empty;
+
+         end if;
+
+         Par := Parent (Par);
+      end loop;
+
+      return Par;
+   end Enclosing_HSS;
+
    -------------------------------
    -- Enclosing_Lib_Unit_Entity --
    -------------------------------
@@ -31180,9 +31208,9 @@ package body Sem_Util is
                --  If the prefix is of an anonymous access type, then returns
                --  the designated type of that type.
 
-            -----------------------------
+               -----------------------------
                -- Designated_Subtype_Mark --
-            -----------------------------
+               -----------------------------
 
                function Designated_Subtype_Mark return Node_Id is
                   Typ : Entity_Id := Prefix_Type;
@@ -31220,6 +31248,16 @@ package body Sem_Util is
                   Append_Item (Temp_Decl, Is_Eval_Stmt => False);
                end if;
 
+               --  When a type associated with an indirect temporary gets
+               --  created for a 'Old attribute reference we need to mark
+               --  the type as such. This allows, for example, finalization
+               --  masters associated with them to be finalized in the correct
+               --  order after postcondition checks.
+
+               if Attribute_Name (Parent (Attr_Prefix)) = Name_Old then
+                  Set_Stores_Attribute_Old_Prefix (Access_Type_Id);
+               end if;
+
                Analyze (Access_Type_Decl);
                Analyze (Temp_Decl);
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 2e913594bc08c55cfa62d621fce9702a60a27213..d812b295fcaa1880c2146f8df7b89124aef0ee16 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -765,6 +765,10 @@ package Sem_Util is
    --  Returns the Node_Id associated with the innermost enclosing generic
    --  unit, if any. If none, then returns Empty.
 
+   function Enclosing_HSS (Stmt : Node_Id) return Node_Id;
+   --  Returns the nearest handled sequence of statements that encloses a given
+   --  statement, or Empty.
+
    function Enclosing_Lib_Unit_Entity
      (E : Entity_Id := Current_Scope) return Entity_Id;
    --  Returns the entity of enclosing library unit node which is the root of
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 647fb62f589bf6db0a088009cf0e2e36cee1ab23..715a53a5e4b5e226c3b74486ad96353c3e03e00d 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -168,6 +168,8 @@ package Snames is
    Name_uEntry_Bodies                  : constant Name_Id := N + $;
    Name_uExpunge                       : constant Name_Id := N + $;
    Name_uFinalizer                     : constant Name_Id := N + $;
+   Name_uFinalizer_Old                 : constant Name_Id := N + $;
+   Name_uFinalization_Controller       : constant Name_Id := N + $;
    Name_uIdepth                        : constant Name_Id := N + $;
    Name_uInit                          : constant Name_Id := N + $;
    Name_uInit_Level                    : constant Name_Id := N + $;
@@ -176,11 +178,14 @@ package Snames is
    Name_uObject                        : constant Name_Id := N + $;
    Name_uPost                          : constant Name_Id := N + $;
    Name_uPostconditions                : constant Name_Id := N + $;
+   Name_uPostcond_Enabled              : constant Name_Id := N + $;
    Name_uPre                           : constant Name_Id := N + $;
    Name_uPriority                      : constant Name_Id := N + $;
    Name_uProcess_ATSD                  : constant Name_Id := N + $;
    Name_uRelative_Deadline             : constant Name_Id := N + $;
    Name_uResult                        : constant Name_Id := N + $;
+   Name_uResult_Object_For_Postcond    : constant Name_Id := N + $;
+   Name_uReturn_Success_For_Postcond   : constant Name_Id := N + $;
    Name_uSecondary_Stack               : constant Name_Id := N + $;
    Name_uSecondary_Stack_Size          : constant Name_Id := N + $;
    Name_uService                       : constant Name_Id := N + $;