This patch modifies the analysis of Part_Of indicators to verify their
associated rules even when the indicator appears in non-SPARK code. This
prevents possible tamperings of Part_Of constituents of single concurrent
types outside of SPARK code.
------------
-- Source --
------------
-- pack.ads
pragma Profile (Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);
package Pack with SPARK_Mode is
protected PO is
end PO;
X : Boolean := True with Part_Of => PO;
end Pack;
-- pack.adb
package body Pack is
protected body PO is
end PO;
begin
X := not X; -- OK
end Pack;
-- flip.adb
pragma Profile (Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);
with Pack; use Pack;
procedure Flip with SPARK_Mode => Off is
begin
X := not X; -- Error
end Flip;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c flip.adb
$ gcc -c pack.adb
flip.adb:8:04: reference to variable "X" cannot appear in this context
flip.adb:8:04: "X" is constituent of single protected type "PO"
flip.adb:8:13: reference to variable "X" cannot appear in this context
flip.adb:8:13: "X" is constituent of single protected type "PO"
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-12-15 Hristian Kirtchev <kirtc...@adacore.com>
* sem_prag.adb (Analyze_Part_Of): The context-specific portion of the
analysis is now directed to several specialized routines.
(Check_Part_Of_Abstract_State): New routine.
(Check_Part_Of_Concurrent_Type): New routine. Reimplement the checks
involving the item, the single concurrent type, and their respective
contexts.
* sem_res.adb (Resolve_Entity_Name): Potential constituents of a single
concurrent type are now recorded regardless of the SPARK mode.
* sem_util.adb (Check_Part_Of_Reference): Split some of the tests in
individual predicates. A Part_Of reference is legal when it appears
within the statement list of the object's immediately enclosing
package.
(Is_Enclosing_Package_Body): New routine.
(Is_Internal_Declaration_Or_Body): New routine.
(Is_Single_Declaration_Or_Body): New routine.
(Is_Single_Task_Pragma): New routine.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 255685)
+++ sem_prag.adb (working copy)
@@ -3168,71 +3168,26 @@
Encap_Id : out Entity_Id;
Legal : out Boolean)
is
- Encap_Typ : Entity_Id;
- Item_Decl : Node_Id;
- Pack_Id : Entity_Id;
- Placement : State_Space_Kind;
- Parent_Unit : Entity_Id;
+ procedure Check_Part_Of_Abstract_State;
+ pragma Inline (Check_Part_Of_Abstract_State);
+ -- Verify the legality of indicator Part_Of when the encapsulator is an
+ -- abstract state.
- begin
- -- Assume that the indicator is illegal
+ procedure Check_Part_Of_Concurrent_Type;
+ pragma Inline (Check_Part_Of_Concurrent_Type);
+ -- Verify the legality of indicator Part_Of when the encapsulator is a
+ -- single concurrent type.
- Encap_Id := Empty;
- Legal := False;
+ ----------------------------------
+ -- Check_Part_Of_Abstract_State --
+ ----------------------------------
- if Nkind_In (Encap, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
- then
- Analyze (Encap);
- Resolve_State (Encap);
+ procedure Check_Part_Of_Abstract_State is
+ Pack_Id : Entity_Id;
+ Placement : State_Space_Kind;
+ Parent_Unit : Entity_Id;
- Encap_Id := Entity (Encap);
-
- -- The encapsulator is an abstract state
-
- if Ekind (Encap_Id) = E_Abstract_State then
- null;
-
- -- The encapsulator is a single concurrent type (SPARK RM 9.3)
-
- elsif Is_Single_Concurrent_Object (Encap_Id) then
- null;
-
- -- Otherwise the encapsulator is not a legal choice
-
- else
- SPARK_Msg_N
- ("indicator Part_Of must denote abstract state, single "
- & "protected type or single task type", Encap);
- return;
- end if;
-
- -- This is a syntax error, always report
-
- else
- Error_Msg_N
- ("indicator Part_Of must denote abstract state, single protected "
- & "type or single task type", Encap);
- return;
- end if;
-
- -- Catch a case where indicator Part_Of denotes the abstract view of a
- -- variable which appears as an abstract state (SPARK RM 10.1.2 2).
-
- if From_Limited_With (Encap_Id)
- and then Present (Non_Limited_View (Encap_Id))
- and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable
- then
- SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap);
- SPARK_Msg_N ("\& denotes abstract view of object", Encap);
- return;
- end if;
-
- -- The encapsulator is an abstract state
-
- if Ekind (Encap_Id) = E_Abstract_State then
-
+ begin
-- Determine where the object, package instantiation or state lives
-- with respect to the enclosing packages or package bodies.
@@ -3250,6 +3205,7 @@
SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
+
Error_Msg_Name_1 := Chars (Scope (Encap_Id));
SPARK_Msg_NE
("\& is not part of the hidden state of package %",
@@ -3267,14 +3223,14 @@
and then Is_Private_Descendant (Pack_Id)
then
-- A variable or state abstraction which is part of the visible
- -- state of a private child unit (or one of its public
- -- descendants) must have its Part_Of indicator specified. The
- -- Part_Of indicator must denote a state abstraction declared
- -- by either the parent unit of the private unit or by a public
- -- descendant of that parent unit.
+ -- state of a private child unit or its public descendants must
+ -- have its Part_Of indicator specified. The Part_Of indicator
+ -- must denote a state declared by either the parent unit of
+ -- the private unit or by a public descendant of that parent
+ -- unit.
- -- Find nearest private ancestor (which can be the current unit
- -- itself).
+ -- Find the nearest private ancestor (which can be the current
+ -- unit itself).
Parent_Unit := Pack_Id;
while Present (Parent_Unit) loop
@@ -3288,8 +3244,8 @@
if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
SPARK_Msg_NE
- ("indicator Part_Of must denote abstract state of & "
- & "or of its public descendant (SPARK RM 7.2.6(3))",
+ ("indicator Part_Of must denote abstract state of & or of "
+ & "its public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
return;
@@ -3302,8 +3258,8 @@
else
SPARK_Msg_NE
- ("indicator Part_Of must denote abstract state of & "
- & "or of its public descendant (SPARK RM 7.2.6(3))",
+ ("indicator Part_Of must denote abstract state of & or of "
+ & "its public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
return;
end if;
@@ -3315,6 +3271,7 @@
SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
+
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("\& is declared in the visible part of package %",
@@ -3330,6 +3287,7 @@
SPARK_Msg_NE
("indicator Part_Of must denote an abstract state of "
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
+
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("\& is declared in the private part of package %",
@@ -3354,11 +3312,77 @@
return;
end if;
- -- The encapsulator is a single concurrent type
+ -- At this point it is known that the Part_Of indicator is legal
- else
- Encap_Typ := Etype (Encap_Id);
+ Legal := True;
+ end Check_Part_Of_Abstract_State;
+ -----------------------------------
+ -- Check_Part_Of_Concurrent_Type --
+ -----------------------------------
+
+ procedure Check_Part_Of_Concurrent_Type is
+ function In_Proper_Order
+ (First : Node_Id;
+ Second : Node_Id) return Boolean;
+ pragma Inline (In_Proper_Order);
+ -- Determine whether node First precedes node Second
+
+ procedure Placement_Error;
+ pragma Inline (Placement_Error);
+ -- Emit an error concerning the illegal placement of the item with
+ -- respect to the single concurrent type.
+
+ ---------------------
+ -- In_Proper_Order --
+ ---------------------
+
+ function In_Proper_Order
+ (First : Node_Id;
+ Second : Node_Id) return Boolean
+ is
+ N : Node_Id;
+
+ begin
+ if List_Containing (First) = List_Containing (Second) then
+ N := First;
+ while Present (N) loop
+ if N = Second then
+ return True;
+ end if;
+
+ Next (N);
+ end loop;
+ end if;
+
+ return False;
+ end In_Proper_Order;
+
+ ---------------------
+ -- Placement_Error --
+ ---------------------
+
+ procedure Placement_Error is
+ begin
+ SPARK_Msg_N
+ ("indicator Part_Of must denote a previously declared single "
+ & "protected type or single task type", Encap);
+ end Placement_Error;
+
+ -- Local variables
+
+ Conc_Typ : constant Entity_Id := Etype (Encap_Id);
+ Encap_Decl : constant Node_Id := Declaration_Node (Encap_Id);
+ Encap_Context : constant Node_Id := Parent (Encap_Decl);
+
+ Item_Context : Node_Id;
+ Item_Decl : Node_Id;
+ Prv_Decls : List_Id;
+ Vis_Decls : List_Id;
+
+ -- Start of processing for Check_Part_Of_Concurrent_Type
+
+ begin
-- Only abstract states and variables can act as constituents of an
-- encapsulating single concurrent type.
@@ -3370,7 +3394,7 @@
elsif Ekind (Item_Id) = E_Constant then
Error_Msg_Name_1 := Chars (Encap_Id);
SPARK_Msg_NE
- (Fix_Msg (Encap_Typ, "constant & cannot act as constituent of "
+ (Fix_Msg (Conc_Typ, "constant & cannot act as constituent of "
& "single protected type %"), Indic, Item_Id);
return;
@@ -3379,7 +3403,7 @@
else
Error_Msg_Name_1 := Chars (Encap_Id);
SPARK_Msg_NE
- (Fix_Msg (Encap_Typ, "package instantiation & cannot act as "
+ (Fix_Msg (Conc_Typ, "package instantiation & cannot act as "
& "constituent of single protected type %"), Indic, Item_Id);
return;
end if;
@@ -3398,64 +3422,159 @@
Item_Decl := Declaration_Node (Item_Id);
end if;
- -- Both the item and its encapsulating single concurrent type must
- -- appear in the same declarative region (SPARK RM 9.3). Note that
- -- privacy is ignored.
+ Item_Context := Parent (Item_Decl);
- if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then
+ -- The item and the single concurrent type must appear in the same
+ -- declarative region, with the item following the declaration of
+ -- the single concurrent type (SPARK RM 9(3)).
+
+ if Item_Context = Encap_Context then
+ if Nkind_In (Item_Context, N_Package_Specification,
+ N_Protected_Definition,
+ N_Task_Definition)
+ then
+ Prv_Decls := Private_Declarations (Item_Context);
+ Vis_Decls := Visible_Declarations (Item_Context);
+
+ -- The placement is OK when the single concurrent type appears
+ -- within the visible declarations and the item in the private
+ -- declarations.
+ --
+ -- package Pack is
+ -- protected PO ...
+ -- private
+ -- Constit : ... with Part_Of => PO;
+ -- end Pack;
+
+ if List_Containing (Encap_Decl) = Vis_Decls
+ and then List_Containing (Item_Decl) = Prv_Decls
+ then
+ null;
+
+ -- The placement is illegal when the item appears within the
+ -- visible declarations and the single concurrent type is in
+ -- the private declarations.
+ --
+ -- package Pack is
+ -- Constit : ... with Part_Of => PO;
+ -- private
+ -- protected PO ...
+ -- end Pack;
+
+ elsif List_Containing (Item_Decl) = Vis_Decls
+ and then List_Containing (Encap_Decl) = Prv_Decls
+ then
+ Placement_Error;
+ return;
+
+ -- Otherwise both the item and the single concurrent type are
+ -- in the same list. Ensure that the declaration of the single
+ -- concurrent type precedes that of the item.
+
+ elsif not In_Proper_Order
+ (First => Encap_Decl,
+ Second => Item_Decl)
+ then
+ Placement_Error;
+ return;
+ end if;
+
+ -- Otherwise both the item and the single concurrent type are
+ -- in the same list. Ensure that the declaration of the single
+ -- concurrent type precedes that of the item.
+
+ elsif not In_Proper_Order
+ (First => Encap_Decl,
+ Second => Item_Decl)
+ then
+ Placement_Error;
+ return;
+ end if;
+
+ -- Otherwise the item and the single concurrent type reside within
+ -- unrelated regions.
+
+ else
Error_Msg_Name_1 := Chars (Encap_Id);
SPARK_Msg_NE
- (Fix_Msg (Encap_Typ, "constituent & must be declared "
+ (Fix_Msg (Conc_Typ, "constituent & must be declared "
& "immediately within the same region as single protected "
& "type %"), Indic, Item_Id);
return;
end if;
- -- The declaration of the item should follow the declaration of its
- -- encapsulating single concurrent type and must appear in the same
- -- declarative region (SPARK RM 9.3).
+ -- At this point it is known that the Part_Of indicator is legal
- declare
- N : Node_Id;
+ Legal := True;
+ end Check_Part_Of_Concurrent_Type;
- begin
- N := Next (Declaration_Node (Encap_Id));
- while Present (N) loop
- exit when N = Item_Decl;
- Next (N);
- end loop;
+ -- Start of processing for Analyze_Part_Of
- -- The single concurrent type might be in the visible part of a
- -- package, and the declaration of the item in the private part
- -- of the same package.
+ begin
+ -- Assume that the indicator is illegal
- if No (N) then
- declare
- Pack : constant Node_Id :=
- Parent (Declaration_Node (Encap_Id));
- begin
- if Nkind (Pack) = N_Package_Specification
- and then not In_Private_Part (Encap_Id)
- then
- N := First (Private_Declarations (Pack));
- while Present (N) loop
- exit when N = Item_Decl;
- Next (N);
- end loop;
- end if;
- end;
- end if;
+ Encap_Id := Empty;
+ Legal := False;
- if No (N) then
- SPARK_Msg_N
- ("indicator Part_Of must denote a previously declared "
- & "single protected type or single task type", Encap);
- return;
- end if;
- end;
+ if Nkind_In (Encap, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ Analyze (Encap);
+ Resolve_State (Encap);
+
+ Encap_Id := Entity (Encap);
+
+ -- The encapsulator is an abstract state
+
+ if Ekind (Encap_Id) = E_Abstract_State then
+ null;
+
+ -- The encapsulator is a single concurrent type (SPARK RM 9.3)
+
+ elsif Is_Single_Concurrent_Object (Encap_Id) then
+ null;
+
+ -- Otherwise the encapsulator is not a legal choice
+
+ else
+ SPARK_Msg_N
+ ("indicator Part_Of must denote abstract state, single "
+ & "protected type or single task type", Encap);
+ return;
+ end if;
+
+ -- This is a syntax error, always report
+
+ else
+ Error_Msg_N
+ ("indicator Part_Of must denote abstract state, single protected "
+ & "type or single task type", Encap);
+ return;
end if;
- Legal := True;
+ -- Catch a case where indicator Part_Of denotes the abstract view of a
+ -- variable which appears as an abstract state (SPARK RM 10.1.2 2).
+
+ if From_Limited_With (Encap_Id)
+ and then Present (Non_Limited_View (Encap_Id))
+ and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable
+ then
+ SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap);
+ SPARK_Msg_N ("\& denotes abstract view of object", Encap);
+ return;
+ end if;
+
+ -- The encapsulator is an abstract state
+
+ if Ekind (Encap_Id) = E_Abstract_State then
+ Check_Part_Of_Abstract_State;
+
+ -- The encapsulator is a single concurrent type
+
+ else
+ Check_Part_Of_Concurrent_Type;
+ end if;
end Analyze_Part_Of;
----------------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 255685)
+++ sem_util.adb (working copy)
@@ -3281,73 +3281,201 @@
-----------------------------
procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id) is
+ function Is_Enclosing_Package_Body
+ (Body_Decl : Node_Id;
+ Obj_Id : Entity_Id) return Boolean;
+ pragma Inline (Is_Enclosing_Package_Body);
+ -- Determine whether package body Body_Decl or its corresponding spec
+ -- immediately encloses the declaration of object Obj_Id.
+
+ function Is_Internal_Declaration_Or_Body
+ (Decl : Node_Id) return Boolean;
+ pragma Inline (Is_Internal_Declaration_Or_Body);
+ -- Determine whether declaration or body denoted by Decl is internal
+
+ function Is_Single_Declaration_Or_Body
+ (Decl : Node_Id;
+ Conc_Typ : Entity_Id) return Boolean;
+ pragma Inline (Is_Single_Declaration_Or_Body);
+ -- Determine whether protected/task declaration or body denoted by Decl
+ -- belongs to single concurrent type Conc_Typ.
+
+ function Is_Single_Task_Pragma
+ (Prag : Node_Id;
+ Task_Typ : Entity_Id) return Boolean;
+ pragma Inline (Is_Single_Task_Pragma);
+ -- Determine whether pragma Prag belongs to single task type Task_Typ
+
+ -------------------------------
+ -- Is_Enclosing_Package_Body --
+ -------------------------------
+
+ function Is_Enclosing_Package_Body
+ (Body_Decl : Node_Id;
+ Obj_Id : Entity_Id) return Boolean
+ is
+ Obj_Context : Node_Id;
+
+ begin
+ -- Find the context of the object declaration
+
+ Obj_Context := Parent (Declaration_Node (Obj_Id));
+
+ if Nkind (Obj_Context) = N_Package_Specification then
+ Obj_Context := Parent (Obj_Context);
+ end if;
+
+ -- The object appears immediately within the package body
+
+ if Obj_Context = Body_Decl then
+ return True;
+
+ -- The object appears immediately within the corresponding spec
+
+ elsif Nkind (Obj_Context) = N_Package_Declaration
+ and then Unit_Declaration_Node (Corresponding_Spec (Body_Decl)) =
+ Obj_Context
+ then
+ return True;
+ end if;
+
+ return False;
+ end Is_Enclosing_Package_Body;
+
+ -------------------------------------
+ -- Is_Internal_Declaration_Or_Body --
+ -------------------------------------
+
+ function Is_Internal_Declaration_Or_Body
+ (Decl : Node_Id) return Boolean
+ is
+ begin
+ if Comes_From_Source (Decl) then
+ return False;
+
+ -- A body generated for an expression function which has not been
+ -- inserted into the tree yet (In_Spec_Expression is True) is not
+ -- considered internal.
+
+ elsif Nkind (Decl) = N_Subprogram_Body
+ and then Was_Expression_Function (Decl)
+ and then not In_Spec_Expression
+ then
+ return False;
+ end if;
+
+ return True;
+ end Is_Internal_Declaration_Or_Body;
+
+ -----------------------------------
+ -- Is_Single_Declaration_Or_Body --
+ -----------------------------------
+
+ function Is_Single_Declaration_Or_Body
+ (Decl : Node_Id;
+ Conc_Typ : Entity_Id) return Boolean
+ is
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Decl);
+
+ begin
+ return
+ Present (Anonymous_Object (Spec_Id))
+ and then Anonymous_Object (Spec_Id) = Conc_Typ;
+ end Is_Single_Declaration_Or_Body;
+
+ ---------------------------
+ -- Is_Single_Task_Pragma --
+ ---------------------------
+
+ function Is_Single_Task_Pragma
+ (Prag : Node_Id;
+ Task_Typ : Entity_Id) return Boolean
+ is
+ Decl : constant Node_Id := Find_Related_Declaration_Or_Body (Prag);
+
+ begin
+ -- To qualify, the pragma must be associated with single task type
+ -- Task_Typ.
+
+ return
+ Is_Single_Task_Object (Task_Typ)
+ and then Nkind (Decl) = N_Object_Declaration
+ and then Defining_Entity (Decl) = Task_Typ;
+ end Is_Single_Task_Pragma;
+
+ -- Local variables
+
Conc_Obj : 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;
+ Prev : Node_Id;
+ -- Start of processing for Check_Part_Of_Reference
+
begin
+ -- Nothing to do when the variable was recorded, but did not become a
+ -- constituent of a single concurrent type.
+
+ if No (Conc_Obj) then
+ return;
+ end if;
+
-- Traverse the parent chain looking for a suitable context for the
-- reference to the concurrent constituent.
- Par := Parent (Ref);
+ Prev := Ref;
+ Par := Parent (Prev);
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).
+ -- elaboration checks for the constituent (SPARK RM 9(3)).
if Nam_In (Prag_Nam, Name_Initial_Condition, Name_Initializes) then
- OK_Use := True;
- exit;
+ return;
-- 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,
+ -- that the pragma may 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_Obj
- then
- OK_Use := True;
- exit;
- end if;
+ elsif Nam_In (Prag_Nam, Name_Depends, Name_Global)
+ and then Is_Single_Task_Pragma (Par, Conc_Obj)
+ then
+ return;
end if;
- -- The reference appears somewhere in the definition of the single
- -- protected/task type (SPARK RM 9.3).
+ -- The reference appears somewhere in the definition of a single
+ -- concurrent type (SPARK RM 9(3)).
elsif Nkind_In (Par, N_Single_Protected_Declaration,
N_Single_Task_Declaration)
and then Defining_Entity (Par) = Conc_Obj
then
- OK_Use := True;
- exit;
+ return;
- -- The reference appears within the expanded declaration or the body
- -- of the single protected/task type (SPARK RM 9.3).
+ -- The reference appears within the declaration or body of a single
+ -- concurrent type (SPARK RM 9(3)).
elsif Nkind_In (Par, N_Protected_Body,
N_Protected_Type_Declaration,
N_Task_Body,
N_Task_Type_Declaration)
+ and then Is_Single_Declaration_Or_Body (Par, Conc_Obj)
then
- Spec_Id := Unique_Defining_Entity (Par);
+ return;
- if Present (Anonymous_Object (Spec_Id))
- and then Anonymous_Object (Spec_Id) = Conc_Obj
- then
- OK_Use := True;
- exit;
- end if;
+ -- The reference appears within the statement list of the object's
+ -- immediately enclosing package (SPARK RM 9(3)).
+ elsif Nkind (Par) = N_Package_Body
+ and then Nkind (Prev) = N_Handled_Sequence_Of_Statements
+ and then Is_Enclosing_Package_Body (Par, Var_Id)
+ then
+ return;
+
-- 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
@@ -3357,26 +3485,10 @@
N_Package_Declaration,
N_Subprogram_Body,
N_Subprogram_Declaration)
- and then not Comes_From_Source (Par)
+ and then Is_Internal_Declaration_Or_Body (Par)
then
- -- Continue to examine the context if the reference appears in a
- -- subprogram body which was previously an expression function,
- -- unless this is during preanalysis (when In_Spec_Expression is
- -- True), as the body may not yet be inserted in the tree.
+ return;
- if Nkind (Par) = N_Subprogram_Body
- and then Was_Expression_Function (Par)
- and then not In_Spec_Expression
- then
- null;
-
- -- Otherwise the reference is legal
-
- else
- OK_Use := True;
- exit;
- end if;
-
-- 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.
@@ -3385,30 +3497,27 @@
and then Nkind (Par) = N_Subprogram_Body
and then Chars (Defining_Entity (Par)) = Name_uParent
then
- OK_Use := True;
- exit;
+ return;
end if;
- Par := Parent (Par);
+ Prev := Par;
+ Par := Parent (Prev);
end loop;
- -- The reference is illegal as it appears outside the definition or
- -- body of the single protected/task type.
+ -- At this point it is known that the reference does not appear within a
+ -- legal context.
- 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 Is_Single_Protected_Object (Conc_Obj) then
Error_Msg_NE
- ("reference to variable & cannot appear in this context",
- Ref, Var_Id);
- Error_Msg_Name_1 := Chars (Var_Id);
+ ("\% is constituent of single protected type &", Ref, Conc_Obj);
- if Is_Single_Protected_Object (Conc_Obj) then
- Error_Msg_NE
- ("\% is constituent of single protected type &", Ref, Conc_Obj);
-
- else
- Error_Msg_NE
- ("\% is constituent of single task type &", Ref, Conc_Obj);
- end if;
+ else
+ Error_Msg_NE
+ ("\% is constituent of single task type &", Ref, Conc_Obj);
end if;
end Check_Part_Of_Reference;
@@ -22127,7 +22236,7 @@
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,
+ -- 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
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 255678)
+++ sem_res.adb (working copy)
@@ -7380,15 +7380,15 @@
then
Check_Elab_Call (N);
end if;
+ 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).
+ -- 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;
+ if Ekind (E) = E_Variable then
+ Record_Possible_Part_Of_Reference (E, N);
end if;
-- A Ghost entity must appear in a specific context
