[Ada] Tech debt: Expansion of contracts

This patch modifies the expansion of contracts such that the statements
and declarations of a subprogram with post-execution checks get moved to
a local internally generated subprogram which the original subprogram
calls directly followed by the required post-execution checks.

This differs from the current implementation which requires delicate
machinary which coordinates with the finalization process to emulate the
desired behavior within the "at end" procedure.

gcc/ada/

	* contracts.adb, contracts.ads
	(Analyze_Pragmas_In_Declarations): Added to aid in the new
	expansion model so that pragmas relating to contracts can get
	processed early before the rest of the subprogram containing them.
	(Build_Subprogram_Contract_Wrapper): Created to do the majority of
	expansion for postconditions. It builds a local wrapper with the
	statements and declarations within a given subprogram.
	(Is_Prologue_Renaming): Moved out from Process_Preconditions to be
	used generally within the contracts package.
	(Build_Entry_Contract_Wrapper): Moved from exp_ch7.
	(Expand_Subprogram_Contract): Add new local variable Decls to
	store expanded declarations needed for evaluation of contracts.
	Call new wrapper building procedure and modify comments to match
	new expansion model.
	(Get_Postcond_Enabled): Deleted.
	(Get_Result_Object_For_Postcond): Deleted.
	(Get_Return_Success_For_Postcond): Deleted.
	(Process_Contract_Cases): Add new parameter to store declarations.
	(Process_Postconditions): Add new parameter to store declarations.
	(Process_Preconditions): Add new parameter to store declarations.
	Add code to move entry-call prologue renamings
	* einfo.ads: Document new field Wrapped_Statements and modify
	comment for Postconditions_Proc.
	* exp_attr.adb
	(Analyze_Attribute): Modify expansion of the 'Old attribute to
	recognize new expansion model and use Wrapped_Statements instead
	of Postconditions_Proc.
	* exp_ch6.adb
	(Add_Return): Remove special expansion for postconditions.
	(Expand_Call): Modify condition checking for calls to access
	subprogram wrappers to handle new expansion models.
	(Expand_Call_Helper): Remove special expansion for postconditions.
	(Expand_Non_Function_Return): Remove special expansion for
	postconditions.
	(Expand_Simple_Function_Return): Remove special expansion for
	postconditions.
	* exp_ch7.adb
	(Build_Finalizer): Deleted, but replaced by code in
	Build_Finalizer_Helper
	(Build_Finalizer_Helper): Renamed to Build_Finalizer, and special
	handling of 'Old objects removed.
	* exp_ch9.adb
	(Build_Contract_Wrapper): Renamed and moved to contracts package.
	* exp_prag.adb
	(Expand_Pragma_Contract_Cases): Delay analysis of contracts since
	they now instead get analyzed as part of the wrapper generation
	instead of after analysis of their corresponding subprogram's
	body.
	(Expand_Pragma_Check): Label expanded if-statements which come
	from the expansion of assertion statements as
	Comes_From_Check_Or_Contract.
	* freeze.adb
	(Freeze_Entity): Add special case to avoid freezing when a freeze
	node gets generated as part of the expansion of a postcondition
	check.
	* gen_il-gen-gen_nodes.adb: Add new flag
	Comes_From_Check_Or_Contract.
	* gen_il-fields.ads: Add new field Wrapped_Statements. Add new
	flag Comes_From_Check_Or_Contract.
	* gen_il-gen-gen_entities.adb: Add new field Wrapped_Statements.
	* ghost.adb
	(Is_OK_Declaration): Replace Name_uPostconditions with
	Name_uWrapped_Statements.
	(Is_OK_Statement): Simplify condition due to the loss of
	Original_Node as a result of the new expansion model of contracts
	and use new flag Comes_From_Check_Or_Contract in its place.
	* inline.adb
	(Declare_Postconditions_Result): Replace Name_uPostconditions with
	Name_uWrapped_Statements.
	(Expand_Inlined_Call): Replace Name_uPostconditions with
	Name_uWrapped_Statements.
	* lib.adb, lib.ads
	(ipu): Created to aid in debugging.
	* lib-xref.adb
	(Generate_References): Remove special handling for postcondition
	procedures.
	* sem_attr.adb
	(Analyze_Attribute_Old_Result): Add new context in which 'Old can
	appear due to the changes in expansion. Replace
	Name_uPostconditions with Name_uWrapped_Statements.
	(Result): Replace Name_uPostconditions with
	Name_uWrapped_Statements.
	* sem_ch11.adb
	(Analyze_Handled_Statements): Remove check to exclude warnings on
	useless assignments within postcondition procedures since
	postconditions no longer get isolated into separate subprograms.
	* sem_ch6.adb
	(Analyze_Generic_Subprogram_Body): Modify expansion of generic
	subprogram bodies so that contracts (and their associated pragmas)
	get analyzed first.
	(Analyze_Subprogram_Body_Helper): Remove global HSS variable due
	to the HSS of the body potentially changing during the expansion
	of contracts. In cases where it was used instead directly call
	Handled_Statement_Sequence. Modify expansion of subprogram bodies
	so that contracts (and their associated pragmas) get analyzed
	first.
	(Check_Missing_Return): Create local HSS variable instead of using
	a global one.
	(Move_Pragmas): Use new pragma table instead of an explicit list.
	* sem_elab.adb
	(Is_Postconditions_Proc): Deleted since the new scheme of
	expansion no longer divides postcondition checks to a separate
	subprogram and so cannot be easily identified (similar to
	pre-condition checks).
	(Info_Call): Remove info printing for _Postconditions subprograms.
	(Is_Assertion_Pragma_Target): Remove check for postconditions
	procedure
	(Is_Bridge_Target): Remove check for postconditions procedure.
	(Get_Invocation_Attributes): Remove unneeded local variables and
	check for postconditions procedure.
	(Output_Call): Remove info printing for _Postconditions
	subprograms.
	* sem_prag.adb, sem_prag.ads: Add new Pragma table for pragmas
	significant to subprograms, along with tech-debt comment.
	(Check_Arg_Is_Local_Name): Modified to recognize the new
	_Wrapped_Statements internal subprogram and the new expansion
	model.
	(Relocate_Pragmas_To_Body): Replace Name_uPostconditions with
	Name_uWrapped_Statements.
	* sem_res.adb
	(Resolve_Entry_Call): Add conditional to detect both contract
	based wrappers of entries, but also wrappers generated as part of
	general contract expansion (e.g. local postconditions
	subprograms).
	* sem_util.adb
	(Accessibility_Level): Verify 'Access is not taken based on a
	component of a function result.
	(Has_Significant_Contracts): Replace Name_uPostconditions with
	Name_uWrapped_Statements.
	(Same_Or_Aliased_Subprogram): Add conditional to detect and obtain
	the original subprogram based on the new concept of
	"postcondition" wrappers.
	* sinfo.ads: Add documentation for new flag
	Comes_From_Check_Or_Contract.
	* snames.ads-tmpl: Remove Name_uPostconditions and add
	Name_uWrapped_Statements

27 files changed, 900 insertions, 1620 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 1081b98..3f85ebc9 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -68,6 +68,19 @@ package body Contracts is
    --
    --    Part_Of
 
+   procedure Build_Subprogram_Contract_Wrapper
+     (Body_Id : Entity_Id;
+      Stmts   : List_Id;
+      Decls   : List_Id;
+      Result  : Entity_Id);
+   --  Generate a wrapper for a given subprogram body when the expansion of
+   --  postconditions require it by moving its declarations and statements
+   --  into a locally declared subprogram _Wrapped_Statements.
+
+   --  Postcondition and precondition checks then get inserted in place of
+   --  the original statements and declarations along with a call to
+   --  _Wrapped_Statements.
+
    procedure Check_Class_Condition
      (Cond            : Node_Id;
       Subp            : Entity_Id;
@@ -78,6 +91,10 @@ package body Contracts is
    --  In SPARK_Mode, an inherited operation that is not overridden but has
    --  inherited modified conditions pre/postconditions is illegal.
 
+   function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
+   --  Determine whether arbitrary declaration Decl denotes a renaming of
+   --  a discriminant or protection field _object.
+
    procedure Check_Type_Or_Object_External_Properties
      (Type_Or_Obj_Id : Entity_Id);
    --  Perform checking of external properties pragmas that is common to both
@@ -488,6 +505,45 @@ package body Contracts is
       end loop;
    end Analyze_Contracts;
 
+   -------------------------------------
+   -- Analyze_Pragmas_In_Declarations --
+   -------------------------------------
+
+   procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id) is
+      Curr_Decl : Node_Id;
+
+   begin
+      --  Move through the body's declarations analyzing all pragmas which
+      --  appear at the top of the declarations.
+
+      Curr_Decl := First (Declarations (Unit_Declaration_Node (Body_Id)));
+      while Present (Curr_Decl) loop
+
+         if Nkind (Curr_Decl) = N_Pragma then
+
+            if Pragma_Significant_To_Subprograms
+                 (Get_Pragma_Id (Curr_Decl))
+            then
+               Analyze (Curr_Decl);
+            end if;
+
+         --  Skip the renamings of discriminants and protection fields
+
+         elsif Is_Prologue_Renaming (Curr_Decl) then
+            null;
+
+         --  We have reached something which is not a pragma so we can be sure
+         --  there are no more contracts or pragmas which need to be taken into
+         --  account.
+
+         else
+            exit;
+         end if;
+
+         Next (Curr_Decl);
+      end loop;
+   end Analyze_Pragmas_In_Declarations;
+
    -----------------------------------------------
    -- Analyze_Entry_Or_Subprogram_Body_Contract --
    -----------------------------------------------
@@ -644,7 +700,7 @@ package body Contracts is
 
          else
             declare
-               Bod          : Node_Id;
+               Bod          : Node_Id := Empty;
                Freeze_Types : Boolean := False;
 
             begin
@@ -1499,6 +1555,442 @@ package body Contracts is
         (Type_Or_Obj_Id => Type_Id);
    end Analyze_Type_Contract;
 
