diff mbox series

[COMMITTED,29/30] ada: Fix checking of SPARK RM on ghost with concurrent part

Message ID 20240620085321.2412421-29-poulhies@adacore.com
State New
Headers show
Series [COMMITTED,01/30] ada: Fix list of attributes defined by Ada 2022 | expand

Commit Message

Marc Poulhiès June 20, 2024, 8:53 a.m. UTC 
From: Yannick Moy <moy@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/ghost.adb | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index d220e0e1ec0..84fd40ed98a 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;