[gcc r15-1498] ada: Fix checking of SPARK RM on ghost with concurrent part
Marc Poulhi?s
dkm@gcc.gnu.org
Thu Jun 20 08:55:39 GMT 2024
https://gcc.gnu.org/g:4c98b695fd8ee8246d84ba954dd59ddb87ac16d7
commit r15-1498-g4c98b695fd8ee8246d84ba954dd59ddb87ac16d7
Author: Yannick Moy <moy@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;
More information about the Gcc-cvs
mailing list