2013-10-10 Ed Schonberg <schonberg@adacore.com>

	* par-ch13.adb (Aspect_Specifications_Present)): In earlier than
	Ada2012 mode, assume that a legal aspect name following "with"
	keyword is an older gnat switch and not a misplaced with_clause.

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

	* aspects.adb: Add an entry for Aspect_Refined_Pre in
	table Canonical_Aspect.
	(Aspects_On_Body_OK): Renamed to
	Aspects_On_Body_Or_Stub_OK.
	(Aspects_On_Body_Or_Stub_OK):
	Update the query in table Aspect_On_Body_OK.
	* aspects.ads: Add an entry for Aspect_Refined_Pre in tables
	Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
	Aspect_On_Body_Or_Stub_OK. Table Aspect_On_Body_OK is now known as
	Aspect_On_Body_Or_Stub_OK.  Add a section of aspect specifications
	that apply to body stubs.
	(Aspects_On_Body_OK): Renamed to Aspects_On_Body_Or_Stub_OK.
	(Aspects_On_Body_Or_Stub_OK): Update the comment on usage.
	* par-prag.adb: Add pragma Refined_Pre to the list of pragmas
	that do not require special processing by the parser.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Delay the
	analysis of aspect specifications that apply to a body stub
	until the proper body is analyzed.
	* sem_ch10.adb: Add with and use clause for Sem_Ch13.
	(Analyze_Package_Body_Stub): Set the corresponding spec of the stub.
	(Analyze_Proper_Body): Relocate all pragmas that apply
	to a subprogram body stub to the declarations of the proper
	body. Analyze the aspect specifications of the stub when the
	proper body is not present.
	(Analyze_Protected_Body_Stub): Set the corresponding spec of the stub.
	(Analyze_Task_Body_Stub): Set the corresponding spec of the stub.
	(Move_Stub_Pragmas_To_Body): New routine.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Pre.
	(Check_Aspect_At_Freeze_Point): Aspect
	Refined_Pre does not need delayed processing at the freeze point.
	* sem_prag.adb: Remove with and use clause for Snames. Add
	an entry for Pragma_Refined_Pre in table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma Refined_Pre.
	* sem_prag.ads: Add with and use clause for Snames. Add table
	Pragma_On_Stub_OK.
	* sinfo.adb (Corresponding_Spec_Of_Stub): New routine.
	(Set_Corresponding_Spec_Of_Stub): New routine.
	* sinfo.ads: Add new attribute Corresponding_Spec_Of_Stub
	along with comment on usage and occurrences in nodes.
	(Corresponding_Spec_Of_Stub): New routine along with pragma
	Inline.
	(Set_Corresponding_Spec_Of_Stub): New routine along
	with pragma Inline.
	* snames.ads-tmpl: Add new predefined name for Refined_Pre. Add
	new Pragma_Id for Refined_Pre.

2013-10-10  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb (Analyze_Package_Instantiation,
	Analyze_Subprogram_Instantiation): Improve error message when
	name in instantiation does not designate a generic unit of the
	right kind.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@203355 138bc75d-0d04-0410-961f-82ee72b054a4

