[multiple changes]

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb Add an entry for entry bodies in table
	Has_Aspect_Specifications_Flag.
	(Aspects_On_Body_Or_Stub_OK): Entry bodies now allow for certain
	aspects.
	* contracts.adb (Add_Contract_Items): Code cleanup. Add
	processing for entry bodies, entry declarations and task units.
	(Analyze_Subprogram_Body_Contract): Renamed
	to Analyze_Entry_Or_Subprogram_Body_Contract. Do not
	analyze the contract of an entry body unless annotating the
	original tree.
	(Analyze_Subprogram_Contract): Renamed to
	Analyze_Entry_Or_Subprogram_Contract.  Do not analyze the contract
	of an entry declaration unless annotating the original tree.
	(Analyze_Task_Contract): New routine.
	* contracts.ads (Add_Contract_Item): Update the comment on usage.
	(Analyze_Package_Body_Contract): Update comment on usage.
	(Analyze_Package_Contract): Update the comment on usage.
	(Analyze_Subprogram_Body_Contract): Renamed to
	Analyze_Entry_Or_Subprogram_Body_Contract.
	(Analyze_Subprogram_Body_Stub_Contract): Update the comment on usage.
	(Analyze_Subprogram_Contract): Renamed to
	Analyze_Entry_Or_Subprogram_Contract.
	(Analyze_Task_Contract): New routine.
	* einfo.adb (Contract): Restructure the assertion to include
	entries and task units.
	(SPARK_Pragma): This attribute now applies to operators.
	(SPARK_Pragma_Inherited): This flag now applies to operators.
	(Set_Contract): Restructure the assertion to include entries and task
	units.
	(Set_SPARK_Pragma): This attribute now applies to operators.
	(Set_SPARK_Pragma_Inherited): This flag now applies to operators.
	(Write_Field34_Name): Write out all Ekinds that have a contract.
	(Write_Field40_Name): SPARK_Pragma now applies to operators.
	* einfo.ads: Update the documentation of attribute Contract along
	with usage in nodes.  Update the documentation of attributes
	SPARK_Pragma and SPARK_Pragma_Inherited.
	* exp_ch6.adb (Freeze_Subprogram): Update the call to
	Analyze_Subprogram_Contract.
	* par-ch9.adb (P_Entry_Barrier): Do not parse keyword "is" as it
	is not part of the entry barrier production.
	(P_Entry_Body): Parse the optional aspect specifications. Diagnose
	misplaced aspects.
	* sem_attr.adb (Analyze_Attribute_Old_Result): Update the call
	to Find_Related_Subprogram_Or_Body.
	* sem_aux.adb (Unit_Declaration_Node) Add an entry for entry
	declarations and bodies.
	* sem_ch3.adb (Analyze_Declarations): Analyze the contracts of
	entry declarations, entry bodies and task units.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	Update the call to Analyze_Subprogram_Body_Contract.
	(Analyze_Subprogram_Body_Helper): Update the call to
	Analyze_Subprogram_Body_Contract.
	* sem_ch9.adb (Analyze_Entry_Body): Analyze the aspect
	specifications and the contract.
	* sem_ch10.adb (Analyze_Compilation_Unit): Update the call to
	Analyze_Subprogram_Contract.
	* sem_ch12.adb (Save_References_In_Pragma): Update the call to
	Find_Related_Subprogram_Or_Body.
	* sem_ch13.adb (Analyze_Aspects_On_Body_Or_Stub): Use
	Unique_Defining_Entity rather than rummaging around in nodes.
	(Diagnose_Misplaced_Aspects): Update comment on usage. Update the
	error messages to accomondate the increasing number of contexts.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Update the call to Find_Related_Subprogram_Or_Body.
	(Analyze_Depends_Global): Update the call to
	Find_Related_Subprogram_Or_Body. Add processing for entry
	declarations.
	(Analyze_Depends_In_Decl_Part): Update the call
	to Find_Related_Subprogram_Or_Body. Task units have no formal
	parameters to install.	(Analyze_Global_In_Decl_Part): Update
	the call to Find_Related_Subprogram_Or_Body. Task units have no
	formal parameters to install.
	(Analyze_Global_Item): Use Fix_Msg to handle the increasing number of
	contexts.
	(Analyze_Pragma): Update the call to Find_Related_Subprogram_Or_Body.
	Perform full analysis when various pragmas appear in an entry body.
	(Analyze_Pre_Post_Condition): Update the call to
	Find_Related_Subprogram_Or_Body. Perform full analysis when the pragma
	appears in an entry body.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Update the call to
	Find_Related_Subprogram_Or_Body.
	(Analyze_Refined_Depends_Global_Post): Update
	the call to Find_Related_Subprogram_Or_Body. Use
	Fix_Msg to handle the increasing number of contexts.
	(Analyze_Refined_Depends_In_Decl_Part): Update
	the call to Find_Related_Subprogram_Or_Body. Use
	Unique_Defining_Entity to obtain the entity of the
	spec. Use Fix_Msg to handle the increasing number of contexts.
	(Analyze_Refined_Global_In_Decl_Part): Update the call to
	Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain
	the entity of the spec. Use Fix_Msg to handle the increasing number of
	contexts.
	(Analyze_Test_Case_In_Decl_Part): Update the call to
	Find_Related_Subprogram_Or_Body.
	(Check_Dependency_Clause): Use Fix_Msg to handle the increasing number
	of contexts.
	(Check_Mode_Restriction_In_Enclosing_Context): Use
	Fix_Msg to handle the increasing number of contexts.
	(Collect_Subprogram_Inputs_Outputs): Use the refined
	versions of the pragmas when the context is an entry body or
	a task body.
	(Find_Related_Subprogram_Or_Body): Renamed to
	Find_Related_Declaration_Or_Body.  Add processing for entries
	and task units.
	(Fix_Msg): New routine.
	(Role_Error): Use Fix_Msg to handle the increasing number of contexts.
	* sem_prag.ads (Find_Related_Subprogram_Or_Body): Renamed to
	Find_Related_Declaration_Or_Body.  Update the comment on usage.
	* sem_util.adb (Is_Entry_Body): New routine.
	(Is_Entry_Declaration): New routine.
	* sem_util.ads (Is_Entry_Body): New routine.
	(Is_Entry_Declaration): New routine.

