sem_prag.adb (Analyze_Global_Item): Move the check concerning the use of…

sem_prag.adb (Analyze_Global_Item): Move the check concerning the use of volatile objects as global items in a...

2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Global_Item): Move the check concerning
	the use of volatile objects as global items in a function to
	the variable related checks section.
	* sem_util.adb (Async_Readers_Enabled): Directly call
	Has_Enabled_Property.
	(Async_Writers_Enabled): Directly call Has_Enabled_Property.
	(Effective_Reads_Enabled): Directly call Has_Enabled_Property.
	(Effective_Writes_Enabled): Directly call Has_Enabled_Property.
	(Has_Enabled_Property): Rename formal parameter State_Id to Item_Id.
	Update the comment on usage. State_Has_Enabled_Property how handles
	the original logic of the routine. Add processing for variables.
	(State_Has_Enabled_Property): New routine.
	(Variable_Has_Enabled_Property): New routine.

From-SVN: r208077

gcc/ada/ChangeLog

+2014-02-24  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Global_Item): Move the check concerning
+	the use of volatile objects as global items in a function to
+	the variable related checks section.
+	* sem_util.adb (Async_Readers_Enabled): Directly call
+	Has_Enabled_Property.
+	(Async_Writers_Enabled): Directly call Has_Enabled_Property.
+	(Effective_Reads_Enabled): Directly call Has_Enabled_Property.
+	(Effective_Writes_Enabled): Directly call Has_Enabled_Property.
+	(Has_Enabled_Property): Rename formal parameter State_Id to Item_Id.
+	Update the comment on usage. State_Has_Enabled_Property how handles
+	the original logic of the routine. Add processing for variables.
+	(State_Has_Enabled_Property): New routine.
+	(Variable_Has_Enabled_Property): New routine.
+
 2014-02-24  Robert Dewar  <dewar@adacore.com>
 
 	* sinfo.ads, sem_ch12.adb, sem_res.adb, sem_ch4.adb, par-ch12.adb:

gcc/ada/sem_prag.adb

@@ -2060,16 +2060,28 @@ package body Sem_Prag is
 
                --  Variable related checks
 
-               else
+               elsif Is_SPARK_Volatile_Object (Item_Id) then
+
+                  --  A volatile object cannot appear as a global item of a
+                  --  function. This check is only relevant when SPARK_Mode is
+                  --  on as it is not a standard Ada legality rule.
+
+                  if SPARK_Mode = On
+                    and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                  then
+                     Error_Msg_NE
+                       ("volatile object & cannot act as global item of a "
+                        & "function (SPARK RM 7.1.3(9))", Item, Item_Id);
+                     return;
+
                   --  A volatile object with property Effective_Reads set to
                   --  True must have mode Output or In_Out.
 
-                  if Is_SPARK_Volatile_Object (Item_Id)
-                    and then Effective_Reads_Enabled (Item_Id)
+                  elsif Effective_Reads_Enabled (Item_Id)
                     and then Global_Mode = Name_Input
                   then
                      Error_Msg_NE
-                       ("volatile item & with property Effective_Reads must "
+                       ("volatile object & with property Effective_Reads must "
                         & "have mode In_Out or Output (SPARK RM 7.1.3(11))",
                         Item, Item_Id);
                      return;
@@ -2100,19 +2112,6 @@ package body Sem_Prag is
                Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id);
             end if;
 
-            --  A volatile object cannot appear as a global item of a function.
-            --  This check is only relevant when SPARK_Mode is on as it is not
-            --  a standard Ada legality rule.
-
-            if SPARK_Mode = On
-              and then Is_SPARK_Volatile_Object (Item)
-              and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
-            then
-               Error_Msg_NE
-                 ("volatile object & cannot act as global item of a function "
-                  & "(SPARK RM 7.1.3(9))", Item, Item_Id);
-            end if;
-
             --  The same entity might be referenced through various way. Check
             --  the entity of the item rather than the item itself.
 

gcc/ada/sem_util.adb

@@ -116,11 +116,11 @@ package body Sem_Util is
    --  have a default.
 
    function Has_Enabled_Property
