[Ada] States that act as constituents of other states

Arnaud Charlet charlet@adacore.com
Tue Oct 15 10:49:00 GMT 2013


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  <kirtchev@adacore.com>

	* 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.

-------------- next part --------------
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",


More information about the Gcc-patches mailing list