2015-10-26  Ed Schonberg  <schonberg@adacore.com>

	* inline.adb (Has_Excluded_Declaration): A subtype declaration
	with a predicate aspect generates a subprogram, and therefore
	prevents the inlining of the enclosing subprogram.
	* osint.ads: Fix typo.

From-SVN: r229333

1 files changed, 351 insertions, 232 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index e41ae20..87c39fb 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -121,7 +121,7 @@ package body Contracts is
          Set_Contract (Id, Items);
       end if;
 
-      --  Contract items related to constants. Applicable pragmas are:
+      --  Constants, the applicable pragmas are:
       --    Part_Of
 
       if Ekind (Id) = E_Constant then
@@ -134,37 +134,17 @@ package body Contracts is
             raise Program_Error;
          end if;
 
-      --  Contract items related to [generic] packages or instantiations. The
-      --  applicable pragmas are:
-      --    Abstract_States
-      --    Initial_Condition
-      --    Initializes
-      --    Part_Of (instantiation only)
-
-      elsif Ekind_In (Id, E_Generic_Package, E_Package) then
-         if Nam_In (Prag_Nam, Name_Abstract_State,
-                              Name_Initial_Condition,
-                              Name_Initializes)
-         then
-            Add_Classification;
-
-         --  Indicator Part_Of must be associated with a package instantiation
+      --  Entry bodies, the applicable pragmas are:
+      --    Refined_Depends
+      --    Refined_Global
+      --    Refined_Post
 
-         elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
+      elsif Is_Entry_Body (Id) then
+         if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
             Add_Classification;
 
