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);