-     (State_Id : Node_Id;
+     (Item_Id  : Entity_Id;
       Property : Name_Id) return Boolean;
    --  Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-   --  Determine whether an abstract state denoted by its entity State_Id has
-   --  enabled property Property.
+   --  Determine whether an abstract state or a variable denoted by entity
+   --  Item_Id has enabled property Property.
 
    function Has_Null_Extension (T : Entity_Id) return Boolean;
    --  T is a derived tagged type. Check whether the type extension is null.
@@ -575,12 +575,7 @@ package body Sem_Util is
 
    function Async_Readers_Enabled (Id : Entity_Id) return Boolean is
    begin
-      if Ekind (Id) = E_Abstract_State then
       return Has_Enabled_Property (Id, Name_Async_Readers);
-
-      else pragma Assert (Ekind (Id) = E_Variable);
-         return Present (Get_Pragma (Id, Pragma_Async_Readers));
-      end if;
    end Async_Readers_Enabled;
 
    ---------------------------
@@ -589,12 +584,7 @@ package body Sem_Util is
 
    function Async_Writers_Enabled (Id : Entity_Id) return Boolean is
    begin
-      if Ekind (Id) = E_Abstract_State then
       return Has_Enabled_Property (Id, Name_Async_Writers);
-
-      else pragma Assert (Ekind (Id) = E_Variable);
-         return Present (Get_Pragma (Id, Pragma_Async_Writers));
-      end if;
    end Async_Writers_Enabled;
 
    --------------------------------------
@@ -4737,12 +4727,7 @@ package body Sem_Util is
 
    function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is
    begin
-      if Ekind (Id) = E_Abstract_State then
       return Has_Enabled_Property (Id, Name_Effective_Reads);
-
-      else pragma Assert (Ekind (Id) = E_Variable);
-         return Present (Get_Pragma (Id, Pragma_Effective_Reads));
-      end if;
    end Effective_Reads_Enabled;
 
    ------------------------------
@@ -4751,12 +4736,7 @@ package body Sem_Util is
 
    function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is
    begin
-      if Ekind (Id) = E_Abstract_State then
       return Has_Enabled_Property (Id, Name_Effective_Writes);
-
-      else pragma Assert (Ekind (Id) = E_Variable);
-         return Present (Get_Pragma (Id, Pragma_Effective_Writes));
-      end if;
    end Effective_Writes_Enabled;
 
    ------------------------------
@@ -7292,10 +7272,21 @@ package body Sem_Util is
    --------------------------
 
    function Has_Enabled_Property
-     (State_Id : Node_Id;
+     (Item_Id  : Entity_Id;
       Property : Name_Id) return Boolean
    is
-      Decl     : constant Node_Id := Parent (State_Id);
+      function State_Has_Enabled_Property return Boolean;
+      --  Determine whether a state denoted by Item_Id has the property
+
+      function Variable_Has_Enabled_Property return Boolean;
+      --  Determine whether a variable denoted by Item_Id has the property
+
+      --------------------------------
+      -- State_Has_Enabled_Property --
+      --------------------------------
+
+      function State_Has_Enabled_Property return Boolean is
+         Decl     : constant Node_Id := Parent (Item_Id);
          Opt      : Node_Id;
          Opt_Nam  : Node_Id;
          Prop     : Node_Id;
@@ -7303,8 +7294,9 @@ package body Sem_Util is
          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.
+         --  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;
@@ -7375,6 +7367,78 @@ package body Sem_Util is
          end loop;
 
          return False;
+      end State_Has_Enabled_Property;
+
+      -----------------------------------
+      -- Variable_Has_Enabled_Property --
+      -----------------------------------
+
+      function Variable_Has_Enabled_Property return Boolean is
+         AR : constant Node_Id :=
+                Get_Pragma (Item_Id, Pragma_Async_Readers);
+         AW : constant Node_Id :=
+                Get_Pragma (Item_Id, Pragma_Async_Writers);
+         ER : constant Node_Id :=
+                Get_Pragma (Item_Id, Pragma_Effective_Reads);
+         EW : constant Node_Id :=
+                Get_Pragma (Item_Id, Pragma_Effective_Writes);
+      begin
+         --  A non-volatile object can never possess external properties
+
+         if not Is_SPARK_Volatile_Object (Item_Id) then
+            return False;
+
+         --  External properties related to variables come in two flavors -
+         --  explicit and implicit. The explicit case is characterized by the
+         --  presence of a property pragma while the implicit case lacks all
+         --  such pragmas.
+
+         elsif Property = Name_Async_Readers
+           and then
+             (Present (AR)
+                or else
+             (No (AW) and then No (ER) and then No (EW)))
+         then
+            return True;
+
+         elsif Property = Name_Async_Writers
+           and then
+             (Present (AW)
+                or else
+             (No (AR) and then No (ER) and then No (EW)))
+         then
+            return True;
+
+         elsif Property = Name_Effective_Reads
+           and then
+             (Present (ER)
+                or else
+             (No (AR) and then No (AW) and then No (EW)))
+         then
+            return True;
+
+         elsif Property = Name_Effective_Writes
+           and then
+             (Present (EW)
+                or else
+             (No (AR) and then No (AW) and then No (ER)))
+         then
+            return True;
+
+         else
+            return False;
+         end if;
+      end Variable_Has_Enabled_Property;
+
+   --  Start of processing for Has_Enabled_Property
+
+   begin
+      if Ekind (Item_Id) = E_Abstract_State then
+         return State_Has_Enabled_Property;
+
+      else pragma Assert (Ekind (Item_Id) = E_Variable);
+         return Variable_Has_Enabled_Property;
+      end if;
    end Has_Enabled_Property;
 
    --------------------