freeze.adb (Freeze_Record_Type): Update the use of Is_SPARK_Volatile.

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

	* freeze.adb (Freeze_Record_Type): Update the use of
	Is_SPARK_Volatile.
	* sem_ch3.adb (Analyze_Object_Contract): Update the use of
	Is_SPARK_Volatile.
	(Process_Discriminants): Update the use of Is_SPARK_Volatile.
	* sem_ch5.adb (Analyze_Iterator_Specification): Update the use
	of Is_SPARK_Volatile.
	(Analyze_Loop_Parameter_Specification):
	Update the use of Is_SPARK_Volatile.
	* sem_ch6.adb (Process_Formals): Catch an illegal use of an IN
	formal parameter when its type is volatile.
	* sem_prag.adb (Analyze_Global_Item): Update the use of
	Is_SPARK_Volatile.
	* sem_res.adb (Resolve_Entity_Name): Correct the guard which
	determines whether an entity is a volatile source SPARK object.
	* sem_util.adb (Has_Enabled_Property): Accout for external
	properties being set on objects other than abstract states
	and variables. An example would be a formal parameter.
	(Is_SPARK_Volatile): New routine.
	(Is_SPARK_Volatile_Object):
	Remove the entity-specific tests. Call routine Is_SPARK_Volatile
	when checking entities and/or types.
	* sem_util.ads (Is_SPARK_Volatile): New routine.

From-SVN: r210708

9 files changed, 92 insertions, 37 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 26df7be..dd5f7e1 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,29 @@
+2014-05-21  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* freeze.adb (Freeze_Record_Type): Update the use of
+	Is_SPARK_Volatile.
+	* sem_ch3.adb (Analyze_Object_Contract): Update the use of
+	Is_SPARK_Volatile.
+	(Process_Discriminants): Update the use of Is_SPARK_Volatile.
+	* sem_ch5.adb (Analyze_Iterator_Specification): Update the use
+	of Is_SPARK_Volatile.
+	(Analyze_Loop_Parameter_Specification):
+	Update the use of Is_SPARK_Volatile.
+	* sem_ch6.adb (Process_Formals): Catch an illegal use of an IN
+	formal parameter when its type is volatile.
+	* sem_prag.adb (Analyze_Global_Item): Update the use of
+	Is_SPARK_Volatile.
+	* sem_res.adb (Resolve_Entity_Name): Correct the guard which
+	determines whether an entity is a volatile source SPARK object.
+	* sem_util.adb (Has_Enabled_Property): Accout for external
+	properties being set on objects other than abstract states
+	and variables. An example would be a formal parameter.
+	(Is_SPARK_Volatile): New routine.
+	(Is_SPARK_Volatile_Object):
+	Remove the entity-specific tests. Call routine Is_SPARK_Volatile
+	when checking entities and/or types.
+	* sem_util.ads (Is_SPARK_Volatile): New routine.
+
 2014-05-21  Robert Dewar  <dewar@adacore.com>
 
 	* sem_warn.adb: Minor fix to warning messages (use ?? instead
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 6a382b9..e48cb9f 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -3318,7 +3318,7 @@ package body Freeze is
          --  they are not standard Ada legality rules.
 
          if SPARK_Mode = On then
-            if Is_SPARK_Volatile_Object (Rec) then
+            if Is_SPARK_Volatile (Rec) then
 
                --  A discriminated type cannot be volatile (SPARK RM C.6(4))
 
@@ -3340,7 +3340,7 @@ package body Freeze is
                Comp := First_Component (Rec);
                while Present (Comp) loop
                   if Comes_From_Source (Comp)
-                    and then Is_SPARK_Volatile_Object (Comp)
+                    and then Is_SPARK_Volatile (Comp)
                   then
                      Error_Msg_Name_1 := Chars (Rec);
                      Error_Msg_N
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 5db4bb7..293a3f6 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2988,7 +2988,7 @@ package body Sem_Ch3 is
          --  actuals in instantiations (SPARK RM 7.1.3(6)).
 
          if SPARK_Mode = On
-           and then Is_SPARK_Volatile_Object (Obj_Id)
+           and then Is_SPARK_Volatile (Obj_Id)
            and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
          then
             Error_Msg_N ("constant cannot be volatile", Obj_Id);
@@ -3000,7 +3000,7 @@ package body Sem_Ch3 is
          --  they are not standard Ada legality rules.
 
          if SPARK_Mode = On then
-            if Is_SPARK_Volatile_Object (Obj_Id) then
+            if Is_SPARK_Volatile (Obj_Id) then
 
                --  The declaration of a volatile object must appear at the
                --  library level (SPARK RM 7.1.3(7), C.6(6)).
@@ -3030,7 +3030,7 @@ package body Sem_Ch3 is
                --  A non-volatile object cannot have volatile components
                --  (SPARK RM 7.1.3(7)).
 
-               if not Is_SPARK_Volatile_Object (Obj_Id)
+               if not Is_SPARK_Volatile (Obj_Id)
                  and then Has_Volatile_Component (Obj_Typ)
                then
                   Error_Msg_N
@@ -18051,7 +18051,7 @@ package body Sem_Ch3 is
          --  (SPARK RM 7.1.3(6)).
 
          if SPARK_Mode = On
-           and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr))
+           and then Is_SPARK_Volatile (Defining_Identifier (Discr))
          then
             Error_Msg_N ("discriminant cannot be volatile", Discr);
          end if;
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 5f14622..60080ed 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1986,7 +1986,7 @@ package body Sem_Ch5 is
 
       if SPARK_Mode = On
         and then not Of_Present (N)