-         --  The pragma is not a proper contract item
-
-         else
-            raise Program_Error;
-         end if;
-
-      --  Contract items related to package bodies. The applicable pragmas are:
-      --    Refined_States
-
-      elsif Ekind (Id) = E_Package_Body then
-         if Prag_Nam = Name_Refined_State then
-            Add_Classification;
+         elsif Prag_Nam = Name_Refined_Post then
+            Add_Pre_Post_Condition;
 
          --  The pragma is not a proper contract item
 
@@ -172,8 +152,7 @@ package body Contracts is
             raise Program_Error;
          end if;
 
-      --  Contract items related to subprogram or entry declarations. The
-      --  applicable pragmas are:
+      --  Entry or subprogram declarations, the applicable pragmas are:
       --    Contract_Cases
       --    Depends
       --    Extensions_Visible
@@ -183,9 +162,11 @@ package body Contracts is
       --    Test_Case
       --    Volatile_Function
 
-      elsif Ekind_In (Id, E_Entry, E_Entry_Family)
-        or else Is_Generic_Subprogram (Id)
-        or else Is_Subprogram (Id)
+      elsif Is_Entry_Declaration (Id)
+        or else Ekind_In (Id, E_Function,
+                              E_Generic_Function,
+                              E_Generic_Procedure,
+                              E_Procedure)
       then
          if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
             Add_Pre_Post_Condition;
@@ -210,7 +191,44 @@ package body Contracts is
             raise Program_Error;
          end if;
 
-      --  Contract items related to subprogram bodies. Applicable pragmas are:
+      --  Packages or instantiations, the applicable pragmas are:
+      --    Abstract_States
+      --    Initial_Condition
+      --    Initializes
+      --    Part_Of (instantiation only)
+
+      elsif Ekind_In (Id, E_Generic_Package, E_Package) then
+         if Nam_In (Prag_Nam, Name_Abstract_State,
+                              Name_Initial_Condition,
+                              Name_Initializes)
+         then
+            Add_Classification;
+
+         --  Indicator Part_Of must be associated with a package instantiation
+
+         elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
+            Add_Classification;
+
+         --  The pragma is not a proper contract item
+
+         else
+            raise Program_Error;
+         end if;
+
+      --  Package bodies, the applicable pragmas are:
+      --    Refined_States
+
+      elsif Ekind (Id) = E_Package_Body then
+         if Prag_Nam = Name_Refined_State then
+            Add_Classification;
+
+         --  The pragma is not a proper contract item
+
+         else
+            raise Program_Error;
+         end if;
+
+      --  Subprogram bodies, the applicable pragmas are:
       --    Postcondition
       --    Precondition
       --    Refined_Depends
@@ -233,7 +251,35 @@ package body Contracts is
             raise Program_Error;
          end if;
 
-      --  Contract items related to variables. Applicable pragmas are:
+      --  Task bodies, the applicable pragmas are:
+      --    Refined_Depends
+      --    Refined_Global
+
+      elsif Ekind (Id) = E_Task_Body then
+         if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
+            Add_Classification;
+
+         --  The pragma is not a proper contract item
+
+         else
+            raise Program_Error;
+         end if;
+
+      --  Task units, the applicable pragmas are:
+      --    Depends
+      --    Global
+
+      elsif Ekind (Id) = E_Task_Type then
+         if Nam_In (Prag_Nam, Name_Depends, Name_Global) then
+            Add_Classification;
+
+         --  The pragma is not a proper contract item
+
+         else
+            raise Program_Error;
+         end if;
+
+      --  Variables, the applicable pragmas are:
       --    Async_Readers
       --    Async_Writers
       --    Constant_After_Elaboration
@@ -284,6 +330,231 @@ package body Contracts is
       end loop;
    end Analyze_Enclosing_Package_Body_Contract;
 