+   ---------------------------------------
+   -- Build_Subprogram_Contract_Wrapper --
+   ---------------------------------------
+
+   procedure Build_Subprogram_Contract_Wrapper
+     (Body_Id : Entity_Id;
+      Stmts   : List_Id;
+      Decls   : List_Id;
+      Result  : Entity_Id)
+   is
+      Actuals   : constant List_Id    := Empty_List;
+      Body_Decl : constant Entity_Id  := Unit_Declaration_Node (Body_Id);
+      Loc       : constant Source_Ptr := Sloc (Body_Decl);
+      Spec_Id   : constant Entity_Id  := Corresponding_Spec (Body_Decl);
+      Subp_Id   : Entity_Id;
+      Ret_Type  : Entity_Id;
+
+      Wrapper_Id   : Entity_Id;
+      Wrapper_Body : Node_Id;
+      Wrapper_Spec : Node_Id;
+
+   begin
+      --  When there are no postcondition statements we do not need to
+      --  generate a wrapper.
+
+      if No (Stmts) then
+         return;
+      end if;
+
+      --  Obtain the related subprogram id from the body id.
+
+      if Present (Spec_Id) then
+         Subp_Id := Spec_Id;
+      else
+         Subp_Id := Body_Id;
+      end if;
+      Ret_Type := Etype (Subp_Id);
+
+      --  Generate the contracts wrapper by moving the original declarations
+      --  and statements within a local subprogram and calling it within
+      --  an extended return to preserve the result for the purpose of
+      --  evaluating postconditions, contracts, type invariants, etc.
+
+      --  Generate:
+      --
+      --  function Original_Func (X : in out Integer) return Typ is
+      --     <prologue renamings>
+      --     <preconditions>
+      --
+      --     function _Wrapped_Statements return Typ is
+      --        <original declarations>
+      --     begin
+      --        <original statements>
+      --     end;
+      --
+      --  begin
+      --     return
+      --        Result_Obj : constant Typ := _Wrapped_Statements
+      --     do
+      --        <postconditions statments>
+      --     end return;
+      --  end;
+      --
+      --  Or, in the case of a procedure:
+      --
+      --  procedure Original_Proc (X : in out Integer) is
+      --     <prologue renamings>
+      --     <preconditions>
+      --
+      --     procedure _Wrapped_Statements is
+      --        <original declarations>
+      --     begin
+      --        <original statements>
+      --     end;
+      --
+      --  begin
+      --     _Wrapped_Statements;
+      --     <postconditions statments>
+      --  end;
+      --
+
+      --  Create Identifier
+
+      Wrapper_Id := Make_Defining_Identifier (Loc, Name_uWrapped_Statements);
+      Set_Debug_Info_Needed  (Wrapper_Id);
+      Set_Wrapped_Statements (Subp_Id, Wrapper_Id);
+
+      --  Create specification and declaration for the wrapper
+
+      if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
+         Wrapper_Spec :=
+           Make_Procedure_Specification (Loc,
+             Defining_Unit_Name => Wrapper_Id);
+      else
+         Wrapper_Spec :=
+           Make_Function_Specification (Loc,
+             Defining_Unit_Name => Wrapper_Id,
+             Result_Definition  => New_Occurrence_Of (Ret_Type, Loc));
+      end if;
+
+      --  Create the wrapper body using Body_Id's statements and declarations
+
+      Wrapper_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification              => Wrapper_Spec,
+          Declarations               => Declarations (Body_Decl),
+          Handled_Statement_Sequence =>
+            Relocate_Node (Handled_Statement_Sequence (Body_Decl)));
+
+      Append_To (Decls, Wrapper_Body);
+      Set_Declarations (Body_Decl, Decls);
+      Set_Handled_Statement_Sequence (Body_Decl,
+        Make_Handled_Sequence_Of_Statements (Loc,
+          End_Label  => Make_Identifier (Loc, Chars (Wrapper_Id)),
+          Statements => New_List));
+
+      --  Move certain flags which are relevant to the body
+
+      --  Wouldn't a better way be to perform some sort of copy of Body_Decl
+      --  for Wrapper_Body be less error-prone ???
+
+      if Was_Expression_Function (Body_Decl) then
+         Set_Was_Expression_Function (Body_Decl, False);
+         Set_Was_Expression_Function (Wrapper_Body);
+      end if;
+
+      Set_Has_Pragma_Inline (Wrapper_Id, Has_Pragma_Inline (Subp_Id));
+      Set_Has_Pragma_Inline_Always
+        (Wrapper_Id, Has_Pragma_Inline_Always (Subp_Id));
+
+      --  Generate call to the wrapper
+
+      if No (Ret_Type) or else Ret_Type = Standard_Void_Type then
+         Prepend_To (Stmts,
+           Make_Procedure_Call_Statement (Loc,
+             Name => New_Occurrence_Of (Wrapper_Id, Loc)));
+         Set_Statements
+           (Handled_Statement_Sequence (Body_Decl), Stmts);
+
+      --  Generate the post-execution statements and the extended return
+      --  when the subprogram being wrapped is a function.
+
+      else
+         Set_Statements (Handled_Statement_Sequence (Body_Decl), New_List (
+           Make_Extended_Return_Statement (Loc,
+             Return_Object_Declarations => New_List (
+                Make_Object_Declaration (Loc,
+                  Defining_Identifier => Result,
+                  Object_Definition   =>
+                    New_Occurrence_Of (Ret_Type, Loc),
+                  Expression          =>
+                    Make_Function_Call (Loc,
+                      Name                   =>
+                        New_Occurrence_Of (Wrapper_Id, Loc),
+                      Parameter_Associations => Actuals))),
+             Handled_Statement_Sequence =>
+               Make_Handled_Sequence_Of_Statements (Loc,
+                 Statements => Stmts))));
+      end if;
+   end Build_Subprogram_Contract_Wrapper;
+
+   ----------------------------------
+   -- Build_Entry_Contract_Wrapper --
+   ----------------------------------
+
+   procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
+      Conc_Typ : constant Entity_Id  := Scope (E);
+      Loc      : constant Source_Ptr := Sloc (E);
+
+      procedure Add_Discriminant_Renamings
+        (Obj_Id : Entity_Id;
+         Decls  : List_Id);
+      --  Add renaming declarations for all discriminants of concurrent type
+      --  Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
+      --  represents the concurrent object.
+
+      procedure Add_Matching_Formals
+        (Formals : List_Id;
+         Actuals : in out List_Id);
+      --  Add formal parameters that match those of entry E to list Formals.
+      --  The routine also adds matching actuals for the new formals to list
+      --  Actuals.
+
+      procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
+      --  Relocate pragma Prag to list To. The routine creates a new list if
+      --  To does not exist.
+
+      --------------------------------
+      -- Add_Discriminant_Renamings --
+      --------------------------------
+
+      procedure Add_Discriminant_Renamings
+        (Obj_Id : Entity_Id;
+         Decls  : List_Id)
+      is
+         Discr         : Entity_Id;
+         Renaming_Decl : Node_Id;
+
+      begin
+         --  Inspect the discriminants of the concurrent type and generate a
+         --  renaming for each one.
+
+         if Has_Discriminants (Conc_Typ) then
+            Discr := First_Discriminant (Conc_Typ);
+            while Present (Discr) loop
+               Renaming_Decl :=
+                 Make_Object_Renaming_Declaration (Loc,
+                   Defining_Identifier =>
+                     Make_Defining_Identifier (Loc, Chars (Discr)),
+                   Subtype_Mark        =>
+                     New_Occurrence_Of (Etype (Discr), Loc),
+                   Name                =>
+                     Make_Selected_Component (Loc,
+                       Prefix        => New_Occurrence_Of (Obj_Id, Loc),
+                       Selector_Name =>
+                         Make_Identifier (Loc, Chars (Discr))));
+
+               Prepend_To (Decls, Renaming_Decl);
+
+               Next_Discriminant (Discr);
+            end loop;
+         end if;
+      end Add_Discriminant_Renamings;
+
+      --------------------------
+      -- Add_Matching_Formals --
+      --------------------------
+
+      procedure Add_Matching_Formals
+        (Formals : List_Id;
+         Actuals : in out List_Id)
+      is
+         Formal     : Entity_Id;
+         New_Formal : Entity_Id;
+
+      begin
+         --  Inspect the formal parameters of the entry and generate a new
+         --  matching formal with the same name for the wrapper. A reference
+         --  to the new formal becomes an actual in the entry call.
+
+         Formal := First_Formal (E);
+         while Present (Formal) loop
+            New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
+            Append_To (Formals,
+              Make_Parameter_Specification (Loc,
+                Defining_Identifier => New_Formal,
+                In_Present          => In_Present  (Parent (Formal)),
+                Out_Present         => Out_Present (Parent (Formal)),
+                Parameter_Type      =>
+                  New_Occurrence_Of (Etype (Formal), Loc)));
+
+            if No (Actuals) then
+               Actuals := New_List;
+            end if;
+
+            Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
+            Next_Formal (Formal);
+         end loop;
+      end Add_Matching_Formals;
+
+      ---------------------
+      -- Transfer_Pragma --
+      ---------------------
+
+      procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
+         New_Prag : Node_Id;
+
+      begin
+         if No (To) then
+            To := New_List;
+         end if;
+
+         New_Prag := Relocate_Node (Prag);
+
+         Set_Analyzed (New_Prag, False);
+         Append       (New_Prag, To);
+      end Transfer_Pragma;
+
+      --  Local variables
+
+      Items      : constant Node_Id := Contract (E);
+      Actuals    : List_Id := No_List;
+      Call       : Node_Id;
+      Call_Nam   : Node_Id;
+      Decls      : List_Id := No_List;
+      Formals    : List_Id;
+      Has_Pragma : Boolean := False;
+      Index_Id   : Entity_Id;
+      Obj_Id     : Entity_Id;
+      Prag       : Node_Id;
+      Wrapper_Id : Entity_Id;
+
+   --  Start of processing for Build_Entry_Contract_Wrapper
+
+   begin
+      --  This routine generates a specialized wrapper for a protected or task
+      --  entry [family] which implements precondition/postcondition semantics.
+      --  Preconditions and case guards of contract cases are checked before
+      --  the protected action or rendezvous takes place.
+
+      --    procedure Wrapper
+      --      (Obj_Id    : Conc_Typ;    --  concurrent object
+      --       [Index    : Index_Typ;]  --  index of entry family
+      --       [Formal_1 : ...;         --  parameters of original entry
+      --        Formal_N : ...])
+      --    is
+      --       [Discr_1 : ... renames Obj_Id.Discr_1;   --  discriminant
+      --        Discr_N : ... renames Obj_Id.Discr_N;]  --  renamings
+
+      --       <contracts pragmas>
+      --       <case guard checks>
+
+      --    begin
+      --       Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
+      --    end Wrapper;
+
+      --  Create the wrapper only when the entry has at least one executable
+      --  contract item such as contract cases, precondition or postcondition.
+
+      if Present (Items) then
+
+         --  Inspect the list of pre/postconditions and transfer all available
+         --  pragmas to the declarative list of the wrapper.
+
+         Prag := Pre_Post_Conditions (Items);
+         while Present (Prag) loop
+            if Pragma_Name_Unmapped (Prag) in Name_Postcondition
+                                            | Name_Precondition
+              and then Is_Checked (Prag)
+            then
+               Has_Pragma := True;
+               Transfer_Pragma (Prag, To => Decls);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+
+         --  Inspect the list of test/contract cases and transfer only contract
+         --  cases pragmas to the declarative part of the wrapper.
+
+         Prag := Contract_Test_Cases (Items);
+         while Present (Prag) loop
+            if Pragma_Name (Prag) = Name_Contract_Cases
+              and then Is_Checked (Prag)
+            then
+               Has_Pragma := True;
+               Transfer_Pragma (Prag, To => Decls);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+      end if;
+
+      --  The entry lacks executable contract items and a wrapper is not needed
+
+      if not Has_Pragma then
+         return;
+      end if;
+
+      --  Create the profile of the wrapper. The first formal parameter is the
+      --  concurrent object.
+
+      Obj_Id :=
+        Make_Defining_Identifier (Loc,
+          Chars => New_External_Name (Chars (Conc_Typ), 'A'));
+
+      Formals := New_List (
+        Make_Parameter_Specification (Loc,
+          Defining_Identifier => Obj_Id,
+          Out_Present         => True,
+          In_Present          => True,
+          Parameter_Type      => New_Occurrence_Of (Conc_Typ, Loc)));
+
+      --  Construct the call to the original entry. The call will be gradually
+      --  augmented with an optional entry index and extra parameters.
+
+      Call_Nam :=
+        Make_Selected_Component (Loc,
+          Prefix        => New_Occurrence_Of (Obj_Id, Loc),
+          Selector_Name => New_Occurrence_Of (E, Loc));
+
+      --  When creating a wrapper for an entry family, the second formal is the
+      --  entry index.
+
+      if Ekind (E) = E_Entry_Family then
+         Index_Id := Make_Defining_Identifier (Loc, Name_I);
+
+         Append_To (Formals,
+           Make_Parameter_Specification (Loc,
+             Defining_Identifier => Index_Id,
+             Parameter_Type      =>
+               New_Occurrence_Of (Entry_Index_Type (E), Loc)));
+
+         --  The call to the original entry becomes an indexed component to
+         --  accommodate the entry index.
+
+         Call_Nam :=
+           Make_Indexed_Component (Loc,
+             Prefix      => Call_Nam,
+             Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
+      end if;
+
+      --  Add formal parameters to match those of the entry and build actuals
+      --  for the entry call.
+
+      Add_Matching_Formals (Formals, Actuals);
+
+      Call :=
+        Make_Procedure_Call_Statement (Loc,
+          Name                   => Call_Nam,
+          Parameter_Associations => Actuals);
+
+      --  Add renaming declarations for the discriminants of the enclosing type
+      --  as the various contract items may reference them.
+
+      Add_Discriminant_Renamings (Obj_Id, Decls);
+
+      Wrapper_Id :=
+        Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
+      Set_Contract_Wrapper (E, Wrapper_Id);
+      Set_Is_Entry_Wrapper (Wrapper_Id);
+
+      --  The wrapper body is analyzed when the enclosing type is frozen
+
+      Append_Freeze_Action (Defining_Entity (Decl),
+        Make_Subprogram_Body (Loc,
+          Specification              =>
+            Make_Procedure_Specification (Loc,
+              Defining_Unit_Name       => Wrapper_Id,
+              Parameter_Specifications => Formals),
+          Declarations               => Decls,
+          Handled_Statement_Sequence =>
+            Make_Handled_Sequence_Of_Statements (Loc,
+              Statements => New_List (Call))));
+   end Build_Entry_Contract_Wrapper;
+
    ---------------------------
    -- Check_Class_Condition --
    ---------------------------
@@ -1804,16 +2296,9 @@ package body Contracts is
       --  the item denotes a pragma, it is added to the list only when it is
       --  enabled.
 
-      procedure Build_Postconditions_Procedure
-        (Subp_Id : Entity_Id;
-         Stmts   : List_Id;
-         Result  : Entity_Id);
-      --  Create the body of procedure _Postconditions which handles various
-      --  assertion actions on exit from subprogram Subp_Id. Stmts is the list
-      --  of statements to be checked on exit. Parameter Result is the entity
-      --  of parameter _Result when Subp_Id denotes a function.
-
-      procedure Process_Contract_Cases (Stmts : in out List_Id);
+      procedure Process_Contract_Cases
+        (Stmts : in out List_Id;
+         Decls : List_Id);
       --  Process pragma Contract_Cases. This routine prepends items to the
       --  body declarations and appends items to list Stmts.
 
@@ -1821,7 +2306,7 @@ package body Contracts is
       --  Collect all [inherited] spec and body postconditions and accumulate
       --  their pragma Check equivalents in list Stmts.
 
-      procedure Process_Preconditions;
+      procedure Process_Preconditions (Decls : in out List_Id);
       --  Collect all [inherited] spec and body preconditions and prepend their
       --  pragma Check equivalents to the declarations of the body.
 
@@ -2309,260 +2794,14 @@ package body Contracts is
          end if;
       end Append_Enabled_Item;
 
-      ------------------------------------
-      -- Build_Postconditions_Procedure --
-      ------------------------------------
-
-      procedure Build_Postconditions_Procedure
-        (Subp_Id : Entity_Id;
-         Stmts   : List_Id;
-         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
-
-         if No (Stmts) then
-            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);
-
-         --  Mark it inlined to speed up the call
-
-         Set_Is_Inlined (Proc_Id);
-
-         --  Force the front-end inlining of _Postconditions when generating C
-         --  code, since its body may have references to itypes defined in the
-         --  enclosing subprogram, which would cause problems for unnesting
-         --  routines in the absence of inlining.
-
-         if Modify_Tree_For_C then
-            Set_Has_Pragma_Inline        (Proc_Id);
-            Set_Has_Pragma_Inline_Always (Proc_Id);
-         end if;
-
-         --  The related subprogram is a function: create the specification of
-         --  parameter _Result.
-
-         if Present (Result) then
-            Params := New_List (
-              Make_Parameter_Specification (Loc,
-                Defining_Identifier => Result,
-                Parameter_Type      =>
-                  New_Occurrence_Of (Etype (Result), Loc)));
-         end if;
-
-         Proc_Spec :=
-           Make_Procedure_Specification (Loc,
-             Defining_Unit_Name       => Proc_Id,
-             Parameter_Specifications => Params);
-
-         Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
-
-         --  Insert _Postconditions before the first source declaration of the
-         --  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
-
-         --  In the example above, Obj is of type T but the incorrect placement
-         --  of _Postconditions will cause a crash in gigi due to an out-of-
-         --  order reference. The body of _Postconditions must be placed after
-         --  the declaration of Temp to preserve correct visibility.
-
-         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.
-
-         --  NOTE: This flag could be made into a predicate since we should be
-         --  able at compile time to recognize when finalization and cleanup
-         --  actions occur, but in practice this is not possible ???
-
-         --  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.
-
-         --  NOTE: Coverage-analysis and static-analysis tools rely on the
-         --  postconditions procedure being free of internally generated code
-         --  since some of these tools, like CodePeer, treat _postconditions
-         --  as original source.
-
-         --  Generate:
-         --
-         --    procedure _postconditions is
-         --    begin
-         --       [Stmts];
-         --    end;
-
-         Proc_Bod :=
-           Make_Subprogram_Body (Loc,
-             Specification              =>
-               Copy_Subprogram_Spec (Proc_Spec),
-             Declarations               => Empty_List,
-             Handled_Statement_Sequence =>
-               Make_Handled_Sequence_Of_Statements (Loc,
-                 End_Label  => Make_Identifier (Loc, Chars (Proc_Id)),
-                 Statements => Stmts));
-         Insert_After_And_Analyze (Last_Decl, Proc_Bod);
-
-      end Build_Postconditions_Procedure;
-
       ----------------------------
       -- Process_Contract_Cases --
       ----------------------------
 
-      procedure Process_Contract_Cases (Stmts : in out List_Id) is
+      procedure Process_Contract_Cases
+        (Stmts : in out List_Id;
+         Decls : List_Id)
+      is
          procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
          --  Process pragma Contract_Cases for subprogram Subp_Id
 
@@ -2583,14 +2822,14 @@ package body Contracts is
                         Expand_Pragma_Contract_Cases
                           (CCs     => Prag,
                            Subp_Id => Subp_Id,
-                           Decls   => Declarations (Body_Decl),
+                           Decls   => Decls,
                            Stmts   => Stmts);
 
                      elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
                         Expand_Pragma_Subprogram_Variant
                           (Prag       => Prag,
                            Subp_Id    => Subp_Id,
-                           Body_Decls => Declarations (Body_Decl));
+                           Body_Decls => Decls);
                      end if;
                   end if;
 
