[multiple changes]

2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for Aspect_Refined_Post in table
	Canonical_Aspect.
	* aspects.ads: Add an entry for Aspect_Refined_Post in tables
	Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
	Aspect_On_Body_Or_Stub_OK. Update the comment on the use of
	table Aspect_On_Body_Or_Stub_OK.
	* par-prag.adb: Add pragma Refined_Post to the list of pragmas
	that do not require special processing by the parser.
	* sem_attr.adb (Analyze_Attribute): Add special analysis for
	attributes 'Old and 'Result when code generation is disabled and
	they appear in aspect/pragma Refined_Post.
	(In_Refined_Post): New routine.
	* sem_ch6.adb (Analyze_Expression_Function): Move various
	aspects and/or pragmas that apply to an expression function to the
	corresponding spec or body.
	(Collect_Body_Postconditions): New routine.
	(Process_PPCs): Use routine Collect_Body_Postconditions
	to gather all postcondition pragmas.
	* sem_ch10.adb (Analyze_Proper_Body): Use routine
	Relocate_Pragmas_To_Body to move all source pragmas that follow
	a body stub to the proper body.
	(Move_Stub_Pragmas_To_Body): Removed.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Post.
	(Check_Aspect_At_Freeze_Point): Aspect
	Refined_Post does not need delayed processing at the freeze point.
	* sem_prag.adb: Add an entry for pragma Refined_Post in
	table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma
	Refined_Post. Update the processing of pragma Refined_Pre
	to use common routine Analyze_Refined_Pre_Post.
	(Analyze_Refined_Pre_Post): New routine.
	(Relocate_Pragmas_To_Body): New routine.
	* sem_prag.ads: Table Pragma_On_Stub_OK is now known as
	Pragma_On_Body_Or_Stub_OK. Update the comment on usage of
	table Pragma_On_Body_Or_Stub_OK.
	(Relocate_Pragmas_To_Body): New routine.
	* snames.ads-tmpl: Add new predefined name for Refined_Post. Add
	new Pragma_Id for Refined_Post.