+   -----------------------------------------------
+   -- Analyze_Entry_Or_Subprogram_Body_Contract --
+   -----------------------------------------------
+
+   procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
+      Body_Decl : constant Node_Id   := Unit_Declaration_Node (Body_Id);
+      Items     : constant Node_Id   := Contract (Body_Id);
+      Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
+      Mode      : SPARK_Mode_Type;
+
+   begin
+      --  When a subprogram body declaration is illegal, its defining entity is
+      --  left unanalyzed. There is nothing left to do in this case because the
+      --  body lacks a contract, or even a proper Ekind.
+
+      if Ekind (Body_Id) = E_Void then
+         return;
+
+      --  Do not analyze the contract of an entry body unless annotating the
+      --  original tree. It is preferable to analyze the contract after the
+      --  entry body has been transformed into a subprogram body to properly
+      --  handle references to unpacked formals.
+
+      elsif Ekind_In (Body_Id, E_Entry, E_Entry_Family)
+        and then not ASIS_Mode
+        and then not GNATprove_Mode
+      then
+         return;
+
+      --  Do not analyze a contract multiple times
+
+      elsif Present (Items) then
+         if Analyzed (Items) then
+            return;
+         else
+            Set_Analyzed (Items);
+         end if;
+      end if;
+
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related subprogram body.
+
+      Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
+      --  Ensure that the contract cases or postconditions mention 'Result or
+      --  define a post-state.
+
+      Check_Result_And_Post_State (Body_Id);
+
+      --  A stand-alone nonvolatile function body cannot have an effectively
+      --  volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
+      --  check is relevant only when SPARK_Mode is on, as it is not a standard
+      --  legality rule. The check is performed here because Volatile_Function
+      --  is processed after the analysis of the related subprogram body.
+
+      if SPARK_Mode = On
+        and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+        and then not Is_Volatile_Function (Body_Id)
+      then
+         Check_Nonvolatile_Function_Profile (Body_Id);
+      end if;
+
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
+      Restore_SPARK_Mode (Mode);
+
+      --  Capture all global references in a generic subprogram body now that
+      --  the contract has been analyzed.
+
+      if Is_Generic_Declaration_Or_Body (Body_Decl) then
+         Save_Global_References_In_Contract
+           (Templ  => Original_Node (Body_Decl),
+            Gen_Id => Spec_Id);
+      end if;
+
+      --  Deal with preconditions, [refined] postconditions, Contract_Cases,
+      --  invariants and predicates associated with body and its spec. Do not
+      --  expand the contract of subprogram body stubs.
+
+      if Nkind (Body_Decl) = N_Subprogram_Body then
+         Expand_Subprogram_Contract (Body_Id);
+      end if;
+   end Analyze_Entry_Or_Subprogram_Body_Contract;
+
+   ------------------------------------------
+   -- Analyze_Entry_Or_Subprogram_Contract --
+   ------------------------------------------
+
+   procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is
+      Items     : constant Node_Id := Contract (Subp_Id);
+      Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+      Depends   : Node_Id := Empty;
+      Global    : Node_Id := Empty;
+      Mode      : SPARK_Mode_Type;
+      Prag      : Node_Id;
+      Prag_Nam  : Name_Id;
+
+   begin
+      --  Do not analyze the contract of an entry declaration unless annotating
+      --  the original tree. It is preferable to analyze the contract after the
+      --  entry declaration has been transformed into a subprogram declaration
+      --  to properly handle references to unpacked formals.
+
+      if Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
+        and then not ASIS_Mode
+        and then not GNATprove_Mode
+      then
+         return;
+
+      --  Do not analyze a contract multiple times
+
+      elsif Present (Items) then
+         if Analyzed (Items) then
+            return;
+         else
+            Set_Analyzed (Items);
+         end if;
+      end if;
+
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related subprogram body.
+
+      Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+
+      --  All subprograms carry a contract, but for some it is not significant
+      --  and should not be processed.
+
+      if not Has_Significant_Contract (Subp_Id) then
+         null;
+
+      elsif Present (Items) then
+
+         --  Analyze pre- and postconditions
+
+         Prag := Pre_Post_Conditions (Items);
+         while Present (Prag) loop
+            Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
+            Prag := Next_Pragma (Prag);
+         end loop;
+
+         --  Analyze contract-cases and test-cases
+
+         Prag := Contract_Test_Cases (Items);
+         while Present (Prag) loop
+            Prag_Nam := Pragma_Name (Prag);
+
+            if Prag_Nam = Name_Contract_Cases then
+               Analyze_Contract_Cases_In_Decl_Part (Prag);
+            else
+               pragma Assert (Prag_Nam = Name_Test_Case);
+               Analyze_Test_Case_In_Decl_Part (Prag);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+
+         --  Analyze classification pragmas
+
+         Prag := Classifications (Items);
+         while Present (Prag) loop
+            Prag_Nam := Pragma_Name (Prag);
+
+            if Prag_Nam = Name_Depends then
+               Depends := Prag;
+
+            elsif Prag_Nam = Name_Global then
+               Global := Prag;
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+
+         --  Analyze Global first, as Depends may mention items classified in
+         --  the global categorization.
+
+         if Present (Global) then
+            Analyze_Global_In_Decl_Part (Global);
+         end if;
+
+         --  Depends must be analyzed after Global in order to see the modes of
+         --  all global items.
+
+         if Present (Depends) then
+            Analyze_Depends_In_Decl_Part (Depends);
+         end if;
+
+         --  Ensure that the contract cases or postconditions mention 'Result
+         --  or define a post-state.
+
+         Check_Result_And_Post_State (Subp_Id);
+      end if;
+
+      --  A nonvolatile function cannot have an effectively volatile formal
+      --  parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
+      --  only when SPARK_Mode is on, as it is not a standard legality rule.
+      --  The check is performed here because pragma Volatile_Function is
+      --  processed after the analysis of the related subprogram declaration.
+
+      if SPARK_Mode = On
+        and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+        and then not Is_Volatile_Function (Subp_Id)
+      then
+         Check_Nonvolatile_Function_Profile (Subp_Id);
+      end if;
+
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
+      Restore_SPARK_Mode (Mode);
+
+      --  Capture all global references in a generic subprogram now that the
+      --  contract has been analyzed.
+
+      if Is_Generic_Declaration_Or_Body (Subp_Decl) then
+         Save_Global_References_In_Contract
+           (Templ  => Original_Node (Subp_Decl),
+            Gen_Id => Subp_Id);
+      end if;
+   end Analyze_Entry_Or_Subprogram_Contract;
+
    -----------------------------
    -- Analyze_Object_Contract --
    -----------------------------
