===================================================================
@@ -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 =>
===================================================================
@@ -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);
===================================================================
@@ -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
===================================================================
@@ -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 --
----------------
===================================================================
@@ -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
===================================================================
@@ -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
===================================================================
@@ -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.
===================================================================
@@ -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);
===================================================================
@@ -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);
===================================================================
@@ -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)
This patch modifies the analysis of variable contracts to enforce the following SPARK RM rule: 9.3 - If a variable or a package which declares a state abstraction is declared immediately within the same declarative region as a single_task_declaration or a single_protected_declaration, then the Part_Of aspect of the variable or state abstraction may denote the task or protected unit. This indicates that the object or state abstraction is not part of the visible state or private state of its enclosing package. An object or state abstraction which "belongs" to a task unit in this way is treated as a local object of the task (e.g., it cannot be named in a Global aspect specification occurring outside of the body of the task unit, just as an object declared immediately within the task body could not be). An object or state abstraction which "belongs" to a protected unit in this way is treated as a component of the (anonymous) protected type (e.g., it can never be named in any Global aspect specification, just as a protected component could not be). The notional equivalences described above break down in the case of package elaboration. The presence or absence of such a Part_Of aspect specification is ignored in determining the legality of an Initializes or Initial_Condition aspect specification. ------------ -- Source -- ------------ -- pack.ads package Pack with SPARK_Mode, Initializes => (Var_1, Var_2, Var_3, Var_4), -- OK Initial_Condition => (Var_1 = 1 -- OK and then Var_2 = 2 -- OK and then Var_3 = 3 -- OK and then Var_4 = 4) -- OK is Var_1 : Integer := 1 with Part_Of => Prot; Var_2 : Integer := 2 with Part_Of => Tsk; protected Prot is entry Error_1 (Formal : out Integer) with Global => (Input => Var_2), -- Error Depends => (Formal => Var_2); -- Error procedure Error_2 (Formal : Integer) with Global => (Output => Var_2), -- Error Depends => (Var_2 => Formal); -- Error function Error_3 return Boolean with Global => (Input => Var_2), -- Error Depends => (Error_3'Result => Var_2); -- Error entry OK_1 (Formal : out Integer) with Global => (Input => Var_1), -- OK Depends => (Formal => Var_1); -- OK procedure OK_2 (Formal : Integer) with Global => (Output => Var_1), -- OK Depends => (Var_1 => Formal); -- OK function OK_3 return Boolean with Global => (Input => Var_1), -- OK Depends => (OK_3'Result => Var_1); -- OK end Prot; task Error_4 with Global => (Input => Var_1), -- Error Depends => (null => Var_1); -- Error task Tsk with Global => (Input => Var_2), -- OK Depends => (null => Var_2); -- OK procedure Error_5; procedure Error_6 with Pre => Var_1 = 1, -- Error Post => Var_2 > 3; -- Error package Error_7 is procedure Error_8; end Error_7; Var_3 : Integer := 3 with Part_Of => Prot; Var_4 : Integer := 4 with Part_Of => Tsk; end Pack; -- pack.adb package body Pack with SPARK_Mode is protected body Prot is entry Error_1 (Formal : out Integer) when True is procedure Nested_Proc is begin Var_2 := Var_4; -- Error end Nested_Proc; begin Var_2 := Var_4; -- Error end Error_1; procedure Error_2 (Formal : Integer) is procedure Nested_Proc (Formal : Integer) is begin null; end Nested_Proc; begin Var_2 := Var_4; -- Error Nested_Proc (Var_2); -- Error Nested_Proc (Var_4); -- Error end Error_2; function Error_3 return Boolean is begin return Var_2 = Var_4; -- Error end Error_3; entry OK_1 (Formal : out Integer) when True is begin Var_1 := Var_3; -- OK end OK_1; procedure OK_2 (Formal : Integer) is begin Var_1 := Var_3; -- OK end OK_2; function OK_3 return Boolean is begin return Var_1 = Var_3; -- OK end OK_3; end Prot; task body Error_4 is begin Var_1 := Var_3; -- Error end Error_4; task body Tsk is procedure Proc is begin Var_2 := Var_4; -- OK end Proc; begin Var_2 := Var_4; -- OK end Tsk; procedure Error_5 is begin Var_1 := 2; -- Error Var_2 := 3; -- Error Var_3 := Var_4; -- Error end Error_5; procedure Error_6 is begin null; end Error_6; package body Error_7 is procedure Error_8 is begin Var_1 := Var_2 - Var_3 * Var_4; -- Error end Error_8; begin Var_1 := Var_2 + Var_3 / Var_4; -- Error end Error_7; begin Var_1 := Var_2 * Var_3 * Var_4; -- Error end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb pack.adb:6:13: reference to variable "Var_2" cannot appear in this context pack.adb:6:13: "Var_2" is constituent of single task type "Tsk" pack.adb:6:22: reference to variable "Var_4" cannot appear in this context pack.adb:6:22: "Var_4" is constituent of single task type "Tsk" pack.adb:9:10: reference to variable "Var_2" cannot appear in this context pack.adb:9:10: "Var_2" is constituent of single task type "Tsk" pack.adb:9:19: reference to variable "Var_4" cannot appear in this context pack.adb:9:19: "Var_4" is constituent of single task type "Tsk" pack.adb:16:10: reference to variable "Var_2" cannot appear in this context pack.adb:16:10: "Var_2" is constituent of single task type "Tsk" pack.adb:16:19: reference to variable "Var_4" cannot appear in this context pack.adb:16:19: "Var_4" is constituent of single task type "Tsk" pack.adb:17:23: reference to variable "Var_2" cannot appear in this context pack.adb:17:23: "Var_2" is constituent of single task type "Tsk" pack.adb:18:23: reference to variable "Var_4" cannot appear in this context pack.adb:18:23: "Var_4" is constituent of single task type "Tsk" pack.adb:23:17: reference to variable "Var_2" cannot appear in this context pack.adb:23:17: "Var_2" is constituent of single task type "Tsk" pack.adb:23:25: reference to variable "Var_4" cannot appear in this context pack.adb:23:25: "Var_4" is constituent of single task type "Tsk" pack.adb:44:07: reference to variable "Var_1" cannot appear in this context pack.adb:44:07: "Var_1" is constituent of single task type "Prot" pack.adb:44:16: reference to variable "Var_3" cannot appear in this context pack.adb:44:16: "Var_3" is constituent of single task type "Prot" pack.adb:58:07: reference to variable "Var_1" cannot appear in this context pack.adb:58:07: "Var_1" is constituent of single task type "Prot" pack.adb:59:07: reference to variable "Var_2" cannot appear in this context pack.adb:59:07: "Var_2" is constituent of single task type "Tsk" pack.adb:60:07: reference to variable "Var_3" cannot appear in this context pack.adb:60:07: "Var_3" is constituent of single task type "Prot" pack.adb:60:16: reference to variable "Var_4" cannot appear in this context pack.adb:60:16: "Var_4" is constituent of single task type "Tsk" pack.adb:68:10: reference to variable "Var_1" cannot appear in this context pack.adb:68:10: "Var_1" is constituent of single task type "Prot" pack.adb:68:19: reference to variable "Var_2" cannot appear in this context pack.adb:68:19: "Var_2" is constituent of single task type "Tsk" pack.adb:68:27: reference to variable "Var_3" cannot appear in this context pack.adb:68:27: "Var_3" is constituent of single task type "Prot" pack.adb:68:35: reference to variable "Var_4" cannot appear in this context pack.adb:68:35: "Var_4" is constituent of single task type "Tsk" pack.adb:71:07: reference to variable "Var_1" cannot appear in this context pack.adb:71:07: "Var_1" is constituent of single task type "Prot" pack.adb:71:16: reference to variable "Var_2" cannot appear in this context pack.adb:71:16: "Var_2" is constituent of single task type "Tsk" pack.adb:71:24: reference to variable "Var_3" cannot appear in this context pack.adb:71:24: "Var_3" is constituent of single task type "Prot" pack.adb:71:32: reference to variable "Var_4" cannot appear in this context pack.adb:71:32: "Var_4" is constituent of single task type "Tsk" pack.adb:75:04: reference to variable "Var_1" cannot appear in this context pack.adb:75:04: "Var_1" is constituent of single task type "Prot" pack.adb:75:13: reference to variable "Var_2" cannot appear in this context pack.adb:75:13: "Var_2" is constituent of single task type "Tsk" pack.adb:75:21: reference to variable "Var_3" cannot appear in this context pack.adb:75:21: "Var_3" is constituent of single task type "Prot" pack.adb:75:29: reference to variable "Var_4" cannot appear in this context pack.adb:75:29: "Var_4" is constituent of single task type "Tsk" pack.ads:16:35: reference to variable "Var_2" cannot appear in this context pack.ads:16:35: "Var_2" is constituent of single task type "Tsk" pack.ads:17:36: reference to variable "Var_2" cannot appear in this context pack.ads:17:36: "Var_2" is constituent of single task type "Tsk" pack.ads:20:36: reference to variable "Var_2" cannot appear in this context pack.ads:20:36: "Var_2" is constituent of single task type "Tsk" pack.ads:21:26: reference to variable "Var_2" cannot appear in this context pack.ads:21:26: "Var_2" is constituent of single task type "Tsk" pack.ads:24:35: reference to variable "Var_2" cannot appear in this context pack.ads:24:35: "Var_2" is constituent of single task type "Tsk" pack.ads:25:44: reference to variable "Var_2" cannot appear in this context pack.ads:25:44: "Var_2" is constituent of single task type "Tsk" pack.ads:41:32: reference to variable "Var_1" cannot appear in this context pack.ads:41:32: "Var_1" is constituent of single task type "Prot" pack.ads:42:31: reference to variable "Var_1" cannot appear in this context pack.ads:42:31: "Var_1" is constituent of single task type "Prot" pack.ads:51:19: reference to variable "Var_1" cannot appear in this context pack.ads:51:19: "Var_1" is constituent of single task type "Prot" pack.ads:52:19: reference to variable "Var_2" cannot appear in this context pack.ads:52:19: "Var_2" is constituent of single task type "Tsk" Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-18 Hristian Kirtchev <kirtchev@adacore.com> * atree.adb (Elist11): New routine. (Set_Elist11): New routine. * atree.ads (Elist11): New routine. (Set_Elist11): New routine. * atree.h: Define Elist11. * contracts.adb (Analyze_Object_Contract): Verify the legality of all references to a variable given that the variable is a constituent of a single protected/task type. * einfo.adb: Part_Of_References now utilizes Elist11. (Part_Of_References): New routine. (Set_Part_Of_References): New routine. (Write_Field11_Name): Add output for Part_Of_References. * einfo.ads New attribute Part_Of_References along with usage in entities. (Part_Of_References): New routine along with pragma Inline. (Set_Part_Of_References): New routine along with pragma Inline. * sem_prag.adb (Analyze_Constituent): Record a possible reference to a concurrent constituent. (Analyze_Global_Item): Record a possible reference to a concurrent constituent. (Analyze_Input_Output): Record a possible reference to a concurrent constituent. * sem_res.adb (Resolve_Entity_Name): Record a possible reference to a concurrent constituent. * sem_util.adb (Check_Part_Of_Reference): New routine. (Record_Possible_Part_Of_Reference): New routine. * sem_util.ads (Check_Part_Of_Reference): New routine. (Record_Possible_Part_Of_Reference): New routine.