2013-10-10  Robert Dewar  <dewar@adacore.com>

	* exp_ch3.adb (Expand_N_Variant_Part): Now null, expansion of
	last choice to others is moved to Freeze_Record_Type.
	* freeze.adb (Freeze_Record_Type): Expand last variant to others
	if necessary (moved here from Expand_N_Variant_Part

From-SVN: r203359

gcc/ada/ChangeLog

@@ -1,3 +1,52 @@
+2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add an entry for Aspect_Refined_Post in table
+	Canonical_Aspect.
+	* aspects.ads: Add an entry for Aspect_Refined_Post in tables
+	Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
+	Aspect_On_Body_Or_Stub_OK. Update the comment on the use of
+	table Aspect_On_Body_Or_Stub_OK.
+	* par-prag.adb: Add pragma Refined_Post to the list of pragmas
+	that do not require special processing by the parser.
+	* sem_attr.adb (Analyze_Attribute): Add special analysis for
+	attributes 'Old and 'Result when code generation is disabled and
+	they appear in aspect/pragma Refined_Post.
+	(In_Refined_Post): New routine.
+	* sem_ch6.adb (Analyze_Expression_Function): Move various
+	aspects and/or pragmas that apply to an expression function to the
+	corresponding spec or body.
+	(Collect_Body_Postconditions): New routine.
+	(Process_PPCs): Use routine Collect_Body_Postconditions
+	to gather all postcondition pragmas.
+	* sem_ch10.adb (Analyze_Proper_Body): Use routine
+	Relocate_Pragmas_To_Body to move all source pragmas that follow
+	a body stub to the proper body.
+	(Move_Stub_Pragmas_To_Body): Removed.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+	for aspect Refined_Post.
+	(Check_Aspect_At_Freeze_Point): Aspect
+	Refined_Post does not need delayed processing at the freeze point.
+	* sem_prag.adb: Add an entry for pragma Refined_Post in
+	table Sig_Flags.
+	(Analyze_Pragma): Add processing for pragma
+	Refined_Post. Update the processing of pragma Refined_Pre
+	to use common routine Analyze_Refined_Pre_Post.
+	(Analyze_Refined_Pre_Post): New routine.
+	(Relocate_Pragmas_To_Body): New routine.
+	* sem_prag.ads: Table Pragma_On_Stub_OK is now known as
+	Pragma_On_Body_Or_Stub_OK. Update the comment on usage of
+	table Pragma_On_Body_Or_Stub_OK.
+	(Relocate_Pragmas_To_Body): New routine.
+	* snames.ads-tmpl: Add new predefined name for Refined_Post. Add
+	new Pragma_Id for Refined_Post.
+
+2013-10-10  Robert Dewar  <dewar@adacore.com>
+
+	* exp_ch3.adb (Expand_N_Variant_Part): Now null, expansion of
+	last choice to others is moved to Freeze_Record_Type.
+	* freeze.adb (Freeze_Record_Type): Expand last variant to others
+	if necessary (moved here from Expand_N_Variant_Part
+
 2013-10-10  Robert Dewar  <dewar@adacore.com>
 
 	* lib-xref-spark_specific.adb, par-ch13.adb, sem_prag.adb, sem_prag.ads,

gcc/ada/aspects.adb

@@ -466,6 +466,7 @@ package body Aspects is
     Aspect_Pure_05                      => Aspect_Pure_05,
     Aspect_Pure_12                      => Aspect_Pure_12,
     Aspect_Pure_Function                => Aspect_Pure_Function,
+    Aspect_Refined_Post                 => Aspect_Refined_Post,
     Aspect_Refined_Pre                  => Aspect_Refined_Pre,
     Aspect_Remote_Access_Type           => Aspect_Remote_Access_Type,
     Aspect_Remote_Call_Interface        => Aspect_Remote_Call_Interface,

gcc/ada/aspects.ads

@@ -111,6 +111,7 @@ package Aspects is
       Aspect_Predicate,                     -- GNAT
       Aspect_Priority,
       Aspect_Read,
+      Aspect_Refined_Post,                  -- GNAT
       Aspect_Refined_Pre,                   -- GNAT
       Aspect_Relative_Deadline,
       Aspect_Scalar_Storage_Order,          -- GNAT
@@ -320,6 +321,7 @@ package Aspects is
       Aspect_Predicate               => Expression,
       Aspect_Priority                => Expression,
       Aspect_Read                    => Name,
+      Aspect_Refined_Post            => Expression,
       Aspect_Refined_Pre             => Expression,
       Aspect_Relative_Deadline       => Expression,
       Aspect_Scalar_Storage_Order    => Expression,
@@ -417,6 +419,7 @@ package Aspects is
       Aspect_Pure_12                      => Name_Pure_12,
       Aspect_Pure_Function                => Name_Pure_Function,
       Aspect_Read                         => Name_Read,
+      Aspect_Refined_Post                 => Name_Refined_Post,
       Aspect_Refined_Pre                  => Name_Refined_Pre,
       Aspect_Relative_Deadline            => Name_Relative_Deadline,
       Aspect_Remote_Access_Type           => Name_Remote_Access_Type,
@@ -639,6 +642,7 @@ package Aspects is
       Aspect_Convention                   => Never_Delay,
       Aspect_Dimension                    => Never_Delay,
       Aspect_Dimension_System             => Never_Delay,
+      Aspect_Refined_Post                 => Never_Delay,
       Aspect_Refined_Pre                  => Never_Delay,
       Aspect_SPARK_Mode                   => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
@@ -695,8 +699,12 @@ package Aspects is
    --    package P with SPARK_Mode ...;
    --    package body P with SPARK_Mode is ...;
 
+   --  The table should be synchronized with Pragma_On_Body_Or_Stub_OK in unit
+   --  Sem_Prag if the aspects below are implemented by a pragma.
+
    Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean :=
-     (Aspect_Refined_Pre                  => True,
+     (Aspect_Refined_Post                 => True,
+      Aspect_Refined_Pre                  => True,
       Aspect_SPARK_Mode                   => True,
       Aspect_Warnings                     => True,
       others                              => False);

gcc/ada/exp_ch3.adb

@@ -5846,31 +5846,18 @@ package body Exp_Ch3 is
    -- Expand_N_Variant_Part --
    ---------------------------
 
+   --  Note: this procedure no longer has any effect. It used to be that we
+   --  would replace the choices in the last variant by a when others, and
+   --  also expanded static predicates in variant choices here, but both of
+   --  those activities were being done too early, since we can't check the
+   --  choices until the statically predicated subtypes are frozen, which can
+   --  happen as late as the free point of the record, and we can't change the
+   --  last choice to an others before checking the choices, which is now done
+   --  at the freeze point of the record.
+
    procedure Expand_N_Variant_Part (N : Node_Id) is
-      Last_Var    : constant Node_Id := Last_Non_Pragma (Variants (N));
-      Others_Node : Node_Id;
-
    begin
-      --  If the last variant does not contain the Others choice, replace it
+      null;
-      --  with an N_Others_Choice node since Gigi always wants an Others. Note
-      --  that we do not bother to call Analyze on the modified variant part,
-      --  since its only effect would be to compute the Others_Discrete_Choices
-      --  node laboriously, and of course we already know the list of choices
-      --  corresponding to the others choice (it's the list we're replacing!)
-
-      if Nkind (First (Discrete_Choices (Last_Var))) /= N_Others_Choice then
-         Others_Node := Make_Others_Choice (Sloc (Last_Var));
-         Set_Others_Discrete_Choices
-           (Others_Node, Discrete_Choices (Last_Var));
-         Set_Discrete_Choices (Last_Var, New_List (Others_Node));
-      end if;
-
-      --  We have one more expansion activity, which is to deal with static
-      --  predicates in the variant choices. But we have to defer that to
-      --  the freeze point, because the statically predicated subtype won't
-      --  be fully processed till then, so this expansion activity is carried
-      --  out in Freeze_Record_Type.
-
    end Expand_N_Variant_Part;
 
    ---------------------------------

gcc/ada/freeze.adb

@@ -2748,12 +2748,38 @@ package body Freeze is
                end if;
             end if;
 
-            --  If we have a variant part, check choices
+            --  Case of variant part present
 
             if Present (C) and then Present (Variant_Part (C)) then
                V := Variant_Part (C);
+
+               --  Check choices
+
                Check_Choices
                  (V, Variants (V), Etype (Name (V)), Others_Present);
+
+               --  If the last variant does not contain the Others choice,
+               --  replace it with an N_Others_Choice node since Gigi always
+               --  wants an Others. Note that we do not bother to call Analyze
+               --  on the modified variant part, since its only effect would be
+               --  to compute the Others_Discrete_Choices node laboriously, and
+               --  of course we already know the list of choices corresponding
+               --  to the others choice (it's the list we're replacing!)
+
+               declare
+                  Last_Var    : constant Node_Id :=
+                                  Last_Non_Pragma (Variants (V));
+                  Others_Node : Node_Id;
+               begin
+                  if Nkind (First (Discrete_Choices (Last_Var))) /=
+                                                            N_Others_Choice
+                  then
+                     Others_Node := Make_Others_Choice (Sloc (Last_Var));
+                     Set_Others_Discrete_Choices
+                       (Others_Node, Discrete_Choices (Last_Var));
+                     Set_Discrete_Choices (Last_Var, New_List (Others_Node));
+                  end if;
+               end;
             end if;
          end Check_Variant_Part;
       end Freeze_Record_Type;

gcc/ada/par-prag.adb

@@ -1250,6 +1250,7 @@ begin
            Pragma_Pure_12                        |
            Pragma_Pure_Function                  |
            Pragma_Queuing_Policy                 |
+           Pragma_Refined_Post                   |
            Pragma_Refined_Pre                    |
            Pragma_Relative_Deadline              |
            Pragma_Remote_Access_Type             |

gcc/ada/sem_attr.adb

@@ -303,10 +303,6 @@ package body Sem_Attr is
       --  Verify that prefix of attribute N is a float type and that
       --  two attribute expressions are present
 
-      procedure Legal_Formal_Attribute;
-      --  Common processing for attributes Definite and Has_Discriminants.
-      --  Checks that prefix is generic indefinite formal type.
-
       procedure Check_SPARK_Restriction_On_Attribute;
       --  Issue an error in formal mode because attribute N is allowed
 
@@ -377,6 +373,14 @@ package body Sem_Attr is
       pragma No_Return (Error_Attr);
       --  Like Error_Attr, but error is posted at the start of the prefix
 
+      function In_Refined_Post return Boolean;
+      --  Determine whether the current attribute appears in pragma
+      --  Refined_Post.
+
+      procedure Legal_Formal_Attribute;
+      --  Common processing for attributes Definite and Has_Discriminants.
+      --  Checks that prefix is generic indefinite formal type.
+
       procedure Standard_Attribute (Val : Int);
       --  Used to process attributes whose prefix is package Standard which
       --  yield values of type Universal_Integer. The attribute reference
@@ -1927,6 +1931,60 @@ package body Sem_Attr is
          Error_Attr;
       end Error_Attr_P;
 
+      ---------------------
+      -- In_Refined_Post --
+      ---------------------
+
+      function In_Refined_Post return Boolean is
+         function Is_Refined_Post (Prag : Node_Id) return Boolean;
+         --  Determine whether Prag denotes one of the incarnations of pragma
+         --  Refined_Post (either as is or pragma Check (Refined_Post, ...).
+
+         ---------------------
+         -- Is_Refined_Post --
+         ---------------------
+
+         function Is_Refined_Post (Prag : Node_Id) return Boolean is
+            Args : constant List_Id := Pragma_Argument_Associations (Prag);
+            Nam  : constant Name_Id := Pragma_Name (Prag);
+
+         begin
+            if Nam = Name_Refined_Post then
+               return True;
+
+            elsif Nam = Name_Check then
+               pragma Assert (Present (Args));
+
+               return Chars (Expression (First (Args))) = Name_Refined_Post;
+            end if;
+
+            return False;
+         end Is_Refined_Post;
+
+         --  Local variables
+
+         Stmt : Node_Id;
+
+      --  Start of processing for In_Refined_Post
+
+      begin
+         Stmt := Parent (N);
+         while Present (Stmt) loop
+            if Nkind (Stmt) = N_Pragma and then Is_Refined_Post (Stmt) then
+               return True;
+
+            --  Prevent the search from going too far
+
+            elsif Is_Body_Or_Package_Declaration (Stmt) then
+               exit;
+            end if;
+
+            Stmt := Parent (Stmt);
+         end loop;
+
+         return False;
+      end In_Refined_Post;
+
       ----------------------------
       -- Legal_Formal_Attribute --
       ----------------------------
@@ -4281,7 +4339,32 @@ package body Sem_Attr is
                Error_Attr ("% attribute can only appear in postcondition", P);
             end if;
 
-         --  Body case, where we must be inside a generated _Postcondition
+         --  Check the legality of attribute 'Old 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 'Old is determined as usual.
+
+         elsif not Expander_Active and then In_Refined_Post then
+            Preanalyze_And_Resolve (P);
+            P_Type := Etype (P);
+            Set_Etype (N, P_Type);
+
+            if Is_Limited_Type (P_Type) then
+               Error_Attr ("attribute % cannot apply to limited objects", P);
+            end if;
+
+            if Is_Entity_Name (P)
+              and then Is_Constant_Object (Entity (P))
+            then
+               Error_Msg_N
+                 ("??attribute Old applied to constant has no effect", P);
+            end if;
+
+            return;
+
+         --  Body case, where we must be inside a generated _Postconditions
          --  procedure, or else the attribute use is definitely misplaced. The
          --  postcondition itself may have generated transient scopes, and is
          --  not necessarily the current one.
@@ -4302,8 +4385,8 @@ package body Sem_Attr is
 
          --  If the attribute reference is generated for a Requires clause,
          --  then no expressions follow. Otherwise it is a primary, in which
-         --  case, if expressions follow, the attribute reference must be
+         --  case, if expressions follow, the attribute reference must be an
-         --  an indexable object, so rewrite the node accordingly.
+         --  indexable object, so rewrite the node accordingly.
 
          if Present (E1) then
             Rewrite (N,
@@ -4320,8 +4403,8 @@ package body Sem_Attr is
 
          Check_E0;
 
-         --  Prefix has not been analyzed yet, and its full analysis will
+         --  Prefix has not been analyzed yet, and its full analysis will take
-         --  take place during expansion (see below).
+         --  place during expansion (see below).
 
          Preanalyze_And_Resolve (P);
          P_Type := Etype (P);
@@ -4725,7 +4808,32 @@ package body Sem_Attr is
                Set_Is_Overloaded (P, False);
             end if;
 
-         --  Body case, where we must be inside a generated _Postcondition
+         --  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.
+
+         elsif not Expander_Active and then In_Refined_Post then
+            PS := Current_Scope;
+
+            --  The prefix denotes the proper related function
+
+            if Is_Entity_Name (P)
+              and then Ekind (Entity (P)) = E_Function
+              and then Entity (P) = PS
+            then
+               null;
+
+            else
+               Error_Msg_Name_2 := Chars (PS);
+               Error_Attr ("incorrect prefix for % attribute, expected %", P);
+            end if;
+
+            Set_Etype (N, Etype (PS));
+
+         --  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
@@ -4763,9 +4871,9 @@ package body Sem_Attr is
                   null;
 
                else
-                  Error_Msg_NE
+                  Error_Msg_Name_2 := Chars (PS);
-                    ("incorrect prefix for % attribute, expected &", P, PS);
+                  Error_Attr
-                  Error_Attr;
+                    ("incorrect prefix for % attribute, expected %", P);
                end if;
 
                Rewrite (N, Make_Identifier (Sloc (N), Name_uResult));

gcc/ada/sem_ch10.adb

@@ -1596,85 +1596,12 @@ package body Sem_Ch10 is
       Subunit_Name : constant Unit_Name_Type := Get_Unit_Name (N);
       Unum         : Unit_Number_Type;
 
-      procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id);
-      --  Relocate all pragmas that apply to a subprogram body stub to the
-      --  declarations of proper body Bod.
-      --  Should we do this for the reamining body stub kinds???
-
       procedure Optional_Subunit;
       --  This procedure is called when the main unit is a stub, or when we
       --  are not generating code. In such a case, we analyze the subunit if
       --  present, which is user-friendly and in fact required for ASIS, but
       --  we don't complain if the subunit is missing.
 
-      -------------------------------
-      -- Move_Stub_Pragmas_To_Body --
-      -------------------------------
-
-      procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id) is
-         procedure Move_Pragma (Prag : Node_Id);
-         --  Relocate one pragma to the declarations of Bod
-
-         -----------------
-         -- Move_Pragma --
-         -----------------
-
-         procedure Move_Pragma (Prag : Node_Id) is
-            Decls : List_Id := Declarations (Bod);
-
-         begin
-            if No (Decls) then
-               Decls := New_List;
-               Set_Declarations (Bod, Decls);
-            end if;
-
-            --  Unhook the pragma from its current list
-
-            Remove (Prag);
-            Prepend (Prag, Decls);
-         end Move_Pragma;
-
-         --  Local variables
-
-         Next_Stmt : Node_Id;
-         Stmt      : Node_Id;
-
-      --  Start of processing for Move_Stub_Pragmas_To_Body
-
-      begin
-         pragma Assert (Nkind (N) = N_Subprogram_Body_Stub);
-
-         --  Perform a bit of a lookahead - peek at any subsequent source
-         --  pragmas while skipping internally generated code.
-
-         Stmt := Next (N);
-         while Present (Stmt) loop
-            Next_Stmt := Next (Stmt);
-
-            --  Move a source pragma that applies to a subprogram stub to the
-            --  declarations of the proper body.
-
-            if Comes_From_Source (Stmt)
-              and then Nkind (Stmt) = N_Pragma
-              and then Pragma_On_Stub_OK (Get_Pragma_Id (Stmt))
-            then
-               Move_Pragma (Stmt);
-
-            --  Skip internally generated code
-
-            elsif not Comes_From_Source (Stmt) then
-               null;
-
-            --  No valid pragmas are available for relocation
-
-            else
-               exit;
-            end if;
-
-            Stmt := Next_Stmt;
-         end loop;
-      end Move_Stub_Pragmas_To_Body;
-
       ----------------------
       -- Optional_Subunit --
       ----------------------
@@ -1932,11 +1859,11 @@ package body Sem_Ch10 is
 
                      Move_Or_Merge_Aspects (From => N, To => Prop_Body);
 
-                     --  Propagate all source pragmas associated with a
+                     --  Move all source pragmas that follow the body stub and
-                     --  subprogram body stub to the proper body.
+                     --  apply to it to the declarations of the proper body.
 
                      if Nkind (N) = N_Subprogram_Body_Stub then
-                        Move_Stub_Pragmas_To_Body (Prop_Body);
+                        Relocate_Pragmas_To_Body (N, Target_Body => Prop_Body);
                      end if;
 
                      --  Analyze the unit if semantics active

gcc/ada/sem_ch13.adb

@@ -1928,6 +1928,15 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_SPARK_Mode);
 
+               --  Refined_Post
+
+               when Aspect_Refined_Post =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Refined_Post);
+
                --  Refined_Pre
 
                when Aspect_Refined_Pre =>
@@ -7788,6 +7797,7 @@ package body Sem_Ch13 is
               Aspect_Postcondition        |
               Aspect_Pre                  |
               Aspect_Precondition         |
+              Aspect_Refined_Post         |
               Aspect_Refined_Pre          |
               Aspect_SPARK_Mode           |
               Aspect_Test_Case            =>

gcc/ada/sem_ch6.adb

@@ -349,15 +349,25 @@ package body Sem_Ch6 is
             Make_Handled_Sequence_Of_Statements (LocX,
               Statements => New_List (Ret)));
 
