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 <kirtc...@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.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 229414)
+++ sem_prag.adb (working copy)
@@ -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
