OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2016-10-12  Ed Schonberg  <schonberg@adacore.com>

	* lib-writ.adb (Write_ALI): Removal of unused file entries from
	dependency list must be performed before the list is sorted,
	so that the dependency number of other files is properly set-up
	for use in tools that relate entity information to the unit in
	which they are declared.

2016-10-12  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_aggr.adb (Initialize_Ctrl_Array_Component):
	Create a copy of the initialization expression to avoid sharing
	it between multiple components.

2016-10-12  Yannick Moy  <moy@adacore.com>

	* einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
	in abtract states.
	(Has_Non_Null_Visible_Refinement): Return true for patial refinement.
	(Partial_Refinement_Constituents): New function returns the full or
	partial refinement constituents depending on scope.
	* sem_ch3.adb (Analyze_Declarations): Remove partial visible
	refinements when exiting the scope of a package spec or body
	and those partial refinements are not in scope afterwards.
	* sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
	abstract states of parent units with partial refinement so that
	it is visible.
	* sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
	abstract state if any as having partial refinement in that scope.
	(Analyze_Refined_Global_In_Decl_Part): Check constituent usage
	based on full or partial refinement depending on scope.

2016-10-12  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch4.adb (Expand_N_Type_Conversion): If the target type
	has an invariant aspect, insert invariant call at the proper
	place in the code rather than rewriting the expression as an
	expression with actions, to prevent spurious semantic errors on
	the rewritten conversion when it is the object in a renaming.

From-SVN: r241048
This commit is contained in:
Arnaud Charlet 2016-10-12 15:53:46 +02:00
parent 432b6d9572
commit d89ce4324c
10 changed files with 243 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
gcc/ada/ChangeLog
View File

@ -1,3 +1,43 @@
2016-10-12 Ed Schonberg <schonberg@adacore.com>
* lib-writ.adb (Write_ALI): Removal of unused file entries from
dependency list must be performed before the list is sorted,
so that the dependency number of other files is properly set-up
for use in tools that relate entity information to the unit in
which they are declared.
2016-10-12 Hristian Kirtchev <kirtchev@adacore.com>
* exp_aggr.adb (Initialize_Ctrl_Array_Component):
Create a copy of the initialization expression to avoid sharing
it between multiple components.
2016-10-12 Yannick Moy <moy@adacore.com>
* einfo.adb, einfo.ads (Has_Partial_Visible_Refinement): New flag
in abtract states.
(Has_Non_Null_Visible_Refinement): Return true for patial refinement.
(Partial_Refinement_Constituents): New function returns the full or
partial refinement constituents depending on scope.
* sem_ch3.adb (Analyze_Declarations): Remove partial visible
refinements when exiting the scope of a package spec or body
and those partial refinements are not in scope afterwards.
* sem_ch7.adb, sem_ch7.ads (Install_Partial_Declarations): Mark
abstract states of parent units with partial refinement so that
it is visible.
* sem_prag.adb (Analyze_Part_Of_In_Decl_Part): Mark enclosing
abstract state if any as having partial refinement in that scope.
(Analyze_Refined_Global_In_Decl_Part): Check constituent usage
based on full or partial refinement depending on scope.
2016-10-12 Ed Schonberg <schonberg@adacore.com>
* exp_ch4.adb (Expand_N_Type_Conversion): If the target type
has an invariant aspect, insert invariant call at the proper
place in the code rather than rewriting the expression as an
expression with actions, to prevent spurious semantic errors on
the rewritten conversion when it is the object in a renaming.
2016-10-12 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch5.adb, sem_ch3.adb, exp_ch9.adb, a-tags.adb, sem_prag.adb,

48
gcc/ada/einfo.adb
View File

