diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 40 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 48 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 20 | ||||
| -rw-r--r-- | gcc/ada/exp_aggr.adb | 28 | ||||
| -rw-r--r-- | gcc/ada/exp_ch4.adb | 23 | ||||
| -rw-r--r-- | gcc/ada/lib-writ.adb | 52 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 41 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 28 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.ads | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 32 |
10 files changed, 243 insertions, 73 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 436f9a55714..db7b6c82b55 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -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, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 1748efd0b66..dedc8a3312c 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -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 -- ------------------------ diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 1085862f9b6..405d97815af 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -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); diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 33374d35882..e83b07affdd 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -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 diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 7931c13ee92..905467b8a6b 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -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; diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index b78e3eb3855..0cd615fd504 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -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; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 3b9435f92f7..a97d0172100 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -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 diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 4a3b2de0429..55ec81e1f51 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -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. diff --git a/gcc/ada/sem_ch7.ads b/gcc/ada/sem_ch7.ads index 2963aed984c..4e645adf7fb 100644 --- a/gcc/ada/sem_ch7.ads +++ b/gcc/ada/sem_ch7.ads @@ -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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index d95cab895b6..9b9fe82985d 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -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 |