-      if Present (Prev) and then Ekind (Prev) = E_Generic_Function then
-
       --  If the expression completes a generic subprogram, we must create a
       --  separate node for the body, because at instantiation the original
       --  node of the generic copy must be a generic subprogram body, and
       --  cannot be a expression function. Otherwise we just rewrite the
       --  expression with the non-generic body.
 
+      if Present (Prev) and then Ekind (Prev) = E_Generic_Function then
          Insert_After (N, New_Body);
+
+         --  Propagate any aspects or pragmas that apply to the expression
+         --  function to the proper body when the expression function acts
+         --  as a completion.
+
+         if Has_Aspects (N) then
+            Move_Aspects (N, To => New_Body);
+         end if;
+
+         Relocate_Pragmas_To_Body (New_Body);
+
          Rewrite (N, Make_Null_Statement (Loc));
          Set_Has_Completion (Prev, False);
          Analyze (N);
@@ -371,6 +381,12 @@ package body Sem_Ch6 is
 
          Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
          Rewrite (N, New_Body);
+
+         --  Propagate any pragmas that apply to the expression function to the
+         --  proper body when the expression function acts as a completion.
+         --  Aspects are automatically transfered because of node rewriting.
+
+         Relocate_Pragmas_To_Body (N);
          Analyze (N);
 
          --  Prev is the previous entity with the same name, but it is can