14 files changed, 460 insertions, 64 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index fa6cf6b7121..be5c54763d6 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,65 @@
+2013-10-10  Ed Schonberg  <schonberg@adacore.com>
+
+	* par-ch13.adb (Aspect_Specifications_Present)): In earlier than
+	Ada2012 mode, assume that a legal aspect name following "with"
+	keyword is an older gnat switch and not a misplaced with_clause.
+
+2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add an entry for Aspect_Refined_Pre in
+	table Canonical_Aspect.
+	(Aspects_On_Body_OK): Renamed to
+	Aspects_On_Body_Or_Stub_OK.
+	(Aspects_On_Body_Or_Stub_OK):
+	Update the query in table Aspect_On_Body_OK.
+	* aspects.ads: Add an entry for Aspect_Refined_Pre in tables
+	Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
+	Aspect_On_Body_Or_Stub_OK. Table Aspect_On_Body_OK is now known as
+	Aspect_On_Body_Or_Stub_OK.  Add a section of aspect specifications
+	that apply to body stubs.
+	(Aspects_On_Body_OK): Renamed to Aspects_On_Body_Or_Stub_OK.
+	(Aspects_On_Body_Or_Stub_OK): Update the comment on usage.
+	* par-prag.adb: Add pragma Refined_Pre to the list of pragmas
+	that do not require special processing by the parser.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Delay the
+	analysis of aspect specifications that apply to a body stub
+	until the proper body is analyzed.
+	* sem_ch10.adb: Add with and use clause for Sem_Ch13.
+	(Analyze_Package_Body_Stub): Set the corresponding spec of the stub.
+	(Analyze_Proper_Body): Relocate all pragmas that apply
+	to a subprogram body stub to the declarations of the proper
+	body. Analyze the aspect specifications of the stub when the
+	proper body is not present.
+	(Analyze_Protected_Body_Stub): Set the corresponding spec of the stub.
+	(Analyze_Task_Body_Stub): Set the corresponding spec of the stub.
+	(Move_Stub_Pragmas_To_Body): New routine.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+	for aspect Refined_Pre.
+	(Check_Aspect_At_Freeze_Point): Aspect
+	Refined_Pre does not need delayed processing at the freeze point.
+	* sem_prag.adb: Remove with and use clause for Snames. Add
+	an entry for Pragma_Refined_Pre in table Sig_Flags.
+	(Analyze_Pragma): Add processing for pragma Refined_Pre.
+	* sem_prag.ads: Add with and use clause for Snames. Add table
+	Pragma_On_Stub_OK.
+	* sinfo.adb (Corresponding_Spec_Of_Stub): New routine.
+	(Set_Corresponding_Spec_Of_Stub): New routine.
+	* sinfo.ads: Add new attribute Corresponding_Spec_Of_Stub
+	along with comment on usage and occurrences in nodes.
+	(Corresponding_Spec_Of_Stub): New routine along with pragma
+	Inline.
+	(Set_Corresponding_Spec_Of_Stub): New routine along
+	with pragma Inline.
+	* snames.ads-tmpl: Add new predefined name for Refined_Pre. Add
+	new Pragma_Id for Refined_Pre.
+
+2013-10-10  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch12.adb (Analyze_Package_Instantiation,
+	Analyze_Subprogram_Instantiation): Improve error message when
+	name in instantiation does not designate a generic unit of the
+	right kind.
+
 2013-10-10  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch3.adb (Expand_N_Variant_Part): Expand statically
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 1d736467b46..e20cae4782f 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -140,11 +140,11 @@ package body Aspects is
       end if;
    end Aspect_Specifications;
 
-   ------------------------
-   -- Aspects_On_Body_OK --
-   ------------------------
+   --------------------------------
+   -- Aspects_On_Body_Or_Stub_OK --
+   --------------------------------
 
-   function Aspects_On_Body_OK (N : Node_Id) return Boolean is
+   function Aspects_On_Body_Or_Stub_OK (N : Node_Id) return Boolean is
       Aspect  : Node_Id;
       Aspects : List_Id;
 
@@ -159,12 +159,12 @@ package body Aspects is
                                             N_Task_Body));
 
       --  Look through all aspects and see whether they can be applied to a
-      --  body.
+      --  body [stub].
 
       Aspects := Aspect_Specifications (N);
       Aspect  := First (Aspects);
       while Present (Aspect) loop
-         if not Aspect_On_Body_OK (Get_Aspect_Id (Aspect)) then
+         if not Aspect_On_Body_Or_Stub_OK (Get_Aspect_Id (Aspect)) then
             return False;
          end if;
 
@@ -172,7 +172,7 @@ package body Aspects is
       end loop;
 
       return True;
-   end Aspects_On_Body_OK;
+   end Aspects_On_Body_Or_Stub_OK;
 
    -----------------
    -- Find_Aspect --
@@ -368,9 +368,9 @@ package body Aspects is
       N_Single_Protected_Declaration           => True,
       N_Single_Task_Declaration                => True,
       N_Subprogram_Body                        => True,
+      N_Subprogram_Body_Stub                   => True,
       N_Subprogram_Declaration                 => True,
       N_Subprogram_Renaming_Declaration        => True,
-      N_Subprogram_Body_Stub                   => True,
       N_Subtype_Declaration                    => True,
       N_Task_Body                              => True,
       N_Task_Body_Stub                         => True,
@@ -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_Pre                  => Aspect_Refined_Pre,
     Aspect_Remote_Access_Type           => Aspect_Remote_Access_Type,
     Aspect_Remote_Call_Interface        => Aspect_Remote_Call_Interface,
     Aspect_Remote_Types                 => Aspect_Remote_Types,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 5e8046d1ad0..66c4b857da0 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -111,6 +111,7 @@ package Aspects is
       Aspect_Predicate,                     -- GNAT
       Aspect_Priority,
       Aspect_Read,
