ada: Implement change to SPARK RM rule on state refinement

SPARK RM 7.1.4(4) does not mandate anymore that a package with abstract
states has a completing body, unless the package state is mentioned in
Part_Of specifications. Implement that change.

gcc/ada/

	* sem_prag.adb (Check_Part_Of_Abstract_State): Add verification
	related to use of Part_Of, so that constituents in private childs
	that refer to state in a sibling or parent unit force that unit to
	have a body.
	* sem_util.adb (Check_State_Refinements): Drop the requirement to
	have always a package body for state refinement, when the package
	state is mentioned in no Part_Of specification.
	* sem_ch3.adb (Analyze_Declarations): Refresh SPARK refs in comment.
	* sem_ch7.adb (Analyze_Package_Declaration): Likewise.

1 files changed, 2 insertions, 1 deletions

diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index ce5a00b..61386e2 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2942,7 +2942,8 @@ package body Sem_Ch3 is
          --  Verify that all abstract states found in any package declared in
          --  the input declarative list have proper refinements. The check is
          --  performed only when the context denotes a block, entry, package,
-         --  protected, subprogram, or task body (SPARK RM 7.2.2(3)).
+         --  protected, subprogram, or task body (SPARK RM 7.1.4(4) and SPARK
+         --  RM 7.2.2(3)).
 
          Check_State_Refinements (Context);