This patch updates the analysis of aspect/pragma Refined_Global to interpret states and variables with an encapsulating state as constituents only when the related state has visible refinement.
------------ -- Source -- ------------ -- parent.ads package Parent with Abstract_State => State is procedure Dummy; private Var : Integer := 0 with Part_Of => State; end Parent; -- parent.adb with Parent.Priv_Child; package body Parent with Refined_State => (State => (Var, Parent.Priv_Child.Priv_State)) is procedure Dummy is begin null; end Dummy; end Parent; -- parent-priv_child.ads private package Parent.Priv_Child with Abstract_State => (Priv_State with Part_Of => State) is procedure OK (Param : Integer) with Global => (In_Out => (Var, Priv_State)); end Parent.Priv_Child; -- parent-priv_child.adb package body Parent.Priv_Child with Refined_State => (Priv_State => Priv_Var) is Priv_Var : Integer := 0; procedure OK (Param : Integer) with Refined_Global => (In_Out => (Var, Priv_Var)) is begin null; end OK; end Parent.Priv_Child; ----------------- -- Compilation -- ----------------- $ gcc -c parent-priv_child.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-19 Hristian Kirtchev <kirtc...@adacore.com> * sem_prag.adb (Check_Refined_Global_Item): A state or variable acts as a constituent only it is part of an encapsulating state and the state has visible refinement.
Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 207884) +++ sem_prag.adb (working copy) @@ -22610,10 +22610,13 @@ -- Start of processing for Check_Refined_Global_Item begin - -- The state or variable acts as a constituent of a state, collect - -- it for the state completeness checks performed later on. + -- When the state or variable acts as a constituent of another + -- state with a visible refinement, collect it for the state + -- completeness checks performed later on. - if Present (Encapsulating_State (Item_Id)) then + if Present (Encapsulating_State (Item_Id)) + and then Has_Visible_Refinement (Encapsulating_State (Item_Id)) + then if Global_Mode = Name_Input then Add_Item (Item_Id, In_Constits);