@@ -11274,6 +11290,11 @@ package body Sem_Ch6 is
       --  under the same visibility conditions as for other invariant checks,
       --  the type invariant must be applied to the returned value.
 
+      procedure Collect_Body_Postconditions (Post_Nam : Name_Id);
+      --  Examine the declarations of the body, looking for pragmas with name
+      --  Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or
+      --  Name_Refined_Post. Chain any relevant postconditions to Plist.
+
       function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
       --  Prag contains an analyzed precondition or postcondition pragma. This
       --  function copies the pragma, changes it to the corresponding Check
@@ -11365,6 +11386,60 @@ package body Sem_Ch6 is
          end if;
       end Check_Access_Invariants;
 
+      ---------------------------------
+      -- Collect_Body_Postconditions --
+      ---------------------------------
+
+      procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is
+         Next_Prag : Node_Id;
+
+      begin
+         pragma Assert
+           (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post));
+
+         Prag := First (Declarations (N));
+         while Present (Prag) loop
+            Next_Prag := Next (Prag);
+
+            if Nkind (Prag) = N_Pragma then
+
+               --  Capture postcondition pragmas
+
+               if Pragma_Name (Prag) = Post_Nam then
+                  Analyze (Prag);
+
+                  --  All Refined_Post pragmas must be relocated to the body
+                  --  of the generated _Postconditions routine, otherwise they
+                  --  will be duplicated twice - once in the declarations of
+                  --  the body and once in _Postconditions.
+
+                  if Pragma_Name (Prag) = Name_Refined_Post then
+                     Remove (Prag);
+                  end if;
+
+                  --  If expansion is disabled, as in a generic unit, save
+                  --  pragma for later expansion.
+
+                  if not Expander_Active then
+                     Prepend (Grab_PPC, Declarations (N));
+                  else
+                     Append_Enabled_Item (Grab_PPC, Plist);
+                  end if;
+               end if;
+
+            --  Skip internally generated code
+
+            elsif not Comes_From_Source (Prag) then
+               null;
+
+            else
+               exit;
+            end if;
+
+            Prag := Next_Prag;
+         end loop;
+      end Collect_Body_Postconditions;
+
       --------------
       -- Grab_PPC --
       --------------
