[multiple changes]

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

	* aspects.adb: Add entries in table Canonical_Aspects for aspects
	Refined_Depends and Refined_Global.
	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
	Aspect_Names, Aspect_Declay, Aspect_On_Body_Or_Stub_OK for
	aspects Refined_Depends and Refined_Global.
	* einfo.adb (Contract): Subprogram bodies are now valid owners
	of contracts.
	(Set_Contract): Subprogram bodies are now valid
	owners of contracts.
	(Write_Field24_Name): Output the contract
	attribute for subprogram bodies.
	* exp_ch6.adb (Expand_Subprogram_Contract): New routine.
	* exp_ch6.ads (Expand_Subprogram_Contract): New routine.
	* par-prag.adb: Pragmas Refined_Depends and Refined_Global do
	not require any special processing by the parser.
	* sem_ch3.adb (Adjust_D): Renamed to Adjust_Decl.
	(Analyze_Declarations): Code reformatting. Analyze the contract
	of a subprogram body at the end of the declarative region.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	Subprogram bodies can now have contracts.  Use
	Expand_Subprogram_Contract to handle the various contract
	assertions.
	(Analyze_Subprogram_Body_Contract): New null routine.
	(Analyze_Subprogram_Body_Helper): Subprogram bodies can now have
	contracts.  Use Expand_Subprogram_Contract to handle the various
	contract assertions.
	(Analyze_Subprogram_Contract): Add local
	variable Nam. Update the call to Analyze_PPC_In_Decl_Part. Capture
	the pragma name in Nam.
	(Process_PPCs): Removed.
	* sem_ch6.ads (Analyze_Subprogram_Body_Contract): New routine.
	(Analyze_Subprogram_Contract): Update the comment on usage.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add null
	implementations for aspects Refined_Depends and Refined_Global.
	(Check_Aspect_At_Freeze_Point): Aspects Refined_Depends and
	Refined_Global do not need to be checked at the freeze point.
	* sem_prag.adb: Add entries in table Sig_Flags
	for pragmas Refined_Depends and Refined_Global.
	(Analyze_Contract_Cases_In_Decl_Part): Add local
	variable Restore. Use Restore to pop the scope.
	(Analyze_Depends_In_Decl_Part): Add local variable Restore. Use
	Restore to pop the scope.
	(Analyze_Global_In_Decl_List): Add local variable Restore. Use Restore
	to pop the scope.
	(Analyze_PPC_In_Decl_Part): Renamed to
	Analyze_Pre_Post_Condition_In_Decl_Part.
	(Analyze_Pragma):
	Add null implementations for pragmas Refined_Depends and
	Refined_Global. Refined_Pre and Refined_Post are now
	handled by routine Analyze_Refined_Pre_Post_Condition
	exclusively.
	(Analyze_Refined_Depends_In_Decl_Part): New
	null routine.
	(Analyze_Refined_Global_In_Decl_Part):
	New null routine.
	(Analyze_Refined_Pre_Post):
	Renamed to Analyze_Refined_Pre_Post_Condition.
	(Analyze_Refined_Pre_Post_Condition): Analyze the boolean
	expression.
	(Check_Precondition_Postcondition): Update the call
	to Analyze_PPC_In_Decl_Part.
	* sem_prag.ads: Add entries in table
	Pragma_On_Body_Or_Stub_OK for pragmas Refined_Depends
	and Refined_Global.
	(Analyze_PPC_In_Decl_Part): Renamed
	to Analyze_Pre_Post_Condition_In_Decl_Part.  Update the
	comment on usage.
	(Analyze_Refined_Depends_In_Decl_Part): New routine.
	(Analyze_Refined_Global_In_Decl_Part): New routine.
	(Analyze_Test_Case_In_Decl_Part): Update the comment on usage.
	* sem_util.adb (Add_Contract_Item): Rename formal Item to Prag
	and update all occurrences.  Subprogram body contracts can now
	contain pragmas Refined_Depends and Refined_Global.
	* sem_util.ads (Add_Contract_Item): Rename formal Item to
	Prag. Update the comment on usage.
	* sinfo.ads: Update the comment on structure and usage of
	N_Contract.
	* snames.ads-tmpl: Add new predefined names for Refined_Depends
	and Refined_Global. Add entries in table Pragma_Id for
	Refined_Depends and Refined_Global.

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

	* types.ads: Minor reformatting.

