[Ada] Removal of SPARK RM 6.9 (11)

[Arnaud Charlet <charlet at adacore dot com>]

This patch removes the (incorrect) implementation of the following rule:

   SPARK RM 6.9 (11) - A non-ghost library unit package or generic package
   specification shall not require a completion solely because of ghost
   declarations. [In other words, if a library unit package or generic package
   specification requires a body, then it must still require a body if all of
   the ghost declarations therein were to be removed.

The patch also updates references to SPARK RM 6.9 in various compiler files.

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-05-22  Hristian Kirtchev  <kirtchev@adacore.com>

	* ghost.adb (Check_Ghost_Completion): Update references to SPARK
	RM 6.9 rules.
	(Check_Ghost_Policy): Update references to SPARK RM 6.9 rules.
	* sem_ch3.adb (Analyze_Object_Declaration): Update references
	to SPARK RM 6.9 rules.
	(Check_Completion): Ghost entities do not require a special form of
	completion.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body): Update references
	to SPARK RM 6.9 rules.
	(Analyze_Subprogram_Body_Helper): Update references to SPARK RM 6.9
	rules.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Update references
	to SPARK RM 6.9 rules.
	(Requires_Completion_In_Body): Ghost entities do not require a special
	form of completion.

Attachment: difs
Description: Text document