[Ada] States that act as constituents of other states

[Arnaud Charlet <charlet at adacore dot com>]

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.

Attachment: difs
Description: Text document