@@ -11791,6 +11866,8 @@ package body Sem_Ch6 is
 
       --     procedure _postconditions [(_Result : resulttype)] is
       --     begin
+      --        pragma Check (Refined_Post, condition);
+      --        pragma Check (Refined_Post, condition);
       --        pragma Check (Postcondition, condition [,message]);
       --        pragma Check (Postcondition, condition [,message]);
       --        ...
@@ -11801,43 +11878,8 @@ package body Sem_Ch6 is
 
       --  First we deal with the postconditions in the body
 
-      if Is_Non_Empty_List (Declarations (N)) then
+      Collect_Body_Postconditions (Name_Refined_Post);
-
+      Collect_Body_Postconditions (Name_Postcondition);
-         --  Loop through declarations
-
-         Prag := First (Declarations (N));
-         while Present (Prag) loop
-            if Nkind (Prag) = N_Pragma then
-
-               --  Capture postcondition pragmas
-
-               if Pragma_Name (Prag) = Name_Postcondition then
-                  Analyze (Prag);
-
-                  --  If expansion is disabled, as in a generic unit, save
-                  --  pragma for later expansion.
-
-                  if not Expander_Active then
-                     Prepend (Grab_PPC, Declarations (N));
-                  else
-                     Append_Enabled_Item (Grab_PPC, Plist);
-                  end if;
-               end if;
-
-               Next (Prag);
-
-            --  Not a pragma, if comes from source, then end scan
-
-            elsif Comes_From_Source (Prag) then
-               exit;
-
-            --  Skip stuff not coming from source
-
-            else
-               Next (Prag);
-            end if;
-         end loop;
-      end if;
 
       --  Now deal with any postconditions from the spec
 

gcc/ada/sem_prag.adb

@@ -1922,6 +1922,16 @@ package body Sem_Prag is
       --  In Ada 95 or 05 mode, these are implementation defined pragmas, so
       --  should be caught by the No_Implementation_Pragmas restriction.
 
