This patch modifies the legality checks of aspect/pragma Refined_State to
ensure that when a state acts as a constituent of another state, the said state
has a Part_Of dependency in its corresponding aspect/pragma Abstract_State.
------------
-- Source --
------------
-- abstract_state_illegal.ads
package Abstract_State_Illegal
with Abstract_State => State
is
procedure P;
end Abstract_State_Illegal;
-- abstract_state_illegal.adb
with Abstract_State_Illegal.Pr_Child;
package body Abstract_State_Illegal
with Refined_State => (State => Abstract_State_Illegal.Pr_Child.Pr_State)
is
procedure P is begin null; end P;
end Abstract_State_Illegal;
-- abstract_state_illegal-pub_child.ads
package Abstract_State_Illegal.Pub_Child
with Abstract_State => Pub_State
is
procedure Pub_P;
end Abstract_State_Illegal.Pub_Child;
-- abstract_state_illegal-pub_child.adb
with Abstract_State_Illegal.Pr_Child;
package body Abstract_State_Illegal.Pub_Child
with Refined_State =>
(Pub_State => Abstract_State_Illegal.Pr_Child.Pr_State)
is
procedure Pub_P is begin null; end Pub_P;
end Abstract_State_Illegal.Pub_Child;
-- abstract_state_illegal-pr_child.ads
private package Abstract_State_Illegal.Pr_Child
with Abstract_State => (Pr_State with Part_Of => State)
is
procedure Pr_P;
end Abstract_State_Illegal.Pr_Child;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnatd.V abstract_state_illegal.adb
$ gcc -c -gnatd.V abstract_state_illegal-pub_child.adb
abstract_state_illegal-pub_child.adb:4:71: state "Pr_State" is not a valid
constituent of ancestor state "Pub_State"
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-15 Hristian Kirtchev <[email protected]>
* sem_prag.adb (Analyze_Constituent): When
a state acts as a constituent of another state, ensure that
the said state has a Part_Of dependency in its corresponding
aspect/pragma Abstract_State.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203594)
+++ sem_prag.adb (working copy)
@@ -21521,6 +21521,20 @@
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",