From-SVN: r203365

gcc/ada/ChangeLog

+2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add entries in table Canonical_Aspects for aspects
+	Refined_Depends and Refined_Global.
+	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
+	Aspect_Names, Aspect_Declay, Aspect_On_Body_Or_Stub_OK for
+	aspects Refined_Depends and Refined_Global.
+	* einfo.adb (Contract): Subprogram bodies are now valid owners
+	of contracts.
+	(Set_Contract): Subprogram bodies are now valid
+	owners of contracts.
+	(Write_Field24_Name): Output the contract
+	attribute for subprogram bodies.
+	* exp_ch6.adb (Expand_Subprogram_Contract): New routine.
+	* exp_ch6.ads (Expand_Subprogram_Contract): New routine.
+	* par-prag.adb: Pragmas Refined_Depends and Refined_Global do
+	not require any special processing by the parser.
+	* sem_ch3.adb (Adjust_D): Renamed to Adjust_Decl.
+	(Analyze_Declarations): Code reformatting. Analyze the contract
+	of a subprogram body at the end of the declarative region.
+	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
+	Subprogram bodies can now have contracts.  Use
+	Expand_Subprogram_Contract to handle the various contract
+	assertions.
+	(Analyze_Subprogram_Body_Contract): New null routine.
+	(Analyze_Subprogram_Body_Helper): Subprogram bodies can now have
+	contracts.  Use Expand_Subprogram_Contract to handle the various
+	contract assertions.
+	(Analyze_Subprogram_Contract): Add local
+	variable Nam. Update the call to Analyze_PPC_In_Decl_Part. Capture
+	the pragma name in Nam.
+	(Process_PPCs): Removed.
+	* sem_ch6.ads (Analyze_Subprogram_Body_Contract): New routine.
+	(Analyze_Subprogram_Contract): Update the comment on usage.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add null
+	implementations for aspects Refined_Depends and Refined_Global.
+	(Check_Aspect_At_Freeze_Point): Aspects Refined_Depends and
+	Refined_Global do not need to be checked at the freeze point.
+	* sem_prag.adb: Add entries in table Sig_Flags
+	for pragmas Refined_Depends and Refined_Global.
+	(Analyze_Contract_Cases_In_Decl_Part): Add local
+	variable Restore. Use Restore to pop the scope.
+	(Analyze_Depends_In_Decl_Part): Add local variable Restore. Use
+	Restore to pop the scope.
+	(Analyze_Global_In_Decl_List): Add local variable Restore. Use Restore
+	to pop the scope.
+	(Analyze_PPC_In_Decl_Part): Renamed to
+	Analyze_Pre_Post_Condition_In_Decl_Part.
+	(Analyze_Pragma):
+	Add null implementations for pragmas Refined_Depends and
+	Refined_Global. Refined_Pre and Refined_Post are now
+	handled by routine Analyze_Refined_Pre_Post_Condition
+	exclusively.
+	(Analyze_Refined_Depends_In_Decl_Part): New
+	null routine.
+	(Analyze_Refined_Global_In_Decl_Part):
+	New null routine.
+	(Analyze_Refined_Pre_Post):
+	Renamed to Analyze_Refined_Pre_Post_Condition.
+	(Analyze_Refined_Pre_Post_Condition): Analyze the boolean
+	expression.
+	(Check_Precondition_Postcondition): Update the call
+	to Analyze_PPC_In_Decl_Part.
+	* sem_prag.ads: Add entries in table
+	Pragma_On_Body_Or_Stub_OK for pragmas Refined_Depends
+	and Refined_Global.
+	(Analyze_PPC_In_Decl_Part): Renamed
+	to Analyze_Pre_Post_Condition_In_Decl_Part.  Update the
+	comment on usage.
+	(Analyze_Refined_Depends_In_Decl_Part): New routine.
+	(Analyze_Refined_Global_In_Decl_Part): New routine.
+	(Analyze_Test_Case_In_Decl_Part): Update the comment on usage.
+	* sem_util.adb (Add_Contract_Item): Rename formal Item to Prag
+	and update all occurrences.  Subprogram body contracts can now
+	contain pragmas Refined_Depends and Refined_Global.
+	* sem_util.ads (Add_Contract_Item): Rename formal Item to
+	Prag. Update the comment on usage.
+	* sinfo.ads: Update the comment on structure and usage of
+	N_Contract.
+	* snames.ads-tmpl: Add new predefined names for Refined_Depends
+	and Refined_Global. Add entries in table Pragma_Id for
+	Refined_Depends and Refined_Global.
+
+2013-10-10  Robert Dewar  <dewar@adacore.com>
+
+	* types.ads: Minor reformatting.
+
 2013-10-10  Thomas Quinot  <quinot@adacore.com>
 
 	* s-taprop-posix.adb: Add missing comment.