@@ -617,94 +888,47 @@ package body Contracts is
       end if;
    end Analyze_Package_Contract;
 
-   --------------------------------------
-   -- Analyze_Subprogram_Body_Contract --
-   --------------------------------------
+   -------------------------------------------
+   -- Analyze_Subprogram_Body_Stub_Contract --
+   -------------------------------------------
 
-   procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
-      Body_Decl : constant Node_Id   := Unit_Declaration_Node (Body_Id);
-      Items     : constant Node_Id   := Contract (Body_Id);
-      Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
-      Mode      : SPARK_Mode_Type;
+   procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
+      Stub_Decl : constant Node_Id   := Parent (Parent (Stub_Id));
+      Spec_Id   : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
 
    begin
-      --  When a subprogram body declaration is illegal, its defining entity is
-      --  left unanalyzed. There is nothing left to do in this case because the
-      --  body lacks a contract, or even a proper Ekind.
-
-      if Ekind (Body_Id) = E_Void then
-         return;
-
-      --  Do not analyze a contract multiple times
-
-      elsif Present (Items) then
-         if Analyzed (Items) then
-            return;
-         else
-            Set_Analyzed (Items);
-         end if;
-      end if;
-
-      --  Due to the timing of contract analysis, delayed pragmas may be
-      --  subject to the wrong SPARK_Mode, usually that of the enclosing
-      --  context. To remedy this, restore the original SPARK_Mode of the
-      --  related subprogram body.
-
-      Save_SPARK_Mode_And_Set (Body_Id, Mode);
-
-      --  Ensure that the contract cases or postconditions mention 'Result or
-      --  define a post-state.
-
-      Check_Result_And_Post_State (Body_Id);
-
-      --  A stand-alone nonvolatile function body cannot have an effectively
-      --  volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
-      --  check is relevant only when SPARK_Mode is on, as it is not a standard
-      --  legality rule. The check is performed here because Volatile_Function
-      --  is processed after the analysis of the related subprogram body.
-
-      if SPARK_Mode = On
-        and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
-        and then not Is_Volatile_Function (Body_Id)
-      then
-         Check_Nonvolatile_Function_Profile (Body_Id);
-      end if;
-
-      --  Restore the SPARK_Mode of the enclosing context after all delayed
-      --  pragmas have been analyzed.
-
-      Restore_SPARK_Mode (Mode);
+      --  A subprogram body stub may act as its own spec or as the completion
+      --  of a previous declaration. Depending on the context, the contract of
+      --  the stub may contain two sets of pragmas.
 