+      procedure Analyze_Refined_Pre_Post
+        (Body_Decl : out Node_Id;
+         Spec_Id   : out Entity_Id;
+         Legal     : out Boolean);
+      --  Subsidiary routine to the analysis of pragmas Refined_Pre and
+      --  Refined_Post. Body_Decl is the declaration of the subprogram body
+      --  [stub] subject to the pragma. Spec_Id is the corresponding spec of
+      --  the subprogram body [stub]. Flag Legal denotes whether the pragma
+      --  passes all legality rules.
+
       procedure Check_Ada_83_Warning;
       --  Issues a warning message for the current pragma if operating in Ada
       --  83 mode (used for language pragmas that are not a standard part of
@@ -2448,6 +2458,129 @@ package body Sem_Prag is
          end if;
       end Ada_2012_Pragma;
 
+      ------------------------------
+      -- Analyze_Refined_Pre_Post --
+      ------------------------------
+
+      procedure Analyze_Refined_Pre_Post
+        (Body_Decl : out Node_Id;
+         Spec_Id   : out Entity_Id;
+         Legal     : out Boolean)
+      is
+         Pack_Spec : Node_Id;
+         Spec_Decl : Node_Id;
+         Stmt      : Node_Id;
+
+      begin
+         --  Assume that the pragma is illegal
+
+         Body_Decl := Parent (N);
+         Spec_Id   := Empty;
+         Legal     := False;
+
+         GNAT_Pragma;
+         Check_Arg_Count (1);
+         Check_No_Identifiers;
+
+         --  Verify the placement of the pragma and check for duplicates
+
+         Stmt := Prev (N);
+         while Present (Stmt) loop
+
+            --  Skip prior pragmas, but check for duplicates
+
+            if Nkind (Stmt) = N_Pragma then
+               if Pragma_Name (Stmt) = Pname then
+                  Error_Msg_Name_1 := Pname;
+                  Error_Msg_Sloc   := Sloc (Stmt);
+                  Error_Msg_N ("pragma % duplicates pragma declared #", N);
+               end if;
+
+            --  Emit an error when the pragma applies to an expression function
+            --  that does not act as a completion.
+
+            elsif Nkind (Stmt) = N_Subprogram_Declaration
+              and then Nkind (Original_Node (Stmt)) = N_Expression_Function
+              and then not
+                Has_Completion (Defining_Unit_Name (Specification (Stmt)))
+            then
+               Error_Pragma
+                 ("pragma % cannot apply to a stand alone expression "
+                  & "function");
+               return;
+
+            --  The pragma applies to a subprogram body stub
+
+            elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
+               Body_Decl := Stmt;
+               exit;
+
+            --  Skip internally generated code
+
+            elsif not Comes_From_Source (Stmt) then
+               null;
+
+            --  The pragma does not apply to a legal construct, issue an error
+            --  and stop the analysis.
+
+            else
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Stmt := Prev (Stmt);
+         end loop;
+
+         --  Pragma Refined_Pre/Post must apply to a subprogram body [stub]
+
+         if not Nkind_In (Body_Decl, N_Subprogram_Body,
+                                     N_Subprogram_Body_Stub)
+         then
+            Pragma_Misplaced;
+            return;
+         end if;
+
+         --  The body [stub] must not act as a spec, in other words it has to
+         --  be paired with a corresponding spec.
+
+         if Nkind (Body_Decl) = N_Subprogram_Body then
+            Spec_Id := Corresponding_Spec (Body_Decl);
+         else
+            Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+         end if;
+
+         if No (Spec_Id) then
+            Error_Pragma ("pragma % cannot apply to a stand alone body");
+            return;
+         end if;
+
+         --  Refined_Pre/Post may only apply to the body [stub] of a subprogram
+         --  declared in the visible part of a package. Retrieve the context of
+         --  the subprogram declaration.
+
+         Spec_Decl := Parent (Parent (Spec_Id));
+
+         pragma Assert
+           (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration,
+                                 N_Generic_Subprogram_Declaration,
+                                 N_Subprogram_Declaration));
+
+         Pack_Spec := Parent (Spec_Decl);
+
+         if Nkind (Pack_Spec) /= N_Package_Specification
+           or else List_Containing (Spec_Decl) /=
+                     Visible_Declarations (Pack_Spec)
+         then
+            Error_Pragma
+              ("pragma % must apply to the body of a visible subprogram");
+            return;
+         end if;
+
+         --  If we get here, the placement and legality of the pragma is OK
+
+         Legal := True;
+      end Analyze_Refined_Pre_Post;
+
       --------------------------
       -- Check_Ada_83_Warning --
       --------------------------
@@ -15933,6 +16066,33 @@ package body Sem_Prag is
          when Pragma_Rational =>
             Set_Rational_Profile;
 
+         ------------------
+         -- Refined_Post --
+         ------------------
+
+         --  pragma Refined_Post (boolean_EXPRESSION);
+
+         when Pragma_Refined_Post => Refined_Post : declare
+            Body_Decl : Node_Id;
+            Legal     : Boolean;
+            Spec_Id   : Entity_Id;
+
+         begin
+            --  Verify the legal placement of the pragma. The pragma is left
+            --  intentionally semi-analyzed. Process_PPCs does the remaining
+            --  analysis of the expression when Refined_Post is converted into
+            --  pragma Check.
+
+            Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
+
+            --  Analyze the expression when code generation is disabled because
+            --  the contract of the related subprogram will never be processed.
+
+            if Legal and then not Expander_Active then
+               Analyze_And_Resolve (Get_Pragma_Arg (Arg1), Standard_Boolean);
+            end if;
+         end Refined_Post;
+
          -----------------
          -- Refined_Pre --
          -----------------
