https://gcc.gnu.org/g:4c98b695fd8ee8246d84ba954dd59ddb87ac16d7
commit r15-1498-g4c98b695fd8ee8246d84ba954dd59ddb87ac16d7 Author: Yannick Moy <m...@adacore.com> Date: Mon May 27 12:06:47 2024 +0200 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. Diff: --- gcc/ada/ghost.adb | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index d220e0e1ec0d..84fd40ed98af 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;