-      --  Capture all global references in a generic subprogram body now that
-      --  the contract has been analyzed.
+      --  The stub is a completion, the applicable pragmas are:
+      --    Refined_Depends
+      --    Refined_Global
 
-      if Is_Generic_Declaration_Or_Body (Body_Decl) then
-         Save_Global_References_In_Contract
-           (Templ  => Original_Node (Body_Decl),
-            Gen_Id => Spec_Id);
-      end if;
+      if Present (Spec_Id) then
+         Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
 
-      --  Deal with preconditions, [refined] postconditions, Contract_Cases,
-      --  invariants and predicates associated with body and its spec. Do not
-      --  expand the contract of subprogram body stubs.
+      --  The stub acts as its own spec, the applicable pragmas are:
+      --    Contract_Cases
+      --    Depends
+      --    Global
+      --    Postcondition
+      --    Precondition
+      --    Test_Case
 
-      if Nkind (Body_Decl) = N_Subprogram_Body then
-         Expand_Subprogram_Contract (Body_Id);
+      else
+         Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
       end if;
-   end Analyze_Subprogram_Body_Contract;
+   end Analyze_Subprogram_Body_Stub_Contract;
 
-   ---------------------------------
-   -- Analyze_Subprogram_Contract --
-   ---------------------------------
+   ---------------------------
+   -- Analyze_Task_Contract --
+   ---------------------------
 
-   procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
-      Items     : constant Node_Id := Contract (Subp_Id);
-      Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
-      Depends   : Node_Id := Empty;
-      Global    : Node_Id := Empty;
-      Mode      : SPARK_Mode_Type;
-      Prag      : Node_Id;
-      Prag_Nam  : Name_Id;
+   procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
+      Items : constant Node_Id := Contract (Task_Id);
+      Mode  : SPARK_Mode_Type;
+      Prag  : Node_Id;
 
    begin
       --  Do not analyze a contract multiple times
@@ -722,136 +946,31 @@ package body Contracts is
       --  context. To remedy this, restore the original SPARK_Mode of the
       --  related subprogram body.
 