@@ -15940,111 +16100,17 @@ package body Sem_Prag is
          --  pragma Refined_Pre (boolean_EXPRESSION);
 
          when Pragma_Refined_Pre => Refined_Pre : declare
-            Body_Decl : Node_Id := Parent (N);
+            Body_Decl : Node_Id;
-            Pack_Spec : Node_Id;
+            Legal     : Boolean;
             Restore   : Boolean := False;
-            Spec_Decl : Node_Id;
             Spec_Id   : Entity_Id;
-            Stmt      : Node_Id;
 
          begin
-            GNAT_Pragma;
+            Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
-            Check_Arg_Count (1);
-            Check_No_Identifiers;
 
-            --  Verify the placement of the pragma and check for duplicates
+            if Legal then
-
+               pragma Assert (Present (Body_Decl));
-            Stmt := Prev (N);
+               pragma Assert (Present (Spec_Id));
-            while Present (Stmt) loop
-
-               --  Skip prior pragmas, but check for duplicates
-
-               if Nkind (Stmt) = N_Pragma then
-                  if Pragma_Name (Stmt) = Pname then
-                     Error_Msg_Name_1 := Pname;
-                     Error_Msg_Sloc   := Sloc (Stmt);
-                     Error_Msg_N ("pragma % duplicates pragma declared #", N);
-                  end if;
-
-               --  The pragma applies to a subprogram body stub
-
-               elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
-                  Body_Decl := Stmt;
-                  exit;
-
-               --  The pragma applies to an expression function that does not
-               --  act as a completion of a previous function declaration.
-
-               elsif Nkind (Stmt) = N_Subprogram_Declaration
-                 and then Nkind (Original_Node (Stmt)) = N_Expression_Function
-                 and then not
-                   Has_Completion (Defining_Unit_Name (Specification (Stmt)))
-               then
-                  Error_Pragma ("pragma % cannot apply to a stand alone body");
-                  return;
-
-               --  Skip internally generated code
-
-               elsif not Comes_From_Source (Stmt) then
-                  null;
-
-               --  The pragma does not apply to a legal construct, issue an
-               --  error and stop the analysis.
-
-               else
-                  Pragma_Misplaced;
-                  return;
-               end if;
-
-               Stmt := Prev (Stmt);
-            end loop;
-
-            --  Pragma Refined_Pre must apply to a subprogram body [stub]
-
-            if not Nkind_In (Body_Decl, N_Subprogram_Body,
-                                        N_Subprogram_Body_Stub)
-            then
-               Pragma_Misplaced;
-               return;
-            end if;
-
-            --  The body [stub] must not act as a spec
-
-            if Nkind (Body_Decl) = N_Subprogram_Body then
-               Spec_Id := Corresponding_Spec (Body_Decl);
-            else
-               Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
-            end if;
-
-            if No (Spec_Id) then
-               Error_Pragma ("pragma % cannot apply to a stand alone body");
-               return;
-            end if;
-
-            --  Refined_Pre may only apply to the body [stub] of a subprogram
-            --  declared in the visible part of a package. Retrieve the context
-            --  of the subprogram declaration.
-
-            Spec_Decl := Parent (Parent (Spec_Id));
-
-            pragma Assert
-              (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration,
-                                    N_Generic_Subprogram_Declaration,
-                                    N_Subprogram_Declaration));
-
-            Pack_Spec := Parent (Spec_Decl);
-
-            if Nkind (Pack_Spec) /= N_Package_Specification
-              or else List_Containing (Spec_Decl) /=
-                        Visible_Declarations (Pack_Spec)
-            then
-               Error_Pragma
-                 ("pragma % must apply to the body of a visible subprogram");
-            end if;
-
-            --  When the pragma applies to a subprogram stub without a proper
-            --  body, we have to restore the visibility of the stub and its
-            --  formals to perform analysis.
 
                if Nkind (Body_Decl) = N_Subprogram_Body_Stub
                  and then No (Library_Unit (Body_Decl))
@@ -16055,8 +16121,8 @@ package body Sem_Prag is
                   Install_Formals (Spec_Id);
                end if;
 