+      Aspect_Refined_Pre,                   -- GNAT
       Aspect_Relative_Deadline,
       Aspect_Scalar_Storage_Order,          -- GNAT
       Aspect_Simple_Storage_Pool,           -- GNAT
@@ -319,6 +320,7 @@ package Aspects is
       Aspect_Predicate               => Expression,
       Aspect_Priority                => Expression,
       Aspect_Read                    => Name,
+      Aspect_Refined_Pre             => Expression,
       Aspect_Relative_Deadline       => Expression,
       Aspect_Scalar_Storage_Order    => Expression,
       Aspect_Simple_Storage_Pool     => Name,
@@ -415,6 +417,7 @@ package Aspects is
       Aspect_Pure_12                      => Name_Pure_12,
       Aspect_Pure_Function                => Name_Pure_Function,
       Aspect_Read                         => Name_Read,
+      Aspect_Refined_Pre                  => Name_Refined_Pre,
       Aspect_Relative_Deadline            => Name_Relative_Deadline,
       Aspect_Remote_Access_Type           => Name_Remote_Access_Type,
       Aspect_Remote_Call_Interface        => Name_Remote_Call_Interface,
@@ -636,6 +639,7 @@ package Aspects is
       Aspect_Convention                   => Never_Delay,
       Aspect_Dimension                    => Never_Delay,
       Aspect_Dimension_System             => Never_Delay,
+      Aspect_Refined_Pre                  => Never_Delay,
       Aspect_SPARK_Mode                   => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,
@@ -657,15 +661,44 @@ package Aspects is
       Aspect_Volatile                     => Rep_Aspect,
       Aspect_Volatile_Components          => Rep_Aspect);
 
-   --  The following table indicates which aspects can apply simultaneously to
-   --  both subprogram/package specs and bodies. For instance, the following is
-   --  legal:
+   ------------------------------------------------
+   -- Handling of Aspect Specifications on Stubs --
+   ------------------------------------------------
+
+   --  Aspects that appear on the following stub nodes
+
+   --    N_Package_Body_Stub
+   --    N_Protected_Body_Stub
+   --    N_Subprogram_Body_Stub
+   --    N_Task_Body_Stub
+
+   --  are treated as if they apply to the corresponding proper body. Their
+   --  analysis is postponed until the analysis of the proper body takes place
+   --  (see Analyze_Proper_Body). The delay is required because the analysis
+   --  may generate extra code which would be harder to relocate to the body.
+   --  If the proper body is present, the aspect specifications are relocated
+   --  to the corresponding body node:
+
+   --    N_Package_Body
+   --    N_Protected_Body
+   --    N_Subprogram_Body
+   --    N_Task_Body
+
+   --  The subsequent analysis takes care of the aspect-to-pragma conversions
+   --  and verification of pragma legality. In the case where the proper body
+   --  is not available, the aspect specifications are analyzed on the spot
+   --  (see Analyze_Proper_Body) to catch potential errors.
+
+   --  The following table lists all aspects that can apply to a subprogram
+   --  body [stub]. For instance, the following example is legal:
 
    --    package P with SPARK_Mode ...;
    --    package body P with SPARK_Mode is ...;
 