@@ -2599,11 +2838,6 @@ package body Contracts is
             end if;
          end Process_Contract_Cases_For;
 
-         pragma Unmodified (Stmts);
-         --  Stmts is passed as IN OUT to signal that the list can be updated,
-         --  even if the corresponding integer value representing the list does
-         --  not change.
-
       --  Start of processing for Process_Contract_Cases
 
       begin
@@ -2829,15 +3063,11 @@ package body Contracts is
       -- Process_Preconditions --
       ---------------------------
 
-      procedure Process_Preconditions is
+      procedure Process_Preconditions (Decls : in out List_Id) is
          Insert_Node : Node_Id := Empty;
          --  The insertion node after which all pragma Check equivalents are
          --  inserted.
 
-         function Is_Prologue_Renaming (Decl : Node_Id) return Boolean;
-         --  Determine whether arbitrary declaration Decl denotes a renaming of
-         --  a discriminant or protection field _object.
-
          procedure Prepend_To_Decls (Item : Node_Id);
          --  Prepend a single item to the declarations of the subprogram body
 
@@ -2849,64 +3079,12 @@ package body Contracts is
          --  Collect all preconditions of subprogram Subp_Id and prepend their
          --  pragma Check equivalents to the declarations of the body.
 
-         --------------------------
-         -- Is_Prologue_Renaming --
-         --------------------------
-
-         function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
-            Nam  : Node_Id;
-            Obj  : Entity_Id;
-            Pref : Node_Id;
-            Sel  : Node_Id;
-
-         begin
-            if Nkind (Decl) = N_Object_Renaming_Declaration then
-               Obj := Defining_Entity (Decl);
-               Nam := Name (Decl);
-
-               if Nkind (Nam) = N_Selected_Component then
-                  Pref := Prefix (Nam);
-                  Sel  := Selector_Name (Nam);
-
-                  --  A discriminant renaming appears as
-                  --    Discr : constant ... := Prefix.Discr;
-
-                  if Ekind (Obj) = E_Constant
-                    and then Is_Entity_Name (Sel)
-                    and then Present (Entity (Sel))
-                    and then Ekind (Entity (Sel)) = E_Discriminant
-                  then
-                     return True;
-
-                  --  A protection field renaming appears as
-                  --    Prot : ... := _object._object;
-
-                  --  A renamed private component is just a component of
-                  --  _object, with an arbitrary name.
-
-                  elsif Ekind (Obj) in E_Variable | E_Constant
-                    and then Nkind (Pref) = N_Identifier
-                    and then Chars (Pref) = Name_uObject
-                    and then Nkind (Sel) = N_Identifier
-                  then
-                     return True;
-                  end if;
-               end if;
-            end if;
-
-            return False;
-         end Is_Prologue_Renaming;
-
          ----------------------
          -- Prepend_To_Decls --
          ----------------------
 
          procedure Prepend_To_Decls (Item : Node_Id) is
-            Decls : List_Id;
-
          begin
-            Decls := Declarations (Body_Decl);
-
             --  Ensure that the body has a declarative list
 
             if No (Decls) then
@@ -2937,14 +3115,8 @@ package body Contracts is
 
             else
                Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+               Prepend_To_Decls (Check_Prag);
 
-               if Present (Insert_Node) then
-                  Insert_After (Insert_Node, Check_Prag);
-               else
-                  Prepend_To_Decls (Check_Prag);
-               end if;
-
-               Analyze (Check_Prag);
             end if;
          end Prepend_Pragma_To_Decls;
 
@@ -3037,16 +3209,17 @@ package body Contracts is
 
          --  Local variables
 
-         Decls : constant List_Id := Declarations (Body_Decl);
-         Decl  : Node_Id;
+         Body_Decls : constant List_Id := Declarations (Body_Decl);
+         Decl       : Node_Id;
+         Next_Decl  : Node_Id;
 
       --  Start of processing for Process_Preconditions
 
       begin
          --  Find the proper insertion point for all pragma Check equivalents
 
-         if Present (Decls) then
-            Decl := First (Decls);
+         if Present (Body_Decls) then
+            Decl := First (Body_Decls);
             while Present (Decl) loop
 
                --  First source declaration terminates the search, because all
@@ -3091,6 +3264,19 @@ package body Contracts is
             --    <preconditions from body>
 
             Process_Preconditions_For (Body_Id);
+
+            --  Move the generated entry-call prologue renamings into the
+            --  outer declarations for use in the preconditions.
+
+            Decl := First (Body_Decls);
+            while Present (Decl) and then Present (Insert_Node) loop
+               Next_Decl := Next (Decl);
+               Remove (Decl);
+               Prepend_To_Decls (Decl);
+
+               exit when Decl = Insert_Node;
+               Decl := Next_Decl;
+            end loop;
          end if;
 
          if Present (Spec_Id) then
@@ -3103,6 +3289,7 @@ package body Contracts is
       Restore_Scope : Boolean := False;
       Result        : Entity_Id;
       Stmts         : List_Id := No_List;
+      Decls         : List_Id := New_List;
       Subp_Id       : Entity_Id;
 
    --  Start of processing for Expand_Subprogram_Contract
@@ -3181,33 +3368,33 @@ package body Contracts is
       --  pragmas to verify the contract assertions of the spec and body in a
       --  particular order. The order is as follows:
 
-      --    function Example (...) return ... is
-      --       procedure _Postconditions (...) is
+      --    function Original_Code (...) return ... is
+      --       <prologue renamings>
+      --       <inherited preconditions>
+      --       <preconditions from spec>
+      --       <preconditions from body>
+      --       <contract case conditions>
+
+      --       function _wrapped_statements (...) return ... is
+      --          <source declarations>
       --       begin
+      --          <source statements>
+      --       end _wrapped_statements;
+
+      --    begin
+      --       return
+      --          Result : ... := _wrapped_statements
+      --       do
       --          <refined postconditions from body>
       --          <postconditions from body>
       --          <postconditions from spec>
       --          <inherited postconditions>
       --          <contract case consequences>
       --          <invariant check of function result>
-      --          <invariant and predicate checks of parameters>
-      --       end _Postconditions;
-
-      --       <inherited preconditions>
-      --       <preconditions from spec>
-      --       <preconditions from body>
-      --       <contract case conditions>
-
-      --       <source declarations>
-      --    begin
-      --       <source statements>
-
-      --       _Preconditions (Result);
-      --       return Result;
-      --    end Example;
-
-      --  Routine _Postconditions holds all contract assertions that must be
-      --  verified on exit from the related subprogram.
+      --          <invariant and predicate checks of parameters
+      --          return Result;
+      --       end return;
+      --    end Original_Code;
 
       --  Step 1: augment contracts list with postconditions associated with
       --  Stable_Properties and Stable_Properties'Class aspects. This must
@@ -3222,7 +3409,7 @@ package body Contracts is
       --  processing of pragma Contract_Cases because the pragma prepends items
       --  to the body declarations.
 
-      Process_Preconditions;
+      Process_Preconditions (Decls);
 
       --  Step 3: Handle all postconditions. This action must come before the
       --  processing of pragma Contract_Cases because the pragma appends items
@@ -3234,16 +3421,26 @@ package body Contracts is
       --  the processing of invariants and predicates because those append
       --  items to list Stmts.
 
-      Process_Contract_Cases (Stmts);
+      Process_Contract_Cases (Stmts, Decls);
 
       --  Step 5: Apply invariant and predicate checks on a function result and
       --  all formals. The resulting checks are accumulated in list Stmts.
 
       Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
 
-      --  Step 6: Construct procedure _Postconditions
+      --  Step 6: Construct subprogram _wrapped_statements
+
+      --  When no statements are present we still need to insert contract
+      --  related declarations.
+
+      if No (Stmts) then
+         Prepend_List_To (Declarations (Body_Decl), Decls);
+
+      --  Otherwise, we need a wrapper
 
-      Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
+      else
+         Build_Subprogram_Contract_Wrapper (Body_Id, Stmts, Decls, Result);
+      end if;
 
       if Restore_Scope then
          End_Scope;
@@ -3448,81 +3645,6 @@ package body Contracts is
       Freeze_Contracts;
    end Freeze_Previous_Contracts;
 
-   --------------------------
-   -- Get_Postcond_Enabled --
-   --------------------------
-
-   function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_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 Entity_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 Entity_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 --
    ---------------------------------
@@ -3617,6 +3739,65 @@ package body Contracts is
       end if;
    end Instantiate_Subprogram_Contract;
 