gcc/ada/aspects.adb

@@ -466,6 +466,8 @@ package body Aspects is
     Aspect_Pure_05                      => Aspect_Pure_05,
     Aspect_Pure_12                      => Aspect_Pure_12,
     Aspect_Pure_Function                => Aspect_Pure_Function,
+    Aspect_Refined_Depends              => Aspect_Refined_Depends,
+    Aspect_Refined_Global               => Aspect_Refined_Global,
     Aspect_Refined_Post                 => Aspect_Refined_Post,
     Aspect_Refined_Pre                  => Aspect_Refined_Pre,
     Aspect_Remote_Access_Type           => Aspect_Remote_Access_Type,

gcc/ada/aspects.ads

@@ -111,6 +111,8 @@ package Aspects is
       Aspect_Predicate,                     -- GNAT
       Aspect_Priority,
       Aspect_Read,
+      Aspect_Refined_Depends,               -- GNAT
+      Aspect_Refined_Global,                -- GNAT
       Aspect_Refined_Post,                  -- GNAT
       Aspect_Refined_Pre,                   -- GNAT
       Aspect_Relative_Deadline,
@@ -321,6 +323,8 @@ package Aspects is
       Aspect_Predicate               => Expression,
       Aspect_Priority                => Expression,
       Aspect_Read                    => Name,
+      Aspect_Refined_Depends         => Expression,
+      Aspect_Refined_Global          => Expression,
       Aspect_Refined_Post            => Expression,
       Aspect_Refined_Pre             => Expression,
       Aspect_Relative_Deadline       => Expression,
@@ -419,6 +423,8 @@ package Aspects is
       Aspect_Pure_12                      => Name_Pure_12,
       Aspect_Pure_Function                => Name_Pure_Function,
       Aspect_Read                         => Name_Read,
+      Aspect_Refined_Depends              => Name_Refined_Depends,
+      Aspect_Refined_Global               => Name_Refined_Global,
       Aspect_Refined_Post                 => Name_Refined_Post,
       Aspect_Refined_Pre                  => Name_Refined_Pre,
       Aspect_Relative_Deadline            => Name_Relative_Deadline,
@@ -612,6 +618,8 @@ package Aspects is
       Aspect_Pure_12                      => Always_Delay,
       Aspect_Pure_Function                => Always_Delay,
       Aspect_Read                         => Always_Delay,
+      Aspect_Refined_Depends              => Always_Delay,
+      Aspect_Refined_Global               => Always_Delay,
       Aspect_Relative_Deadline            => Always_Delay,
       Aspect_Remote_Access_Type           => Always_Delay,
       Aspect_Remote_Call_Interface        => Always_Delay,
@@ -703,7 +711,9 @@ package Aspects is
    --  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_Post                 => True,
