sem_ch6.adb (Process_Formals): Set ghost flag on formal entities of ghost subprograms.
authorYannick Moy <moy@adacore.com>
Thu, 7 Jul 2016 12:59:06 +0000 (12:59 +0000)
committerArnaud Charlet <charlet@gcc.gnu.org>
Thu, 7 Jul 2016 12:59:06 +0000 (14:59 +0200)
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
gcc/ada/ghost.adb
gcc/ada/sem_ch6.adb

index 8954f8b..6303d81 100644 (file)
@@ -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
index 3d3d67c..2a640a2 100644 (file)
@@ -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
index c9c0f7f..dcec1e3 100644 (file)
@@ -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);