[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

1 files changed, 617 insertions, 436 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 --
    -----------------------------------