+   --------------------------
+   -- Is_Prologue_Renaming --
+   --------------------------
+
+   --  This should be turned into a flag and set during the expansion of
+   --  task and protected types when the renamings get generated ???
+
+   function Is_Prologue_Renaming (Decl : Node_Id) return Boolean is
+      Nam  : Node_Id;
+      Obj  : Entity_Id;
+      Pref : Node_Id;
+      Sel  : Node_Id;
+
+   begin
+      if Nkind (Decl) = N_Object_Renaming_Declaration
+        and then not Comes_From_Source (Decl)
+      then
+         Obj := Defining_Entity (Decl);
+         Nam := Name (Decl);
+
+         if Nkind (Nam) = N_Selected_Component then
+            --  Analyze the renaming declaration so we can further examine it
+
+            if not Analyzed (Decl) then
+               Analyze (Decl);
+            end if;
+
+            Pref := Prefix (Nam);
+            Sel  := Selector_Name (Nam);
+
+            --  A discriminant renaming appears as
+            --    Discr : constant ... := Prefix.Discr;
+
+            if Ekind (Obj) = E_Constant
+              and then Is_Entity_Name (Sel)
+              and then Present (Entity (Sel))
+              and then Ekind (Entity (Sel)) = E_Discriminant
+            then
+               return True;
+
+            --  A protection field renaming appears as
+            --    Prot : ... := _object._object;
+
+            --  A renamed private component is just a component of
+            --  _object, with an arbitrary name.
+
+            elsif Ekind (Obj) in E_Variable | E_Constant
+              and then Nkind (Pref) = N_Identifier
+              and then Chars (Pref) = Name_uObject
+              and then Nkind (Sel) = N_Identifier
+            then
+               return True;
+            end if;
+         end if;
+      end if;
+
+      return False;
+   end Is_Prologue_Renaming;
+
    -----------------------------------
    -- Make_Class_Precondition_Subps --
    -----------------------------------
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 5178373..bde32ff 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -64,6 +64,16 @@ package Contracts is
    procedure Analyze_Contracts (L : List_Id);
    --  Analyze the contracts of all eligible constructs found in list L
 
+   procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id);
+   --  Perform early analysis of pragmas at the top of a given subprogram's
+   --  declarations.
+   --
+   --  The purpose of this is to analyze contract-related pragmas for later
+   --  processing, but also to handle other such pragmas before these
+   --  declarations get moved to an internal wrapper as part of contract
+   --  expansion. For example, pragmas Inline, Ghost, Volatile all need to
+   --  apply directly to the subprogram and not be moved to a wrapper.
+
    procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
    --  Analyze all delayed pragmas chained on the contract of entry or
    --  subprogram body Body_Id as if they appeared at the end of a declarative
@@ -177,6 +187,17 @@ package Contracts is
    --    Depends
    --    Global
 
+   procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id);
+   --  Build the body of a wrapper procedure for an entry or entry family that
+   --  has contract cases, preconditions, or postconditions, and add it to the
+   --  freeze actions of the related synchronized type.
+   --
+   --  The body first verifies the preconditions and case guards of the
+   --  contract cases, then invokes the entry [family], and finally verifies
+   --  the postconditions and the consequences of the contract cases. E denotes
+   --  the entry family. Decl denotes the declaration of the enclosing
+   --  synchronized type.
+
    procedure Create_Generic_Contract (Unit : Node_Id);
    --  Create a contract node for a generic package, generic subprogram, or a
    --  generic body denoted by Unit by collecting all source contract-related
@@ -188,21 +209,6 @@ 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.ads b/gcc/ada/einfo.ads
index ed63019..7ac8cf6 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -4014,9 +4014,7 @@ package Einfo is
 --       fully initialized when the full view is frozen.
 
 --    Postconditions_Proc
---       Defined in functions, procedures, entries, and entry families. Refers
---       to the entity of the _Postconditions procedure used to check contract
---       assertions on exit from a subprogram.
+--       Obsolete field which can be removed once CodePeer is fixed ???
 
 --    Predicate_Function (synthesized)
 --       Defined in all types. Set for types for which (Has_Predicates is True)
@@ -4767,6 +4765,13 @@ package Einfo is
 --       Defined in functions and procedures which have been classified as
 --       Is_Primitive_Wrapper. Set to the entity being wrapper.
 
+--    Wrapped_Statements
+--       Defined in functions, procedures, entries, and entry families. Refers
+--       to the entity of the _Wrapped_Statements procedure which gets
+--       generated as part of the expansion of contracts and postconditions
+--       and contains its enclosing subprogram's original source declarations
+--       and statements.
+
 --    LSP_Subprogram
 --       Defined in subprogram entities. Set on wrappers created to handle
 --       inherited class-wide pre/post conditions that call overridden
@@ -5412,7 +5417,6 @@ package Einfo is
    --    Protected_Body_Subprogram
    --    Barrier_Function
    --    Elaboration_Entity
-   --    Postconditions_Proc
    --    Entry_Parameters_Type
    --    First_Entity
    --    Alias                                (for entry only. Empty)
@@ -5527,7 +5531,6 @@ package Einfo is
    --    Protected_Body_Subprogram
    --    Next_Inlined_Subprogram
    --    Elaboration_Entity                   (not implicit /=)
-   --    Postconditions_Proc                  (non-generic case only)
    --    DT_Position
    --    DTC_Entity
    --    First_Entity
@@ -5891,7 +5894,6 @@ package Einfo is
    --    Protected_Body_Subprogram
    --    Next_Inlined_Subprogram
    --    Elaboration_Entity
-   --    Postconditions_Proc                  (non-generic case only)
    --    DT_Position
    --    DTC_Entity
    --    First_Entity
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index 4a26671..6f49db7 100644
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -4895,24 +4895,25 @@ package body Exp_Attr is
          use Old_Attr_Util.Indirect_Temps;
       begin
          --  Generating C code we don't need to expand this attribute when
-         --  we are analyzing the internally built nested postconditions
+         --  we are analyzing the internally built nested _Wrapped_Statements
          --  procedure since it will be expanded inline (and later it will
          --  be removed by Expand_N_Subprogram_Body). It this expansion is
          --  performed in such case then the compiler generates unreferenced
          --  extra temporaries.
 
          if Modify_Tree_For_C
-           and then Chars (Current_Scope) = Name_uPostconditions
+           and then Chars (Current_Scope) = Name_uWrapped_Statements
          then
             return;
          end if;
 
-         --  Climb the parent chain looking for subprogram _Postconditions
+         --  Climb the parent chain looking for subprogram _Wrapped_Statements
 
          Subp := N;
          while Present (Subp) loop
             exit when Nkind (Subp) = N_Subprogram_Body
-              and then Chars (Defining_Entity (Subp)) = Name_uPostconditions;
+              and then Chars (Defining_Entity (Subp))
+                         = Name_uWrapped_Statements;
 
             --  If assertions are disabled, no need to create the declaration
             --  that preserves the value. The postcondition pragma in which
@@ -4925,14 +4926,11 @@ package body Exp_Attr is
 
             Subp := Parent (Subp);
          end loop;
+         Subp := Empty;
 
-         --  'Old can only appear in a postcondition, the generated body of
-         --  _Postconditions must be in the tree (or inlined if we are
-         --  generating C code).
-
-         pragma Assert
-           (Present (Subp)
-             or else (Modify_Tree_For_C and then In_Inlined_Body));
+         --  'Old can only appear in the case where local contract-related
+         --  wrapper has been generated with the purpose of wrapping the
+         --  original declarations and statements.
 
          Temp := Make_Temporary (Loc, 'T', Pref);
 
@@ -4952,8 +4950,7 @@ package body Exp_Attr is
          --  No need to push the scope when generating C code since the
          --  _Postcondition procedure has been inlined.
 
-         else pragma Assert (Modify_Tree_For_C);
-            pragma Assert (In_Inlined_Body);
+         else
             null;
          end if;
 
@@ -4963,17 +4960,23 @@ package body Exp_Attr is
          if Present (Subp) then
             Ins_Nod := Subp;
 
-         --  Generating C, the postcondition procedure has been inlined and the
-         --  temporary is added before the first declaration of the enclosing
-         --  subprogram.
+         --  General case where the postcondtion checks occur after the call
+         --  to _Wrapped_Statements.
 
-         else pragma Assert (Modify_Tree_For_C);
+         else
             Ins_Nod := N;
             while Nkind (Ins_Nod) /= N_Subprogram_Body loop
                Ins_Nod := Parent (Ins_Nod);
             end loop;
 
-            Ins_Nod := First (Declarations (Ins_Nod));
+            if Present (Corresponding_Spec (Ins_Nod))
+              and then Present
+                         (Wrapped_Statements (Corresponding_Spec (Ins_Nod)))
+            then
+               Ins_Nod := Last (Declarations (Ins_Nod));
+            else
+               Ins_Nod := First (Declarations (Ins_Nod));
+            end if;
          end if;
 
          if Eligible_For_Conditional_Evaluation (N) then
@@ -4986,9 +4989,9 @@ package body Exp_Attr is
                --  unconditionally) or an evaluation statement (which is
                --  to be executed conditionally).
 
-               -------------------------------
-               --  Append_For_Indirect_Temp --
-               -------------------------------
+               ------------------------------
+               -- Append_For_Indirect_Temp --
+               ------------------------------
 
                procedure Append_For_Indirect_Temp
                  (N : Node_Id; Is_Eval_Stmt : Boolean)
@@ -5008,7 +5011,7 @@ package body Exp_Attr is
                Declare_Indirect_Temporary
                  (Attr_Prefix => Pref, Indirect_Temp => Temp);
 
-               Insert_Before_And_Analyze (
+               Insert_After_And_Analyze (
                  Ins_Nod,
                  Make_If_Statement
                    (Sloc            => Loc,
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index fe3bb5b..f4630c9 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -26,7 +26,6 @@
 with Atree;          use Atree;
 with Aspects;        use Aspects;
 with Checks;         use Checks;
-with Contracts;      use Contracts;
 with Debug;          use Debug;
 with Einfo;          use Einfo;
 with Einfo.Entities; use Einfo.Entities;
@@ -2729,11 +2728,16 @@ package body Exp_Ch6 is
                                 | N_Function_Call
                                 | N_Procedure_Call_Statement);
 
-      --  Check that this is not the call in the body of the wrapper
+      --  Check that this is not the call in the body of the access
+      --  subprogram wrapper or the postconditions wrapper.
 
       if Must_Rewrite_Indirect_Call
         and then (not Is_Overloadable (Current_Scope)
-             or else not Is_Access_Subprogram_Wrapper (Current_Scope))
+             or else not (Is_Access_Subprogram_Wrapper (Current_Scope)
+                           or else
+                             (Chars (Current_Scope) = Name_uWrapped_Statements
+                               and then Is_Access_Subprogram_Wrapper
+                                          (Scope (Current_Scope)))))
       then
          declare
             Loc      : constant Source_Ptr := Sloc (N);
@@ -4871,11 +4875,12 @@ package body Exp_Ch6 is
                   then
                      Must_Inline := not In_Extended_Main_Source_Unit (Subp);
 
-                  --  Inline calls to _postconditions when generating C code
+                  --  Inline calls to _Wrapped_Statements when generating C
 
                   elsif Modify_Tree_For_C
                     and then In_Same_Extended_Unit (Sloc (Bod), Loc)
-                    and then Chars (Name (Call_Node)) = Name_uPostconditions
+                    and then Chars (Name (Call_Node))
+                               = Name_uWrapped_Statements
                   then
                      Must_Inline := True;
                   end if;
@@ -5567,45 +5572,6 @@ package body Exp_Ch6 is
             Append_To (Stmts, Stmt);
             Set_Analyzed (Stmt);
 
-            --  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 by setting
-            --  Return_Success_For_Postcond to be True.
-
-            if Ekind (Spec_Id) = E_Procedure
-              and then Present (Postconditions_Proc (Spec_Id))
-            then
-               --  Generate:
-               --
-               --    Return_Success_For_Postcond := True;
-               --    if Postcond_Enabled then
-               --       _postconditions;
-               --    end if;
-
-               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)));
-
-               --  Wrap the call to _postconditions within a test of the
-               --  Postcond_Enabled flag to delay postcondition evaluation
-               --  until after finalization when required.
-
-               Insert_Action (Stmt,
-                 Make_If_Statement (Loc,
-                   Condition       =>
-                     New_Occurrence_Of (Get_Postcond_Enabled (Spec_Id), Loc),
-                   Then_Statements => New_List (
-                     Make_Procedure_Call_Statement (Loc,
-                       Name =>
-                         New_Occurrence_Of
-                           (Postconditions_Proc (Spec_Id), Loc)))));
-            end if;
-
             --  Ada 2022 (AI12-0279): append the call to 'Yield unless this is
             --  a generic subprogram (since in such case it will be added to
             --  the instantiations).
@@ -6013,44 +5979,6 @@ package body Exp_Ch6 is
       Lab_Node  : Node_Id;
 
    begin
-      --  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;
-         --    if Postcond_Enabled then
-         --       _postconditions;
-         --    end if;
-
-         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)));
-
-         --  Wrap the call to _postconditions within a test of the
-         --  Postcond_Enabled flag to delay postcondition evaluation until
-         --  after finalization when required.
-
-         Insert_Action (N,
-           Make_If_Statement (Loc,
-             Condition       =>
-               New_Occurrence_Of (Get_Postcond_Enabled (Scope_Id), Loc),
-             Then_Statements => New_List (
-               Make_Procedure_Call_Statement (Loc,
-                 Name =>
-                   New_Occurrence_Of
-                     (Postconditions_Proc (Scope_Id), Loc)))));
-      end if;
-
       --  Ada 2022 (AI12-0279)
 
       if Has_Yield_Aspect (Scope_Id)
@@ -6995,84 +6923,6 @@ package body Exp_Ch6 is
          end;
       end if;
 