@ -610,8 +610,8 @@ package body Einfo is
-- Is_Actual_Subtype Flag293
-- Has_Pragma_Unused Flag294
-- Is_Ignored_Transient Flag295
-- Has_Partial_Visible_Refinement Flag296
-- (unused) Flag296
-- (unused) Flag297
-- (unused) Flag298
-- (unused) Flag299
@ -1682,6 +1682,12 @@ package body Einfo is
return Flag232 (Id);
end Has_Own_Invariants;
function Has_Partial_Visible_Refinement (Id : E) return B is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
return Flag296 (Id);
end Has_Partial_Visible_Refinement;
function Has_Per_Object_Constraint (Id : E) return B is
begin
return Flag154 (Id);
@ -4698,6 +4704,12 @@ package body Einfo is
Set_Flag232 (Id, V);
end Set_Has_Own_Invariants;
procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True) is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
Set_Flag296 (Id, V);
end Set_Has_Partial_Visible_Refinement;
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True) is
begin
Set_Flag154 (Id, V);
@ -7485,13 +7497,14 @@ package body Einfo is
pragma Assert (Ekind (Id) = E_Abstract_State);
Constits := Refinement_Constituents (Id);
-- For a refinement to be non-null, the first constituent must be
-- anything other than null.
-- A partial refinement is always non-null. For a full refinement to be
-- non-null, the first constituent must be anything other than null.
return
Has_Visible_Refinement (Id)
and then Present (Constits)
and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
Has_Partial_Visible_Refinement (Id)
or else (Has_Visible_Refinement (Id)
and then Present (Constits)
and then Nkind (Node (First_Elmt (Constits))) /= N_Null);
end Has_Non_Null_Visible_Refinement;
-----------------------------
@ -8370,6 +8383,29 @@ package body Einfo is
return Empty;
end Partial_Invariant_Procedure;
-------------------------------------
-- Partial_Refinement_Constituents --
-------------------------------------
function Partial_Refinement_Constituents (Id : E) return L is
Constits : Elist_Id;
begin
-- "Refinement" is a concept applicable only to abstract states
pragma Assert (Ekind (Id) = E_Abstract_State);
Constits := Refinement_Constituents (Id);
-- A refinement may be partially visible when objects declared in the
-- private part of a package are subject to a Part_Of indicator.
if No (Constits) then
Constits := Part_Of_Constituents (Id);
end if;
return Constits;
end Partial_Refinement_Constituents;
------------------------
-- Predicate_Function --
------------------------

20
gcc/ada/einfo.ads
View File

