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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8954f8b04ea52bf0e2fa1ea1f3f2bb8fdf579f81..6303d819fd7cc9d0c7e58e341f2e98c718c62670 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+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

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 3d3d67c995cd37f28383e448f31616af9f950855..2a640a2b88c14b00b53928914109d2197cb114ea 100644 (file)
--- a/gcc/ada/ghost.adb
+++ b/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

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index c9c0f7f46056f02f97012f993034bf4c9181e69f..dcec1e33d57a65be14d16ebf8f4d312a35abbbd1 100644 (file)
--- a/gcc/ada/sem_ch6.adb
+++ b/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);