This adds support in GNAT for ghost generic formal parameters, as
included in SPARK RM 6.9.

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

gcc/ada/

	* ghost.adb (Check_Ghost_Context): Delay checking for generic
	associations.
	(Check_Ghost_Context_In_Generic_Association): Perform ghost
	checking in analyzed generic associations.
	(Check_Ghost_Formal_Procedure_Or_Package): Check SPARK RM
	6.9(13-14) for formal procedures and packages.
	(Check_Ghost_Formal_Variable): Check SPARK RM 6.9(13-14) for
	variables.
	* ghost.ads: Declarations for the above.
	* sem_ch12.adb (Analyze_Associations): Apply delayed checking
	for generic associations.
	(Analyze_Formal_Object_Declaration): Same.
	(Analyze_Formal_Subprogram_Declaration): Same.
	(Instantiate_Formal_Package): Same.
	(Instantiate_Formal_Subprogram): Same.
	(Instantiate_Object): Same.  Copy ghost aspect to newly declared
	object for actual for IN formal object. Use new function
	Get_Enclosing_Deep_Object to retrieve root object.
	(Instantiate_Type): Copy ghost aspect to declared subtype for
	actual for formal type.
	* sem_prag.adb (Analyze_Pragma): Recognize new allowed
	declarations.
	* sem_util.adb (Copy_Ghost_Aspect): Copy the ghost aspect
	between nodes.
	(Get_Enclosing_Deep_Object): New function to return enclosing
	deep object (or root for reachable part).
	* sem_util.ads (Copy_Ghost_Aspect): Same.
	(Get_Enclosing_Deep_Object): Same.
	* libgnat/s-imageu.ads: Declare formal subprograms as ghost.
	* libgnat/s-valuei.ads: Same.
	* libgnat/s-valuti.ads: Same.