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 --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index dea27dc8d6b65ad17b84fcda03f59cb33a6b559d..0b4a2965ad8264ae231f3869098d75df2b44d0c5 100644 (file)
--- 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 dda031f351658d5ff36d7b50f03ba733a6935d99..a809cdbaa07bb27717e8c9640d699440becbbe81 100644 (file)
--- 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