From d89ce4324c613e79d9e4855a284c809773cbc30f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 12 Oct 2016 15:53:46 +0200 Subject: [PATCH] [multiple changes] 2016-10-12 Ed Schonberg * 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 * 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 * 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 * 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 --- gcc/ada/ChangeLog | 40 ++++++++++++++++++++++++++++++++++ gcc/ada/einfo.adb | 48 +++++++++++++++++++++++++++++++++++----- gcc/ada/einfo.ads | 20 +++++++++++++++++ gcc/ada/exp_aggr.adb | 28 ++++++++++++++++-------- gcc/ada/exp_ch4.adb | 23 +++++++++----------- gcc/ada/lib-writ.adb | 52 ++++++++++++++++++-------------------------- gcc/ada/sem_ch3.adb | 41 +++++++++++++++++++++++++++++++++- gcc/ada/sem_ch7.adb | 28 ++++++++++++++++++++++++ gcc/ada/sem_ch7.ads | 4 ++-- 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 + + * 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 + + * 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 + + * 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 + + * 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 * 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; - - <> - 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 -- 2.30.2