-            --  Convert pragma Refined_Pre into pragma Check. The analysis of
+               --  Convert pragma Refined_Pre into pragma Check. The analysis
-            --  the generated pragma will take care of the expression.
+               --  of the generated pragma will take care of the expression.
 
                Rewrite (N,
                  Make_Pragma (Loc,
@@ -16073,6 +16139,7 @@ package body Sem_Prag is
                if Restore then
                   Pop_Scope;
                end if;
+            end if;
          end Refined_Pre;
 
          -----------------------
@@ -19158,6 +19225,7 @@ package body Sem_Prag is
       Pragma_Queuing_Policy                 => -1,
       Pragma_Rational                       => -1,
       Pragma_Ravenscar                      => -1,
+      Pragma_Refined_Post                   => -1,
       Pragma_Refined_Pre                    => -1,
       Pragma_Relative_Deadline              => -1,
       Pragma_Remote_Access_Type             => -1,
@@ -19593,6 +19661,116 @@ package body Sem_Prag is
 
    end Process_Compilation_Unit_Pragmas;
 
+   ------------------------------
+   -- Relocate_Pragmas_To_Body --
+   ------------------------------
+
+   procedure Relocate_Pragmas_To_Body
+     (Subp_Body   : Node_Id;
+      Target_Body : Node_Id := Empty)
+   is
+      procedure Relocate_Pragma (Prag : Node_Id);
+      --  Remove a single pragma from its current list and add it to the
+      --  declarations of the proper body (either Subp_Body or Target_Body).
+
+      ---------------------
+      -- Relocate_Pragma --
+      ---------------------
+
+      procedure Relocate_Pragma (Prag : Node_Id) is
+         Decls  : List_Id;
+         Target : Node_Id;
+
+      begin
+         --  When subprogram stubs or expression functions are involves, the
+         --  destination declaration list belongs to the proper body.
+
+         if Present (Target_Body) then
+            Target := Target_Body;
+         else
+            Target := Subp_Body;
+         end if;
+
+         Decls := Declarations (Target);
+
+         if No (Decls) then
+            Decls := New_List;
+            Set_Declarations (Target, Decls);
+         end if;
+
+         --  Unhook the pragma from its current list
+
+         Remove  (Prag);
+         Prepend (Prag, Decls);
+      end Relocate_Pragma;
+
+      --  Local variables
+
+      Body_Id   : constant Entity_Id :=
+                    Defining_Unit_Name (Specification (Subp_Body));
+      Next_Stmt : Node_Id;
+      Stmt      : Node_Id;
+
+   --  Start of processing for Relocate_Pragmas_To_Body
+
+   begin
+      --  Do not process a body that comes from a separate unit as no construct
+      --  can possibly follow it.
+
+      if not Is_List_Member (Subp_Body) then
+         return;
+
+      --  Do not relocate pragmas that follow a stub if the stub does not have
+      --  a proper body.
+
+      elsif Nkind (Subp_Body) = N_Subprogram_Body_Stub
+        and then No (Target_Body)
+      then
+         return;
+
+      --  Do not process internally generated routine _Postconditions
+
+      elsif Ekind (Body_Id) = E_Procedure
+        and then Chars (Body_Id) = Name_uPostconditions
+      then
+         return;
+      end if;
+
+      --  Look at what is following the body. We are interested in certain kind
+      --  of pragmas (either from source or byproducts of expansion) that can
+      --  apply to a body [stub].
+
+      Stmt := Next (Subp_Body);
+      while Present (Stmt) loop
+
+         --  Preserve the following statement for iteration purposes due to a
+         --  possible relocation of a pragma.
+
+         Next_Stmt := Next (Stmt);
+
+         --  Move a candidate pragma following the body to the declarations of
+         --  the body.
+
+         if Nkind (Stmt) = N_Pragma
+           and then Pragma_On_Body_Or_Stub_OK (Get_Pragma_Id (Stmt))
+         then
+            Relocate_Pragma (Stmt);
+
+         --  Skip internally generated code
+
+         elsif not Comes_From_Source (Stmt) then
+            null;
+
+         --  No candidate pragmas are available for relocation
+
+         else
+            exit;
+         end if;
+
+         Stmt := Next_Stmt;
+      end loop;
+   end Relocate_Pragmas_To_Body;
+
    ----------------------------
    -- Rewrite_Assertion_Kind --
    ----------------------------

gcc/ada/sem_prag.ads

@@ -33,11 +33,15 @@ with Types;  use Types;
 package Sem_Prag is
 
    --  The following table lists all the implementation-defined pragmas that
-   --  may apply to a body stub (no language defined pragmas apply).
+   --  may apply to a body stub (no language defined pragmas apply). The table
+   --  should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if
+   --  the pragmas below implement an aspect.
 
-   Pragma_On_Stub_OK : constant array (Pragma_Id) of Boolean :=
+   Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
-     (Pragma_Refined_Pre  => True,
+     (Pragma_Refined_Post => True,
+      Pragma_Refined_Pre  => True,
       Pragma_SPARK_Mode   => True,
+      Pragma_Warnings     => True,
       others              => False);
 
    -----------------
@@ -164,6 +168,15 @@ package Sem_Prag is
    --  Suppress_All at this stage, since it can appear after the unit instead
    --  of before (actually we allow it to appear anywhere).
 
+   procedure Relocate_Pragmas_To_Body
+     (Subp_Body   : Node_Id;
+      Target_Body : Node_Id := Empty);
+   --  Resocate all pragmas that follow and apply to subprogram body Subp_Body
+   --  to its own declaration list. Candidate pragmas are classified in table
+   --  Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved
+   --  to the declarations of Target_Body. This formal should be set when
+   --  dealing with subprogram body stubs or expression functions.
+
    procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id);
    --  This routine is used to set an encoded interface name. The node S is an
    --  N_String_Literal node for the external name to be set, and E is an

gcc/ada/snames.ads-tmpl

@@ -580,6 +580,7 @@ package Snames is
    Name_Pure_05                        : constant Name_Id := N + $; -- GNAT
    Name_Pure_12                        : constant Name_Id := N + $; -- GNAT
    Name_Pure_Function                  : constant Name_Id := N + $; -- GNAT
+   Name_Refined_Post                   : constant Name_Id := N + $; -- GNAT
    Name_Refined_Pre                    : constant Name_Id := N + $; -- GNAT
    Name_Relative_Deadline              : constant Name_Id := N + $; -- Ada 05
    Name_Remote_Access_Type             : constant Name_Id := N + $; -- GNAT
@@ -1861,6 +1862,7 @@ package Snames is
       Pragma_Pure_05,
       Pragma_Pure_12,
       Pragma_Pure_Function,
+      Pragma_Refined_Post,
       Pragma_Refined_Pre,
       Pragma_Relative_Deadline,
       Pragma_Remote_Access_Type,