[Ada] Spurious error on synchronous refinement

This patch ensures that an abstract state declared with simple option
"synchronous" is automatically considered "external".

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

gcc/ada/

	* einfo.adb (Is_External_State): An abstract state is also external
	when it is declared with option "synchronous".
	* einfo.ads: Update the documentation of synthesized attribute
	Is_External_State.
	* sem_util.adb (Find_Simple_Properties): New routine.
	(Is_Enabled_External_Property): New routine.
	(State_Has_Enabled_Property): Reimplemented. The two flavors of option
	External have precedence over option Synchronous when determining
	whether a property is in effect.

gcc/testsuite/

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

From-SVN: r260453

gcc/ada/ChangeLog

+2018-05-21  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.adb (Is_External_State): An abstract state is also external
+	when it is declared with option "synchronous".
+	* einfo.ads: Update the documentation of synthesized attribute
+	Is_External_State.
+	* sem_util.adb (Find_Simple_Properties): New routine.
+	(Is_Enabled_External_Property): New routine.
+	(State_Has_Enabled_Property): Reimplemented. The two flavors of option
+	External have precedence over option Synchronous when determining
+	whether a property is in effect.
+
 2018-04-04  Yannick Moy  <moy@adacore.com>
 
 	* sem_eval.adb (Static_Length): Take into account case of variable of

gcc/ada/einfo.adb

@@ -8083,8 +8083,14 @@ package body Einfo is
 
    function Is_External_State (Id : E) return B is
    begin
+      --  To qualify, the abstract state must appear with option "external" or
+      --  "synchronous" (SPARK RM 7.1.4(8) and (10)).
+
       return
-        Ekind (Id) = E_Abstract_State and then Has_Option (Id, Name_External);
+        Ekind (Id) = E_Abstract_State
+          and then (Has_Option (Id, Name_External)
+                      or else
+                    Has_Option (Id, Name_Synchronous));
    end Is_External_State;
 
    ------------------
@@ -8255,6 +8261,9 @@ package body Einfo is
 
    function Is_Synchronized_State (Id : E) return B is
    begin
+      --  To qualify, the abstract state must appear with simple option
+      --  "synchronous" (SPARK RM 7.1.4(10)).
+
       return
         Ekind (Id) = E_Abstract_State
           and then Has_Option (Id, Name_Synchronous);

gcc/ada/einfo.ads

@@ -2553,7 +2553,7 @@ package Einfo is
 
 --    Is_External_State (synthesized)
 --       Applies to all entities, true for abstract states that are subject to
---       option External.
+--       option External or Synchronous.
 
 --    Is_Finalized_Transient (Flag252)
 --       Defined in constants, loop parameters of generalized iterators, and

gcc/ada/sem_util.adb

@@ -10262,38 +10262,59 @@ package body Sem_Util is
 
       function State_Has_Enabled_Property return Boolean is
          Decl : constant Node_Id := Parent (Item_Id);
+
+         procedure Find_Simple_Properties
+           (Has_External    : out Boolean;
+            Has_Synchronous : out Boolean);
+         --  Extract the simple properties associated with declaration Decl
+
+         function Is_Enabled_External_Property return Boolean;
+         --  Determine whether property Property appears within the external
+         --  property list of declaration Decl, and return its status.
+
+         ----------------------------
+         -- Find_Simple_Properties --
+         ----------------------------
+
+         procedure Find_Simple_Properties
+           (Has_External    : out Boolean;
+            Has_Synchronous : out Boolean)
+         is
             Opt : Node_Id;
-         Opt_Nam  : Node_Id;
-         Prop     : Node_Id;
-         Prop_Nam : Node_Id;
-         Props    : Node_Id;
 
          begin
-         --  The declaration of an external abstract state appears as an
-         --  extension aggregate. If this is not the case, properties can never
-         --  be set.
+            --  Assume that none of the properties are available
 