-      Save_SPARK_Mode_And_Set (Subp_Id, Mode);
-
-      --  All subprograms carry a contract, but for some it is not significant
-      --  and should not be processed.
-
-      if not Has_Significant_Contract (Subp_Id) then
-         null;
-
-      elsif Present (Items) then
-
-         --  Analyze pre- and postconditions
-
-         Prag := Pre_Post_Conditions (Items);
-         while Present (Prag) loop
-            Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
-            Prag := Next_Pragma (Prag);
-         end loop;
-
-         --  Analyze contract-cases and test-cases
-
-         Prag := Contract_Test_Cases (Items);
-         while Present (Prag) loop
-            Prag_Nam := Pragma_Name (Prag);
-
-            if Prag_Nam = Name_Contract_Cases then
-               Analyze_Contract_Cases_In_Decl_Part (Prag);
-            else
-               pragma Assert (Prag_Nam = Name_Test_Case);
-               Analyze_Test_Case_In_Decl_Part (Prag);
-            end if;
-
-            Prag := Next_Pragma (Prag);
-         end loop;
-
-         --  Analyze classification pragmas
-
-         Prag := Classifications (Items);
-         while Present (Prag) loop
-            Prag_Nam := Pragma_Name (Prag);
-
-            if Prag_Nam = Name_Depends then
-               Depends := Prag;
-
-            elsif Prag_Nam = Name_Global then
-               Global := Prag;
-            end if;
-
-            Prag := Next_Pragma (Prag);
-         end loop;
-
-         --  Analyze Global first, as Depends may mention items classified in
-         --  the global categorization.
-
-         if Present (Global) then
-            Analyze_Global_In_Decl_Part (Global);
-         end if;
-
-         --  Depends must be analyzed after Global in order to see the modes of
-         --  all global items.
+      Save_SPARK_Mode_And_Set (Task_Id, Mode);
 
-         if Present (Depends) then
-            Analyze_Depends_In_Decl_Part (Depends);
-         end if;
+      --  Analyze Global first, as Depends may mention items classified in the
+      --  global categorization.
 
-         --  Ensure that the contract cases or postconditions mention 'Result
-         --  or define a post-state.
+      Prag := Get_Pragma (Task_Id, Pragma_Global);
 
-         Check_Result_And_Post_State (Subp_Id);
+      if Present (Prag) then
+         Analyze_Global_In_Decl_Part (Prag);
       end if;
 
-      --  A nonvolatile function cannot have an effectively volatile formal
-      --  parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
-      --  only when SPARK_Mode is on, as it is not a standard legality rule.
-      --  The check is performed here because pragma Volatile_Function is
-      --  processed after the analysis of the related subprogram declaration.
+      --  Depends must be analyzed after Global in order to see the modes of
+      --  all global items.
 
-      if SPARK_Mode = On
-        and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
-        and then not Is_Volatile_Function (Subp_Id)
-      then
-         Check_Nonvolatile_Function_Profile (Subp_Id);
+      Prag := Get_Pragma (Task_Id, Pragma_Depends);
+
+      if Present (Prag) then
+         Analyze_Depends_In_Decl_Part (Prag);
       end if;
 
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
       Restore_SPARK_Mode (Mode);
-
-      --  Capture all global references in a generic subprogram now that the
-      --  contract has been analyzed.
-
-      if Is_Generic_Declaration_Or_Body (Subp_Decl) then
-         Save_Global_References_In_Contract
-           (Templ  => Original_Node (Subp_Decl),
-            Gen_Id => Subp_Id);
-      end if;
-   end Analyze_Subprogram_Contract;
-
-   -------------------------------------------
-   -- Analyze_Subprogram_Body_Stub_Contract --
-   -------------------------------------------
-
-   procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
-      Stub_Decl : constant Node_Id   := Parent (Parent (Stub_Id));
-      Spec_Id   : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
-
-   begin
-      --  A subprogram body stub may act as its own spec or as the completion
-      --  of a previous declaration. Depending on the context, the contract of
-      --  the stub may contain two sets of pragmas.
-
-      --  The stub is a completion, the applicable pragmas are:
-      --    Refined_Depends
-      --    Refined_Global
-
-      if Present (Spec_Id) then
-         Analyze_Subprogram_Body_Contract (Stub_Id);
-
-      --  The stub acts as its own spec, the applicable pragmas are:
-      --    Contract_Cases
-      --    Depends
-      --    Global
-      --    Postcondition
-      --    Precondition
-      --    Test_Case
-
-      else
-         Analyze_Subprogram_Contract (Stub_Id);
-      end if;
-   end Analyze_Subprogram_Body_Stub_Contract;
+   end Analyze_Task_Contract;
 
    -----------------------------
    -- Create_Generic_Contract --