diff options
| author | Yannick Moy <moy@adacore.com> | 2024-05-27 12:06:47 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-06-20 10:50:58 +0200 |
| commit | 4c98b695fd8ee8246d84ba954dd59ddb87ac16d7 (patch) | |
| tree | 0f658dad85de347885ac1d2e6a960f8c8c9cd760 /gcc | |
| parent | a688a0281946b1cc11333ca548db031a9aa0e9fd (diff) | |
| download | gcc-4c98b695fd8ee8246d84ba954dd59ddb87ac16d7.zip gcc-4c98b695fd8ee8246d84ba954dd59ddb87ac16d7.tar.gz gcc-4c98b695fd8ee8246d84ba954dd59ddb87ac16d7.tar.bz2 | |
ada: Fix checking of SPARK RM on ghost with concurrent part
SPARK RM 6.9(21) forbids a ghost type to have concurrent parts.
This was not enforced, instead only the type itself was checked to
be concurrent. Now fixed.
gcc/ada/
* ghost.adb (Check_Ghost_Type): Fix checking.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ghost.adb | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index d220e0e..84fd40e 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -1054,7 +1054,9 @@ package body Ghost is Full_Typ : Entity_Id; begin - if Is_Ghost_Entity (Typ) then + if Is_Ghost_Entity (Typ) + and then Comes_From_Source (Typ) + then Conc_Typ := Empty; Full_Typ := Typ; @@ -1062,7 +1064,9 @@ package body Ghost is Conc_Typ := Anonymous_Object (Typ); Full_Typ := Conc_Typ; - elsif Is_Concurrent_Type (Typ) then + elsif Has_Protected (Typ) + or else Has_Task (Typ) + then Conc_Typ := Typ; end if; |