[Ada] Spurious error on legal synchronized constituent

This patch corrects the predicate which determines whether an entity denotes a
synchronized object as per SPARK RM 9.1. to account for a case where the object
is not atomic, but its type is.

The patch also cleans up various atomic object-related predicates.

2018-05-30  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* sem_util.adb (Is_Atomic_Object): Cleaned up. Split the entity logic
	in a separate routine.
	(Is_Atomic_Object_Entity): New routine.
	(Is_Atomic_Prefix): Cleaned up.
	(Is_Synchronized_Object): Check that the object is atomic, or its type
	is atomic.
	(Object_Has_Atomic_Components): Removed.
	* sem_util.ads (Is_Atomic_Object): Reword the comment on usage.
	(Is_Atomic_Object_Entity): New routine.

gcc/testsuite/

	* gnat.dg/synchronized1.adb, gnat.dg/synchronized1.ads: New testcase.

From-SVN: r260933

gcc/ada/ChangeLog

+2018-05-30  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_util.adb (Is_Atomic_Object): Cleaned up. Split the entity logic
+	in a separate routine.
+	(Is_Atomic_Object_Entity): New routine.
+	(Is_Atomic_Prefix): Cleaned up.
+	(Is_Synchronized_Object): Check that the object is atomic, or its type
+	is atomic.
+	(Object_Has_Atomic_Components): Removed.
+	* sem_util.ads (Is_Atomic_Object): Reword the comment on usage.
+	(Is_Atomic_Object_Entity): New routine.
+
 2018-05-30  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch3.adb (Access_Subprogram_Declaration): The flag

gcc/ada/sem_util.adb

@@ -13156,86 +13156,84 @@ package body Sem_Util is
    ----------------------
 
    function Is_Atomic_Object (N : Node_Id) return Boolean is
+      function Is_Atomic_Entity (Id : Entity_Id) return Boolean;
+      pragma Inline (Is_Atomic_Entity);
+      --  Determine whether arbitrary entity Id is either atomic or has atomic
+      --  components.
 
-      function Object_Has_Atomic_Components (N : Node_Id) return Boolean;
-      --  Determines if given object has atomic components
-
-      function Is_Atomic_Prefix (N : Node_Id) return Boolean;
-      --  If prefix is an implicit dereference, examine designated type
+      function Is_Atomic_Prefix (Pref : Node_Id) return Boolean;
+      --  Determine whether prefix Pref of a indexed or selected component is
+      --  an atomic object.
 
       ----------------------
-      -- Is_Atomic_Prefix --
+      -- Is_Atomic_Entity --
       ----------------------
 
-      function Is_Atomic_Prefix (N : Node_Id) return Boolean is
+      function Is_Atomic_Entity (Id : Entity_Id) return Boolean is
       begin
-         if Is_Access_Type (Etype (N)) then
-            return
-              Has_Atomic_Components (Designated_Type (Etype (N)));
-         else
-            return Object_Has_Atomic_Components (N);
-         end if;
-      end Is_Atomic_Prefix;
+         return Is_Atomic (Id) or else Has_Atomic_Components (Id);
+      end Is_Atomic_Entity;
+
+      ----------------------
+      -- Is_Atomic_Prefix --
+      ----------------------
 
-      ----------------------------------
-      -- Object_Has_Atomic_Components --
-      ----------------------------------
+      function Is_Atomic_Prefix (Pref : Node_Id) return Boolean is
+         Typ : constant Entity_Id := Etype (Pref);
 
-      function Object_Has_Atomic_Components (N : Node_Id) return Boolean is
       begin
-         if Has_Atomic_Components (Etype (N))
-           or else Is_Atomic (Etype (N))
-         then
-            return True;
+         if Is_Access_Type (Typ) then
+            return Has_Atomic_Components (Designated_Type (Typ));
 
-         elsif Is_Entity_Name (N)
-           and then (Has_Atomic_Components (Entity (N))
-                      or else Is_Atomic (Entity (N)))
-         then
+         elsif Is_Atomic_Entity (Typ) then
             return True;
 
-         elsif Nkind (N) = N_Selected_Component
-           and then Is_Atomic (Entity (Selector_Name (N)))
+         elsif Is_Entity_Name (Pref)
+           and then Is_Atomic_Entity (Entity (Pref))
          then
             return True;
 
-         elsif Nkind (N) = N_Indexed_Component
-           or else Nkind (N) = N_Selected_Component
-         then
-            return Is_Atomic_Prefix (Prefix (N));
+         elsif Nkind (Pref) = N_Indexed_Component then
+            return Is_Atomic_Prefix (Prefix (Pref));
 
