diff options
| author | Yannick Moy <moy@adacore.com> | 2016-07-07 12:59:06 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-07-07 14:59:06 +0200 |
| commit | 0bb97bdf5adbeedb4de5551438a65554c99befaf (patch) | |
| tree | 2424008a13a9abb7c2ef895df45f86d0050bcde6 /gcc/ada | |
| parent | f965d3dad7edb527e465d7d2811294177daee53c (diff) | |
| download | gcc-0bb97bdf5adbeedb4de5551438a65554c99befaf.zip gcc-0bb97bdf5adbeedb4de5551438a65554c99befaf.tar.gz gcc-0bb97bdf5adbeedb4de5551438a65554c99befaf.tar.bz2 | |
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
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
| -rw-r--r-- | gcc/ada/ghost.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 7 |
3 files changed, 22 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8954f8b..6303d81 100644 --- 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 3d3d67c..2a640a2 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 c9c0f7f..dcec1e3 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); |