-   Aspect_On_Body_OK : constant array (Aspect_Id) of Boolean :=
-     (Aspect_SPARK_Mode                   => True,
+   Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean :=
+     (Aspect_Refined_Pre                  => True,
+      Aspect_SPARK_Mode                   => True,
+      Aspect_Warnings                     => True,
       others                              => False);
 
    ---------------------------------------------------
@@ -696,9 +729,9 @@ package Aspects is
    --  Replace calls, and this function may be used to retrieve the aspect
    --  specifications for the original rewritten node in such cases.
 
-   function Aspects_On_Body_OK (N : Node_Id) return Boolean;
+   function Aspects_On_Body_Or_Stub_OK (N : Node_Id) return Boolean;
    --  N denotes a body [stub] with aspects. Determine whether all aspects of N
-   --  can appear simultaneously in bodies and specs.
+   --  are allowed to appear on a body [stub].
 
    function Find_Aspect (Id : Entity_Id; A : Aspect_Id) return Node_Id;
    --  Find the aspect specification of aspect A associated with entity I.
diff --git a/gcc/ada/par-ch13.adb b/gcc/ada/par-ch13.adb
index 34d2f8f4379..0fadd302daa 100644
--- a/gcc/ada/par-ch13.adb
+++ b/gcc/ada/par-ch13.adb
@@ -111,9 +111,11 @@ package body Ch13 is
 
             --  The identifier may be the name of a boolean aspect with a
             --  defaulted True value. Further checks when analyzing aspect
-            --  specification.
+            --  specification, which may include further aspects.
 
-            elsif Token = Tok_Comma then
+            elsif Token = Tok_Comma
+              or else Token = Tok_Semicolon
+            then
                Result := True;
 
             elsif Token = Tok_Apostrophe then
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 5de6ecc0081..91e9b96b138 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1250,6 +1250,7 @@ begin
            Pragma_Pure_12                        |
            Pragma_Pure_Function                  |
            Pragma_Queuing_Policy                 |
+           Pragma_Refined_Pre                    |
            Pragma_Relative_Deadline              |
            Pragma_Remote_Access_Type             |
            Pragma_Remote_Call_Interface          |
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index 6c36bf2cdb7..c68c5caa46a 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -53,6 +53,7 @@ with Sem_Ch3;  use Sem_Ch3;
 with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch7;  use Sem_Ch7;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
 with Sem_Dist; use Sem_Dist;
 with Sem_Prag; use Sem_Prag;
 with Sem_Util; use Sem_Util;
@@ -1581,6 +1582,7 @@ package body Sem_Ch10 is
 
          Set_Has_Completion (Nam);
          Set_Scope (Defining_Entity (N), Current_Scope);
+         Set_Corresponding_Spec_Of_Stub (N, Nam);
          Generate_Reference (Nam, Id, 'b');
          Analyze_Proper_Body (N, Nam);
       end if;
@@ -1594,12 +1596,85 @@ 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 --
       ----------------------
@@ -1664,6 +1739,10 @@ package body Sem_Ch10 is
          end if;
       end Optional_Subunit;
 
+      --  Local variables
+
+      Stub_Id : Entity_Id;
+
    --  Start of processing for Analyze_Proper_Body
 
    begin
@@ -1818,6 +1897,7 @@ package body Sem_Ch10 is
 
                declare
                   Comp_Unit : constant Node_Id := Cunit (Unum);
+                  Prop_Body : Node_Id;
 
                begin
                   --  Check for child unit instead of subunit
@@ -1830,6 +1910,8 @@ package body Sem_Ch10 is
                   --  OK, we have a subunit
 
                   else
+                     Prop_Body := Proper_Body (Unit (Comp_Unit));
+
                      --  Set corresponding stub (even if errors)
 
                      Set_Corresponding_Stub (Unit (Comp_Unit), N);
@@ -1845,11 +1927,17 @@ package body Sem_Ch10 is
                         SCO_Record (Unum);
                      end if;
 
-                     --  Propagate any aspect specifications associated with
-                     --  with the stub to the proper body.
+                     --  Propagate all aspect specifications associated with
+                     --  the stub to the proper body.
 
-                     Move_Or_Merge_Aspects
-                       (From => N, To => Proper_Body (Unit (Comp_Unit)));
+                     Move_Or_Merge_Aspects (From => N, To => Prop_Body);
+
+                     --  Propagate all source pragmas associated with a
+                     --  subprogram body stub to the proper body.
+
+                     if Nkind (N) = N_Subprogram_Body_Stub then
+                        Move_Stub_Pragmas_To_Body (Prop_Body);
+                     end if;
 
                      --  Analyze the unit if semantics active
 
@@ -1869,6 +1957,24 @@ package body Sem_Ch10 is
                      Version_Update (Cunit (Main_Unit), Comp_Unit);
                   end if;
                end;
+
+            --  The unit which should contain the proper subprogram body does
+            --  not exist. Analyze the aspect specifications of the stub (if
+            --  any).
+
+            elsif Nkind (N) = N_Subprogram_Body_Stub
+              and then Has_Aspects (N)
+            then
+               Stub_Id := Defining_Unit_Name (Specification (N));
+
+               --  Restore the proper visibility of the stub and its formals
+
+               Push_Scope (Stub_Id);
+               Install_Formals (Stub_Id);
+
+               Analyze_Aspect_Specifications (N, Stub_Id);
+
+               Pop_Scope;
             end if;
          end if;
 
@@ -1906,6 +2012,7 @@ package body Sem_Ch10 is
       else
          Set_Scope (Defining_Entity (N), Current_Scope);
          Set_Has_Completion (Etype (Nam));
+         Set_Corresponding_Spec_Of_Stub (N, Nam);
          Generate_Reference (Nam, Defining_Identifier (N), 'b');
          Analyze_Proper_Body (N, Etype (Nam));
       end if;
@@ -2351,6 +2458,7 @@ package body Sem_Ch10 is
       else
          Set_Scope (Defining_Entity (N), Current_Scope);
          Generate_Reference (Nam, Defining_Identifier (N), 'b');
+         Set_Corresponding_Spec_Of_Stub (N, Nam);
 
          --  Check for duplicate stub, if so give message and terminate
 
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 035d0b0bfda..f9e525652d4 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3479,8 +3479,8 @@ package body Sem_Ch12 is
             Error_Msg_N
               ("cannot instantiate a limited withed package", Gen_Id);
          else
-            Error_Msg_N
-              ("expect name of generic package in instantiation", Gen_Id);
+            Error_Msg_NE
+              ("& is not the name of a generic package", Gen_Id, Gen_Unit);
          end if;
 
          Restore_Env;
@@ -4669,34 +4669,17 @@ package body Sem_Ch12 is
       --  Verify that it is a generic subprogram of the right kind, and that
       --  it does not lead to a circular instantiation.
 
-      if not Ekind_In (Gen_Unit, E_Generic_Procedure, E_Generic_Function) then
-         Error_Msg_N ("expect generic subprogram in instantiation", Gen_Id);
+      if K = E_Procedure and then Ekind (Gen_Unit) /= E_Generic_Procedure then
+         Error_Msg_NE
+           ("& is not the name of a generic procedure", Gen_Id, Gen_Unit);
+
+      elsif K = E_Function and then Ekind (Gen_Unit) /= E_Generic_Function then
+         Error_Msg_NE
+           ("& is not the name of a generic function", Gen_Id, Gen_Unit);
 
       elsif In_Open_Scopes (Gen_Unit) then
          Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
 
-      elsif K = E_Procedure
-        and then Ekind (Gen_Unit) /= E_Generic_Procedure
-      then
-         if Ekind (Gen_Unit) = E_Generic_Function then
-            Error_Msg_N
-              ("cannot instantiate generic function as procedure", Gen_Id);
-         else
-            Error_Msg_N
-              ("expect name of generic procedure in instantiation", Gen_Id);
-         end if;
-
-      elsif K = E_Function
-        and then Ekind (Gen_Unit) /= E_Generic_Function
-      then
-         if Ekind (Gen_Unit) = E_Generic_Procedure then
-            Error_Msg_N
-              ("cannot instantiate generic procedure as function", Gen_Id);
-         else
-            Error_Msg_N
-              ("expect name of generic function in instantiation", Gen_Id);
-         end if;
-
       else
          Set_Entity (Gen_Id, Gen_Unit);
          Set_Is_Instantiated (Gen_Unit);
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index bc2be8b8eea..864d42d3b1b 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1928,6 +1928,15 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_SPARK_Mode);
 
