sem_ch6.adb (Process_Formals): Set ghost flag on formal entities of ghost subprograms.

2016-07-07  Yannick Moy  <moy@adacore.com>

	* sem_ch6.adb (Process_Formals): Set ghost flag
	on formal entities of ghost subprograms.
	* ghost.adb (Check_Ghost_Context.Is_OK_Ghost_Context): Accept ghost
	entities in use type clauses.

From-SVN: r238106

gcc/ada/ChangeLog

+2016-07-07  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb (Process_Formals): Set ghost flag
+	on formal entities of ghost subprograms.
+	* ghost.adb (Check_Ghost_Context.Is_OK_Ghost_Context): Accept ghost
+	entities in use type clauses.
+
 2016-07-06  Javier Miranda  <miranda@adacore.com>
 
 	* sem_ch6.adb (Check_Inline_Pragma): if the subprogram has no spec

gcc/ada/ghost.adb

@@ -469,6 +469,14 @@ package body Ghost is
          if Ghost_Mode > None then
             return True;
 
+         --  A Ghost type may be referenced in a use_type clause
+         --  (SPARK RM 6.9.10).
+
+         elsif Present (Parent (Context))
+           and then Nkind (Parent (Context)) = N_Use_Type_Clause
+         then
+            return True;
+
          --  Routine Expand_Record_Extension creates a parent subtype without
          --  inserting it into the tree. There is no good way of recognizing
          --  this special case as there is no parent. Try to approximate the

gcc/ada/sem_ch6.adb

@@ -10975,6 +10975,13 @@ package body Sem_Ch6 is
 
          Set_Etype (Formal, Formal_Type);
 
+         --  A formal parameter declared within a Ghost region is automatically
+         --  Ghost (SPARK RM 6.9(2)).
+
+         if Ghost_Mode > None then
+            Set_Is_Ghost_Entity (Formal);
+         end if;
+
          --  Deal with default expression if present
 
          Default := Expression (Param_Spec);