===================================================================
@@ -527,7 +527,7 @@
-- E_Constant - "constant"
-- E_Discriminant - "discriminant"
-- E_Generic_In_Out_Parameter - "generic parameter"
- -- E_Generic_Out_Parameter - "generic parameter"
+ -- E_Generic_In_Parameter - "generic parameter"
-- E_In_Parameter - "parameter"
-- E_In_Out_Parameter - "parameter"
-- E_Loop_Parameter - "loop parameter"
@@ -24057,6 +24057,9 @@
Spec_Id : Entity_Id;
-- The entity of the subprogram subject to pragma Refined_Global
+ States : Elist_Id := No_Elist;
+ -- A list of all states with visible refinement found in pragma Global
+
procedure Check_In_Out_States;
-- Determine whether the corresponding Global pragma mentions In_Out
-- states with visible refinement and if so, ensure that one of the
@@ -24566,11 +24569,14 @@
begin
-- When the state or object acts as a constituent of another
-- state with a visible refinement, collect it for the state
- -- completeness checks performed later on.
+ -- completeness checks performed later on. Note that the item
+ -- acts as a constituent only when the encapsulating state is
+ -- present in pragma Global.
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 Contains (States, Encapsulating_State (Item_Id))
then
if Global_Mode = Name_Input then
Append_New_Elmt (Item_Id, In_Constits);
@@ -24715,6 +24721,8 @@
Has_Null_State := True;
elsif Has_Non_Null_Refinement (Item_Id) then
+ Append_New_Elmt (Item_Id, States);
+
if Item_Mode = Name_Input then
Has_In_State := True;
elsif Item_Mode = Name_In_Out then
This patch modifies the analysis of pragma Refined_Global to treat objects and states as constituents only when their encapsulating state appears in pragma Global. ------------ -- Source -- ------------ -- pack.ads package Pack with Abstract_State => (State1, State2), Initializes => (Var, State1, State2) is Var : Integer := 0; procedure Initialize_State with Global => (Output => State1), Depends => (State1 => null); end Pack; -- pack.adb package body Pack with Refined_State => (State1 => (A, B), State2 => (Inner.Inner_Var, Inner.Inner_State)) is A, B : Integer; package Inner with Abstract_State => Inner_State, Initializes => (Inner_State, Inner_Var => Var) is Inner_Var : Integer; procedure Initialize_Inner with Global => (Output => (Inner_State, Inner_Var), Input => Var), Depends => (Inner_State => null, Inner_Var => Var); end Inner; procedure Initialize_State is separate with Refined_Global => (Output => (A, B)), Refined_Depends => ((A, B) => null); procedure Double_B is separate with Global => (In_Out => B), Depends => (B => B); package body Inner is separate; begin Initialize_State; Double_B; end Pack; -- pack-double_b.adb separate (Pack) procedure Double_B is begin B := B * 2; end Double_B; -- pack-initialize_state.adb separate (Pack) procedure Initialize_State is begin A := 0; B := 0; end Initialize_State; -- pack-inner.adb separate (Pack) package body Inner with Refined_State => (Inner_State => Inner_Body_Var) is Inner_Body_Var : Integer; procedure Initialize_Inner with Refined_Global => (Output => (Inner_Body_Var, Inner_Var), Input => Var), Refined_Depends => (Inner_Body_Var => null, Inner_Var => Var) is begin Inner_Body_Var := 0; Inner_Var := Var; end Initialize_Inner; begin Initialize_Inner; end Inner; ----------------- -- Compilation -- ----------------- $ gcc -c pack.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-27 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Analyze_Refined_Global_In_Decl_Part): Add variable States. (Check_Refined_Global_Item): An object or state acts as a constituent only when the corresponding encapsulating state appears in pragma Global. (Collect_Global_Item): Add a state with non-null visible refinement to list States.