From 0bb97bdf5adbeedb4de5551438a65554c99befaf Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 7 Jul 2016 12:59:06 +0000 Subject: [PATCH] sem_ch6.adb (Process_Formals): Set ghost flag on formal entities of ghost subprograms. 2016-07-07 Yannick Moy * 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 | 7 +++++++ gcc/ada/ghost.adb | 8 ++++++++ gcc/ada/sem_ch6.adb | 7 +++++++ 3 files changed, 22 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8954f8b04ea..6303d819fd7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2016-07-07 Yannick Moy + + * 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 * 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 3d3d67c995c..2a640a2b88c 100644 --- 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 c9c0f7f4605..dcec1e33d57 100644 --- 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); -- 2.30.2