Index: einfo.adb
===================================================================
--- einfo.adb	(revision 230536)
+++ einfo.adb	(working copy)
@@ -95,13 +95,14 @@
    --    Normalized_Position_Max         Uint10
    --    Part_Of_Constituents            Elist10
 
+   --    Block_Node                      Node11
    --    Component_Bit_Offset            Uint11
    --    Full_View                       Node11
    --    Entry_Component                 Node11
    --    Enumeration_Pos                 Uint11
    --    Generic_Homonym                 Node11
+   --    Part_Of_References              Elist11
    --    Protected_Body_Subprogram       Node11
-   --    Block_Node                      Node11
 
    --    Barrier_Function                Node12
    --    Enumeration_Rep                 Uint12
@@ -2861,6 +2862,12 @@
       return Elist10 (Id);
    end Part_Of_Constituents;
 
+   function Part_Of_References (Id : E) return L is
+   begin
+      pragma Assert (Ekind (Id) = E_Variable);
+      return Elist11 (Id);
+   end Part_Of_References;
+
    function Partial_View_Has_Unknown_Discr (Id : E) return B is
    begin
       pragma Assert (Is_Type (Id));
@@ -5897,6 +5904,12 @@
       Set_Elist10 (Id, V);
    end Set_Part_Of_Constituents;
 
+   procedure Set_Part_Of_References (Id : E; V : L) is
+   begin
+      pragma Assert (Ekind (Id) = E_Variable);
+      Set_Elist11 (Id, V);
+   end Set_Part_Of_References;
+
    procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Type (Id));
@@ -9363,10 +9376,13 @@
          when E_Generic_Package                            =>
             Write_Str ("Generic_Homonym");
 
-         when E_Function                                   |
-              E_Procedure                                  |
-              E_Entry                                      |
-              E_Entry_Family                               =>
+         when E_Variable                                   =>
+            Write_Str ("Part_Of_References");
+
+         when E_Entry                                      |
+              E_Entry_Family                               |
+              E_Function                                   |
+              E_Procedure                                  =>
             Write_Str ("Protected_Body_Subprogram");
 
          when others                                       =>
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 230536)
+++ einfo.ads	(working copy)
@@ -3696,6 +3696,12 @@
 --       constituents that are subject to indicator Part_Of (both aspect and
 --       option variants).
 
+--    Part_Of_References (Elist11)
+--       Present in variable entities. Contains all references to the variable
+--       when it is subject to pragma Part_Of. If the variable is a constituent
+--       of a single protected/task type, the references are examined as they
+--       must appear only within the type defintion and the corresponding body.
+
 --    Partial_View_Has_Unknown_Discr (Flag280)
 --       Present in all types. Set to Indicate that the partial view of a type
 --       has unknown discriminants. A default initialization of an object of
@@ -6431,6 +6437,7 @@
    --    Hiding_Loop_Variable                (Node8)
    --    Current_Value                       (Node9)
    --    Part_Of_Constituents                (Elist10)
+   --    Part_Of_References                  (Elist11)
    --    Esize                               (Uint12)
    --    Extra_Accessibility                 (Node13)
    --    Alignment                           (Uint14)
@@ -7089,6 +7096,7 @@
    function Packed_Array_Impl_Type              (Id : E) return E;
    function Parent_Subtype                      (Id : E) return E;
    function Part_Of_Constituents                (Id : E) return L;
+   function Part_Of_References                  (Id : E) return L;
    function Partial_View_Has_Unknown_Discr      (Id : E) return B;
    function Pending_Access_Types                (Id : E) return L;
    function Postconditions_Proc                 (Id : E) return E;
@@ -7756,6 +7764,7 @@
    procedure Set_Packed_Array_Impl_Type          (Id : E; V : E);
    procedure Set_Parent_Subtype                  (Id : E; V : E);
    procedure Set_Part_Of_Constituents            (Id : E; V : L);
+   procedure Set_Part_Of_References              (Id : E; V : L);
    procedure Set_Partial_View_Has_Unknown_Discr  (Id : E; V : B := True);
    procedure Set_Pending_Access_Types            (Id : E; V : L);
    procedure Set_Postconditions_Proc             (Id : E; V : E);
@@ -8582,6 +8591,7 @@
    pragma Inline (Parameter_Mode);
    pragma Inline (Parent_Subtype);
    pragma Inline (Part_Of_Constituents);
+   pragma Inline (Part_Of_References);
    pragma Inline (Partial_View_Has_Unknown_Discr);
    pragma Inline (Pending_Access_Types);
    pragma Inline (Postconditions_Proc);
