[Ada] Support ghost generic formal parameters

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

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.

1 files changed, 11 insertions, 0 deletions

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index de7883c..a8afda0 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -625,6 +625,11 @@ package Sem_Util is
    --  create a new compatible record type. Loc is the source location assigned
    --  to the created nodes.
 
+   procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id);
+   --  Copy the Ghost aspect if present in the aspect specifications of node
+   --  From to node To. On entry it is assumed that To does not have aspect
+   --  specifications. If From has no aspects, the routine has no effect.
+
    function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
    --  Utility to create a parameter profile for a new subprogram spec, when
    --  the subprogram has a body that acts as spec. This is done for some cases
@@ -1183,6 +1188,12 @@ package Sem_Util is
    --  If expression N references a part of an object, return this object.
    --  Otherwise return Empty. Expression N should have been resolved already.
 
+   function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id;
+   --  If expression N references a reachable part of an object (as defined in
+   --  SPARK RM 6.9), return this object. Otherwise return Empty. It is similar
+   --  to Get_Enclosing_Object, but treats pointer dereference like component
+   --  selection. Expression N should have been resolved already.
+
    function Get_Generic_Entity (N : Node_Id) return Entity_Id;
    --  Returns the true generic entity in an instantiation. If the name in the
    --  instantiation is a renaming, the function returns the renamed generic.