-        and then Is_SPARK_Volatile_Object (Ent)
+        and then Is_SPARK_Volatile (Ent)
       then
          Error_Msg_N ("loop parameter cannot be volatile", Ent);
       end if;
@@ -2706,7 +2706,7 @@ package body Sem_Ch5 is
       --  when SPARK_Mode is on as it is not a standard Ada legality check
       --  (SPARK RM 7.1.3(6)).
 
-      if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then
+      if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then
          Error_Msg_N ("loop parameter cannot be volatile", Id);
       end if;
    end Analyze_Loop_Parameter_Specification;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 5305b31..0118783 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -11511,23 +11511,35 @@ package body Sem_Ch6 is
          --  The following checks are relevant when SPARK_Mode is on as these
          --  are not standard Ada legality rules.
 
-         if SPARK_Mode = On
-           and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
-         then
-            --  A function cannot have a parameter of mode IN OUT or OUT
-            --  (SPARK RM 6.1).
+         if SPARK_Mode = On then
+            if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
 
-            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
-               Error_Msg_N
-                 ("function cannot have parameter of mode `OUT` or `IN OUT`",
-                  Formal);
+               --  A function cannot have a parameter of mode IN OUT or OUT
+               --  (SPARK RM 6.1).
 
-            --  A function cannot have a volatile formal parameter
-            --  (SPARK RM 7.1.3(10)).
+               if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+                  Error_Msg_N
+                    ("function cannot have parameter of mode `OUT` or "
+                     & "`IN OUT`", Formal);
 
-            elsif Is_SPARK_Volatile_Object (Formal) then
+               --  A function cannot have a volatile formal parameter
+               --  (SPARK RM 7.1.3(10)).
+
+               elsif Is_SPARK_Volatile (Formal) then
+                  Error_Msg_N
+                    ("function cannot have a volatile formal parameter",
+                     Formal);
+               end if;
+
+            --  A procedure cannot have a formal parameter of mode IN because
+            --  it behaves as a constant (SPARK RM 7.1.3(6)).
+
+            elsif Ekind (Scope (Formal)) = E_Procedure
+              and then Ekind (Formal) = E_In_Parameter
+              and then Is_SPARK_Volatile (Formal)
+            then
                Error_Msg_N