-      --  Call the _Postconditions procedure if the related function has
-      --  contract assertions that need to be verified on exit.
-
-      if Ekind (Scope_Id) = E_Function
-        and then Present (Postconditions_Proc (Scope_Id))
-      then
-         --  In the case of discriminated objects, we have created a
-         --  constrained subtype above, and used the underlying type. This
-         --  transformation is post-analysis and harmless, except that now the
-         --  call to the post-condition will be analyzed and the type kinds
-         --  have to match.
-
-         if Nkind (Exp) = N_Unchecked_Type_Conversion
-           and then Is_Private_Type (R_Type) /= Is_Private_Type (Etype (Exp))
-         then
-            Rewrite (Exp, Expression (Relocate_Node (Exp)));
-         end if;
-
-         --  We are going to reference the returned value twice in this case,
-         --  once in the call to _Postconditions, and once in the actual return
-         --  statement, but we can't have side effects happening twice.
-
-         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;
-         --    if Postcond_Enabled then
-         --       _Postconditions ([exp]);
-         --    end if;
-
-         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)));
-
-         --  Wrap the call to _postconditions within a test of the
-         --  Postcond_Enabled flag to delay postcondition evaluation until
-         --  after finalization when required.
-
-         Insert_Action (Exp,
-           Make_If_Statement (Loc,
-             Condition       =>
-               New_Occurrence_Of (Get_Postcond_Enabled (Scope_Id), Loc),
-             Then_Statements => New_List (
-               Make_Procedure_Call_Statement (Loc,
-                 Name                   =>
-                   New_Occurrence_Of
-                     (Postconditions_Proc (Scope_Id), Loc),
-                 Parameter_Associations => New_List (New_Copy_Tree (Exp))))));
-      end if;
-
       --  Ada 2005 (AI-251): If this return statement corresponds with an
       --  simple return statement associated with an extended return statement
       --  and the type of the returned object is an interface then generate an
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 3ffebfb..fc4516d 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -28,7 +28,6 @@
 --    - transient scopes
 
 with Atree;          use Atree;
-with Contracts;      use Contracts;
 with Debug;          use Debug;
 with Einfo;          use Einfo;
 with Einfo.Entities; use Einfo.Entities;
@@ -305,17 +304,6 @@ 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 that contains a handled sequence of statements, Fin_Id
    --  is the entity of a finalizer. Create an At_End handler that covers the
@@ -1377,18 +1365,17 @@ package body Exp_Ch7 is
       end;
    end Build_Finalization_Master;
 
-   ----------------------------
-   -- Build_Finalizer_Helper --
-   ----------------------------
+   ---------------------
+   -- Build_Finalizer --
+   ---------------------
 
-   procedure Build_Finalizer_Helper
+   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;
-      Finalize_Old_Only : Boolean)
+      Fin_Id            : out Entity_Id)
    is
       Acts_As_Clean    : constant Boolean :=
                            Present (Mark_Id)
@@ -1682,15 +1669,9 @@ package body Exp_Ch7 is
             --  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;
+            Fin_Id :=
+              Make_Defining_Identifier (Loc,
+                Chars => New_External_Name (Name_uFinalizer));
 
             --  The visibility semantics of AT_END handlers force a strange
             --  separation of spec and body for stack-related finalizers:
@@ -2222,26 +2203,9 @@ 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
 
-            elsif Nkind (Decl) = N_Full_Type_Declaration then
+            if Nkind (Decl) = N_Full_Type_Declaration then
                Typ := Defining_Identifier (Decl);
 
                --  Ignored Ghost types do not need any cleanup actions because
@@ -3528,7 +3492,7 @@ package body Exp_Ch7 is
                New_Occurrence_Of (DT_Ptr, Loc))));
       end Process_Tagged_Type_Declaration;
 
-   --  Start of processing for Build_Finalizer_Helper
+   --  Start of processing for Build_Finalizer
 
    begin
       Fin_Id := Empty;
@@ -3685,7 +3649,7 @@ package body Exp_Ch7 is
       if Acts_As_Clean or Has_Ctrl_Objs or Has_Tagged_Types then
          Create_Finalizer;
       end if;
-   end Build_Finalizer_Helper;
+   end Build_Finalizer;
 
    --------------------------
    -- Build_Finalizer_Call --
@@ -3758,496 +3722,6 @@ package body Exp_Ch7 is
    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
-      --         and then Return_Success_For_Postcond
-      --       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
-         --  occurred taking care to enable the postconditions and save any
-         --  exception occurrences.
-
-         --  Generate:
-         --
-         --    if not Raised_Finalization_Exception
-         --      and then Return_Success_For_Postcond
-         --    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_And_Then (Loc,
-                 Left_Opnd  =>
-                   Make_Op_Not (Loc,
-                     Right_Opnd =>
-                       New_Occurrence_Of
-                         (Raised_Finalization_Exception_Id, Loc)),
-                 Right_Opnd =>
-                   New_Occurrence_Of
-                     (Get_Return_Success_For_Postcond (Def_Ent), 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;
-
-         --  Note that we do not disable early evaluation of postconditions
-         --  for return types that are unconstrained or have unconstrained
-         --  elements since the temporary result object could get allocated on
-         --  the stack and be out of scope at the point where we perform late
-         --  evaluation of postconditions - leading to uninitialized memory
-         --  reads.
-
-         --  This disabling of early evaluation can lead to incorrect run-time
-         --  semantics where functions with unconstrained elements will
-         --  have their corresponding postconditions evaluated before
-         --  finalization. The proper solution here is to generate a wrapper
-         --  to capture the result instead of using multiple flags and playing
-         --  with flags which does not even work in all cases ???
-
-         if not Has_Unconstrained_Elements (Etype (Def_Ent))
-           or else (Is_Array_Type (Etype (Def_Ent))
-                     and then not Is_Constrained (Etype (Def_Ent)))
-         then
-            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)));
-         end if;
-
-         --  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 --
    ---------------------
 
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 757f492..8abff55 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -26,6 +26,7 @@
 with Atree;          use Atree;
 with Aspects;        use Aspects;
 with Checks;         use Checks;
+with Contracts;      use Contracts;
 with Einfo;          use Einfo;
 with Einfo.Entities; use Einfo.Entities;
 with Einfo.Utils;    use Einfo.Utils;
@@ -134,15 +135,6 @@ package body Exp_Ch9 is
    --  Build a specification for a function implementing the protected entry
    --  barrier of the specified entry body.
 
-   procedure Build_Contract_Wrapper (E : Entity_Id; Decl : Node_Id);
-   --  Build the body of a wrapper procedure for an entry or entry family that
-   --  has contract cases, preconditions, or postconditions. The body gathers
-   --  the executable contract items and expands them in the usual way, and
-   --  performs the entry call itself. This way preconditions are evaluated
-   --  before the call is queued. E is the entry in question, and Decl is the
-   --  enclosing synchronized type declaration at whose freeze point the
-   --  generated body is analyzed.
-
    function Build_Corresponding_Record
      (N    : Node_Id;
       Ctyp : Entity_Id;
@@ -1296,288 +1288,6 @@ package body Exp_Ch9 is
       Set_Master_Id (Typ, Master_Id);
    end Build_Class_Wide_Master;
 
-   ----------------------------
-   -- Build_Contract_Wrapper --
-   ----------------------------
-
-   procedure Build_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
-      Conc_Typ : constant Entity_Id  := Scope (E);
-      Loc      : constant Source_Ptr := Sloc (E);
-
-      procedure Add_Discriminant_Renamings
-        (Obj_Id : Entity_Id;
-         Decls  : List_Id);
-      --  Add renaming declarations for all discriminants of concurrent type
-      --  Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
-      --  represents the concurrent object.
-
-      procedure Add_Matching_Formals
-        (Formals : List_Id;
-         Actuals : in out List_Id);
-      --  Add formal parameters that match those of entry E to list Formals.
-      --  The routine also adds matching actuals for the new formals to list
-      --  Actuals.
-
-      procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
-      --  Relocate pragma Prag to list To. The routine creates a new list if
-      --  To does not exist.
-
-      --------------------------------
-      -- Add_Discriminant_Renamings --
-      --------------------------------
-
-      procedure Add_Discriminant_Renamings
-        (Obj_Id : Entity_Id;
-         Decls  : List_Id)
-      is
-         Discr : Entity_Id;
-
-      begin
-         --  Inspect the discriminants of the concurrent type and generate a
-         --  renaming for each one.
-
-         if Has_Discriminants (Conc_Typ) then
-            Discr := First_Discriminant (Conc_Typ);
-            while Present (Discr) loop
-               Prepend_To (Decls,
-                 Make_Object_Renaming_Declaration (Loc,
-                   Defining_Identifier =>
-                     Make_Defining_Identifier (Loc, Chars (Discr)),
-                   Subtype_Mark        =>
-                     New_Occurrence_Of (Etype (Discr), Loc),
-                   Name                =>
-                     Make_Selected_Component (Loc,
-                       Prefix        => New_Occurrence_Of (Obj_Id, Loc),
-                       Selector_Name =>
-                         Make_Identifier (Loc, Chars (Discr)))));
-
-               Next_Discriminant (Discr);
-            end loop;
-         end if;
-      end Add_Discriminant_Renamings;
-
-      --------------------------
-      -- Add_Matching_Formals --
-      --------------------------
-
-      procedure Add_Matching_Formals
-        (Formals : List_Id;
-         Actuals : in out List_Id)
-      is
-         Formal     : Entity_Id;
-         New_Formal : Entity_Id;
-
-      begin
-         --  Inspect the formal parameters of the entry and generate a new
-         --  matching formal with the same name for the wrapper. A reference
-         --  to the new formal becomes an actual in the entry call.
-
-         Formal := First_Formal (E);
-         while Present (Formal) loop
-            New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
-            Append_To (Formals,
-              Make_Parameter_Specification (Loc,
-                Defining_Identifier => New_Formal,
-                In_Present          => In_Present  (Parent (Formal)),
-                Out_Present         => Out_Present (Parent (Formal)),
-                Parameter_Type      =>
-                  New_Occurrence_Of (Etype (Formal), Loc)));
-
-            if No (Actuals) then
-               Actuals := New_List;
-            end if;
-
-            Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
-            Next_Formal (Formal);
-         end loop;
-      end Add_Matching_Formals;
-
-      ---------------------
-      -- Transfer_Pragma --
-      ---------------------
-
-      procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
-         New_Prag : Node_Id;
-
-      begin
-         if No (To) then
-            To := New_List;
-         end if;
-
-         New_Prag := Relocate_Node (Prag);
-
-         Set_Analyzed (New_Prag, False);
-         Append       (New_Prag, To);
-      end Transfer_Pragma;
-
-      --  Local variables
-
-      Items      : constant Node_Id := Contract (E);
-      Actuals    : List_Id := No_List;
-      Call       : Node_Id;
-      Call_Nam   : Node_Id;
-      Decls      : List_Id := No_List;
-      Formals    : List_Id;
-      Has_Pragma : Boolean := False;
-      Index_Id   : Entity_Id;
-      Obj_Id     : Entity_Id;
-      Prag       : Node_Id;
-      Wrapper_Id : Entity_Id;
-
-   --  Start of processing for Build_Contract_Wrapper
-
-   begin
-      --  This routine generates a specialized wrapper for a protected or task
-      --  entry [family] which implements precondition/postcondition semantics.
-      --  Preconditions and case guards of contract cases are checked before
-      --  the protected action or rendezvous takes place. Postconditions and
-      --  consequences of contract cases are checked after the protected action
-      --  or rendezvous takes place. The structure of the generated wrapper is
-      --  as follows:
-
-      --    procedure Wrapper
-      --      (Obj_Id    : Conc_Typ;    --  concurrent object
-      --       [Index    : Index_Typ;]  --  index of entry family
-      --       [Formal_1 : ...;         --  parameters of original entry
-      --        Formal_N : ...])
-      --    is
-      --       [Discr_1 : ... renames Obj_Id.Discr_1;   --  discriminant
-      --        Discr_N : ... renames Obj_Id.Discr_N;]  --  renamings
-
-      --       <precondition checks>
-      --       <case guard checks>
-
-      --       procedure _Postconditions is
-      --       begin
-      --          <postcondition checks>
-      --          <consequence checks>
-      --       end _Postconditions;
-
-      --    begin
-      --       Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
-      --       _Postconditions;
-      --    end Wrapper;
-
-      --  Create the wrapper only when the entry has at least one executable
-      --  contract item such as contract cases, precondition or postcondition.
-
-      if Present (Items) then
-
-         --  Inspect the list of pre/postconditions and transfer all available
-         --  pragmas to the declarative list of the wrapper.
-
-         Prag := Pre_Post_Conditions (Items);
-         while Present (Prag) loop
-            if Pragma_Name_Unmapped (Prag) in Name_Postcondition
-                                            | Name_Precondition
-              and then Is_Checked (Prag)
-            then
-               Has_Pragma := True;
-               Transfer_Pragma (Prag, To => Decls);
-            end if;
-
-            Prag := Next_Pragma (Prag);
-         end loop;
-
-         --  Inspect the list of test/contract cases and transfer only contract
-         --  cases pragmas to the declarative part of the wrapper.
-
-         Prag := Contract_Test_Cases (Items);
-         while Present (Prag) loop
-            if Pragma_Name (Prag) = Name_Contract_Cases
-              and then Is_Checked (Prag)
-            then
-               Has_Pragma := True;
-               Transfer_Pragma (Prag, To => Decls);
-            end if;
-
-            Prag := Next_Pragma (Prag);
-         end loop;
-      end if;
-
-      --  The entry lacks executable contract items and a wrapper is not needed
-
-      if not Has_Pragma then
-         return;
-      end if;
-
-      --  Create the profile of the wrapper. The first formal parameter is the
-      --  concurrent object.
-
-      Obj_Id :=
-        Make_Defining_Identifier (Loc,
-          Chars => New_External_Name (Chars (Conc_Typ), 'A'));
-
-      Formals := New_List (
-        Make_Parameter_Specification (Loc,
-          Defining_Identifier => Obj_Id,
-          Out_Present         => True,
-          In_Present          => True,
-          Parameter_Type      => New_Occurrence_Of (Conc_Typ, Loc)));
-
-      --  Construct the call to the original entry. The call will be gradually
-      --  augmented with an optional entry index and extra parameters.
-
-      Call_Nam :=
-        Make_Selected_Component (Loc,
-          Prefix        => New_Occurrence_Of (Obj_Id, Loc),
-          Selector_Name => New_Occurrence_Of (E, Loc));
-
-      --  When creating a wrapper for an entry family, the second formal is the
-      --  entry index.
-
-      if Ekind (E) = E_Entry_Family then
-         Index_Id := Make_Defining_Identifier (Loc, Name_I);
-
-         Append_To (Formals,
-           Make_Parameter_Specification (Loc,
-             Defining_Identifier => Index_Id,
-             Parameter_Type      =>
-               New_Occurrence_Of (Entry_Index_Type (E), Loc)));
-
-         --  The call to the original entry becomes an indexed component to
-         --  accommodate the entry index.
-
-         Call_Nam :=
-           Make_Indexed_Component (Loc,
-             Prefix      => Call_Nam,
-             Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
-      end if;
-
-      --  Add formal parameters to match those of the entry and build actuals
-      --  for the entry call.
-
-      Add_Matching_Formals (Formals, Actuals);
-
-      Call :=
-        Make_Procedure_Call_Statement (Loc,
-          Name                   => Call_Nam,
-          Parameter_Associations => Actuals);
-
-      --  Add renaming declarations for the discriminants of the enclosing type
-      --  as the various contract items may reference them.
-
-      Add_Discriminant_Renamings (Obj_Id, Decls);
-
-      Wrapper_Id :=
-        Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
-      Set_Contract_Wrapper (E, Wrapper_Id);
-      Set_Is_Entry_Wrapper (Wrapper_Id);
-
-      --  The wrapper body is analyzed when the enclosing type is frozen
-
-      Append_Freeze_Action (Defining_Entity (Decl),
-        Make_Subprogram_Body (Loc,
-          Specification              =>
-            Make_Procedure_Specification (Loc,
-              Defining_Unit_Name       => Wrapper_Id,
-              Parameter_Specifications => Formals),
-          Declarations               => Decls,
-          Handled_Statement_Sequence =>
-            Make_Handled_Sequence_Of_Statements (Loc,
-              Statements => New_List (Call))));
-   end Build_Contract_Wrapper;
-
    --------------------------------
    -- Build_Corresponding_Record --
    --------------------------------
@@ -9135,7 +8845,7 @@ package body Exp_Ch9 is
          --  Build a wrapper procedure to handle contract cases, preconditions,
          --  and postconditions.
 
-         Build_Contract_Wrapper (Ent_Id, N);
+         Build_Entry_Contract_Wrapper (Ent_Id, N);
 
          --  Create the barrier function
 
@@ -12529,7 +12239,7 @@ package body Exp_Ch9 is
          Ent := First_Entity (Tasktyp);
          while Present (Ent) loop
             if Ekind (Ent) in E_Entry | E_Entry_Family then
-               Build_Contract_Wrapper (Ent, N);
+               Build_Entry_Contract_Wrapper (Ent, N);
             end if;
 
             Next_Entity (Ent);
@@ -13731,6 +13441,7 @@ package body Exp_Ch9 is
                   Make_Selected_Component (Loc,
                     Prefix        => New_Occurrence_Of (Obj_Ent, Loc),
                     Selector_Name => Make_Identifier (Loc, Name_uObject)));
+
             Add (Decl);
          end;
       end if;
@@ -13762,6 +13473,7 @@ package body Exp_Ch9 is
                      Make_Selected_Component (Loc,
                        Prefix        => New_Occurrence_Of (Obj_Ent, Loc),
                        Selector_Name => Make_Identifier (Loc, Chars (D))));