+     (Aspect_Refined_Depends              => True,
+      Aspect_Refined_Global               => True,
+      Aspect_Refined_Post                 => True,
       Aspect_Refined_Pre                  => True,
       Aspect_SPARK_Mode                   => True,
       Aspect_Warnings                     => True,

gcc/ada/einfo.adb

@@ -1065,7 +1065,7 @@ package body Einfo is
    function Contract (Id : E) return N is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Entry, E_Entry_Family)
+        (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body)
           or else Is_Subprogram (Id)
           or else Is_Generic_Subprogram (Id));
       return Node24 (Id);
@@ -3651,7 +3651,7 @@ package body Einfo is
    procedure Set_Contract (Id : E; V : N) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
+        (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body, E_Void)
           or else Is_Subprogram (Id)
           or else Is_Generic_Subprogram (Id));
       Set_Node24 (Id, V);
@@ -9012,10 +9012,15 @@ package body Einfo is
 
          when E_Entry                                      |
               E_Entry_Family                               |
+              E_Subprogram_Body                            |
               Subprogram_Kind                              |
               Generic_Subprogram_Kind                      =>
             Write_Str ("Contract");
 
+            --  The Subprogram_Kind and Generic_Subrpogram_Kind entries
+            --  here are odd, since the assertions for [Set_]Contract do not
+            --  allow these possibilities ???
+
          when others                                       =>
             Write_Str ("Field24???");
       end case;

gcc/ada/exp_ch6.ads

@@ -82,6 +82,18 @@ package Exp_Ch6 is
    --  Subp_Id's body. All generated code is added to list Stmts. If Stmts is
    --  empty, a new list is created.
 
+   procedure Expand_Subprogram_Contract
+     (N       : Node_Id;
+      Spec_Id : Entity_Id;
+      Body_Id : Entity_Id);
+   --  Expand the contracts of a subprogram body and its correspoding spec (if
+   --  any). This routine processes all [refined] pre- and postconditions as
+   --  well as Contract_Cases, invariants and predicates. N is the body of the
+   --  subprogram. Spec_Id denotes the entity of its specification. Body_Id
+   --  denotes the entity of the subprogram body. This routine is not a "pure"
+   --  expansion mechanism as it is invoked during analysis and may perform
+   --  actions for generic subprograms or set up contract assertions for ASIS.
+
    procedure Freeze_Subprogram (N : Node_Id);
    --  generate the appropriate expansions related to Subprogram freeze
    --  nodes (e.g. the filling of the corresponding Dispatch Table for

gcc/ada/par-prag.adb

@@ -1250,6 +1250,8 @@ begin
            Pragma_Pure_12                        |
            Pragma_Pure_Function                  |
            Pragma_Queuing_Policy                 |
+           Pragma_Refined_Depends                |
+           Pragma_Refined_Global                 |
            Pragma_Refined_Post                   |
            Pragma_Refined_Pre                    |
            Pragma_Relative_Deadline              |

gcc/ada/sem_ch13.adb

@@ -1928,6 +1928,20 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_SPARK_Mode);
 
+               --  Refined_Depends
+
+               --  ??? To be implemented
+
+               when Aspect_Refined_Depends =>
+                  null;
+
+               --  Refined_Global
+
+               --  ??? To be implemented
+
+               when Aspect_Refined_Global =>
+                  null;
+
                --  Refined_Post
 
                when Aspect_Refined_Post =>
@@ -7962,6 +7976,8 @@ package body Sem_Ch13 is
               Aspect_Postcondition        |
               Aspect_Pre                  |
               Aspect_Precondition         |
+              Aspect_Refined_Depends      |
+              Aspect_Refined_Global       |
               Aspect_Refined_Post         |
               Aspect_Refined_Pre          |
               Aspect_SPARK_Mode           |

gcc/ada/sem_ch3.adb

@@ -2056,28 +2056,31 @@ package body Sem_Ch3 is
    --------------------------
 
    procedure Analyze_Declarations (L : List_Id) is