+               --  Refined_Pre
+
+               when Aspect_Refined_Pre =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Refined_Pre);
+
                --  Relative_Deadline
 
                when Aspect_Relative_Deadline =>
@@ -7779,6 +7788,7 @@ package body Sem_Ch13 is
               Aspect_Postcondition        |
               Aspect_Pre                  |
               Aspect_Precondition         |
+              Aspect_Refined_Pre          |
               Aspect_SPARK_Mode           |
               Aspect_Test_Case     =>
             raise Program_Error;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 079aed850e4..4fffb88374d 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2672,20 +2672,30 @@ package body Sem_Ch6 is
          end if;
       end if;
 
-      --  Language-defined aspects cannot appear in a subprogram body if the
-      --  corresponding spec already has aspects. Exception to this rule are
-      --  certain user-defined aspects. Aspects that apply to a body stub are
-      --  moved to the proper body. Do not emit an error in this case.
+      --  Language-defined aspects cannot appear in a subprogram body [stub] if
+      --  the corresponding spec already has aspects. An exception to this rule
+      --  are certain user-defined aspects.
 
       if Has_Aspects (N) then
          if Present (Spec_Id)
-           and then Nkind (N) not in N_Body_Stub
-           and then Nkind (Parent (N)) /= N_Subunit
-           and then not Aspects_On_Body_OK (N)
+           and then not Aspects_On_Body_Or_Stub_OK (N)
+
+            --  Do not emit an error on a subprogram body stub that act as
+            --  its own spec.
+
+           and then Nkind (Parent (Parent (Spec_Id))) /= N_Subprogram_Body_Stub
          then
             Error_Msg_N
               ("aspect specifications must appear in subprogram declaration",
                 N);
