This patch modifies the logic in the analysis of aspect/pragma Refined_State
to catch a case where a visible variable is used as a constituent in a state
refinement.
------------
-- Source --
------------
-- pack.ads
package Pack
with Abstract_State => State
is
Var : Integer;
procedure Proc (Formal : Integer)
with Global => (Output => State);
end Pack;
-- pack.adb
package body Pack
with Refined_State => (State => Var)
is
procedure Proc (Formal : Integer)
with Refined_Global => (Output => Var)
is begin null; end Proc;
end Pack;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnatd.V pack.adb
pack.adb:2:35: cannot use "Var" in refinement, constituent is not a hidden
state of package "Pack"
pack.adb:5:11: useless refinement, subprogram "Proc" does not mention abstract
state with visible refinement
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-17 Hristian Kirtchev <kirtc...@adacore.com>
* sem_prag.adb (Analyze_Constituent): Move the check
concerning option Part_Of to routine Check_Matching_Constituent.
(Check_Matching_Constituent): Verify that an abstract state
that acts as a constituent has the prope Part_Op option in
its aspect/pragma Abstract_State. Account for the case when a
constituent comes from a private child or private sibling.
* sem_util.ads, sem_util.adb (Is_Child_Or_Sibling): New routine.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203755)
+++ sem_prag.adb (working copy)
@@ -21439,52 +21439,75 @@
Error_Msg_NE
("duplicate use of constituent &", Constit, Constit_Id);
return;
- end if;
- -- The related package has no hidden states, nothing to match.
- -- This case arises when the constituents are states coming
- -- from a private child.
+ -- A state can act as a constituent only when it is part of
+ -- another state. This relation is expressed by option Part_Of
+ -- of pragma Abstract_State.
- if No (Hidden_States) then
- return;
+ elsif Ekind (Constit_Id) = E_Abstract_State then
+ if not Is_Part_Of (Constit_Id, State_Id) then
+ Error_Msg_Name_1 := Chars (State_Id);
+ Error_Msg_NE
+ ("state & is not a valid constituent of ancestor "
+ & "state %", Constit, Constit_Id);
+ return;
+
+ -- The constituent has the proper Part_Of option, but may
+ -- not appear in the immediate hidden state of the related
+ -- package. This case arises when the constituent comes from
+ -- a private child or a private sibling. Recognize these
+ -- scenarios to avoid generating a bogus error message.
+
+ elsif Is_Child_Or_Sibling
+ (Pack_1 => Scope (State_Id),
+ Pack_2 => Scope (Constit_Id),
+ Private_Child => True)
+ then
+ return;
+ end if;
end if;
-- Inspect the hidden states of the related package looking for
-- a match.
- State_Elmt := First_Elmt (Hidden_States);
- while Present (State_Elmt) loop
+ if Present (Hidden_States) then
+ State_Elmt := First_Elmt (Hidden_States);
+ while Present (State_Elmt) loop
- -- A valid hidden state or variable participates in a
- -- refinement. Add the constituent to the list of processed
- -- items to aid with the detection of duplicate constituent
- -- use. Remove the constituent from Hidden_States to signal
- -- that it has already been used.
+ -- A valid hidden state or variable acts as a constituent
- if Node (State_Elmt) = Constit_Id then
- Add_Item (Constit_Id, Constituents_Seen);
- Remove_Elmt (Hidden_States, State_Elmt);
+ if Node (State_Elmt) = Constit_Id then
- -- Collect the constituent in the list of refinement
- -- items. Establish a relation between the refined state
- -- and its constituent.
+ -- Add the constituent to the lis of processed items
+ -- to aid with the detection of duplicates. Remove the
+ -- constituent from Hidden_States to signal that it
+ -- has already been matched.
- Append_Elmt
- (Constit_Id, Refinement_Constituents (State_Id));
- Set_Refined_State (Constit_Id, State_Id);
+ Add_Item (Constit_Id, Constituents_Seen);
+ Remove_Elmt (Hidden_States, State_Elmt);
- -- The state has at least one legal constituent, mark the
- -- start of the refinement region. The region ends when
- -- the body declarations end (see Analyze_Declarations).
+ -- Collect the constituent in the list of refinement
+ -- items. Establish a relation between the refined
+ -- state and its constituent.
- Set_Has_Visible_Refinement (State_Id);
+ Append_Elmt
+ (Constit_Id, Refinement_Constituents (State_Id));
+ Set_Refined_State (Constit_Id, State_Id);
- return;
- end if;
+ -- The state has at least one legal constituent, mark
+ -- the start of the refinement region. The region ends
+ -- when the body declarations end (see routine
+ -- Analyze_Declarations).
- Next_Elmt (State_Elmt);
- end loop;
+ Set_Has_Visible_Refinement (State_Id);
+ return;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+
-- If we get here, we are refining a state that is not hidden
-- with respect to the related package.
@@ -21548,19 +21571,6 @@
if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then
Check_Matching_Constituent (Constit_Id);
- -- A state can act as a constituent only when it is part
- -- of another state. This relation is expressed by option
- -- "Part_Of" of pragma Abstract_State.
-
- if Ekind (Constit_Id) = E_Abstract_State
- and then not Is_Part_Of (Constit_Id, State_Id)
- then
- Error_Msg_Name_1 := Chars (State_Id);
- Error_Msg_NE
- ("state & is not a valid constituent of ancestor "
- & "state %", Constit, Constit_Id);
- end if;
-
else
Error_Msg_NE
("constituent & must denote a variable or state",
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 203755)
+++ sem_util.adb (working copy)
@@ -8324,6 +8324,181 @@
Is_RTE (Root_Type (Under), RO_WW_Super_String));
end Is_Bounded_String;
+ -------------------------
+ -- Is_Child_Or_Sibling --
+ -------------------------
+
+ function Is_Child_Or_Sibling
+ (Pack_1 : Entity_Id;
+ Pack_2 : Entity_Id;
+ Private_Child : Boolean) return Boolean
+ is
+ function Distance_From_Standard (Pack : Entity_Id) return Nat;
+ -- Given an arbitrary package, return the number of "climbs" necessary
+ -- to reach scope Standard_Standard.
+
+ procedure Equalize_Depths
+ (Pack : in out Entity_Id;
+ Depth : in out Nat;
+ Depth_To_Reach : Nat);
+ -- Given an arbitrary package, its depth and a target depth to reach,
+ -- climb the scope chain until the said depth is reached. The pointer
+ -- to the package and its depth a modified during the climb.
+
+ function Is_Child (Pack : Entity_Id) return Boolean;
+ -- Given a package Pack, determine whether it is a child package that
+ -- satisfies the privacy requirement (if set).
+
+ ----------------------------
+ -- Distance_From_Standard --
+ ----------------------------
+
+ function Distance_From_Standard (Pack : Entity_Id) return Nat is
+ Dist : Nat;
+ Scop : Entity_Id;
+
+ begin
+ Dist := 0;
+ Scop := Pack;
+ while Present (Scop) and then Scop /= Standard_Standard loop
+ Dist := Dist + 1;
+ Scop := Scope (Scop);
+ end loop;
+
+ return Dist;
+ end Distance_From_Standard;
+
+ ---------------------
+ -- Equalize_Depths --
+ ---------------------
+
+ procedure Equalize_Depths
+ (Pack : in out Entity_Id;
+ Depth : in out Nat;
+ Depth_To_Reach : Nat)
+ is
+ begin
+ -- The package must be at a greater or equal depth
+
+ if Depth < Depth_To_Reach then
+ raise Program_Error;
+ end if;
+
+ -- Climb the scope chain until the desired depth is reached
+
+ while Present (Pack) and then Depth /= Depth_To_Reach loop
+ Pack := Scope (Pack);
+ Depth := Depth - 1;
+ end loop;
+ end Equalize_Depths;
+
+ --------------
+ -- Is_Child --
+ --------------
+
+ function Is_Child (Pack : Entity_Id) return Boolean is
+ begin
+ if Is_Child_Unit (Pack) then
+ if Private_Child then
+ return Is_Private_Descendant (Pack);
+ else
+ return True;
+ end if;
+
+ -- The package is nested, it cannot act a child or a sibling
+
+ else
+ return False;
+ end if;
+ end Is_Child;
+
+ -- Local variables
+
+ P_1 : Entity_Id := Pack_1;
+ P_1_Child : Boolean := False;
+ P_1_Depth : Nat := Distance_From_Standard (P_1);
+ P_2 : Entity_Id := Pack_2;
+ P_2_Child : Boolean := False;
+ P_2_Depth : Nat := Distance_From_Standard (P_2);
+
+ -- Start of processing for Is_Child_Or_Sibling
+
+ begin
+ pragma Assert
+ (Ekind (Pack_1) = E_Package and then Ekind (Pack_2) = E_Package);
+
+ -- Both packages denote the same entity, therefore they cannot be
+ -- children or siblings.
+
+ if P_1 = P_2 then
+ return False;
+
+ -- One of the packages is at a deeper level than the other. Note that
+ -- both may still come from differen hierarchies.
+
+ -- (root) P_2
+ -- / \ :
+ -- X P_2 or X
+ -- : :
+ -- P_1 P_1
+
+ elsif P_1_Depth > P_2_Depth then
+ Equalize_Depths (P_1, P_1_Depth, P_2_Depth);
+ P_1_Child := True;
+
+ -- (root) P_1
+ -- / \ :
+ -- P_1 X or X
+ -- : :
+ -- P_2 P_2
+
+ elsif P_2_Depth > P_1_Depth then
+ Equalize_Depths (P_2, P_2_Depth, P_1_Depth);
+ P_2_Child := True;
+ end if;
+
+ -- At this stage the package pointers have been elevated to the same
+ -- depth. If the related entities are the same, then one package is a
+ -- potential child of the other:
+
+ -- P_1
+ -- :
+ -- X became P_1 P_2 or vica versa
+ -- :
+ -- P_2
+
+ if P_1 = P_2 then
+ if P_1_Child then
+ return Is_Child (Pack_1);
+ else pragma Assert (P_2_Child);
+ return Is_Child (Pack_2);
+ end if;
+
+ -- The packages may come from the same package chain or from entirely
+ -- different hierarcies. To determine this, climb the scope stack until
+ -- a common root is found.
+
+ -- (root) (root 1) (root 2)
+ -- / \ | |
+ -- P_1 P_2 P_1 P_2
+
+ else
+ while Present (P_1) and then Present (P_2) loop
+
+ -- The two packages may be siblings
+
+ if P_1 = P_2 then
+ return Is_Child (Pack_1) and then Is_Child (Pack_2);
+ end if;
+
+ P_1 := Scope (P_1);
+ P_2 := Scope (P_2);
+ end loop;
+ end if;
+
+ return False;
+ end Is_Child_Or_Sibling;
+
-----------------------------
-- Is_Concurrent_Interface --
-----------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 203568)
+++ sem_util.ads (working copy)
@@ -945,6 +945,16 @@
-- This is the RM definition, a type is a descendent of another type if it
-- is the same type or is derived from a descendent of the other type.
+ function Is_Child_Or_Sibling
+ (Pack_1 : Entity_Id;
+ Pack_2 : Entity_Id;
+ Private_Child : Boolean) return Boolean;
+ -- Determine the following relations between two arbitrary packages:
+ -- 1) One package is the parent of a child package
+ -- 2) Both packages are siblings and share a common parent
+ -- If flag Private_Child is set, then the child in case 1) or both siblings
+ -- in case 2) must be private.
+
function Is_Concurrent_Interface (T : Entity_Id) return Boolean;
-- First determine whether type T is an interface and then check whether
-- it is of protected, synchronized or task kind.
