diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2016-07-07 12:59:06 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2016-07-07 12:59:06 +0000 |
| commit | 5842a2886551114b1e3207c717f3334293dfc2ab (patch) | |
| tree | 2424008a13a9abb7c2ef895df45f86d0050bcde6 | |
| parent | eeb6872bfdfd1e71b27de6f62a5f5c08a2efb015 (diff) | |
| download | gcc-5842a2886551114b1e3207c717f3334293dfc2ab.tar.gz | |
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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@238106 138bc75d-0d04-0410-961f-82ee72b054a4
| -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 8954f8b04ea..6303d819fd7 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 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); |