@@ -9043,6 +9053,7 @@
    pragma Inline (Set_Packed_Array_Impl_Type);
    pragma Inline (Set_Parent_Subtype);
    pragma Inline (Set_Part_Of_Constituents);
+   pragma Inline (Set_Part_Of_References);
    pragma Inline (Set_Partial_View_Has_Unknown_Discr);
    pragma Inline (Set_Pending_Access_Types);
    pragma Inline (Set_Postconditions_Proc);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 230536)
+++ sem_prag.adb	(working copy)
@@ -957,6 +957,16 @@
 
                      if Ekind (Item_Id) = E_Abstract_State then
                         Append_New_Elmt (Item_Id, States_Seen);
+
+                     --  The variable may eventually become a constituent of a
+                     --  single protected/task type. Record the reference now
+                     --  and verify its legality when analyzing the contract of
+                     --  the variable (SPARK RM 9.3).
+
+                     elsif Ekind (Item_Id) = E_Variable then
+                        Record_Possible_Part_Of_Reference
+                          (Var_Id => Item_Id,
+                           Ref    => Item);
                      end if;
 
                      if Ekind_In (Item_Id, E_Abstract_State,
@@ -2209,6 +2219,16 @@
 
                if Ekind (Item_Id) = E_Abstract_State then
                   Append_New_Elmt (Item_Id, States_Seen);
+
+               --  The variable may eventually become a constituent of a single
+               --  protected/task type. Record the reference now and verify its
+               --  legality when analyzing the contract of the variable
+               --  (SPARK RM 9.3).
+
+               elsif Ekind (Item_Id) = E_Variable then
+                  Record_Possible_Part_Of_Reference
+                    (Var_Id => Item_Id,
+                     Ref    => Item);
                end if;
 
                if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
@@ -25452,6 +25472,17 @@
                   then
                      Match_Constituent (Constit_Id);
 
+                     --  The variable may eventually become a constituent of a
+                     --  single protected/task type. Record the reference now
+                     --  and verify its legality when analyzing the contract of
+                     --  the variable (SPARK RM 9.3).
+
+                     if Ekind (Constit_Id) = E_Variable then
+                        Record_Possible_Part_Of_Reference
+                          (Var_Id => Constit_Id,
+                           Ref    => Constit);
+                     end if;
+
                   --  Otherwise the constituent is illegal
 
                   else
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 230525)
+++ sem_util.adb	(working copy)
@@ -1916,6 +1916,126 @@
       end if;
    end Cannot_Raise_Constraint_Error;
 