@ -1812,6 +1812,14 @@ package Einfo is
-- one invariant of its own. The flag is also set on the full view of a
-- private extension or a private type for completeness.
-- Has_Partial_Visible_Refinement (Flag296)
-- Defined in E_Abstract_State entities. Set when a state has at least
-- one refinement constituent subject to indicator Part_Of, and analysis
-- is in the region between the declaration of the first constituent for
-- this abstract state (in the private part of the package) and the end
-- of the package spec or body with visibility over this private part
-- (which includes the package itself and its child packages).
-- Has_Per_Object_Constraint (Flag154)
-- Defined in E_Component entities. Set if the subtype of the component
-- has a per object constraint. Per object constraints result from the
@ -3780,6 +3788,11 @@ package Einfo is
-- Note: the reason this is marked as a synthesized attribute is that the
-- way this is stored is as an element of the Subprograms_For_Type field.
-- Partial_Refinement_Constituents (synthesized)
-- Present in abstract state entities. Contains the constituents that
-- refine the state in its private part, in other words, all the hidden
-- states that indicate this abstract state in a Part_Of aspect/pragma.
-- 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
@ -5619,6 +5632,7 @@ package Einfo is
-- Non_Limited_View (Node19)
-- Encapsulating_State (Node32)
-- From_Limited_With (Flag159)
-- Has_Partial_Visible_Refinement (Flag296)
-- Has_Visible_Refinement (Flag263)
-- Has_Non_Limited_View (synth)
-- Has_Non_Null_Visible_Refinement (synth)
@ -5626,6 +5640,7 @@ package Einfo is
-- Is_External_State (synth)
-- Is_Null_State (synth)
-- Is_Synchronized_State (synth)
-- Partial_Refinement_Constituents (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
@ -6977,6 +6992,7 @@ package Einfo is
function Has_Object_Size_Clause (Id : E) return B;
function Has_Out_Or_In_Out_Parameter (Id : E) return B;
function Has_Own_Invariants (Id : E) return B;
function Has_Partial_Visible_Refinement (Id : E) return B;
function Has_Per_Object_Constraint (Id : E) return B;
function Has_Pragma_Controlled (Id : E) return B;
function Has_Pragma_Elaborate_Body (Id : E) return B;
@ -7412,6 +7428,7 @@ package Einfo is
function Number_Entries (Id : E) return Nat;
function Number_Formals (Id : E) return Pos;
function Parameter_Mode (Id : E) return Formal_Kind;
function Partial_Refinement_Constituents (Id : E) return L;
function Primitive_Operations (Id : E) return L;
function Root_Type (Id : E) return E;
function Safe_Emax_Value (Id : E) return U;
@ -7652,6 +7669,7 @@ package Einfo is
procedure Set_Has_Object_Size_Clause (Id : E; V : B := True);
procedure Set_Has_Out_Or_In_Out_Parameter (Id : E; V : B := True);
procedure Set_Has_Own_Invariants (Id : E; V : B := True);
procedure Set_Has_Partial_Visible_Refinement (Id : E; V : B := True);
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True);
procedure Set_Has_Pragma_Controlled (Id : E; V : B := True);
procedure Set_Has_Pragma_Elaborate_Body (Id : E; V : B := True);
@ -8444,6 +8462,7 @@ package Einfo is
pragma Inline (Has_Object_Size_Clause);
pragma Inline (Has_Out_Or_In_Out_Parameter);
pragma Inline (Has_Own_Invariants);
pragma Inline (Has_Partial_Visible_Refinement);
pragma Inline (Has_Per_Object_Constraint);
pragma Inline (Has_Pragma_Controlled);
pragma Inline (Has_Pragma_Elaborate_Body);
@ -8959,6 +8978,7 @@ package Einfo is
pragma Inline (Set_Has_Object_Size_Clause);
pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
pragma Inline (Set_Has_Own_Invariants);
pragma Inline (Set_Has_Partial_Visible_Refinement);
pragma Inline (Set_Has_Per_Object_Constraint);
pragma Inline (Set_Has_Pragma_Controlled);
pragma Inline (Set_Has_Pragma_Elaborate_Body);

28
gcc/ada/exp_aggr.adb
View File