-                 ("function cannot have a volatile formal parameter", Formal);
+                 ("formal parameter of mode `IN` cannot be volatile", Formal);
             end if;
          end if;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 416eb04..62caba6 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2038,9 +2038,8 @@ package body Sem_Prag is
                --  SPARK_Mode is on as they are not standard Ada legality
                --  rules.
 
-               elsif SPARK_Mode = On
-                 and then Is_SPARK_Volatile_Object (Item_Id)
-               then
+               elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then
+
                   --  A volatile object cannot appear as a global item of a
                   --  function (SPARK RM 7.1.3(9)).
 
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 50b7f48..2273fe8 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6579,8 +6579,9 @@ package body Sem_Res is
       --  standard Ada legality rules.
 
       if SPARK_Mode = On
-        and then Ekind_In (E, E_Abstract_State, E_Variable)
-        and then Is_SPARK_Volatile_Object (E)
+        and then Is_Object (E)
+        and then Is_SPARK_Volatile (E)
+        and then Comes_From_Source (E)
         and then
           (Async_Writers_Enabled (E)
              or else Effective_Reads_Enabled (E))
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 18a2472..29de16b 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7466,7 +7466,7 @@ package body Sem_Util is
       begin
          --  A non-volatile object can never possess external properties
 
-         if not Is_SPARK_Volatile_Object (Item_Id) then
+         if not Is_SPARK_Volatile (Item_Id) then
             return False;
 
          --  External properties related to variables come in two flavors -
@@ -7514,11 +7514,19 @@ package body Sem_Util is
    --  Start of processing for Has_Enabled_Property
 
    begin
+      --  Abstract states and variables have a flexible scheme of specifying
+      --  external properties.
+
       if Ekind (Item_Id) = E_Abstract_State then
          return State_Has_Enabled_Property;
 
-      else pragma Assert (Ekind (Item_Id) = E_Variable);
+      elsif Ekind (Item_Id) = E_Variable then
          return Variable_Has_Enabled_Property;
+
+      --  Otherwise a property is enabled when the related object is volatile
+
+      else
+         return Is_SPARK_Volatile (Item_Id);
       end if;
    end Has_Enabled_Property;
 
@@ -11413,22 +11421,26 @@ package body Sem_Util is
       end if;
    end Is_SPARK_Object_Reference;
 
+   -----------------------
+   -- Is_SPARK_Volatile --
+   -----------------------
+
+   function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is
+   begin
+      return Is_Volatile (Id) or else Is_Volatile (Etype (Id));
+   end Is_SPARK_Volatile;
+
    ------------------------------
    -- Is_SPARK_Volatile_Object --
    ------------------------------
 
    function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
    begin
-      if Nkind (N) = N_Defining_Identifier then
-         return Is_Volatile (N) or else Is_Volatile (Etype (N));
-
-      elsif Is_Entity_Name (N) then
-         return
-           Is_SPARK_Volatile_Object (Entity (N))
-             or else Is_Volatile (Etype (N));
+      if Is_Entity_Name (N) then
+         return Is_SPARK_Volatile (Entity (N));
 
       elsif Nkind (N) = N_Expanded_Name then
-         return Is_SPARK_Volatile_Object (Entity (N));
+         return Is_SPARK_Volatile (Entity (N));
 
       elsif Nkind (N) = N_Indexed_Component then
          return Is_SPARK_Volatile_Object (Prefix (N));
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 13fe688..8629d76 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1302,10 +1302,15 @@ package Sem_Util is
    function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
    --  Determines if the tree referenced by N represents an object in SPARK
 
+   function Is_SPARK_Volatile (Id : Entity_Id) return Boolean;
+   --  This routine is similar to predicate Is_Volatile, but it takes SPARK
+   --  semantics into account. In SPARK volatile components to not render a
+   --  type volatile.
+
    function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
    --  Determine whether an arbitrary node denotes a volatile object reference
    --  according to the semantics of SPARK. To qualify as volatile, an object
-   --  must be subject to aspect/pragma Volatile or Atomic or have a [sub]type
+   --  must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type
    --  subject to the same attributes. Note that volatile components do not
    --  render an object volatile.