-      D           : Node_Id;
-      Freeze_From : Entity_Id := Empty;
-      Next_Node   : Node_Id;
+      Decl : Node_Id;
 
-      procedure Adjust_D;
-      --  Adjust D not to include implicit label declarations, since these
+      procedure Adjust_Decl;
+      --  Adjust Decl not to include implicit label declarations, since these
       --  have strange Sloc values that result in elaboration check problems.
       --  (They have the sloc of the label as found in the source, and that
       --  is ahead of the current declarative part).
 
-      --------------
-      -- Adjust_D --
-      --------------
+      -----------------
+      -- Adjust_Decl --
+      -----------------
 
-      procedure Adjust_D is
+      procedure Adjust_Decl is
       begin
-         while Present (Prev (D))
-           and then Nkind (D) = N_Implicit_Label_Declaration
+         while Present (Prev (Decl))
+           and then Nkind (Decl) = N_Implicit_Label_Declaration
          loop
-            Prev (D);
+            Prev (Decl);
          end loop;
-      end Adjust_D;
+      end Adjust_Decl;
+
+      --  Local variables
+
+      Freeze_From : Entity_Id := Empty;
+      Next_Decl   : Node_Id;
 
    --  Start of processing for Analyze_Declarations
 
@@ -2086,23 +2089,23 @@ package body Sem_Ch3 is
          Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
       end if;
 
-      D := First (L);
-      while Present (D) loop
+      Decl := First (L);
+      while Present (Decl) loop
 
          --  Package spec cannot contain a package declaration in SPARK
 
-         if Nkind (D) = N_Package_Declaration
+         if Nkind (Decl) = N_Package_Declaration
            and then Nkind (Parent (L)) = N_Package_Specification
          then
             Check_SPARK_Restriction
               ("package specification cannot contain a package declaration",
-               D);
+               Decl);
          end if;
 
          --  Complete analysis of declaration
 
-         Analyze (D);
-         Next_Node := Next (D);
+         Analyze (Decl);
+         Next_Decl := Next (Decl);
 
          if No (Freeze_From) then
             Freeze_From := First_Entity (Current_Scope);
@@ -2124,7 +2127,7 @@ package body Sem_Ch3 is
          --  be a freeze point once delayed freezing of bodies is implemented.
          --  (This is needed in any case for early instantiations ???).
 
-         if No (Next_Node) then
+         if No (Next_Decl) then
             if Nkind_In (Parent (L), N_Component_List,
                                      N_Task_Definition,
                                      N_Protected_Definition)
@@ -2136,8 +2139,8 @@ package body Sem_Ch3 is
                   Freeze_From := First_Entity (Current_Scope);
                end if;
 
-               Adjust_D;
-               Freeze_All (Freeze_From, D);
+               Adjust_Decl;
+               Freeze_All (Freeze_From, Decl);
                Freeze_From := Last_Entity (Current_Scope);
 
             elsif Scope (Current_Scope) /= Standard_Standard
@@ -2150,8 +2153,8 @@ package body Sem_Ch3 is
                or else No (Private_Declarations (Parent (L)))
                or else Is_Empty_List (Private_Declarations (Parent (L)))
             then
-               Adjust_D;
-               Freeze_All (Freeze_From, D);
+               Adjust_Decl;
+               Freeze_All (Freeze_From, Decl);
                Freeze_From := Last_Entity (Current_Scope);
             end if;
 
@@ -2170,44 +2173,39 @@ package body Sem_Ch3 is
          --  care to attach the bodies at a proper place in the tree so as to
          --  not cause unwanted freezing at that point.
 