@ -1277,6 +1277,7 @@ package body Exp_Aggr is
is
Act_Aggr : Node_Id;
Act_Stmts : List_Id;
Expr : Node_Id;
Fin_Call : Node_Id;
Hook_Clear : Node_Id;
@ -1285,20 +1286,29 @@ package body Exp_Aggr is
-- in-place expansion.
begin
-- Duplicate the initialization expression in case the context is
-- a multi choice list or an "others" choice which plugs various
-- holes in the aggregate. As a result the expression is no longer
-- shared between the various components and is reevaluated for
-- each such component.
Expr := New_Copy_Tree (Init_Expr);
Set_Parent (Expr, Parent (Init_Expr));
-- Perform a preliminary analysis and resolution to determine what
-- the initialization expression denotes. An unanalyzed function
-- call may appear as an identifier or an indexed component.
if Nkind_In (Init_Expr, N_Function_Call,
N_Identifier,
N_Indexed_Component)
and then not Analyzed (Init_Expr)
if Nkind_In (Expr, N_Function_Call,
N_Identifier,
N_Indexed_Component)
and then not Analyzed (Expr)
then
Preanalyze_And_Resolve (Init_Expr, Comp_Typ);
Preanalyze_And_Resolve (Expr, Comp_Typ);
end if;
In_Place_Expansion :=
Nkind (Init_Expr) = N_Function_Call
Nkind (Expr) = N_Function_Call
and then not Is_Limited_Type (Comp_Typ);
-- The initialization expression is a controlled function call.
@ -1315,7 +1325,7 @@ package body Exp_Aggr is
-- generation of a transient scope, which leads to out-of-order
-- adjustment and finalization.
Set_No_Side_Effect_Removal (Init_Expr);
Set_No_Side_Effect_Removal (Expr);
-- When the transient component initialization is related to a
-- range or an "others", keep all generated statements within
@ -1341,7 +1351,7 @@ package body Exp_Aggr is
Process_Transient_Component
(Loc => Loc,
Comp_Typ => Comp_Typ,
Init_Expr => Init_Expr,
Init_Expr => Expr,
Fin_Call => Fin_Call,
Hook_Clear => Hook_Clear,
Aggr => Act_Aggr,
@ -1356,7 +1366,7 @@ package body Exp_Aggr is
Initialize_Array_Component
(Arr_Comp => Arr_Comp,
Comp_Typ => Comp_Typ,
Init_Expr => Init_Expr,
Init_Expr => Expr,
Stmts => Stmts);
-- At this point the array element is fully initialized. Complete

23
gcc/ada/exp_ch4.adb
View File

@ -10577,15 +10577,16 @@ package body Exp_Ch4 is
end if;
-- Check for case of converting to a type that has an invariant
-- associated with it. This required an invariant check. We convert
-- associated with it. This requires an invariant check. We insert
-- a call:
-- typ (expr)
-- invariant_check (typ (expr))
-- into
-- do invariant_check (typ (expr)) in typ (expr);
-- using Duplicate_Subexpr to avoid multiple side effects
-- in the code, after removing side effects from the expression.
-- This is clearer than replacing the conversion into an expression
-- with actions, because the context may impose additional actions
-- (tag checks, membership tests, etc.) that conflict with this
-- rewriting (used previously).
-- Note: the Comes_From_Source check, and then the resetting of this
-- flag prevents what would otherwise be an infinite recursion.
@ -10595,12 +10596,8 @@ package body Exp_Ch4 is
and then Comes_From_Source (N)
then
Set_Comes_From_Source (N, False);
Rewrite (N,
Make_Expression_With_Actions (Loc,
Actions => New_List (
Make_Invariant_Call (Duplicate_Subexpr (N))),
Expression => Duplicate_Subexpr_No_Checks (N)));
Analyze_And_Resolve (N, Target_Type);
Remove_Side_Effects (N);
Insert_Action (N, Make_Invariant_Call (Duplicate_Subexpr (N)));
goto Done;
end if;

52
gcc/ada/lib-writ.adb
View File

@ -990,8 +990,27 @@ package body Lib.Writ is
if Cunit_Entity (Unum) = Empty
or else not From_Limited_With (Cunit_Entity (Unum))
then
Num_Sdep := Num_Sdep + 1;
Sdep_Table (Num_Sdep) := Unum;
-- Units that are not analyzed need not appear in the dependency
-- list. These units are either units appearing in limited_with
-- clauses of other units, or units loaded for inlining that end
-- up not inlined by a later decision of the inlining code, to
-- prevent circularities. We want to exclude these files from the
-- list of dependencies, so that the dependency number of other
-- is correctly set, as that number is used by cross-reference
-- tools to relate entity information to the unit in which they
-- are declared.
if Present (Cunit_Entity (Unum))
and then Ekind (Cunit_Entity (Unum)) = E_Void
and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
and then Serious_Errors_Detected = 0
then
null;
else
Num_Sdep := Num_Sdep + 1;
Sdep_Table (Num_Sdep) := Unum;
end if;
end if;
end loop;
@ -1433,32 +1452,6 @@ package body Lib.Writ is
Units.Table (Unum).Dependency_Num := J;
Sind := Units.Table (Unum).Source_Index;
-- The dependency table also contains units that appear in the
-- context of a unit loaded through a limited_with clause. These
-- units are never analyzed, and thus the main unit does not
-- really have a dependency on them. Subunits are always compiled
-- in the context of the parent, and their file table entries are
-- not properly decorated, they are recognized syntactically.
-- This optimization is disabled when inline is active, because
-- inline may propose some bodies for inlining, and decide later
-- that they may lead to circularities, in which case they are
-- also left unanalyzed in the file table. There is no simple way
-- to distinguish between the two kinds of unanalyzed entries,
-- so simplest is to skip this step.
-- Actually, this optimization is always disabled, because it
-- breaks gnatfind.
if False -- ???
and then Present (Cunit_Entity (Unum))
and then Ekind (Cunit_Entity (Unum)) = E_Void
and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
and then not Inline_Active
then
goto Next_Unit;
end if;
Write_Info_Initiate ('D');
Write_Info_Char (' ');
@ -1534,9 +1527,6 @@ package body Lib.Writ is
end if;
Write_Info_EOL;
<<Next_Unit>>
null;
end loop;
end;

41
gcc/ada/sem_ch3.adb
View File

@ -2178,10 +2178,17 @@ package body Sem_Ch3 is
-- case, add a proper spec if the body lacks one. The spec is inserted
-- before Body_Decl and immediately analyzed.
procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id);
-- Spec_Id is the entity of a package that may define abstract states,
-- and in the case of a child unit, whose ancestors may define abstract
-- states. If the states have partial visible refinement, remove the
-- partial visibility of each constituent at the end of the package
-- spec and body declarations.
procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
-- Spec_Id is the entity of a package that may define abstract states.
-- If the states have visible refinement, remove the visibility of each
-- constituent at the end of the package body declarations.
-- constituent at the end of the package body declaration.
-----------------
-- Adjust_Decl --
@ -2335,6 +2342,29 @@ package body Sem_Ch3 is
Insert_Before_And_Analyze (Body_Decl, Decl);
end Handle_Late_Controlled_Primitive;
----------------------------------------
-- Remove_Partial_Visible_Refinements --
----------------------------------------
procedure Remove_Partial_Visible_Refinements (Spec_Id : Entity_Id) is
State_Elmt : Elmt_Id;
begin
if Present (Abstract_States (Spec_Id)) then
State_Elmt := First_Elmt (Abstract_States (Spec_Id));
while Present (State_Elmt) loop
Set_Has_Partial_Visible_Refinement (Node (State_Elmt), False);
Next_Elmt (State_Elmt);
end loop;
end if;
-- For a child unit, also hide the partial state refinement from
-- ancestor packages.
if Is_Child_Unit (Spec_Id) then
Remove_Partial_Visible_Refinements (Scope (Spec_Id));
end if;
end Remove_Partial_Visible_Refinements;
--------------------------------
-- Remove_Visible_Refinements --
--------------------------------
@ -2576,6 +2606,15 @@ package body Sem_Ch3 is
-- restore the original state conditions.
Remove_Visible_Refinements (Corresponding_Spec (Context));
Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
elsif Nkind (Context) = N_Package_Declaration then
-- Partial state refinements are visible up to the end of the
-- package spec declarations. Hide the partial state refinements
-- from visibility to restore the original state conditions.
Remove_Partial_Visible_Refinements (Corresponding_Spec (Context));
end if;
-- Verify that all abstract states found in any package declared in

