Pragmas/aspects Refined_Global and Refined_Depends may be applied in a scope where only partial refinement of abstract states is visible, as defined in SPARK RM 7.2.4. In such a case, the partial refinement should be used instead of the full refinement for checking the refined contracts.
Tested on x86_64-pc-linux-gnu, committed on trunk 2016-10-12 Yannick Moy <m...@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.
Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 241041) +++ sem_ch3.adb (working copy) @@ -2178,10 +2178,17 @@ -- 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 @@ 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 @@ -- 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 Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 241024) +++ sem_ch7.adb (working copy) @@ -2275,6 +2275,34 @@ 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. Index: sem_ch7.ads =================================================================== --- sem_ch7.ads (revision 241024) +++ sem_ch7.ads (working copy) @@ -46,10 +46,10 @@ -- 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 Index: einfo.adb =================================================================== --- einfo.adb (revision 241024) +++ einfo.adb (working copy) @@ -610,8 +610,8 @@ -- 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 @@ 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 @@ 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 @@ 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 @@ 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 -- ------------------------ Index: einfo.ads =================================================================== --- einfo.ads (revision 241024) +++ einfo.ads (working copy) @@ -1812,6 +1812,14 @@ -- 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 @@ -- 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 @@ -- 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 @@ -- 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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); Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 241041) +++ sem_prag.adb (working copy) @@ -3410,6 +3410,13 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ -- 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