-         elsif not Analyzed (Next_Node)
-           and then (Nkind_In (Next_Node, N_Subprogram_Body,
+         elsif not Analyzed (Next_Decl)
+           and then (Nkind_In (Next_Decl, N_Subprogram_Body,
                                           N_Entry_Body,
                                           N_Package_Body,
                                           N_Protected_Body,
                                           N_Task_Body)
                        or else
-                     Nkind (Next_Node) in N_Body_Stub)
+                     Nkind (Next_Decl) in N_Body_Stub)
          then
-            Adjust_D;
-            Freeze_All (Freeze_From, D);
+            Adjust_Decl;
+            Freeze_All (Freeze_From, Decl);
             Freeze_From := Last_Entity (Current_Scope);
          end if;
 
-         D := Next_Node;
+         Decl := Next_Decl;
       end loop;
 
-      --  One more thing to do, we need to scan the declarations to check for
-      --  any precondition/postcondition pragmas (Pre/Post aspects have by this
-      --  stage been converted into corresponding pragmas). It is at this point
-      --  that we analyze the expressions in such pragmas, to implement the
-      --  delayed visibility requirement.
+      --  Analyze the contracts of a subprogram declaration or a body now due
+      --  to delayed visibility requirements of aspects.
 
-      declare
-         Decl    : Node_Id;
-         Subp_Id : Entity_Id;
+      Decl := First (L);
+      while Present (Decl) loop
+         if Nkind (Decl) = N_Subprogram_Body then
+            Analyze_Subprogram_Body_Contract
+              (Defining_Unit_Name (Specification (Decl)));
 
-      begin
-         Decl := First (L);
-         while Present (Decl) loop
-            if Nkind (Decl) = N_Subprogram_Declaration then
-               Subp_Id := Defining_Unit_Name (Specification (Decl));
-               Analyze_Subprogram_Contract (Subp_Id);
-            end if;
+         elsif Nkind (Decl) = N_Subprogram_Declaration then
+            Analyze_Subprogram_Contract
+              (Defining_Unit_Name (Specification (Decl)));
+         end if;
 
-            Next (Decl);
-         end loop;
-      end;
+         Next (Decl);
+      end loop;
    end Analyze_Declarations;
 
    -----------------------------------

gcc/ada/sem_ch6.ads

@@ -46,9 +46,21 @@ package Sem_Ch6 is
    procedure Analyze_Subprogram_Declaration          (N : Node_Id);
    procedure Analyze_Subprogram_Body                 (N : Node_Id);
 
+   procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id);
+   --  Analyze all delayed aspects chained on the contract of subprogram body
+   --  Subp as if they appeared at the end of a declarative region. The aspects
+   --  in question are:
+   --    Refined_Depends
+   --    Refined_Global
+
    procedure Analyze_Subprogram_Contract (Subp : Entity_Id);
    --  Analyze all delayed aspects chained on the contract of subprogram Subp
-   --  as if they appeared at the end of a declarative region.
+   --  as if they appeared at the end of a declarative region. The aspects in
+   --  question are:
+   --    Contract_Cases
+   --    Postcondition
+   --    Precondition
+   --    Test_Case
 
    function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id;
    --  Analyze subprogram specification in both subprogram declarations

gcc/ada/sem_prag.ads

@@ -38,11 +38,13 @@ package Sem_Prag is
    --  the pragmas below implement an aspect.
 
    Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
-     (Pragma_Refined_Post => True,
-      Pragma_Refined_Pre  => True,
-      Pragma_SPARK_Mode   => True,
-      Pragma_Warnings     => True,
-      others              => False);
+     (Pragma_Refined_Depends => True,
+      Pragma_Refined_Global  => True,
+      Pragma_Refined_Post    => True,
+      Pragma_Refined_Pre     => True,
+      Pragma_SPARK_Mode      => True,
+      Pragma_Warnings        => True,
+      others                 => False);
 
    -----------------
    -- Subprograms --
@@ -60,21 +62,27 @@ package Sem_Prag is
    procedure Analyze_Global_In_Decl_Part (N : Node_Id);
    --  Perform full analysis of delayed pragma Global
 
