[gcc r15-6199] ada: Implement new rules about effectively volatile types in SPARK

[Marc Poulhi?s via Gcc-cvs]

https://gcc.gnu.org/g:5bb08a0ea79dc5eda62a66c844c04baa3b82f412

commit r15-6199-g5bb08a0ea79dc5eda62a66c844c04baa3b82f412
Author: Piotr Trojanek <troja...@adacore.com>
Date:   Fri Nov 22 14:31:52 2024 +0100

    ada: Implement new rules about effectively volatile types in SPARK
    
    New rules make record types effectively volatile based on the effective
    volatility of their components; same for effectively volatile for
    reading. Now volatility composition for records works like volatility
    composition for arrays.
    
    gcc/ada/ChangeLog:
    
            * sem_util.adb (Is_Effectively_Volatile,
            Is_Effectively_Volatile_For_Reading): Implement new rule for
            record types.
            * sem_util.ads (Is_Effectively_Volatile,
            Is_Effectively_Volatile_For_Reading): Adjust comments.

Diff:
---
 gcc/ada/sem_util.adb | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 gcc/ada/sem_util.ads |  4 ++++
 2 files changed, 53 insertions(+)

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index dea27dc8d6b6..0b4a2965ad82 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -16728,6 +16728,8 @@ package body Sem_Util is
    -----------------------------
 
    function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
+      Comp         : Entity_Id;
+      Has_Vol_Comp : Boolean := False;
    begin
       if Is_Type (Id) then
 
@@ -16773,6 +16775,35 @@ package body Sem_Util is
          elsif Is_Descendant_Of_Suspension_Object (Id) then
             return True;
 
+         --  A record type for which all components have an effectively
+         --  volatile type.
+
+         elsif Is_Record_Type (Id) then
+
+            --  Inspect all components defined in the scope of the type,
+            --  looking for those whose type is not effecively volatile.
+
+            Comp := First_Component (Id);
+            while Present (Comp) loop
+               if Comes_From_Source (Comp) then
+                  if Is_Effectively_Volatile (Etype (Comp)) then
+                     Has_Vol_Comp := True;
+
+                  --  The component is not effecively volatile
+
+                  else
+                     return False;
+                  end if;
+               end if;
+
+               Next_Component (Comp);
+            end loop;
+
+            --  If we get here, then all components are of an effectively
+            --  volatile type.
+
+            return Has_Vol_Comp;
+
          --  Otherwise the type is not effectively volatile
 
          else
@@ -16801,6 +16832,7 @@ package body Sem_Util is
    function Is_Effectively_Volatile_For_Reading
      (Id : Entity_Id) return Boolean
    is
+      Comp : Entity_Id;
    begin
       --  A concurrent type is effectively volatile for reading
 
@@ -16839,6 +16871,23 @@ package body Sem_Util is
                  and then Is_Effectively_Volatile_For_Reading
                    (Component_Type (Anc));
             end;
+
+         --  In addition, a record type is effectively volatile for reading
+         --  if at least one component has an effectively volatile type for
+         --  reading.
+
+         elsif Is_Record_Type (Id) then
+            Comp := First_Component (Id);
+            while Present (Comp) loop
+               if Comes_From_Source (Comp)
+                 and then Is_Effectively_Volatile_For_Reading (Etype (Comp))
+               then
+                  return True;
+               end if;
+               Next_Component (Comp);
+            end loop;
+
+            return False;
          end if;
       end if;
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index dda031f35165..a809cdbaa07b 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1968,6 +1968,8 @@ package Sem_Util is
    --    * Volatile without No_Caching
    --    * An array type subject to aspect Volatile_Components
    --    * An array type whose component type is effectively volatile
+   --    * A record type for which all components have an effectively volatile
+   --      type
    --    * A protected type
    --    * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
 
@@ -1982,6 +1984,8 @@ package Sem_Util is
    --      Async_Writers and Effective_Reads set to False
    --    * An array type whose component type is effectively volatile for
    --      reading
+   --    * A record type for which at least one component has an effectively
+   --      volatile type for reading
    --    * A protected type
    --    * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object