+   -----------------------------
+   -- Check_Part_Of_Reference --
+   -----------------------------
+
+   procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id) is
+      Conc_Typ : constant Entity_Id := Encapsulating_State (Var_Id);
+      Decl     : Node_Id;
+      OK_Use   : Boolean := False;
+      Par      : Node_Id;
+      Prag_Nam : Name_Id;
+      Spec_Id  : Entity_Id;
+
+   begin
+      --  Traverse the parent chain looking for a suitable context for the
+      --  reference to the concurrent constituent.
+
+      Par := Parent (Ref);
+      while Present (Par) loop
+         if Nkind (Par) = N_Pragma then
+            Prag_Nam := Pragma_Name (Par);
+
+            --  A concurrent constituent is allowed to appear in pragmas
+            --  Initial_Condition and Initializes as this is part of the
+            --  elaboration checks for the constituent (SPARK RM 9.3).
+
+            if Nam_In (Prag_Nam, Name_Initial_Condition, Name_Initializes) then
+               OK_Use := True;
+               exit;
+
+            --  When the reference appears within pragma Depends or Global,
+            --  check whether the pragma applies to a single task type. Note
+            --  that the pragma is not encapsulated by the type definition,
+            --  but this is still a valid context.
+
+            elsif Nam_In (Prag_Nam, Name_Depends, Name_Global) then
+               Decl := Find_Related_Declaration_Or_Body (Par);
+
+               if Nkind (Decl) = N_Object_Declaration
+                 and then Defining_Entity (Decl) = Conc_Typ
+               then
+                  OK_Use := True;
+                  exit;
+               end if;
+            end if;
+
+         --  The reference appears somewhere in the definition of the single
+         --  protected/task type (SPARK RM 9.3).
+
+         elsif Nkind_In (Par, N_Single_Protected_Declaration,
+                              N_Single_Task_Declaration)
+           and then Defining_Entity (Par) = Conc_Typ
+         then
+            OK_Use := True;
+            exit;
+
+         --  The reference appears within the expanded declaration or the body
+         --  of the single protected/task type (SPARK RM 9.3).
+
+         elsif Nkind_In (Par, N_Protected_Body,
+                              N_Protected_Type_Declaration,
+                              N_Task_Body,
+                              N_Task_Type_Declaration)
+         then
+            Spec_Id := Unique_Defining_Entity (Par);
+
+            if Present (Anonymous_Object (Spec_Id))
+              and then Anonymous_Object (Spec_Id) = Conc_Typ
+            then
+               OK_Use := True;
+               exit;
+            end if;
+
+         --  The reference has been relocated within an internally generated
+         --  package or subprogram. Assume that the reference is legal as the
+         --  real check was already performed in the original context of the
+         --  reference.
+
+         elsif Nkind_In (Par, N_Package_Body,
+                              N_Package_Declaration,
+                              N_Subprogram_Body,
+                              N_Subprogram_Declaration)
+           and then not Comes_From_Source (Par)
+         then
+            OK_Use := True;
+            exit;
+
+         --  The reference has been relocated to an inlined body for GNATprove.
+         --  Assume that the reference is legal as the real check was already
+         --  performed in the original context of the reference.
+
+         elsif GNATprove_Mode
+           and then Nkind (Par) = N_Subprogram_Body
+           and then Chars (Defining_Entity (Par)) = Name_uParent
+         then
+            OK_Use := True;
+            exit;
+         end if;
+
+         Par := Parent (Par);
+      end loop;
+
+      --  The reference is illegal as it appears outside the definition or
+      --  body of the single protected/task type.
+
+      if not OK_Use then
+         Error_Msg_NE
+           ("reference to variable & cannot appear in this context",
+            Ref, Var_Id);
+         Error_Msg_Name_1 := Chars (Var_Id);
+
+         if Ekind (Conc_Typ) = E_Protected_Type then
+            Error_Msg_NE
+              ("\% is constituent of single protected type &", Ref, Conc_Typ);
+         else
+            Error_Msg_NE
+              ("\% is constituent of single task type &", Ref, Conc_Typ);
+         end if;
+      end if;
+   end Check_Part_Of_Reference;
+
    -----------------------------------------
    -- Check_Dynamically_Tagged_Expression --
    -----------------------------------------
@@ -17255,6 +17375,42 @@
       Set_Sloc (Endl, Loc);
    end Process_End_Label;
 
+   ---------------------------------------
+   -- Record_Possible_Part_Of_Reference --
+   ---------------------------------------
+
+   procedure Record_Possible_Part_Of_Reference
+     (Var_Id : Entity_Id;
+      Ref    : Node_Id)
+   is
+      Encap : constant Entity_Id := Encapsulating_State (Var_Id);
+      Refs  : Elist_Id;
+
+   begin
+      --  The variable is a constituent of a single protected/task type. Such
+      --  a variable acts as a component of the type and must appear within a
+      --  specific region (SPARK RM 9.3). Instead of recording the reference,
+      --  verify its legality now.
+
+      if Present (Encap) and then Is_Single_Concurrent_Object (Encap) then
+         Check_Part_Of_Reference (Var_Id, Ref);
+
+      --  The variable is subject to pragma Part_Of and may eventually become a
+      --  constituent of a single protected/task type. Record the reference to
+      --  verify its placement when the contract of the variable is analyzed.
+
+      elsif Present (Get_Pragma (Var_Id, Pragma_Part_Of)) then
+         Refs := Part_Of_References (Var_Id);
+
+         if No (Refs) then
+            Refs := New_Elmt_List;
+            Set_Part_Of_References (Var_Id, Refs);
+         end if;
+
+         Append_Elmt (Ref, Refs);
+      end if;
+   end Record_Possible_Part_Of_Reference;
+
    ----------------
    -- Referenced --
    ----------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 230525)
+++ sem_util.ads	(working copy)
@@ -252,6 +252,10 @@
    --  not necessarily mean that CE could be raised, but a response of True
    --  means that for sure CE cannot be raised.
 
+   procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
+   --  Verify the legality of reference Ref to variable Var_Id when the
+   --  variable is a constituent of a single protected/task type.
+
    procedure Check_Dynamically_Tagged_Expression
      (Expr        : Node_Id;
       Typ         : Entity_Id;
@@ -1922,6 +1926,14 @@
    --  parameter Ent gives the entity to which the End_Label refers,
    --  and to which cross-references are to be generated.
 
+   procedure Record_Possible_Part_Of_Reference
+     (Var_Id : Entity_Id;
+      Ref    : Node_Id);
+   --  Save reference Ref to variable Var_Id when the variable is subject to
+   --  pragma Part_Of. If the variable is known to be a constituent of a single
+   --  protected/task type, the legality of the reference is verified and the
+   --  save does not take place.
+
    function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean;
    --  Determine whether entity Id is referenced within expression Expr
 
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 230533)
+++ sem_res.adb	(working copy)
@@ -7240,6 +7240,15 @@
             then
                Check_Elab_Call (N);
             end if;