-   procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id);
-   --  Special analyze routine for precondition/postcondition pragma that
-   --  appears within a declarative part where the pragma is associated
-   --  with a subprogram specification. N is the pragma node, and S is the
-   --  entity for the related subprogram. This procedure does a preanalysis
-   --  of the expressions in the pragma as "spec expressions" (see section
-   --  in Sem "Handling of Default and Per-Object Expressions...").
+   procedure Analyze_Pre_Post_Condition_In_Decl_Part
+     (Prag    : Node_Id;
+      Subp_Id : Entity_Id);
+   --  Perform preanalysis of a [refined] precondition or postcondition that
+   --  appears on a subprogram declaration or body [stub]. Prag denotes the
+   --  pragma, Subp_Id is the entity of the related subprogram. The preanalysis
+   --  of the expression is done as "spec expression" (see section "Handling
+   --  of Default and Per-Object Expressions in Sem).
+
+   procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
+   --  Preform full analysis of delayed pragma Refined_Depends
+
+   procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
+   --  Perform full analysis of delayed pragma Refined_Global
 
    procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
-   --  Special analyze routine for contract-case and test-case pragmas that
-   --  appears within a declarative part where the pragma is associated with
-   --  a subprogram specification. N is the pragma node, and S is the entity
-   --  for the related subprogram. This procedure does a preanalysis of the
-   --  expressions in the pragma as "spec expressions" (see section in Sem
-   --  "Handling of Default and Per-Object Expressions...").
+   --  Perform preanalysis of pragma Test_Case that applies to a subprogram
+   --  declaration. Parameter N denotes the pragma, S is the entity of the
+   --  related subprogram. The preanalysis of the expression is done as "spec
+   --  expression" (see section "Handling of Default and Per-Object Expressions
+   --  in Sem).
 
    procedure Check_Applicable_Policy (N : Node_Id);
    --  N is either an N_Aspect or an N_Pragma node. There are two cases. If

gcc/ada/sem_util.adb

@@ -212,25 +212,25 @@ package body Sem_Util is
    -- Add_Contract_Item --
    -----------------------
 
-   procedure Add_Contract_Item (Item : Node_Id; Subp_Id : Entity_Id) is
+   procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is
       Items : constant Node_Id := Contract (Subp_Id);
       Nam   : Name_Id;
 
    begin
-      if Present (Items) and then Nkind (Item) = N_Pragma then
-         Nam := Pragma_Name (Item);
+      --  The related subprogram [body] must have a contract and the item to be
+      --  added must be a pragma.
 
-         if Nam_In (Nam, Name_Precondition, Name_Postcondition) then
-            Set_Next_Pragma (Item, Pre_Post_Conditions (Items));
-            Set_Pre_Post_Conditions (Items, Item);
+      pragma Assert (Present (Items));
+      pragma Assert (Nkind (Prag) = N_Pragma);
 
-         elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then
-            Set_Next_Pragma (Item, Contract_Test_Cases (Items));
-            Set_Contract_Test_Cases (Items, Item);
+      Nam := Pragma_Name (Prag);
 
-         elsif Nam_In (Nam, Name_Depends, Name_Global) then
-            Set_Next_Pragma (Item, Classifications (Items));
-            Set_Classifications (Items, Item);
+      --  Contract items related to subprogram bodies
+
+      if Ekind (Subp_Id) = E_Subprogram_Body then
+         if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
+            Set_Next_Pragma (Prag, Classifications (Items));
+            Set_Classifications (Items, Prag);
 
          --  The pragma is not a proper contract item
 
@@ -238,10 +238,26 @@ package body Sem_Util is
             raise Program_Error;
          end if;
 
-      --  The subprogram has not been properly decorated or the item is illegal
+      --  Contract items related to subprogram declarations
 
       else
-         raise Program_Error;
+         if Nam_In (Nam, Name_Precondition, Name_Postcondition) then
+            Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
+            Set_Pre_Post_Conditions (Items, Prag);
+
+         elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then
+            Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
+            Set_Contract_Test_Cases (Items, Prag);
+
+         elsif Nam_In (Nam, Name_Depends, Name_Global) then
+            Set_Next_Pragma (Prag, Classifications (Items));
+            Set_Classifications (Items, Prag);
+
+         --  The pragma is not a proper contract item
+
+         else
+            raise Program_Error;
+         end if;
       end if;
    end Add_Contract_Item;
 