28
gcc/ada/sem_ch7.adb
View File

@ -2275,6 +2275,34 @@ package body Sem_Ch7 is
Next_Entity (Id);
end loop;
-- An abstract state is partially refined when it has at least one
-- Part_Of constituent. Since these constituents are being installed
-- into visibility, update the partial refinement status of any state
-- defined in the associated package, subject to at least one Part_Of
-- constituent.
if Ekind_In (P, E_Generic_Package, E_Package) then
declare
States : constant Elist_Id := Abstract_States (P);
State_Elmt : Elmt_Id;
State_Id : Entity_Id;
begin
if Present (States) then
State_Elmt := First_Elmt (States);
while Present (State_Elmt) loop
State_Id := Node (State_Elmt);
if Present (Part_Of_Constituents (State_Id)) then
Set_Has_Partial_Visible_Refinement (State_Id);
end if;
Next_Elmt (State_Elmt);
end loop;
end if;
end;
end if;
-- Indicate that the private part is currently visible, so it can be
-- properly reset on exit.

4
gcc/ada/sem_ch7.ads
View File

@ -46,10 +46,10 @@ package Sem_Ch7 is
-- On entrance to a package body, make declarations in package spec
-- immediately visible.
--
-- When compiling the body of a package, both routines are called in
-- When compiling the body of a package, both routines are called in
-- succession. When compiling the body of a child package, the call
-- to Install_Private_Declaration is immediate for private children,
-- but is deferred until the compilation of the private part of the
-- but is deferred until the compilation of the private part of the
-- child for public child packages.
function Unit_Requires_Body