+
                Add (Decl);
 
                --  Set debug info needed on this renaming declaration even
@@ -13828,6 +13540,7 @@ package body Exp_Ch9 is
                            Make_Selected_Component (Loc,
                              Prefix => New_Occurrence_Of (Obj_Ent, Loc),
                              Selector_Name => Make_Identifier (Loc, Nam)));
+
                      Add (Decl);
                   end if;
 
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 0631172..2def83c 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -453,6 +453,8 @@ package body Exp_Prag is
                            New_Occurrence_Of (RTE (RE_Assert_Failure),
                                                                    Loc))))))));
 
+         Set_Comes_From_Check_Or_Contract (N);
+
       --  Case where we call the procedure
 
       else
@@ -541,6 +543,8 @@ package body Exp_Prag is
                  Name                   =>
                    New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc),
                  Parameter_Associations => New_List (Relocate_Node (Msg))))));
+
+         Set_Comes_From_Check_Or_Contract (N);
       end if;
 
       Analyze (N);
@@ -1433,6 +1437,8 @@ package body Exp_Prag is
                 Condition       => Cond,
                 Then_Statements => New_List (Error));
 
+            Set_Comes_From_Check_Or_Contract (Checks);
+
          else
             if No (Elsif_Parts (Checks)) then
                Set_Elsif_Parts (Checks, New_List);
@@ -1642,6 +1648,8 @@ package body Exp_Prag is
                 Condition       => New_Occurrence_Of (Flag, Loc),
                 Then_Statements => Eval_Stmts);
 
+            Set_Comes_From_Check_Or_Contract (Evals);
+
          --  Otherwise generate:
          --    elsif Flag then
          --       <evaluation statements>
@@ -1836,6 +1844,8 @@ package body Exp_Prag is
                   Set (Flag),
                   Increment (Count)));
 
+            Set_Comes_From_Check_Or_Contract (If_Stmt);
+
             Append_To (Decls, If_Stmt);
             Analyze (If_Stmt);
 
@@ -1904,6 +1914,8 @@ package body Exp_Prag is
               Right_Opnd => Make_Integer_Literal (Loc, 0)),
           Then_Statements => CG_Stmts);
 
+      Set_Comes_From_Check_Or_Contract (CG_Checks);
+
       --  Detect a possible failure due to several case guards evaluating to
       --  True.
 
@@ -1937,15 +1949,17 @@ package body Exp_Prag is
                            New_Occurrence_Of (Msg_Str, Loc))))))))));
       end if;
 
+      --  Append the checks, but do not analyze them at this point, because
+      --  contracts get potentially expanded as part of a wrapper which gets
+      --  fully analyzed once it is fully formed.
+
       Append_To (Decls, CG_Checks);
-      Analyze (CG_Checks);
 
       --  Once all case guards are evaluated and checked, evaluate any prefixes
       --  of attribute 'Old founds in the selected consequence.
 
       if Present (Old_Evals) then
          Append_To (Decls, Old_Evals);
-         Analyze (Old_Evals);
       end if;
 
       --  Raise Assertion_Error when the corresponding consequence of a case
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 52858e2..346904e 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -6248,6 +6248,32 @@ package body Freeze is
         and then Scope (Test_E) /= Current_Scope
         and then Ekind (Test_E) /= E_Constant
       then
+         --  Here we deal with the special case of the expansion of
+         --  postconditions. Previously this was handled by the loop below,
+         --  since these postcondition checks got isolated to a separate,
+         --  internally generated, subprogram. Now, however, the postcondition
+         --  checks get contained within their corresponding subprogram
+         --  directly.
+
+         if not Comes_From_Source (N)
+           and then Nkind (N) = N_Pragma
+           and then From_Aspect_Specification (N)
+           and then Is_Valid_Assertion_Kind (Original_Aspect_Pragma_Name (N))
+
+           --  Now, verify the placement of the pragma is within an expanded
+           --  subprogram which contains postcondition expansion - detected
+           --  through the presence of the "Wrapped_Statements" field.
+
+           and then Present (Enclosing_Subprogram (Current_Scope))
+           and then Present (Wrapped_Statements
+                              (Enclosing_Subprogram (Current_Scope)))
+         then
+            goto Leave;
+         end if;
+
+         --  Otherwise, loop through scopes checking if an enclosing scope
+         --  comes from source or is a generic.
+
          declare
             S : Entity_Id;
 
@@ -8330,9 +8356,9 @@ package body Freeze is
             --  If the parent is a subprogram body, the candidate insertion
             --  point is just ahead of it.
 
-            if  Nkind (Parent_P) = N_Subprogram_Body
-                and then Unique_Defining_Entity (Parent_P) =
-                           Freeze_Outside_Subp
+            if Nkind (Parent_P) = N_Subprogram_Body
+              and then Unique_Defining_Entity (Parent_P) =
+                         Freeze_Outside_Subp
             then
                P := Parent_P;
                exit;
diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads
index ccdaa79..83c7180 100644
--- a/gcc/ada/gen_il-fields.ads
+++ b/gcc/ada/gen_il-fields.ads
@@ -96,6 +96,7 @@ package Gen_IL.Fields is
       Class_Present,
       Classifications,
       Cleanup_Actions,
+      Comes_From_Check_Or_Contract,
       Comes_From_Extended_Return_Statement,
       Compile_Time_Known_Aggregate,
       Component_Associations,
@@ -929,7 +930,8 @@ package Gen_IL.Fields is
       Warnings_Off_Used_Unmodified,
       Warnings_Off_Used_Unreferenced,
       Was_Hidden,
-      Wrapped_Entity
+      Wrapped_Entity,
+      Wrapped_Statements
 
       --  End of entity fields.
      ); -- Opt_Field_Enum
diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb
index 89d8659..2e1e3c9 100644
--- a/gcc/ada/gen_il-gen-gen_entities.adb
+++ b/gcc/ada/gen_il-gen-gen_entities.adb
@@ -1046,7 +1046,8 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Thunk_Entity, Node_Id,
             Pre => "Is_Thunk (N)"),
         Sm (Wrapped_Entity, Node_Id,
-            Pre => "Is_Primitive_Wrapper (N)")));
+            Pre => "Is_Primitive_Wrapper (N)"),
+        Sm (Wrapped_Statements, Node_Id)));
 
    Cc (E_Operator, Subprogram_Kind,
        --  A predefined operator, appearing in Standard, or an implicitly
@@ -1095,7 +1096,8 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Thunk_Entity, Node_Id,
             Pre => "Is_Thunk (N)"),
         Sm (Wrapped_Entity, Node_Id,
-            Pre => "Is_Primitive_Wrapper (N)")));
+            Pre => "Is_Primitive_Wrapper (N)"),
+        Sm (Wrapped_Statements, Node_Id)));
 
    Cc (E_Abstract_State, Overloadable_Kind,
        --  A state abstraction. Used to designate entities introduced by aspect
@@ -1134,7 +1136,8 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Protection_Object, Node_Id),
         Sm (Scope_Depth_Value, Unat),
         Sm (SPARK_Pragma, Node_Id),