gcc/ada/sem_util.ads

@@ -43,10 +43,17 @@ package Sem_Util is
    --  Add A to the list of access types to process when expanding the
    --  freeze node of E.
 
-   procedure Add_Contract_Item (Item : Node_Id; Subp_Id : Entity_Id);
-   --  Add a contract item (pragma Precondition, Postcondition, Test_Case,
-   --  Contract_Cases, Global, Depends) to the contract of a subprogram. Item
-   --  denotes a pragma and Subp_Id is the related subprogram.
+   procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id);
+   --  Add one of the following contract item to the contract of a subprogram.
+   --  Prag denotes a pragma and Subp_Id is the related subprogram [body].
+   --    Contract_Cases
+   --    Depends
+   --    Global
+   --    Postcondition
+   --    Precondition
+   --    Refined_Depends
+   --    Refined_Global
+   --    Test_Case
 
    procedure Add_Global_Declaration (N : Node_Id);
    --  These procedures adds a declaration N at the library level, to be

gcc/ada/sinfo.ads

@@ -7143,11 +7143,10 @@ package Sinfo is
       --------------
 
       --  This node is used to hold the various parts of an entry or subprogram
-      --  contract, consisting in pre- and postconditions on the one hand, and
-      --  test-cases on the other hand.
+      --  [body] contract, consisting of precondition, postconditions, contract
+      --  cases, test cases and global dependencies.
 
-      --  It is referenced from an entry, a subprogram or a generic subprogram
-      --  entity.
+      --  The node appears in an entry and [generic] subprogram [body] entity.
 
       --  Sprint syntax:  <none> as the node should not appear in the tree, but
       --                  only attached to an entry or [generic] subprogram
@@ -7160,9 +7159,10 @@ package Sinfo is
       --  Classifications (Node3) (set to Empty if none)
 
       --  Pre_Post_Conditions contains a collection of pragmas that correspond
-      --  to pre- and postconditions associated with an entry or a subprogram.
-      --  The pragmas can either come from source or be the byproduct of aspect
-      --  expansion. The ordering in the list is in LIFO fashion.
+      --  to pre- and postconditions associated with an entry or a subprogram
+      --  [body or stub]. The pragmas can either come from source or be the
+      --  byproduct of aspect expansion. The ordering in the list is in LIFO
+      --  fashion.
 
       --  Note that there might be multiple preconditions or postconditions
       --  in this list, either because they come from separate pragmas in the
@@ -7175,8 +7175,8 @@ package Sinfo is
 
       --  Classifications contains pragmas that either categorize subprogram
       --  inputs and outputs or establish dependencies between them. Currently
-      --  pragmas Depends and Global are stored in this list. The ordering is
-      --  in LIFO fashion.
+      --  pragmas Depends, Global, Refined_Depends and Refined_Global are
+      --  stored in this list. The ordering is in LIFO fashion.
 
       -------------------
       -- Expanded_Name --

gcc/ada/snames.ads-tmpl

@@ -580,6 +580,8 @@ 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_Depends                : constant Name_Id := N + $; -- GNAT
+   Name_Refined_Global                 : 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
@@ -1865,6 +1867,8 @@ package Snames is
       Pragma_Pure_05,
       Pragma_Pure_12,
       Pragma_Pure_Function,
+      Pragma_Refined_Depends,
+      Pragma_Refined_Global,
       Pragma_Refined_Post,
       Pragma_Refined_Pre,
       Pragma_Relative_Deadline,

gcc/ada/types.ads

@@ -172,7 +172,7 @@ package Types is
    for Physical_Line_Number'Size use 32;
    --  Line number type, used for storing physical line numbers (i.e. line
    --  numbers in the physical file being compiled, unaffected by the presence
-   --  of source reference pragmas.
+   --  of source reference pragmas).
 
    type Column_Number is range 0 .. 32767;
    for Column_Number'Size use 16;