+
+         --  Delay the analysis of aspect specifications that apply to a body
+         --  stub until the proper body is analyzed. If the corresponding body
+         --  is missing, the aspects are still analyzed in Analyze_Proper_Body.
+
+         elsif Nkind (N) in N_Body_Stub then
+            null;
+
          else
             Analyze_Aspect_Specifications (N, Body_Id);
          end if;
@@ -2835,7 +2845,12 @@ package body Sem_Ch6 is
             Reference_Body_Formals (Spec_Id, Body_Id);
          end if;
 
-         if Nkind (N) /= N_Subprogram_Body_Stub then
+         if Nkind (N) = N_Subprogram_Body_Stub then
+            Set_Corresponding_Spec_Of_Stub (N, Spec_Id);
+
+         --  Regular body
+
+         else
             Set_Corresponding_Spec (N, Spec_Id);
 
             --  Ada 2005 (AI-345): If the operation is a primitive operation
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 25ba32702a3..9d8f590ab9e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -75,7 +75,6 @@ with Stand;    use Stand;
 with Sinfo;    use Sinfo;
 with Sinfo.CN; use Sinfo.CN;
 with Sinput;   use Sinput;
-with Snames;   use Snames;
 with Stringt;  use Stringt;
 with Stylesw;  use Stylesw;
 with Table;
@@ -15932,6 +15931,137 @@ package body Sem_Prag is
          when Pragma_Rational =>
             Set_Rational_Profile;
 