-        Sm (SPARK_Pragma_Inherited, Flag)));
+        Sm (SPARK_Pragma_Inherited, Flag),
+        Sm (Wrapped_Statements, Node_Id)));
 
    Cc (E_Entry_Family, Entity_Kind,
        --  An entry family, created by an entry family declaration in a
@@ -1161,7 +1164,8 @@ begin -- Gen_IL.Gen.Gen_Entities
         Sm (Renamed_Or_Alias, Node_Id),
         Sm (Scope_Depth_Value, Unat),
         Sm (SPARK_Pragma, Node_Id),
-        Sm (SPARK_Pragma_Inherited, Flag)));
+        Sm (SPARK_Pragma_Inherited, Flag),
+        Sm (Wrapped_Statements, Node_Id)));
 
    Cc (E_Block, Entity_Kind,
        --  A block identifier, created by an explicit or implicit label on
diff --git a/gcc/ada/gen_il-gen-gen_nodes.adb b/gcc/ada/gen_il-gen-gen_nodes.adb
index f7aadc4..556326a 100644
--- a/gcc/ada/gen_il-gen-gen_nodes.adb
+++ b/gcc/ada/gen_il-gen-gen_nodes.adb
@@ -1098,7 +1098,8 @@ begin -- Gen_IL.Gen.Gen_Nodes
         Sy (Elsif_Parts, List_Id, Default_No_List),
         Sy (Else_Statements, List_Id, Default_No_List),
         Sy (End_Span, Unat, Default_Uint_0),
-        Sm (From_Conditional_Expression, Flag)));
+        Sm (From_Conditional_Expression, Flag),
+        Sm (Comes_From_Check_Or_Contract, Flag)));
 
    Cc (N_Accept_Alternative, Node_Kind,
        (Sy (Accept_Statement, Node_Id),
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 1ce1d6a..0f03285 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -271,11 +271,11 @@ package body Ghost is
 
                if Present (Subp_Id) then
 
-                  --  The context is the internally built _Postconditions
+                  --  The context is the internally built _Wrapped_Statements
                   --  procedure, which is OK because the real check was done
-                  --  before expansion activities.
+                  --  before contract expansion activities.
 
-                  if Chars (Subp_Id) = Name_uPostconditions then
+                  if Chars (Subp_Id) = Name_uWrapped_Statements then
                      return True;
 
                   --  The context is the internally built predicate function,
@@ -432,9 +432,7 @@ package body Ghost is
             --  but it may still contain references to Ghost entities.
 
             elsif Nkind (Stmt) = N_If_Statement
-              and then Nkind (Original_Node (Stmt)) = N_Pragma
-              and then Assertion_Expression_Pragma
-                         (Get_Pragma_Id (Original_Node (Stmt)))
+              and then Comes_From_Check_Or_Contract (Stmt)
             then
                return True;
             end if;
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 91e8f45..e3f35da 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -3257,7 +3257,7 @@ package body Inline is
          pragma Assert
            (Modify_Tree_For_C
              and then Is_Subprogram (Enclosing_Subp)
-             and then Present (Postconditions_Proc (Enclosing_Subp)));
+             and then Present (Wrapped_Statements (Enclosing_Subp)));
 
          if Ekind (Enclosing_Subp) = E_Function then
             if Nkind (First (Parameter_Associations (N))) in
@@ -3851,7 +3851,7 @@ package body Inline is
 
             if Modify_Tree_For_C
               and then Nkind (N) = N_Procedure_Call_Statement
-              and then Chars (Name (N)) = Name_uPostconditions
+              and then Chars (Name (N)) = Name_uWrapped_Statements
             then
                Declare_Postconditions_Result;
             end if;
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index a4ff69a..043444c 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -618,15 +618,6 @@ package body Lib.Xref is
          end if;
       end if;
 
-      --  Do not generate references if we are within a postcondition sub-
-      --  program, because the reference does not comes from source, and the
-      --  preanalysis of the aspect has already created an entry for the ALI
-      --  file at the proper source location.
-
-      if Chars (Current_Scope) = Name_uPostconditions then
-         return;
-      end if;
-
       --  Never collect references if not in main source unit. However, we omit
       --  this test if Typ is 'e' or 'k', since these entries are structural,
       --  and it is useful to have them in units that reference packages as
diff --git a/gcc/ada/lib.adb b/gcc/ada/lib.adb
index 6c51cc7..691d8e4 100644
--- a/gcc/ada/lib.adb
+++ b/gcc/ada/lib.adb
@@ -992,6 +992,15 @@ package body Lib is
       return Is_Predefined_Renaming (Unit);
    end In_Predefined_Renaming;
 
+   ---------
+   -- ipu --
+   ---------
+
+   function ipu (N : Node_Or_Entity_Id) return Boolean is
+   begin
+      return In_Predefined_Unit (N);
+   end ipu;
+
    ------------------------
    -- In_Predefined_Unit --
    ------------------------
diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads
index e29d42a..c308ac1 100644
--- a/gcc/ada/lib.ads
+++ b/gcc/ada/lib.ads
@@ -633,6 +633,12 @@ package Lib is
    function In_Extended_Main_Source_Unit (Loc : Source_Ptr) return Boolean;
    --  Same function as above, but argument is a source pointer
 
+   function ipu (N : Node_Or_Entity_Id) return Boolean;
+   --  Same as In_Predefined_Unit, but renamed so it can assist debugging.
+   --  Otherwise, there is a disambiguous name conflict in the two versions of
+   --  In_Predefined_Unit which makes it inconvient to set as a breakpoint
+   --  condition.
+
    function In_Predefined_Unit (N : Node_Or_Entity_Id) return Boolean;
    --  Returns True if the given node or entity appears within the source text
    --  of a predefined unit (i.e. within Ada, Interfaces, System or within one
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 86c7d0f..6869aca 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1430,12 +1430,11 @@ package body Sem_Attr is
                Placement_Error;
             end if;
 
-         --  'Old attribute reference ok in a _Postconditions procedure
+         --  'Old attribute reference ok in a _Wrapped_Statements procedure
 
          elsif Nkind (Prag) = N_Subprogram_Body
-           and then not Comes_From_Source (Prag)
-           and then Nkind (Corresponding_Spec (Prag)) = N_Defining_Identifier
-           and then Chars (Corresponding_Spec (Prag)) = Name_uPostconditions
+           and then Ekind (Defining_Entity (Prag)) in Subprogram_Kind
+           and then Present (Wrapped_Statements (Defining_Entity (Prag)))
          then
             null;
 
@@ -1450,18 +1449,18 @@ package body Sem_Attr is
          if Nkind (Prag) = N_Aspect_Specification then
             Subp_Decl := Parent (Prag);
          elsif Nkind (Prag) = N_Subprogram_Body then
-            declare
-               Enclosing_Scope : constant Node_Id :=
-                 Scope (Corresponding_Spec (Prag));
-            begin
-               pragma Assert (Postconditions_Proc (Enclosing_Scope)
-                               = Corresponding_Spec (Prag));
-               Subp_Decl := Parent (Parent (Enclosing_Scope));
-            end;
+            Subp_Decl := Prag;
          else
             Subp_Decl := Find_Related_Declaration_Or_Body (Prag);
          end if;
 
+         --  'Old objects appear in extended return statements as part of
+         --  the expansion of contract wrappers.
+
+         if Nkind (Subp_Decl) = N_Extended_Return_Statement then
+            Subp_Decl := Parent (Parent (Subp_Decl));
+         end if;
+
          --  The aspect or pragma where the attribute resides should be
          --  associated with a subprogram declaration or a body. If this is not
          --  the case, then the aspect or pragma is illegal. Return as analysis
@@ -1506,7 +1505,7 @@ package body Sem_Attr is
 
          if Modify_Tree_For_C
            and then Chars (Spec_Id) = Name_uParent
-           and then Chars (Scope (Spec_Id)) = Name_uPostconditions
+           and then Chars (Scope (Spec_Id)) = Name_uWrapped_Statements
          then
             --  This situation occurs only when analyzing the body-to-inline
 
@@ -1750,7 +1749,7 @@ package body Sem_Attr is
          if Is_Entry_Wrapper (Spec_Id) then
             Legal := True;
 
-         elsif Chars (Spec_Id) = Name_uPostconditions
+         elsif Chars (Spec_Id) = Name_uWrapped_Statements
            and then Is_Entry_Wrapper (Scope (Spec_Id))
          then
             Spec_Id := Scope (Spec_Id);
@@ -5881,13 +5880,13 @@ package body Sem_Attr is
             Error_Attr ("prefix of % attribute must be a function", P);
          end if;
 
-         --  Attribute 'Result is part of a _Postconditions procedure. There is
+         --  Attribute 'Result is part of postconditions expansion. There is
          --  no need to perform the semantic checks below as they were already
          --  verified when the attribute was analyzed in its original context.
          --  Instead, rewrite the attribute as a reference to formal parameter
-         --  _Result of the _Postconditions procedure.
+         --  _Result of the _Wrapped_Statements procedure.
 
-         if Chars (Spec_Id) = Name_uPostconditions
+         if Chars (Spec_Id) = Name_uWrapped_Statements
            or else
              (In_Inlined_C_Postcondition
                and then Nkind (Parent (Spec_Id)) = N_Block_Statement)
diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb
index a15fd09..339edd3 100644
--- a/gcc/ada/sem_ch11.adb
+++ b/gcc/ada/sem_ch11.adb
@@ -49,7 +49,6 @@ with Sem_Warn;       use Sem_Warn;
 with Sinfo;          use Sinfo;
 with Sinfo.Nodes;    use Sinfo.Nodes;
 with Sinfo.Utils;    use Sinfo.Utils;
-with Snames;         use Snames;
 with Stand;          use Stand;
 
 package body Sem_Ch11 is
@@ -431,12 +430,10 @@ package body Sem_Ch11 is
 
       --  If the current scope is a subprogram, entry or task body or declare
       --  block then this is the right place to check for hanging useless
-      --  assignments from the statement sequence. Skip this in the body of a
-      --  postcondition, since in that case there are no source references.
+      --  assignments from the statement sequence.
 
-      if (Is_Subprogram_Or_Entry (Current_Scope)
-           and then Chars (Current_Scope) /= Name_uPostconditions)
-         or else Ekind (Current_Scope) in E_Block | E_Task_Type
+      if Is_Subprogram_Or_Entry (Current_Scope)
+        or else Ekind (Current_Scope) in E_Block | E_Task_Type
       then
          Warn_On_Useless_Assignments (Current_Scope);
       end if;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 93eeecb..0459058 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1911,15 +1911,19 @@ package body Sem_Ch6 is
             Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
          end if;
 
-         Analyze_Declarations (Declarations (N));
-         Check_Completion;
-
-         --  Process the contract of the subprogram body after all declarations
-         --  have been analyzed. This ensures that any contract-related pragmas
-         --  are available through the N_Contract node of the body.
+         --  Process the contract of the subprogram body after analyzing all
+         --  the contract-related pragmas within the declarations.
 
+         Analyze_Pragmas_In_Declarations (Body_Id);
          Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
 
+         --  Continue on with analyzing the declarations and statements once
+         --  contract expansion is done and we are done expanding contract
+         --  related wrappers.
+
+         Analyze_Declarations (Declarations (N));
+         Check_Completion;
+
          Analyze (Handled_Statement_Sequence (N));
          Save_Global_References (Original_Node (N));
 
@@ -2895,7 +2899,6 @@ package body Sem_Ch6 is
       Conformant : Boolean;
       Desig_View : Entity_Id := Empty;
       Exch_Views : Elist_Id  := No_Elist;
-      HSS        : Node_Id;
       Mask_Types : Elist_Id  := No_Elist;
       Prot_Typ   : Entity_Id := Empty;
       Spec_Decl  : Node_Id   := Empty;
@@ -3530,6 +3533,8 @@ package body Sem_Ch6 is
       --------------------------
 
       procedure Check_Missing_Return is
+         HSS : constant Node_Id := Handled_Statement_Sequence (N);
+
          Id          : Entity_Id;
          Missing_Ret : Boolean;
 
@@ -3968,18 +3973,9 @@ package body Sem_Ch6 is
 
                --  Move relevant pragmas to the spec
 
-               elsif Pragma_Name_Unmapped (Decl) in Name_Depends
-                                                  | Name_Ghost
-                                                  | Name_Global
-                                                  | Name_Pre
-                                                  | Name_Precondition
-                                                  | Name_Post
-                                                  | Name_Refined_Depends
-                                                  | Name_Refined_Global
-                                                  | Name_Refined_Post
-                                                  | Name_Inline
-                                                  | Name_Pure_Function
-                                                  | Name_Volatile_Function
+               elsif
+                 Pragma_Significant_To_Subprograms
+                   (Get_Pragma_Id (Decl))
                then
                   Remove (Decl);
                   Insert_After (Insert_Nod, Decl);
@@ -4223,7 +4219,6 @@ package body Sem_Ch6 is
             Analyze_Generic_Subprogram_Body (N, Spec_Id);
 
             if Nkind (N) = N_Subprogram_Body then
-               HSS := Handled_Statement_Sequence (N);
                Check_Missing_Return;
             end if;
 
@@ -5157,9 +5152,27 @@ package body Sem_Ch6 is
          end;
       end if;
 
-      --  Now we can go on to analyze the body
+      --  Ada 2012 (AI05-0151): Incomplete types coming from a limited context
+      --  may now appear in parameter and result profiles. Since the analysis
+      --  of a subprogram body may use the parameter and result profile of the
+      --  spec, swap any limited views with their non-limited counterpart.
+
+      if Ada_Version >= Ada_2012 and then Present (Spec_Id) then
+         Exch_Views := Exchange_Limited_Views (Spec_Id);
+      end if;
+
+      --  Analyze any aspect specifications that appear on the subprogram body
+
+      if Has_Aspects (N) then
+         Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
+      end if;
+
+      --  Process the contract of the subprogram body after analyzing all the
+      --  contract-related pragmas within the declarations.
+
+      Analyze_Pragmas_In_Declarations (Body_Id);
+      Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
 
-      HSS := Handled_Statement_Sequence (N);
       Set_Actual_Subtypes (N, Current_Scope);
 
       --  Add a declaration for the Protection object, renaming declarations
@@ -5180,15 +5193,6 @@ package body Sem_Ch6 is
            (Sloc (N), Spec_Id, Prot_Typ, N, Declarations (N));
       end if;
 
-      --  Ada 2012 (AI05-0151): Incomplete types coming from a limited context
-      --  may now appear in parameter and result profiles. Since the analysis
-      --  of a subprogram body may use the parameter and result profile of the
-      --  spec, swap any limited views with their non-limited counterpart.
-
-      if Ada_Version >= Ada_2012 and then Present (Spec_Id) then
-         Exch_Views := Exchange_Limited_Views (Spec_Id);
-      end if;
-
       --  If the return type is an anonymous access type whose designated type
       --  is the limited view of a class-wide type and the non-limited view is
       --  available, update the return type accordingly.
@@ -5225,12 +5229,6 @@ package body Sem_Ch6 is
          end;
       end if;
 
-      --  Analyze any aspect specifications that appear on the subprogram body
-
-      if Has_Aspects (N) then
-         Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
-      end if;
-
       Analyze_Declarations (Declarations (N));
 
       --  Verify that the SPARK_Mode of the body agrees with that of its spec
@@ -5269,17 +5267,11 @@ package body Sem_Ch6 is
          end if;
       end if;
 
-      --  A subprogram body freezes its own contract. Analyze the contract
-      --  after the declarations of the body have been processed as pragmas
-      --  are now chained on the contract of the subprogram body.
-
-      Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
-
       --  Check completion, and analyze the statements
 
       Check_Completion;
       Inspect_Deferred_Constant_Completion (Declarations (N));
-      Analyze (HSS);
+      Analyze (Handled_Statement_Sequence (N));
 
       --  Add the generated minimum accessibility objects to the subprogram
       --  body's list of declarations after analysis of the statements and
@@ -5296,7 +5288,8 @@ package body Sem_Ch6 is
 
       --  Deal with end of scope processing for the body
 
-      Process_End_Label (HSS, 't', Current_Scope);
+      Process_End_Label
+        (Handled_Statement_Sequence (N), 't', Current_Scope);
       Update_Use_Clause_Chain;
       End_Scope;
 
@@ -5410,7 +5403,7 @@ package body Sem_Ch6 is
       --  the warning.
 
       declare
-         Stm : Node_Id := First (Statements (HSS));
+         Stm : Node_Id := First (Statements (Handled_Statement_Sequence (N)));
       begin
          --  Skip call markers installed by the ABE mechanism, labels, and
          --  Push_xxx_Error_Label to find the first real statement.
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index b8e3fb6..f912f8b 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -1809,11 +1809,6 @@ package body Sem_Elab is
       --  Determine whether arbitrary entity Id denotes a partial invariant
       --  procedure.
 
-      function Is_Postconditions_Proc (Id : Entity_Id) return Boolean;
-      pragma Inline (Is_Postconditions_Proc);
-      --  Determine whether arbitrary entity Id denotes internally generated
-      --  routine _Postconditions.
-
       function Is_Preelaborated_Unit (Id : Entity_Id) return Boolean;
       pragma Inline (Is_Preelaborated_Unit);
       --  Determine whether arbitrary entity Id denotes a unit which is subject
@@ -2481,14 +2476,6 @@ package body Sem_Elab is
          elsif Is_Partial_Invariant_Proc (Subp_Id) then
             null;
 
-         --  _Postconditions
-
-         elsif Is_Postconditions_Proc (Subp_Id) then
-            Output_Verification_Call
-              (Pred    => "postconditions",
-               Id      => Find_Enclosing_Scope (Call),
-               Id_Kind => "subprogram");
-
          --  Subprograms must come last because some of the previous cases fall
          --  under this category.
 
@@ -6638,14 +6625,6 @@ package body Sem_Elab is
             elsif Is_Partial_Invariant_Proc (Subp_Id) then
                null;
 
-            --  _Postconditions
-
-            elsif Is_Postconditions_Proc (Subp_Id) then
-               Info_Verification_Call
-                 (Pred    => "postconditions",
-                  Id      => Find_Enclosing_Scope (Call),
-                  Id_Kind => "subprogram");
-
             --  Subprograms must come last because some of the previous cases
             --  fall under this category.
 
@@ -13091,10 +13070,6 @@ package body Sem_Elab is
            (Extra : out Entity_Id;
             Kind  : out Invocation_Kind)
          is
-            Targ_Rep  : constant Target_Rep_Id :=
-                          Target_Representation_Of (Targ_Id, In_State);
-            Spec_Decl : constant Node_Id := Spec_Declaration (Targ_Rep);
-
          begin
             --  Accept within a task body
 
@@ -13180,12 +13155,6 @@ package body Sem_Elab is
                Extra := First_Formal_Type (Targ_Id);
                Kind  := Invariant_Verification;
 
-            --  Postcondition verification
-
-            elsif Is_Postconditions_Proc (Targ_Id) then
-               Extra := Find_Enclosing_Scope (Spec_Decl);
-               Kind  := Postcondition_Verification;
-
             --  Protected entry call
 
             elsif Is_Protected_Entry (Targ_Id) then
@@ -14454,8 +14423,7 @@ package body Sem_Elab is
            Is_Default_Initial_Condition_Proc (Id)
              or else Is_Initial_Condition_Proc (Id)
              or else Is_Invariant_Proc (Id)
-             or else Is_Partial_Invariant_Proc (Id)
-             or else Is_Postconditions_Proc (Id);
+             or else Is_Partial_Invariant_Proc (Id);
       end Is_Assertion_Pragma_Target;
 
       ----------------------------
@@ -14497,7 +14465,6 @@ package body Sem_Elab is
            Is_Accept_Alternative_Proc (Id)
              or else Is_Finalizer_Proc (Id)
              or else Is_Partial_Invariant_Proc (Id)
-             or else Is_Postconditions_Proc (Id)
              or else Is_TSS (Id, TSS_Deep_Adjust)
              or else Is_TSS (Id, TSS_Deep_Finalize)
              or else Is_TSS (Id, TSS_Deep_Initialize);
@@ -14653,18 +14620,6 @@ package body Sem_Elab is
              and then Is_Partial_Invariant_Procedure (Id);
       end Is_Partial_Invariant_Proc;
 
-      ----------------------------
-      -- Is_Postconditions_Proc --
-      ----------------------------
-
-      function Is_Postconditions_Proc (Id : Entity_Id) return Boolean is
-      begin
-         --  To qualify, the entity must denote a _Postconditions procedure
-
-         return
-           Ekind (Id) = E_Procedure and then Chars (Id) = Name_uPostconditions;
-      end Is_Postconditions_Proc;
-
       ---------------------------
       -- Is_Preelaborated_Unit --
       ---------------------------
@@ -17482,7 +17437,7 @@ package body Sem_Elab is
 
       if Nkind (N) = N_Procedure_Call_Statement
         and then Is_Entity_Name (Name (N))
-        and then Chars (Entity (Name (N))) = Name_uPostconditions
+        and then Chars (Entity (Name (N))) = Name_uWrapped_Statements
       then
          return;
       end if;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 13cee59..509a04e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -5548,6 +5548,14 @@ package body Sem_Prag is
                then
                   OK := True;
 
+               --  Special case for postconditions wrappers
+
+               elsif Ekind (Scop) in Subprogram_Kind
+                 and then Present (Wrapped_Statements (Scop))
+                 and then Wrapped_Statements (Scop) = Current_Scope
+               then
+                  OK := True;
+
                --  Default case, just check that the pragma occurs in the scope
                --  of the entity denoted by the name.
 
@@ -32236,10 +32244,10 @@ package body Sem_Prag is
       then
          return;
 
-      --  Do not process internally generated routine _Postconditions
+      --  Do not process internally generated routine _Wrapped_Statements
 
       elsif Ekind (Body_Id) = E_Procedure
-        and then Chars (Body_Id) = Name_uPostconditions
+        and then Chars (Body_Id) = Name_uWrapped_Statements
       then
          return;
       end if;
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index e8a65ce..619f841 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -156,6 +156,9 @@ package Sem_Prag is
       Pragma_Type_Invariant_Class      => True,
       others                           => False);
 
+   --  Should to following constant arrays be renamed to better suit their
+   --  use as a predicate (e.g. Is_Pragma_*) ???
+
    --  The following table lists all the implementation-defined pragmas that
    --  should apply to the anonymous object produced by the analysis of a
    --  single protected or task type. The table should be synchronized with
@@ -200,6 +203,32 @@ package Sem_Prag is
       Pragma_Warnings                      => False,
       others                               => True);
 