-         if Nkind (Decl) /= N_Extension_Aggregate then
-            return False;
-         end if;
-
-         --  When External appears as a simple option, it automatically enables
-         --  all properties.
+            Has_External    := False;
+            Has_Synchronous := False;
 
             Opt := First (Expressions (Decl));
             while Present (Opt) loop
-            if Nkind (Opt) = N_Identifier
-              and then Chars (Opt) = Name_External
-            then
-               return True;
+               if Nkind (Opt) = N_Identifier then
+                  if Chars (Opt) = Name_External then
+                     Has_External := True;
+
+                  elsif Chars (Opt) = Name_Synchronous then
+                     Has_Synchronous := True;
+                  end if;
                end if;
 
                Next (Opt);
             end loop;
+         end Find_Simple_Properties;
 
-         --  When External specifies particular properties, inspect those and
-         --  find the desired one (if any).
+         ----------------------------------
+         -- Is_Enabled_External_Property --
+         ----------------------------------
+
+         function Is_Enabled_External_Property return Boolean is
+            Opt      : Node_Id;
+            Opt_Nam  : Node_Id;
+            Prop     : Node_Id;
+            Prop_Nam : Node_Id;
+            Props    : Node_Id;
 
+         begin
             Opt := First (Component_Associations (Decl));
             while Present (Opt) loop
                Opt_Nam := First (Choices (Opt));
@@ -10349,6 +10370,50 @@ package body Sem_Util is
             end loop;
 
             return False;
+         end Is_Enabled_External_Property;
+
+         --  Local variables
+
+         Has_External    : Boolean;
+         Has_Synchronous : Boolean;
+
+      --  Start of processing for State_Has_Enabled_Property
+
+      begin
+         --  The declaration of an external abstract state appears as an
+         --  extension aggregate. If this is not the case, properties can
+         --  never be set.
+
+         if Nkind (Decl) /= N_Extension_Aggregate then
+            return False;
+         end if;
+
+         Find_Simple_Properties (Has_External, Has_Synchronous);
+
+         --  Simple option External enables all properties (SPARK RM 7.1.2(2))
+
+         if Has_External then
+            return True;
+
+         --  Option External may enable or disable specific properties
+
+         elsif Is_Enabled_External_Property then
+            return True;
+
+         --  Simple option Synchronous
+         --
+         --    enables                disables
+         --       Asynch_Readers         Effective_Reads
+         --       Asynch_Writers         Effective_Writes
+         --
+         --  Note that both forms of External have higher precedence than
+         --  Synchronous (SPARK RM 7.1.4(10)).
+
+         elsif Has_Synchronous then
+            return Nam_In (Property, Name_Async_Readers, Name_Async_Writers);
+         end if;
+
+         return False;
       end State_Has_Enabled_Property;
 
       -----------------------------------

gcc/testsuite/ChangeLog

+2018-04-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* gnat.dg/sync2.adb, gnat.dg/sync2.ads: New testcase.
+
 2018-05-21  Kyrylo Tkachov  <kyrylo.tkachov@arm.com>
 
 	* gcc.c-torture/execute/ssad-run.c: New test.

gcc/testsuite/gnat.dg/sync2.adb

+--  { dg-do compile }
+
+package body Sync2 with
+  SPARK_Mode,
+  Refined_State => (State => (A, P, T))
+is
+   A : Integer := 0 with Atomic, Async_Readers, Async_Writers;
+
+   protected type Prot_Typ is
+   private
+      Comp : Natural := 0;
+   end Prot_Typ;
+
+   P : Prot_Typ;
+
+   task type Task_Typ;
+
+   T : Task_Typ;
+
+   protected body Prot_Typ is
+   end Prot_Typ;
+
+   task body Task_Typ is
+   begin
+      null;
+   end Task_Typ;
+end Sync2;

gcc/testsuite/gnat.dg/sync2.ads

+package Sync2 with
+  SPARK_Mode,
+  Abstract_State => (State with Synchronous)
+is
+   pragma Elaborate_Body;
+end Sync2;