32
gcc/ada/sem_prag.adb
View File

@ -3410,6 +3410,13 @@ package body Sem_Prag is
Append_Elmt (Var_Id, Constits);
Set_Encapsulating_State (Var_Id, Encap_Id);
-- A Part_Of constituent partially refines an abstract state. This
-- property does not apply to protected or task units.
if Ekind (Encap_Id) = E_Abstract_State then
Set_Has_Partial_Visible_Refinement (Encap_Id);
end if;
end if;
-- Emit a clarification message when the encapsulator is undefined,
@ -18717,7 +18724,7 @@ package body Sem_Prag is
Add_Contract_Item (N, Item_Id);
-- A variable may act as consituent of a single concurrent type
-- A variable may act as constituent of a single concurrent type
-- which in turn could be declared after the variable. Due to this
-- discrepancy, the full analysis of indicator Part_Of is delayed
-- until the end of the enclosing declarative region (see routine
@ -24051,7 +24058,7 @@ package body Sem_Prag is
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
Refinement_Constituents (State_Id);
Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
@ -24614,7 +24621,7 @@ package body Sem_Prag is
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
Refinement_Constituents (State_Id);
Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Has_Missing : Boolean := False;
@ -24753,7 +24760,7 @@ package body Sem_Prag is
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
Refinement_Constituents (State_Id);
Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
In_Seen : Boolean := False;
@ -24853,7 +24860,7 @@ package body Sem_Prag is
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
Refinement_Constituents (State_Id);
Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
@ -24952,7 +24959,7 @@ package body Sem_Prag is
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
Constits : constant Elist_Id :=
Refinement_Constituents (State_Id);
Partial_Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Proof_In_Seen : Boolean := False;
@ -25083,7 +25090,10 @@ package body Sem_Prag is
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
and then Present (Encapsulating_State (Item_Id))
and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
and then
(Has_Visible_Refinement (Encapsulating_State (Item_Id))
or else
Has_Partial_Visible_Refinement (Encapsulating_State (Item_Id)))
and then Contains (States, Encapsulating_State (Item_Id))
then
if Global_Mode = Name_Input then
@ -25438,10 +25448,10 @@ package body Sem_Prag is
-- Non-instance case
else
-- The corresponding Global pragma must mention at least one state
-- witha visible refinement at the point Refined_Global is processed.
-- States with null refinements need Refined_Global pragma
-- (SPARK RM 7.2.4(2)).
-- The corresponding Global pragma must mention at least one
-- state with a visible refinement at the point Refined_Global
-- is processed. States with null refinements need Refined_Global
-- pragma (SPARK RM 7.2.4(2)).
if not Has_In_State
and then not Has_In_Out_State