-         else
-            return False;
+         elsif Nkind (Pref) = N_Selected_Component then
+            return
+              Is_Atomic_Prefix (Prefix (Pref))
+                or else Is_Atomic (Entity (Selector_Name (Pref)));
          end if;
-      end Object_Has_Atomic_Components;
+
+         return False;
+      end Is_Atomic_Prefix;
 
    --  Start of processing for Is_Atomic_Object
 
    begin
-      --  Predicate is not relevant to subprograms
+      if Is_Entity_Name (N) then
+         return Is_Atomic_Object_Entity (Entity (N));
 
-      if Is_Entity_Name (N) and then Is_Overloadable (Entity (N)) then
-         return False;
+      elsif Nkind (N) = N_Indexed_Component then
+         return Is_Atomic (Etype (N)) or else Is_Atomic_Prefix (Prefix (N));
 
-      elsif Is_Atomic (Etype (N))
-        or else (Is_Entity_Name (N) and then Is_Atomic (Entity (N)))
-      then
-         return True;
+      elsif Nkind (N) = N_Selected_Component then
+         return
+           Is_Atomic (Etype (N))
+             or else Is_Atomic_Prefix (Prefix (N))
+             or else Is_Atomic (Entity (Selector_Name (N)));
+      end if;
 
-      elsif Nkind (N) = N_Selected_Component
-        and then Is_Atomic (Entity (Selector_Name (N)))
-      then
-         return True;
+      return False;
+   end Is_Atomic_Object;
 
-      elsif Nkind (N) = N_Indexed_Component
-        or else Nkind (N) = N_Selected_Component
-      then
-         return Is_Atomic_Prefix (Prefix (N));
+   -----------------------------
+   -- Is_Atomic_Object_Entity --
+   -----------------------------
 
-      else
-         return False;
-      end if;
-   end Is_Atomic_Object;
+   function Is_Atomic_Object_Entity (Id : Entity_Id) return Boolean is
+   begin
+      return
+        Is_Object (Id)
+          and then (Is_Atomic (Id) or else Is_Atomic (Etype (Id)));
+   end Is_Atomic_Object_Entity;
 
    -----------------------------
    -- Is_Atomic_Or_VFA_Object --
@@ -17353,7 +17351,9 @@ package body Sem_Util is
          --  The object is synchronized if it is atomic and Async_Writers is
          --  enabled.
 
-         elsif Is_Atomic (Id) and then Async_Writers_Enabled (Id) then
+         elsif Is_Atomic_Object_Entity (Id)
+           and then Async_Writers_Enabled (Id)
+         then
             return True;
 
          --  A constant is a synchronized object by default

gcc/ada/sem_util.ads

@@ -1512,12 +1512,16 @@ package Sem_Util is
    --  Determine whether package E1 is an ancestor of E2
 
    function Is_Atomic_Object (N : Node_Id) return Boolean;
-   --  Determines if the given node denotes an atomic object in the sense of
-   --  the legality checks described in RM C.6(12).
+   --  Determine whether arbitrary node N denotes a reference to an atomic
+   --  object as per Ada RM C.6(12).
+
+   function Is_Atomic_Object_Entity (Id : Entity_Id) return Boolean;
+   --  Determine whether arbitrary entity Id denotes an atomic object as per
+   --  Ada RM C.6(12).
 
    function Is_Atomic_Or_VFA_Object (N : Node_Id) return Boolean;
-   --  Determines if the given node is an atomic object (Is_Atomic_Object true)
-   --  or else is an object for which VFA is present.
+   --  Determine whether arbitrary node N denotes a reference to an object
+   --  which is either atomic or Volatile_Full_Access.
 
    function Is_Attribute_Result (N : Node_Id) return Boolean;
    --  Determine whether node N denotes attribute 'Result

gcc/testsuite/ChangeLog

+2018-05-30  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* gnat.dg/synchronized1.adb, gnat.dg/synchronized1.ads: New testcase.
+
 2018-05-29  Uros Bizjak  <ubizjak@gmail.com>
 
 	PR target/85950

gcc/testsuite/gnat.dg/synchronized1.adb

+-- { dg-do compile }
+-- { dg-options "-gnatws" }
+
+package body Synchronized1
+  with SPARK_Mode,
+       Refined_State => (State => Curr_State)
+is
+   type Reactor_State is (Stopped, Working) with Atomic;
+
+   Curr_State : Reactor_State
+     with Async_Readers, Async_Writers;
+
+   procedure Force_Body is null;
+end Synchronized1;

gcc/testsuite/gnat.dg/synchronized1.ads

+package Synchronized1
+  with SPARK_Mode,
+       Abstract_State => (State with Synchronous),
+       Initializes    => State
+is
+   procedure Force_Body;
+end Synchronized1;