+
+            --  The variable may eventually become a constituent of a single
+            --  protected/task type. Record the reference now and verify its
+            --  legality when analyzing the contract of the variable
+            --  (SPARK RM 9.3).
+
+            if Ekind (E) = E_Variable then
+               Record_Possible_Part_Of_Reference (E, N);
+            end if;
          end if;
 
          --  A Ghost entity must appear in a specific context
Index: contracts.adb
===================================================================
--- contracts.adb	(revision 230536)
+++ contracts.adb	(working copy)
@@ -634,6 +634,7 @@
       Items        : Node_Id;
       Mode         : SPARK_Mode_Type;
       Prag         : Node_Id;
+      Ref_Elmt     : Elmt_Id;
       Restore_Mode : Boolean := False;
       Seen         : Boolean := False;
 
@@ -770,6 +771,23 @@
          if Present (Prag) then
             Analyze_Part_Of_In_Decl_Part (Prag);
 
+            --  The variable is a constituent of a single protected/task type
+            --  and behaves as a component of the type. Verify that references
+            --  to the variable occur within the definition or body of the type
+            --  (SPARK RM 9.3).
+
+            if Present (Encapsulating_State (Obj_Id))
+              and then Is_Single_Concurrent_Object
+                         (Encapsulating_State (Obj_Id))
+              and then Present (Part_Of_References (Obj_Id))
+            then
+               Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
+               while Present (Ref_Elmt) loop
+                  Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
+                  Next_Elmt (Ref_Elmt);
+               end loop;
+            end if;
+
          --  Otherwise check whether the lack of indicator Part_Of agrees with
          --  the placement of the variable with respect to the state space.
 
Index: atree.adb
===================================================================
--- atree.adb	(revision 230522)
+++ atree.adb	(working copy)
@@ -3093,6 +3093,17 @@
          end if;
       end Elist10;
 
+      function Elist11 (N : Node_Id) return Elist_Id is
+         pragma Assert (Nkind (N) in N_Entity);
+         Value : constant Union_Id := Nodes.Table (N + 1).Field11;
+      begin
+         if Value = 0 then
+            return No_Elist;
+         else
+            return Elist_Id (Value);
+         end if;
+      end Elist11;
+
       function Elist13 (N : Node_Id) return Elist_Id is
          pragma Assert (Nkind (N) in N_Entity);
          Value : constant Union_Id := Nodes.Table (N + 2).Field6;
@@ -5924,6 +5935,12 @@
          Nodes.Table (N + 1).Field10 := Union_Id (Val);
       end Set_Elist10;
 
+      procedure Set_Elist11 (N : Node_Id; Val : Elist_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 1).Field11 := Union_Id (Val);
+      end Set_Elist11;
+
       procedure Set_Elist13 (N : Node_Id; Val : Elist_Id) is
       begin
          pragma Assert (Nkind (N) in N_Entity);
Index: atree.ads
===================================================================
--- atree.ads	(revision 230522)
+++ atree.ads	(working copy)
@@ -1439,6 +1439,9 @@
       function Elist10 (N : Node_Id) return Elist_Id;
       pragma Inline (Elist10);
 
+      function Elist11 (N : Node_Id) return Elist_Id;
+      pragma Inline (Elist11);
+
       function Elist13 (N : Node_Id) return Elist_Id;
       pragma Inline (Elist13);
 
@@ -2799,6 +2802,9 @@
       procedure Set_Elist10 (N : Node_Id; Val : Elist_Id);
       pragma Inline (Set_Elist10);
 
+      procedure Set_Elist11 (N : Node_Id; Val : Elist_Id);
+      pragma Inline (Set_Elist11);
+
       procedure Set_Elist13 (N : Node_Id; Val : Elist_Id);
       pragma Inline (Set_Elist13);
 
Index: atree.h
===================================================================
--- atree.h	(revision 230522)
+++ atree.h	(working copy)
@@ -516,6 +516,7 @@
 #define Elist8(N)     Field8  (N)
 #define Elist9(N)     Field9  (N)
 #define Elist10(N)    Field10 (N)
+#define Elist11(N)    Field11 (N)
 #define Elist13(N)    Field13 (N)
 #define Elist15(N)    Field15 (N)
 #define Elist16(N)    Field16 (N)
