[Ada] SPARK: update for effectively volatile types and objects

gcc/ada/

	* sem_prag.adb (Analyze_Global_In_Decl_Part): Update check to
	reject volatile object for reading.
	* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Update
	check to reject volatile object for reading.
	* sem_util.adb, sem_util.ads
	(Check_Nonvolatile_Function_Profile,
	Has_Effectively_Volatile_Profile): Detect use of volatile object
	for reading.
	(Has_Enabled_Property): Accept constants as well.
	(Is_Effectively_Volatile_For_Reading): New function based on
	existing Is_Effectively_Volatile.
	(Is_Effectively_Volatile_Object_For_Reading): Adapted from the
	existing Is_Effectively_Volatile_Object, using a shared
	implementation in Is_Effectively_Volatile_Object_Shared.

1 files changed, 101 insertions, 12 deletions

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 2b92cad..9b67a45 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -127,6 +127,15 @@ package body Sem_Util is
    --  Determine whether arbitrary entity Id denotes an atomic object as per
    --  RM C.6(7).
 
+   generic
+      with function Is_Effectively_Volatile_Entity
+        (Id : Entity_Id) return Boolean;
+      --  Function to use on object and type entities
+   function Is_Effectively_Volatile_Object_Shared
+     (N : Node_Id) return Boolean;
+   --  Shared function used to detect effectively volatile objects and
+   --  effectively volatile objects for reading.
+
    function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean;
    --  Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type
    --  with discriminants whose default values are static, examine only the
@@ -3626,7 +3635,7 @@ package body Sem_Util is
 
       Formal := First_Formal (Func_Id);
       while Present (Formal) loop
-         if Is_Effectively_Volatile (Etype (Formal)) then
+         if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then
             Error_Msg_NE
               ("nonvolatile function & cannot have a volatile parameter",
                Formal, Func_Id);
@@ -3637,7 +3646,7 @@ package body Sem_Util is
 
       --  Inspect the return type
 
-      if Is_Effectively_Volatile (Etype (Func_Id)) then
+      if Is_Effectively_Volatile_For_Reading (Etype (Func_Id)) then
          Error_Msg_NE
            ("nonvolatile function & cannot have a volatile return type",
             Result_Definition (Parent (Func_Id)), Func_Id);
@@ -11222,11 +11231,11 @@ package body Sem_Util is
 
    begin
       --  Inspect the formal parameters looking for an effectively volatile
-      --  type.
+      --  type for reading.
 
       Formal := First_Formal (Subp_Id);
       while Present (Formal) loop
-         if Is_Effectively_Volatile (Etype (Formal)) then
+         if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then
             return True;
          end if;
 
@@ -11236,7 +11245,7 @@ package body Sem_Util is
       --  Inspect the return type of functions
 
       if Ekind (Subp_Id) in E_Function | E_Generic_Function
-        and then Is_Effectively_Volatile (Etype (Subp_Id))
+        and then Is_Effectively_Volatile_For_Reading (Etype (Subp_Id))
       then
          return True;
       end if;
@@ -11610,7 +11619,7 @@ package body Sem_Util is
       if Ekind (Item_Id) = E_Abstract_State then
          return State_Has_Enabled_Property;
 
-      elsif Ekind (Item_Id) = E_Variable then
+      elsif Ekind (Item_Id) in E_Variable | E_Constant then
          return Type_Or_Variable_Has_Enabled_Property (Item_Id);
 
       --  Other objects can only inherit properties through their type. We
@@ -15747,35 +15756,115 @@ package body Sem_Util is
       end if;
    end Is_Effectively_Volatile;
 
