+2017-12-15 Bob Duff <duff@adacore.com>
+
+ * einfo.ads: Comment fix.
+
+2017-12-15 Piotr Trojanek <trojanek@adacore.com>
+
+ * s-vercon.adb: Minor style fixes.
+
+2017-12-15 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch6.adb (Freeze_Expr_Types): Do not emit a freeze node for an
+ itype that is the type of a discriminant-dependent component.
+
+2017-12-15 Hristian Kirtchev <kirtchev@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.
+
2017-12-15 Patrick Bernardi <bernardi@adacore.com>
* gnat_ugn.texi: Regenerate.
-- Defined in E_Record_Subtype and E_Class_Wide_Subtype entities.
-- Each such entity can either have a Discriminant_Constraint, in
-- which case it represents a distinct type from the base type (and
--- will have a list of components and discrimants in the list headed by
+-- will have a list of components and discriminants in the list headed by
-- First_Entity) or else no such constraint, in which case it will be a
-- copy of the base type.
--
------------------------
function Get_Version_String
- (V : System.Unsigned_Types.Unsigned)
+ (V : System.Unsigned_Types.Unsigned)
return Version_String
is
S : Version_String;
pragma Pure;
subtype Version_String is String (1 .. 8);
- -- Eight character string returned by Get_version_String;
+ -- Eight character string returned by Get_version_String
function Get_Version_String
- (V : System.Unsigned_Types.Unsigned)
+ (V : System.Unsigned_Types.Unsigned)
return Version_String;
-- The version information in the executable file is stored as unsigned
-- integers. This routine converts the unsigned integer into an eight
procedure Check_And_Freeze_Type (Typ : Entity_Id) is
begin
- -- Skip Itypes created by the preanalysis
+ -- Skip Itypes created by the preanalysis, and itypes
+ -- whose scope is another type (i.e. component subtypes
+ -- that depend on a discriminant),
if Is_Itype (Typ)
- and then Scope_Within_Or_Same (Scope (Typ), Def_Id)
+ and then (Scope_Within_Or_Same (Scope (Typ), Def_Id)
+ or else Is_Type (Scope (Typ)))
then
return;
end if;
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
-
- Encap_Id := Empty;
- Legal := False;
-
- 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;
-
- -- 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;
+ 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.
- -- The encapsulator is an abstract state
+ ----------------------------------
+ -- Check_Part_Of_Abstract_State --
+ ----------------------------------
- if Ekind (Encap_Id) = E_Abstract_State then
+ procedure Check_Part_Of_Abstract_State is
+ Pack_Id : Entity_Id;
+ Placement : State_Space_Kind;
+ Parent_Unit : Entity_Id;
+ begin
-- Determine where the object, package instantiation or state lives
-- with respect to the enclosing packages or package bodies.
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 %",
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
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;
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;
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 %",
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 %",
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.
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;
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;
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);
+
+ -- 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.
- if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then
+ 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;
----------------------------------
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
-----------------------------
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
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.
-
- 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;
+ return;
-- The reference has been relocated to an inlined body for GNATprove.
-- Assume that the reference is legal as the real check was already
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);
+ 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
- ("\% 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;
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
+2017-12-15 Ed Schonberg <schonberg@adacore.com>
+
+ * gnat.dg/expr_func2.ads, gnat.dg/expr_func2.adb: New testcase.
+
2017-12-15 Hristian Kirtchev <kirtchev@adacore.com>
* gnat.dg/dflt_init_cond.adb, gnat.dg/dflt_init_cond_pkg.ads: New
--- /dev/null
+-- { dg-do compile }
+
+package body Expr_Func2 is
+ procedure Foo is null;
+end Expr_Func2;
--- /dev/null
+package Expr_Func2 is
+
+ type T_Index is range 1 .. 255;
+
+ type T_Table is array (T_Index range <>) of Boolean;
+
+ type T_Variable_Table (N : T_Index := T_Index'First) is record
+ Table : T_Table (1 .. N);
+ end record;
+
+ type T_A_Variable_Table is access T_Variable_Table;
+
+ function Element (A_Variable_Table : T_A_Variable_Table) return Boolean;
+
+private
+
+ function Element (A_Variable_Table : T_A_Variable_Table) return Boolean is
+ (A_Variable_Table.all.Table (1));
+
+ procedure Foo;
+
+end Expr_Func2;
projects / gcc.git / commitdiff