+   --  The following table lists all pragmas which are relevant to the analysis
+   --  of subprogram bodies.
+
+   Pragma_Significant_To_Subprograms : constant array (Pragma_Id) of Boolean :=
+     (Pragma_Contract_Cases    => True,
+      Pragma_Depends           => True,
+      Pragma_Ghost             => True,
+      Pragma_Global            => True,
+      Pragma_Inline            => True,
+      Pragma_Inline_Always     => True,
+      Pragma_Post              => True,
+      Pragma_Post_Class        => True,
+      Pragma_Postcondition     => True,
+      Pragma_Pre               => True,
+      Pragma_Pre_Class         => True,
+      Pragma_Precondition      => True,
+      Pragma_Pure              => True,
+      Pragma_Pure_Function     => True,
+      Pragma_Refined_Depends   => True,
+      Pragma_Refined_Global    => True,
+      Pragma_Refined_Post      => True,
+      Pragma_Refined_State     => True,
+      Pragma_Volatile          => True,
+      Pragma_Volatile_Function => True,
+      others                   => False);
+
    -----------------
    -- Subprograms --
    -----------------
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 4b76595..7675070 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -8412,6 +8412,7 @@ package body Sem_Res is
       if Is_Entry (Nam)
         and then Present (Contract_Wrapper (Nam))
         and then Current_Scope /= Contract_Wrapper (Nam)
+        and then Current_Scope /= Wrapped_Statements (Contract_Wrapper (Nam))
       then
          --  Note the entity being called before rewriting the call, so that
          --  it appears used at this point.
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index b708764..8c64ac3 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -597,6 +597,7 @@ package body Sem_Util is
                --  Anonymous access types
 
                elsif Nkind (Pre) in N_Has_Entity
+                 and then Ekind (Entity (Pre)) not in Subprogram_Kind
                  and then Present (Get_Dynamic_Accessibility (Entity (Pre)))
                  and then Level = Dynamic_Level
                then
@@ -14122,9 +14123,10 @@ package body Sem_Util is
       if Subp_Nam = Name_uFinalizer then
          return False;
 
-      --  _Postconditions procedure
+      --  _Wrapped_Statements procedure which gets generated as part of the
+      --  expansion of postconditions.
 
-      elsif Subp_Nam = Name_uPostconditions then
+      elsif Subp_Nam = Name_uWrapped_Statements then
          return False;
 
       --  Predicate function
@@ -28013,8 +28015,18 @@ package body Sem_Util is
       E : Entity_Id) return Boolean
    is
       Subp_Alias : constant Entity_Id := Alias (S);
+      Subp       : Entity_Id := E;
    begin
-      return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
+      --  During expansion of subprograms with postconditions the original
+      --  subprogram's declarations and statements get wrapped into a local
+      --  _Wrapped_Statements subprogram.
+
+      if Chars (Subp) = Name_uWrapped_Statements then
+         Subp := Enclosing_Subprogram (Subp);
+      end if;
+
+      return S = Subp
+        or else (Present (Subp_Alias) and then Subp_Alias = Subp);
    end Same_Or_Aliased_Subprograms;
 
    ---------------
@@ -32462,7 +32474,7 @@ package body Sem_Util is
                and then Ekind (Scope (T))
                  in E_Entry | E_Entry_Family | E_Function | E_Procedure
                and then
-                 (Present (Postconditions_Proc (Scope (T)))
+                 (Present (Wrapped_Statements (Scope (T)))
                   or else Present (Contract (Scope (T))))
             then
                --  ??? Should define a flag for this. We could incorrectly
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 28573c3..53880c5 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -82,6 +82,12 @@ package Sinfo is
    --                 for this purpose, so e.g. in X := (if A then B else C);
    --                 Paren_Count for the right side will be 1.
 
+   --   Comes_From_Check_Or_Contract
+   --                 This flag is present in all N_If_Statement nodes and
+   --                 gets set when an N_If_Statement is generated as part of
+   --                 the expansion of a Check, Assert, or contract-related
+   --                 pragma.
+
    --   Comes_From_Source
    --                 This flag is present in all nodes. It is set if the
    --                 node is built by the scanner or parser, and clear if
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index ee9972d..79557e7 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -190,7 +190,6 @@ package Snames is
    Name_uMaster                        : constant Name_Id := N + $;
    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 + $;
@@ -208,6 +207,7 @@ package Snames is
    Name_uTask_Name                     : constant Name_Id := N + $;
    Name_uType_Invariant                : constant Name_Id := N + $;
    Name_uVariants                      : constant Name_Id := N + $;
+   Name_uWrapped_Statements            : constant Name_Id := N + $;
 
    --  Names of predefined primitives used in the expansion of dispatching
    --  requeue and select statements, Abort, 'Callable and 'Terminated.