+   -----------------------------------------
+   -- Is_Effectively_Volatile_For_Reading --
+   -----------------------------------------
+
+   function Is_Effectively_Volatile_For_Reading
+     (Id : Entity_Id) return Boolean
+   is
+   begin
+      --  A concurrent type is effectively volatile for reading
+
+      if Is_Concurrent_Type (Id) then
+         return True;
+
+      elsif Is_Effectively_Volatile (Id) then
+
+        --  Other volatile types and objects are effectively volatile for
+        --  reading when they have property Async_Writers or Effective_Reads
+        --  set to True. This includes the case of an array type whose
+        --  Volatile_Components aspect is True (hence it is effectively
+        --  volatile) which does not have the properties Async_Writers
+        --  and Effective_Reads set to False.
+
+         if Async_Writers_Enabled (Id)
+           or else Effective_Reads_Enabled (Id)
+         then
+            return True;
+
+         --  In addition, an array type is effectively volatile for reading
+         --  when its component type is effectively volatile for reading.
+
+         elsif Is_Array_Type (Id) then
+            declare
+               Anc : Entity_Id := Base_Type (Id);
+            begin
+               if Is_Private_Type (Anc) then
+                  Anc := Full_View (Anc);
+               end if;
+
+               --  Test for presence of ancestor, as the full view of a
+               --  private type may be missing in case of error.
+
+               return
+                 Present (Anc)
+                   and then Is_Effectively_Volatile_For_Reading
+                     (Component_Type (Anc));
+            end;
+         end if;
+      end if;
+
+      return False;
+
+   end Is_Effectively_Volatile_For_Reading;
+
    ------------------------------------
    -- Is_Effectively_Volatile_Object --
    ------------------------------------
 
    function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is
+      function Is_Effectively_Volatile_Object_Inst
+      is new Is_Effectively_Volatile_Object_Shared (Is_Effectively_Volatile);
+   begin
+      return Is_Effectively_Volatile_Object_Inst (N);
+   end Is_Effectively_Volatile_Object;
+
+   ------------------------------------------------
+   -- Is_Effectively_Volatile_Object_For_Reading --
+   ------------------------------------------------
+
+   function Is_Effectively_Volatile_Object_For_Reading
+     (N : Node_Id) return Boolean
+   is
+      function Is_Effectively_Volatile_Object_For_Reading_Inst
+      is new Is_Effectively_Volatile_Object_Shared
+        (Is_Effectively_Volatile_For_Reading);
+   begin
+      return Is_Effectively_Volatile_Object_For_Reading_Inst (N);
+   end Is_Effectively_Volatile_Object_For_Reading;
+
+   -------------------------------------------
+   -- Is_Effectively_Volatile_Object_Shared --
+   -------------------------------------------
+
+   function Is_Effectively_Volatile_Object_Shared
+     (N : Node_Id) return Boolean
+   is
    begin
       if Is_Entity_Name (N) then
          return Is_Object (Entity (N))
-           and then Is_Effectively_Volatile (Entity (N));
+           and then Is_Effectively_Volatile_Entity (Entity (N));
 
       elsif Nkind (N) in N_Indexed_Component | N_Slice then
-         return Is_Effectively_Volatile_Object (Prefix (N));
+         return Is_Effectively_Volatile_Object_Shared (Prefix (N));
 
       elsif Nkind (N) = N_Selected_Component then
          return
-           Is_Effectively_Volatile_Object (Prefix (N))
+           Is_Effectively_Volatile_Object_Shared (Prefix (N))
              or else
-           Is_Effectively_Volatile_Object (Selector_Name (N));
+           Is_Effectively_Volatile_Object_Shared (Selector_Name (N));
 
       elsif Nkind (N) in N_Qualified_Expression
                        | N_Unchecked_Type_Conversion
                        | N_Type_Conversion
       then
-         return Is_Effectively_Volatile_Object (Expression (N));
+         return Is_Effectively_Volatile_Object_Shared (Expression (N));
 
       else
          return False;
       end if;
-   end Is_Effectively_Volatile_Object;
+   end Is_Effectively_Volatile_Object_Shared;
 
    -------------------
    -- Is_Entry_Body --