+         -----------------
+         -- Refined_Pre --
+         -----------------
+
+         --  pragma Refined_Pre (boolean_EXPRESSION);
+
+         when Pragma_Refined_Pre => Refined_Pre : declare
+            Body_Decl : Node_Id := Parent (N);
+            Pack_Spec : Node_Id;
+            Restore   : Boolean := False;
+            Spec_Decl : Node_Id;
+            Spec_Id   : Entity_Id;
+            Stmt      : Node_Id;
+
+         begin
+            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;
+
+               --  Skip internally generated code
+
+               elsif not Comes_From_Source (Stmt) then
+                  null;
+
+               --  The pragma applies to a subprogram body stub
+
+               elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
+                  Body_Decl := Stmt;
+                  exit;
+
+               --  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))
+              and then Current_Scope /= Spec_Id
+            then
+               Restore := True;
+               Push_Scope (Spec_Id);
+               Install_Formals (Spec_Id);
+            end if;
+
+            --  Convert pragma Refined_Pre into pragma Check. The analysis of
+            --  the generated pragma will take care of the expression.
+
+            Rewrite (N,
+              Make_Pragma (Loc,
+                Chars                        => Name_Check,
+                Pragma_Argument_Associations => New_List (
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Make_Identifier (Loc, Pname)),
+
+                  Make_Pragma_Argument_Association (Sloc (Arg1),
+                    Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
+
+            Analyze (N);
+
+            if Restore then
+               Pop_Scope;
+            end if;
+         end Refined_Pre;
+
          -----------------------
          -- Relative_Deadline --
          -----------------------
@@ -18994,12 +19124,12 @@ package body Sem_Prag is
       Pragma_Page                           => -1,
       Pragma_Partition_Elaboration_Policy   => -1,
       Pragma_Passive                        => -1,
-      Pragma_Preelaborable_Initialization   => -1,
-      Pragma_Polling                        => -1,
       Pragma_Persistent_BSS                 =>  0,
+      Pragma_Polling                        => -1,
       Pragma_Postcondition                  => -1,
       Pragma_Precondition                   => -1,
       Pragma_Predicate                      => -1,
+      Pragma_Preelaborable_Initialization   => -1,
       Pragma_Preelaborate                   => -1,
       Pragma_Preelaborate_05                => -1,
       Pragma_Priority                       => -1,
@@ -19015,6 +19145,7 @@ package body Sem_Prag is
       Pragma_Queuing_Policy                 => -1,
       Pragma_Rational                       => -1,
       Pragma_Ravenscar                      => -1,
+      Pragma_Refined_Pre                    => -1,
       Pragma_Relative_Deadline              => -1,
       Pragma_Remote_Access_Type             => -1,
       Pragma_Remote_Call_Interface          => -1,
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index ecfb3eda75a..c01c5f21c10 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -26,11 +26,20 @@
 --  Pragma handling is isolated in a separate package
 --  (logically this processing belongs in chapter 4)
 
-with Namet; use Namet;
-with Types; use Types;
+with Namet;  use Namet;
+with Snames; use Snames;
+with Types;  use Types;
 
 package Sem_Prag is
 
+   --  The following table lists all the user-defined pragmas that may apply to
+   --  a body stub.
+
+   Pragma_On_Stub_OK : constant array (Pragma_Id) of Boolean :=
+     (Pragma_Refined_Pre  => True,
+      Pragma_SPARK_Mode   => True,
+      others              => False);
+
    -----------------
    -- Subprograms --
    -----------------
diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb
index 6cb18c1890c..4aae39daf88 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -691,6 +691,17 @@ package body Sinfo is
       return Node5 (N);
    end Corresponding_Spec;
 
+   function Corresponding_Spec_Of_Stub
+      (N : Node_Id) return Entity_Id is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Package_Body_Stub
+        or else NT (N).Nkind = N_Protected_Body_Stub
+        or else NT (N).Nkind = N_Subprogram_Body_Stub
+        or else NT (N).Nkind = N_Task_Body_Stub);
+      return Node2 (N);
+   end Corresponding_Spec_Of_Stub;
+
    function Corresponding_Stub
       (N : Node_Id) return Node_Id is
    begin
@@ -3817,6 +3828,17 @@ package body Sinfo is
       Set_Node5 (N, Val); -- semantic field, no parent set
    end Set_Corresponding_Spec;
 
+   procedure Set_Corresponding_Spec_Of_Stub
+      (N : Node_Id; Val : Entity_Id) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Package_Body_Stub
+        or else NT (N).Nkind = N_Protected_Body_Stub
+        or else NT (N).Nkind = N_Subprogram_Body_Stub
+        or else NT (N).Nkind = N_Task_Body_Stub);
+      Set_Node2 (N, Val); -- semantic field, no parent set
+   end Set_Corresponding_Spec_Of_Stub;
+
    procedure Set_Corresponding_Stub
       (N : Node_Id; Val : Node_Id) is
    begin
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index e3508bab252..6028b92540c 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -822,6 +822,11 @@ package Sinfo is
    --    In Ada 2012, Corresponding_Spec is set on expression functions that
    --    complete a subprogram declaration.
 
+   --  Corresponding_Spec_Of_Stub (Node2-Sem)
+   --    This field is present in subprogram, package, task and protected body
+   --    stubs where it points to the corresponding spec of the stub. Due to
+   --    clashes in the structure of nodes, we cannot use Corresponding_Spec.
+
    --  Corresponding_Stub (Node3-Sem)
    --    This field is present in an N_Subunit node. It holds the node in
    --    the parent unit that is the stub declaration for the subunit. It is
@@ -6067,6 +6072,7 @@ package Sinfo is
       --  N_Subprogram_Body_Stub
       --  Sloc points to FUNCTION or PROCEDURE
       --  Specification (Node1)
+      --  Corresponding_Spec_Of_Stub (Node2-Sem)
       --  Library_Unit (Node4-Sem) points to the subunit
       --  Corresponding_Body (Node5-Sem)
 
@@ -6081,6 +6087,7 @@ package Sinfo is
       --  N_Package_Body_Stub
       --  Sloc points to PACKAGE
       --  Defining_Identifier (Node1)
+      --  Corresponding_Spec_Of_Stub (Node2-Sem)
       --  Library_Unit (Node4-Sem) points to the subunit
       --  Corresponding_Body (Node5-Sem)
 
@@ -6095,6 +6102,7 @@ package Sinfo is
       --  N_Task_Body_Stub
       --  Sloc points to TASK
       --  Defining_Identifier (Node1)
+      --  Corresponding_Spec_Of_Stub (Node2-Sem)
       --  Library_Unit (Node4-Sem) points to the subunit
       --  Corresponding_Body (Node5-Sem)
 
@@ -6111,6 +6119,7 @@ package Sinfo is
       --  N_Protected_Body_Stub
       --  Sloc points to PROTECTED
       --  Defining_Identifier (Node1)
+      --  Corresponding_Spec_Of_Stub (Node2-Sem)
       --  Library_Unit (Node4-Sem) points to the subunit
       --  Corresponding_Body (Node5-Sem)
 
@@ -8503,6 +8512,9 @@ package Sinfo is
    function Corresponding_Spec
      (N : Node_Id) return Node_Id;    -- Node5
 
+   function Corresponding_Spec_Of_Stub
+     (N : Node_Id) return Node_Id;    -- Node2
+
    function Corresponding_Stub
      (N : Node_Id) return Node_Id;    -- Node3
 
@@ -9499,6 +9511,9 @@ package Sinfo is
    procedure Set_Corresponding_Spec
      (N : Node_Id; Val : Node_Id);            -- Node5
 
+   procedure Set_Corresponding_Spec_Of_Stub
+     (N : Node_Id; Val : Node_Id);            -- Node2
+
    procedure Set_Corresponding_Stub
      (N : Node_Id; Val : Node_Id);            -- Node3
 
@@ -11509,28 +11524,28 @@ package Sinfo is
 
      N_Subprogram_Body_Stub =>
        (1 => True,    --  Specification (Node1)
-        2 => False,   --  unused
+        2 => False,   --  Corresponding_Spec_Of_Stub (Node2-Sem)
         3 => False,   --  unused
         4 => False,   --  Library_Unit (Node4-Sem)
         5 => False),  --  Corresponding_Body (Node5-Sem)
 
      N_Package_Body_Stub =>
        (1 => True,    --  Defining_Identifier (Node1)
-        2 => False,   --  unused
+        2 => False,   --  Corresponding_Spec_Of_Stub (Node2-Sem)
         3 => False,   --  unused
         4 => False,   --  Library_Unit (Node4-Sem)
         5 => False),  --  Corresponding_Body (Node5-Sem)
 
      N_Task_Body_Stub =>
        (1 => True,    --  Defining_Identifier (Node1)
-        2 => False,   --  unused
+        2 => False,   --  Corresponding_Spec_Of_Stub (Node2-Sem)
         3 => False,   --  unused
         4 => False,   --  Library_Unit (Node4-Sem)
         5 => False),  --  Corresponding_Body (Node5-Sem)
 
      N_Protected_Body_Stub =>
        (1 => True,    --  Defining_Identifier (Node1)
-        2 => False,   --  unused
+        2 => False,   --  Corresponding_Spec_Of_Stub (Node2-Sem)
         3 => False,   --  unused
         4 => False,   --  Library_Unit (Node4-Sem)
         5 => False),  --  Corresponding_Body (Node5-Sem)
@@ -12097,6 +12112,7 @@ package Sinfo is
    pragma Inline (Corresponding_Generic_Association);
    pragma Inline (Corresponding_Integer_Value);
    pragma Inline (Corresponding_Spec);
+   pragma Inline (Corresponding_Spec_Of_Stub);
    pragma Inline (Corresponding_Stub);
    pragma Inline (Dcheck_Function);
    pragma Inline (Declarations);
@@ -12426,6 +12442,7 @@ package Sinfo is
    pragma Inline (Set_Corresponding_Generic_Association);
    pragma Inline (Set_Corresponding_Integer_Value);
    pragma Inline (Set_Corresponding_Spec);
+   pragma Inline (Set_Corresponding_Spec_Of_Stub);
    pragma Inline (Set_Corresponding_Stub);
    pragma Inline (Set_Dcheck_Function);
    pragma Inline (Set_Declarations);
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 70afdb70110..ed483f4c333 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/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_Pre                    : constant Name_Id := N + $; -- GNAT
    Name_Relative_Deadline              : constant Name_Id := N + $; -- Ada 05
    Name_Remote_Access_Type             : constant Name_Id := N + $; -- GNAT
    Name_Remote_Call_Interface          : constant Name_Id := N + $;
@@ -1860,6 +1861,7 @@ package Snames is
       Pragma_Pure_05,
       Pragma_Pure_12,
       Pragma_Pure_Function,
+      Pragma_Refined_Pre,
       Pragma_Relative_Deadline,
       Pragma_Remote_Access_Type,
       Pragma_Remote_Call_Interface,