commit 83e8d37fe39d7c1afce19b61bbc2dd828fa37c6f
author Yannick Moy <moy@adacore.com> Thu Nov 24 16:27:37 2022 +0100
committer Marc Poulhiès <poulhies@adacore.com> Mon Nov 28 13:02:31 2022 +0100
tree 70e71a68004e8053d451c58c5d08892b5f950749
parent 2b293a949c0fbe21e47c4bc99f807dc941c02bb6

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.