[multiple changes]

2015-03-02  Thomas Quinot  <quinot@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference, case Input): When
	expanding a 'Input attribute reference for a class-wide type,
	do not generate a separate object declaration for the controlling
	tag dummy object; instead, generate the expression inline in the
	dispatching call. Otherwise, the declaration (which involves a
	call to String'Input, returning a dynamically sized value on the
	secondary stack) will be expanded outside of proper secondary
	stack mark/release operations, and will thus cause a secondary
	stack leak.

2015-03-02  Hristian Kirtchev  <kirtchev@adacore.com>

	* checks.adb (Add_Validity_Check): Change the names of all
	formal parameters to better illustrate their purpose. Update
	the subprogram documentation. Update all occurrences of the
	formal parameters. Generate a pre/postcondition pragma by
	calling Build_Pre_Post_Condition.
	(Build_PPC_Pragma): Removed.
	(Build_Pre_Post_Condition): New routine.
	* einfo.adb Node8 is no longer used as Postcondition_Proc. Node14
	is now used as Postconditions_Proc. Flag240 is now renamed to
	Has_Expanded_Contract.	(First_Formal): The routine can now
	operate on generic subprograms.
	(First_Formal_With_Extras): The routine can now operate on generic
	subprograms.
	(Has_Expanded_Contract): New routine.
	(Has_Postconditions): Removed.
	(Postcondition_Proc): Removed.
	(Postconditions_Proc): New routine.
	(Set_Has_Expanded_Contract): New routine.
	(Set_Has_Postconditions): Removed.
	(Set_Postcondition_Proc): Removed.
	(Set_Postconditions_Proc): New routine.
	(Write_Entity_Flags): Remove the output of Has_Postconditions. Add
	the output of Has_Expanded_Contract.
	(Write_Field8_Name): Remove the output of Postcondition_Proc.
	(Write_Field14_Name): Add the output of Postconditions_Proc.
	* einfo.ads New attributes Has_Expanded_Contract and
	Postconditions_Proc along with occurrences in entities.
	Remove attributes Has_Postconditions and Postcondition_Proc
	along with occurrences in entities.
	(Has_Expanded_Contract): New routine along with pragma Inline.
	(Has_Postconditions): Removed along with pragma Inline.
	(Postcondition_Proc): Removed along with pragma Inline.
	(Postconditions_Proc): New routine along with pragma Inline.
	(Set_Has_Expanded_Contract): New routine along with pragma Inline.
	(Set_Has_Postconditions): Removed along with pragma Inline.
	(Set_Postcondition_Proc): Removed along with pragma Inline.
	(Set_Postconditions_Proc): New routine along with pragma Inline.
	* exp_ch6.adb (Add_Return): Code cleanup. Update the
	generation of the call to the _Postconditions routine of
	the procedure.	(Expand_Non_Function_Return): Reformat the
	comment on usage. Code cleanup.  Update the generation of
	the call to the _Postconditions routine of the procedure or
	entry [family].
	(Expand_Simple_Function_Return): Update the
	generation of the _Postconditions routine of the function.
	(Expand_Subprogram_Contract): Reimplemented.
	* exp_ch6.ads (Expand_Subprogram_Contract): Update the parameter
	profile along the comment on usage.
	* exp_ch9.adb (Build_PPC_Wrapper): Code cleanup.
	(Expand_N_Task_Type_Declaration): Generate pre/postconditions
	wrapper when the entry [family] has a contract with
	pre/postconditions.
	* exp_prag.adb (Expand_Attributes_In_Consequence): New routine.
	(Expand_Contract_Cases): This routine and its subsidiaries now
	analyze all generated code.
	(Expand_Old_In_Consequence): Removed.
	* sem_attr.adb Add with and use clause for Sem_Prag.
	(Analyze_Attribute): Reimplment the analysis of attribute 'Result.
	(Check_Use_In_Test_Case): Use routine Test_Case_Arg to obtain
	"Ensures".
	* sem_ch3.adb (Analyze_Declarations): Analyze the contract of
	a generic subprogram.
	(Analyze_Object_Declaration): Do not create a contract node.
	(Derive_Subprogram): Do not create a contract node.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Do
	not create a contract node.
	(Analyze_Completion_Contract): New routine.
	(Analyze_Function_Return): Alphabetize.
	(Analyze_Generic_Subprogram_Body): Alphabetize. Do not create a
	contract node.	Do not copy pre/postconditions to the original
	generic template.
	(Analyze_Null_Procedure): Do not create a contract node.
	(Analyze_Subprogram_Body_Contract): Reimplemented.
	(Analyze_Subprogram_Body_Helper): Do not mark the enclosing scope
	as having postconditions. Do not create a contract node. Analyze
	the subprogram body contract of a body that acts as a compilation
	unit. Expand the subprogram contract after the declarations have
	been analyzed.
	(Analyze_Subprogram_Contract): Reimplemented.
	(Analyze_Subprogram_Specification): Do not create a contract node.
	(List_Inherited_Pre_Post_Aspects): Code cleanup.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Update the
	comment on usage.
	(Analyze_Subprogram_Contract): Update the
	parameter profile and the comment on usage.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Do not create a
	contract node.
	(Analyze_Package_Declaration): Do not create a
	contract node.
	(Is_Subp_Or_Const_Ref): Ensure that the prefix has an entity.
	* sem_ch8.adb (Analyze_Subprogram_Renaming): Do not create a
	contract node.
	* sem_ch9.adb (Analyze_Entry_Declaration): Do not create a
	contract node.
	* sem_ch10.adb (Analyze_Compilation_Unit): Move local variables to
	their proper section and alphabetize them. Analyze the contract of
	a [generic] subprogram after all Pragmas_After have been analyzed.
	(Analyze_Subprogram_Body_Stub_Contract): Alphabetize.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Do not
	create a contract node.
	(Analyze_Generic_Subprogram_Declaration):
	Alphabetize local variables. Do not create a contract
	node. Do not generate aspects out of pragmas for ASIS.
	(Analyze_Subprogram_Instantiation): Instantiate
	the contract of the subprogram.  Do not create a
	contract node.	(Instantiate_Contract): New routine.
	(Instantiate_Subprogram_Body): Alphabetize local variables.
	(Save_Global_References_In_Aspects): New routine.
	(Save_References): Do not save the global references found within
	the aspects of a generic subprogram.
	* sem_ch12.ads (Save_Global_References_In_Aspects): New routine.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Do not use
	Original_Node for establishing linkages.
	(Insert_Pragma): Insertion in a subprogram body takes precedence over
	the case where the subprogram body is also a compilation unit.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Use
	Get_Argument to obtain the proper expression. Install the generic
	formals when the related context is a generic subprogram.
	(Analyze_Depends_In_Decl_Part): Use Get_Argument to obtain
	the proper expression. Use Corresponding_Spec_Of to obtain
	the spec. Install the generic formal when the related context
	is a generic subprogram.
	(Analyze_Global_In_Decl_Part): Use Get_Argument to obtain the proper
	expression. Use Corresponding_Spec_Of to obtain the spec. Install the
	generic formal when the related context is a generic subprogram.
	(Analyze_Initial_Condition_In_Decl_Part): Use Get_Argument
	to obtain the proper expression. Remove the call to
	Check_SPARK_Aspect_For_ASIS as the analysis is now done
	automatically.
	(Analyze_Pragma): Update all occurrences
	to Original_Aspect_Name. Pragmas Contract_Cases, Depends,
	Extensions_Visible, Global, Postcondition, Precondition and
	Test_Case now carry generic templates when the related context
	is a generic subprogram. The same pragmas are no longer
	forcefully fully analyzed when the context is a subprogram
	that acts as a compilation unit. Pragmas Abstract_State,
	Initial_Condition, Initializes and Refined_State have been clean
	up. Pragmas Post, Post_Class, Postcondition, Pre, Pre_Class
	and Precondition now use the same routine for analysis. Pragma
	Refined_Post does not need to check the use of 'Result or
	the lack of a post-state in its expression. Reimplement the
	analysis of pragma Test_Case.
	(Analyze_Pre_Post_Condition): New routine.
	(Analyze_Pre_Post_Condition_In_Decl_Part):
	Reimplemented.
	(Analyze_Refined_Depends_In_Decl_Part): Use Get_Argument to obtain the
	proper expression.
	(Analyze_Refined_Global_In_Decl_Part): Use Get_Argument to obtain
	the proper expression.
	(Analyze_Test_Case_In_Decl_Part): Reimplemented.
	(Check_Pre_Post): Removed.
	(Check_Precondition_Postcondition): Removed.
	(Check_SPARK_Aspect_For_ASIS): Removed.
	(Check_Test_Case): Removed.
	(Collect_Subprogram_Inputs_Outputs): Use Get_Argument
	to obtain the proper expression. Use Corresponding_Spec_Of to
	find the proper spec.
	(Create_Generic_Template): New routine.
	(Duplication_Error): New routine.
	(Expression_Function_Error): New routine.
	(Find_Related_Subprogram_Or_Body): Moved to the spec
	of Sem_Prag. Emit precise error messages. Account for cases of
	rewritten expression functions, generic instantiations, handled
	sequence of statements and pragmas from aspects.
	(Get_Argument): New routine.
	(Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed.
	(Preanalyze_CTC_Args): Removed.
	(Process_Class_Wide_Condition): New routine.
	* sem_prag.ads (Analyze_Test_Case_In_Decl_Part): Update
	the parameter profile along with the comment on usage.
	(Find_Related_Subprogram_Or_Body): Moved from the body of Sem_Prag.
	(Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed.
	(Test_Case_Arg): New routine.
	* sem_util.adb Add with and use clauses for Sem_Ch6.
	(Add_Contract_Item): This routine now creates a contract
	node the first time an item is added. Remove the duplicate
	aspect/pragma checks.
	(Check_Result_And_Post_State): Reimplemented.
	(Corresponding_Spec_Of): New routine.
	(Get_Ensures_From_CTC_Pragma): Removed.
	(Get_Requires_From_CTC_Pragma): Removed.
	(Has_Significant_Contract): New routine.
	(Inherit_Subprogram_Contract): Inherit only if the source
	has a contract.
	(Install_Generic_Formals): New routine.
	(Original_Aspect_Name): Removed.
	(Original_Aspect_Pragma_Name): New routine.
	* sem_util.ads (Check_Result_And_Post_State): Reimplemented.
	(Corresponding_Spec_Of): New routine.
	(Get_Ensures_From_CTC_Pragma): Removed.
	(Get_Requires_From_CTC_Pragma): Removed.
	(Has_Significant_Contract): New routine.
	(Install_Generic_Formals): New routine.
	(Original_Aspect_Name): Removed.
	(Original_Aspect_Pragma_Name): New routine.
	* sem_warn.adb Add with and use clauses for Sem_Prag.
	(Within_Postcondition): Use Test_Case_Arg to extract "Ensures".

From-SVN: r221101

1 files changed, 296 insertions, 191 deletions

diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 36f78d1..06b9090 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -59,6 +59,7 @@ with Sem_Dist; use Sem_Dist;
 with Sem_Elab; use Sem_Elab;
 with Sem_Elim; use Sem_Elim;
 with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Type; use Sem_Type;
 with Sem_Util; use Sem_Util;
@@ -4561,7 +4562,7 @@ package body Sem_Attr is
          ----------------------------
 
          procedure Check_Use_In_Test_Case (Prag : Node_Id) is
-            Ensures : constant Node_Id := Get_Ensures_From_CTC_Pragma (Prag);
+            Ensures : constant Node_Id := Test_Case_Arg (Prag, Name_Ensures);
             Expr    : Node_Id;
 
          begin
@@ -4984,269 +4985,373 @@ package body Sem_Attr is
       ------------
 
       when Attribute_Result => Result : declare
-         Post_Id : Entity_Id;
-         --  The entity of the _Postconditions procedure
+         procedure Check_Placement_In_Check (Prag : Node_Id);
+         --  Verify that attribute 'Result appears within pragma Check that
+         --  emulates a postcondition.
 
-         Prag : Node_Id;
-         --  During pre-analysis, Prag is the enclosing pragma node if any
-
-         Subp_Id : Entity_Id;
-         --  The entity of the enclosing subprogram
+         procedure Check_Placement_In_Contract_Cases (Prag : Node_Id);
+         --  Verify that attribute 'Result appears within a consequence of
+         --  pragma Contract_Cases.
 
-      begin
-         --  Find the proper enclosing scope
+         procedure Check_Placement_In_Test_Case (Prag : Node_Id);
+         --  Verify that attribute 'Result appears within the Ensures argument
+         --  of pragma Test_Case.
 
-         Post_Id := Current_Scope;
-         while Present (Post_Id) loop
+         function Is_Within
+           (Nod      : Node_Id;
+            Encl_Nod : Node_Id) return Boolean;
+         --  Subsidiary to Check_Placemenet_In_XXX_Case. Determine whether
+         --  arbitrary node Nod is within enclosing node Encl_Nod.
 
-            --  Skip generated loops
+         ------------------------------
+         -- Check_Placement_In_Check --
+         ------------------------------
 
-            if Ekind (Post_Id) = E_Loop then
-               Post_Id := Scope (Post_Id);
+         procedure Check_Placement_In_Check (Prag : Node_Id) is
+            Args : constant List_Id := Pragma_Argument_Associations (Prag);
+            Nam  : constant Name_Id := Chars (Get_Pragma_Arg (First (Args)));
 
-            --  Skip the special _Parent scope generated to capture references
-            --  to formals during the process of subprogram inlining.
+         begin
+            --  The "Name" argument of pragma Check denotes a postcondition
 
-            elsif Ekind (Post_Id) = E_Function
-              and then Chars (Post_Id) = Name_uParent
+            if Nam_In (Nam, Name_Post,
+                            Name_Postcondition,
+                            Name_Refined_Post)
             then
-               Post_Id := Scope (Post_Id);
+               null;
 
-            --  Otherwise this must be _Postconditions
+            --  Otherwise the placement of attribute 'Result is illegal
 
             else
-               exit;
+               Error_Attr
+                 ("% attribute can only appear in postcondition of function",
+                  P);
             end if;
-         end loop;
+         end Check_Placement_In_Check;
 
-         Subp_Id := Scope (Post_Id);
+         ---------------------------------------
+         -- Check_Placement_In_Contract_Cases --
+         ---------------------------------------
 
-         --  If the enclosing subprogram is always inlined, the enclosing
-         --  postcondition will not be propagated to the expanded call.
+         procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is
+            Args  : constant List_Id := Pragma_Argument_Associations (Prag);
+            Cases : constant Node_Id := Get_Pragma_Arg (First (Args));
+            CCase : Node_Id;
 
-         if not In_Spec_Expression
-           and then Has_Pragma_Inline_Always (Subp_Id)
-           and then Warn_On_Redundant_Constructs
-         then
-            Error_Msg_N
-              ("postconditions on inlined functions not enforced?r?", N);
-         end if;
+         begin
+            if Present (Component_Associations (Cases)) then
+               CCase := First (Component_Associations (Cases));
+               while Present (CCase) loop
+
+                  --  Guard against a malformed contract case. Detect whether
+                  --  attribute 'Result appears within the consequence of the
+                  --  current contract case.
+
+                  if Nkind (CCase) = N_Component_Association
+                    and then Is_Within (N, Expression (CCase))
+                  then
+                     return;
+                  end if;
 
-         --  If we are in the scope of a function and in Spec_Expression mode,
-         --  this is likely the prescan of the postcondition (or contract case,
-         --  or test case) pragma, and we just set the proper type. If there is
-         --  an error it will be caught when the real Analyze call is done.
+                  Next (CCase);
+               end loop;
+            end if;
 
-         if Ekind (Post_Id) = E_Function and then In_Spec_Expression then
+            --  Otherwise pragma Contract_Cases is either malformed in some
+            --  way or attribute 'Result does not appear within a consequence
+            --  expression.
 
-            --  Check OK prefix
+            Error_Attr ("% attribute misplaced inside contract cases", P);
+         end Check_Placement_In_Contract_Cases;
 
-            if Chars (Post_Id) /= Chars (P) then
-               Error_Msg_Name_1 := Name_Result;
-               Error_Msg_NE
-                 ("incorrect prefix for % attribute, expected &", P, Post_Id);
-               Error_Attr;
+         ----------------------------------
+         -- Check_Placement_In_Test_Case --
+         ----------------------------------
+
+         procedure Check_Placement_In_Test_Case (Prag : Node_Id) is
+         begin
+            --  Detect whether attribute 'Result appears within the "Ensures"
+            --  expression of pragma Test_Case.
+
+            if not Is_Within (N, Test_Case_Arg (Prag, Name_Ensures)) then
+               Error_Attr ("% attribute misplaced inside test case", P);
             end if;
+         end Check_Placement_In_Test_Case;
 
-            --  Check in postcondition, Test_Case or Contract_Cases of function
+         ---------------
+         -- Is_Within --
+         ---------------
 
-            Prag := N;
-            while Present (Prag)
-               and then not Nkind_In (Prag, N_Pragma,
-                                            N_Function_Specification,
-                                            N_Aspect_Specification,
-                                            N_Subprogram_Body)
-            loop
-               Prag := Parent (Prag);
-            end loop;
+         function Is_Within
+           (Nod      : Node_Id;
+            Encl_Nod : Node_Id) return Boolean
+         is
+            Par : Node_Id;
 
-            --  In ASIS mode, the aspect itself is analyzed, in addition to the
-            --  corresponding pragma. Do not issue errors when analyzing the
-            --  aspect.
+         begin
+            Par := Nod;
+            while Present (Par) loop
+               if Par = Encl_Nod then
+                  return True;
 
-            if Nkind (Prag) = N_Aspect_Specification then
-               null;
+               --  Prevent the search from going too far
 
-            --  Must have a pragma
+               elsif Is_Body_Or_Package_Declaration (Par) then
+                  exit;
+               end if;
 
-            elsif Nkind (Prag) /= N_Pragma then
-               Error_Attr
-                 ("% attribute can only appear in postcondition of function",
-                  P);
+               Par := Parent (Par);
+            end loop;
 
-            --  Processing depends on which pragma we have
+            return False;
+         end Is_Within;
 
-            else
-               case Get_Pragma_Id (Prag) is
-                  when Pragma_Test_Case =>
-                     declare
-                        Arg_Ens : constant Node_Id :=
-                                    Get_Ensures_From_CTC_Pragma (Prag);
-                        Arg     : Node_Id;
+         --  Local variables
 
-                     begin
-                        Arg := N;
-                        while Arg /= Prag and then Arg /= Arg_Ens loop
-                           Arg := Parent (Arg);
-                        end loop;
+         In_Post   : Boolean := False;
+         Prag      : Node_Id;
+         Prag_Id   : Pragma_Id;
+         Pref_Id   : Entity_Id;
+         Spec_Id   : Entity_Id;
+         Subp_Decl : Node_Id;
+         Subp_Id   : Entity_Id;
+         Subp_Spec : Node_Id;
 
-                        if Arg /= Arg_Ens then
-                           Error_Attr
-                             ("% attribute misplaced inside test case", P);
-                        end if;
-                     end;
+      --  Start of processing for Result
 
-                  when Pragma_Contract_Cases =>
-                     declare
-                        Aggr : constant Node_Id :=
-                          Expression (First
-                                        (Pragma_Argument_Associations (Prag)));
-                        Arg  : Node_Id;
+      begin
+         --  The attribute reference is a primary. If any expressions follow,
+         --  then the attribute reference is an indexable object. Transform the
+         --  attribute into an indexed component and analyze it.
 
-                     begin
-                        Arg := N;
-                        while Arg /= Prag
-                          and then Parent (Parent (Arg)) /= Aggr
-                        loop
-                           Arg := Parent (Arg);
-                        end loop;
+         if Present (E1) then
+            Rewrite (N,
+              Make_Indexed_Component (Loc,
+                Prefix      =>
+                  Make_Attribute_Reference (Loc,
+                    Prefix         => Relocate_Node (P),
+                    Attribute_Name => Name_Result),
+                Expressions => Expressions (N)));
+            Analyze (N);
+            return;
+         end if;
 
-                        --  At this point, Parent (Arg) should be a component
-                        --  association. Attribute Result is only allowed in
-                        --  the expression part of this association.
+         --  Traverse the parent chain to find the aspect or pragma where
+         --  attribute 'Result resides.
 
-                        if Nkind (Parent (Arg)) /= N_Component_Association
-                          or else Arg /= Expression (Parent (Arg))
-                        then
-                           Error_Attr
-                             ("% attribute misplaced inside contract cases",
-                              P);
-                        end if;
-                     end;
+         Prag := N;
+         while Present (Prag) loop
+            if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
+               exit;
 
-                  when Pragma_Postcondition | Pragma_Refined_Post =>
-                     null;
+            --  Prevent the search from going too far
 
-                     when others =>
-                        Error_Attr
-                          ("% attribute can only appear in postcondition "
-                           & "of function", P);
-               end case;
+            elsif Is_Body_Or_Package_Declaration (Prag) then
+               exit;
             end if;
 
-            --  The attribute reference is a primary. If expressions follow,
-            --  the attribute reference is really an indexable object, so
-            --  rewrite and analyze as an indexed component.
+            Prag := Parent (Prag);
+         end loop;
 
-            if Present (E1) then
-               Rewrite (N,
-                 Make_Indexed_Component (Loc,
-                   Prefix      =>
-                     Make_Attribute_Reference (Loc,
-                       Prefix         => Relocate_Node (Prefix (N)),
-                       Attribute_Name => Name_Result),
-                   Expressions => Expressions (N)));
-               Analyze (N);
+         --  Do not emit an error when preanalyzing an aspect for ASIS. If the
+         --  placement of attribute 'Result is illegal, the error is reported
+         --  when analyzing the corresponding pragma.
+
+         if ASIS_Mode and then Nkind (Prag) = N_Aspect_Specification then
+            null;
+
+         --  Attribute 'Result is allowed to appear only in postcondition-like
+         --  pragmas.
+
+         elsif Nkind (Prag) = N_Pragma then
+            Prag_Id := Get_Pragma_Id (Prag);
+
+            if Prag_Id = Pragma_Check then
+               Check_Placement_In_Check (Prag);
+
+            elsif Prag_Id = Pragma_Contract_Cases then
+               Check_Placement_In_Contract_Cases (Prag);
+
+            elsif Prag_Id = Pragma_Postcondition
+              or else Prag_Id = Pragma_Refined_Post
+            then
+               null;
+
+            elsif Prag_Id = Pragma_Test_Case then
+               Check_Placement_In_Test_Case (Prag);
+
+            else
+               Error_Attr
+                 ("% attribute can only appear in postcondition of function",
+                  P);
                return;
             end if;
 
-            Set_Etype (N, Etype (Post_Id));
+         --  Otherwise the placement of the attribute is illegal
 
-            --  If several functions with that name are visible, the intended
-            --  one is the current scope.
+         else
+            Error_Attr
+              ("% attribute can only appear in postcondition of function", P);
+            return;
+         end if;
 
-            if Is_Overloaded (P) then
-               Set_Entity (P, Post_Id);
-               Set_Is_Overloaded (P, False);
-            end if;
+         --  Attribute 'Result appears within a postcondition-like pragma. Find
+         --  the related subprogram subject to the pragma.
 
-         --  Check the legality of attribute 'Result when it appears inside
-         --  pragma Refined_Post. These specialized checks are required only
-         --  when code generation is disabled. In the general case pragma
-         --  Refined_Post is transformed into pragma Check by Process_PPCs
-         --  which in turn is relocated to procedure _Postconditions. From
-         --  then on the legality of 'Result is determined as usual.
+         if Nkind (Prag) = N_Aspect_Specification then
+            Subp_Decl := Parent (Prag);
+         else
+            Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
+         end if;
 
-         elsif not Expander_Active and then In_Refined_Post then
+         --  The pragma where attribute 'Result appears is associated with a
+         --  subprogram declaration or a body.
 
-            --  Routine _Postconditions has not been generated yet, the nearest
-            --  enclosing subprogram is denoted by the current scope.
+         if Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
+                                 N_Entry_Declaration,
+                                 N_Generic_Subprogram_Declaration,
+                                 N_Subprogram_Body,
+                                 N_Subprogram_Body_Stub,
+                                 N_Subprogram_Declaration)
+         then
+            Subp_Id := Defining_Entity (Subp_Decl);
 
-            if Ekind (Post_Id) /= E_Procedure
-              or else Chars (Post_Id) /= Name_uPostconditions
-            then
-               Subp_Id := Current_Scope;
+            --  Attribute 'Result is part of the _Postconditions procedure of
+            --  the related subprogram. Retrieve the related subprogram.
+
+            if Chars (Subp_Id) = Name_uPostconditions then
+               In_Post   := True;
+               Subp_Decl := Parent (Subp_Decl);
+               Subp_Id   := Scope (Subp_Id);
             end if;
 
-            --  The prefix denotes the nearest enclosing function
+            --  Retrieve the entity of the spec (if any)
 
-            if Is_Entity_Name (P)
-              and then Ekind (Entity (P)) = E_Function
-              and then Entity (P) = Subp_Id
+            if Nkind (Subp_Decl) = N_Subprogram_Body
+              and then Present (Corresponding_Spec (Subp_Decl))
             then
-               null;
+               Spec_Id := Corresponding_Spec (Subp_Decl);
 
-            --  Otherwise the use of 'Result is illegal
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+              and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+            then
+               Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
 
             else
-               Error_Msg_Name_2 := Chars (Subp_Id);
-               Error_Attr ("incorrect prefix for % attribute, expected %", P);
+               Spec_Id := Subp_Id;
             end if;
 
-            Set_Etype (N, Etype (Subp_Id));
+            --  When the subprogram is always inlined, the postcondition will
+            --  not be propagated to the expanded body.
 
-         --  Body case, where we must be inside a generated _Postconditions
-         --  procedure, and the prefix must be on the scope stack, or else the
-         --  attribute use is definitely misplaced. The postcondition itself
-         --  may have generated transient scopes, and is not necessarily the
-         --  current one.
+            if Warn_On_Redundant_Constructs
+              and then Has_Pragma_Inline_Always (Spec_Id)
+            then
+               Error_Msg_N
+                 ("postconditions on inlined functions not enforced?r?", P);
+            end if;
 
-         else
-            while Present (Post_Id)
-              and then Post_Id /= Standard_Standard
-            loop
-               if Chars (Post_Id) = Name_uPostconditions then
-                  exit;
-               else
-                  Post_Id := Scope (Post_Id);
+            --  Ensure that the prefix of attribute 'Result denotes the related
+            --  subprogram.
+
+            if Is_Entity_Name (P) then
+               Pref_Id := Entity (P);
+
+               --  When a subprogram with contract assertions is imported, it
+               --  is encapsulated in a wrapper. In this case the scope of the
+               --  wrapper denotes the original imported subprogram.
+
+               if Is_Imported (Pref_Id) then
+                  Pref_Id := Scope (Pref_Id);
                end if;
-            end loop;
 
-            Subp_Id := Scope (Post_Id);
+               if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then
 
-            if Chars (Post_Id) = Name_uPostconditions
-              and then Ekind (Subp_Id) = E_Function
-            then
-               --  Check OK prefix
+                  --  The prefix of attribute 'Result denotes the entity of
+                  --  some other unrelated function.
 
-               if Nkind_In (P, N_Identifier, N_Operator_Symbol)
-                 and then Chars (P) = Chars (Subp_Id)
-               then
-                  null;
+                  if Pref_Id /= Spec_Id then
+                     Subp_Spec := Parent (Spec_Id);
 
-               --  Within an instance, the prefix designates the local renaming
-               --  of the original generic.
+                     --  Attribute 'Result appears in a postcondition of a
+                     --  generic function that acts as a compilation unit:
 
-               elsif Is_Entity_Name (P)
-                 and then Ekind (Entity (P)) = E_Function
-                 and then Present (Alias (Entity (P)))
-                 and then Chars (Alias (Entity (P))) = Chars (Subp_Id)
-               then
-                  null;
+                     --    generic
+                     --    function Gen_Func return ...
+                     --      with Post => Gen_Func'Result ...;
+
+                     --  When the function is instantiated, the Chars field of
+                     --  attribute 'Result's prefix still denotes the generic
+                     --  function. Note that any preemptive transformation is
+                     --  impossible without a proper analysis. The structure of
+                     --  the anonymous wrapper package is as follows:
+
+                     --    package Anon_Gen_Pack is
+                     --       <subtypes and renamings>
+                     --       function Subp_Decl return ...;
+                     --       pragma Postcondition (Gen_Func'Result ...);
+                     --       function Gen_Func ... renames Subp_Decl;
+                     --    end Anon_Gen_Pack;
+
+                     --  Recognize this case and do not flag it as illegal
+
+                     if Nkind (Subp_Spec) = N_Function_Specification
+                       and then Present (Generic_Parent (Subp_Spec))
+                     then
+                        if Generic_Parent (Subp_Spec) = Pref_Id then
+                           null;
+
+                        elsif Ekind (Pref_Id) = E_Function
+                          and then Present (Alias (Pref_Id))
+                          and then Alias (Pref_Id) = Spec_Id
+                        then
+                           null;
+
+                        else
+                           Error_Msg_Name_2 := Chars (Spec_Id);
+                           Error_Attr
+                             ("incorrect prefix for % attribute, expected %",
+                              P);
+                        end if;
+
+                     --  Otherwise the context is not a function instantiation
+                     --  and the prefix is illegal
+
+                     else
+                        Error_Msg_Name_2 := Chars (Spec_Id);
+                        Error_Attr
+                          ("incorrect prefix for % attribute, expected %", P);
+                     end if;
+                  end if;
+
+               --  Otherwise the attribute's prefix denotes some other form of
+               --  a non-function subprogram.
 
                else
-                  Error_Msg_Name_2 := Chars (Subp_Id);
                   Error_Attr
-                    ("incorrect prefix for % attribute, expected %", P);
+                    ("% attribute can only appear in postcondition of "
+                     & "function", P);
                end if;
 
-               Rewrite (N, Make_Identifier (Sloc (N), Name_uResult));
+            --  Otherwise the prefix is illegal
+
+            else
+               Error_Msg_Name_2 := Chars (Spec_Id);
+               Error_Attr ("incorrect prefix for % attribute, expected %", P);
+            end if;
+
+            --  Attribute 'Result is part of the _Postconditions procedure of
+            --  the related subprogram. Rewrite the attribute as a reference to
+            --  the _Result formal parameter of _Postconditions.
+
+            if In_Post then
+               Rewrite (N, Make_Identifier (Loc, Name_uResult));
                Analyze_And_Resolve (N, Etype (Subp_Id));
 
+            --  Otherwise decorate the attribute
+
             else
-               Error_Attr
-                 ("% attribute can only appear in postcondition of function",
-                  P);
+               Set_Etype (N, Etype (Subp_Id));
             end if;
          end if;
       end Result;