[multiple changes]

2016-04-19  Arnaud Charlet  <charlet@adacore.com>

	* sem_prag.adb, sem_attr.adb, par-prag.adb, exp_aggr.adb, sem_type.adb
	sem_ch12.adb, sem_ch3.adb, exp_ch7.adb, exp_ch9.adb: Code cleanup.
	* sem_res.adb, sem_util.ads, sem_util.adb (Is_OK_Volatile_Context):
	Promoted from being a nested subprogram in Sem_Res.Resolve_Entity_Name
	to publicly visible routine in Sem_Util.

2016-04-19  Ed Schonberg  <schonberg@adacore.com>

	* checks.adb (Apply_Parameter_Aliasing_Checks): Do not apply
	the check if the type of the actual is By_Reference.

From-SVN: r235199

14 files changed, 292 insertions, 275 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5be755b..7cc7ff9 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,18 @@
 2016-04-19  Arnaud Charlet  <charlet@adacore.com>
 
+	* sem_prag.adb, sem_attr.adb, par-prag.adb, exp_aggr.adb, sem_type.adb
+	sem_ch12.adb, sem_ch3.adb, exp_ch7.adb, exp_ch9.adb: Code cleanup.
+	* sem_res.adb, sem_util.ads, sem_util.adb (Is_OK_Volatile_Context):
+	Promoted from being a nested subprogram in Sem_Res.Resolve_Entity_Name
+	to publicly visible routine in Sem_Util.
+
+2016-04-19  Ed Schonberg  <schonberg@adacore.com>
+
+	* checks.adb (Apply_Parameter_Aliasing_Checks): Do not apply
+	the check if the type of the actual is By_Reference.
+
+2016-04-19  Arnaud Charlet  <charlet@adacore.com>
+
 	* sem_res.adb (Within_Subprogram_Call): Detect
 	also nodes that appear in entry calls.
 	(Resolve_Actuals, Insert_Default): Propagate
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index e6eab0c..eca82d7 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -2373,7 +2373,10 @@ package body Checks is
          --  Elementary types are always passed by value, therefore actuals of
          --  such types cannot lead to aliasing. An aggregate is an object in
          --  Ada 2012, but an actual that is an aggregate cannot overlap with
-         --  another actual.
+         --  another actual. A type that is By_Reference (such as an array of
+         --  controlled types) is not subject to the check because any update
+         --  will be done in place and a subsequent read will always see the
+         --  correct value, see RM 6.2 (12/3).
 
          if Nkind (Original_Actual (Actual_1)) = N_Aggregate
            or else
@@ -2385,6 +2388,8 @@ package body Checks is
 
          elsif Is_Object_Reference (Original_Actual (Actual_1))
            and then not Is_Elementary_Type (Etype (Original_Actual (Actual_1)))
+           and then
+              not Is_By_Reference_Type (Etype (Original_Actual (Actual_1)))
          then
             Actual_2 := Next_Actual (Actual_1);
             Formal_2 := Next_Formal (Formal_1);
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 2ad72bd..cb97dca 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -4321,7 +4321,7 @@ package body Exp_Aggr is
          Decl     : Node_Id;
          Typ      : constant Entity_Id := Etype (N);
          Indexes  : constant List_Id   := New_List;
-         Num      : Int;
+         Num      : Nat;
          Sub_Agg  : Node_Id;
 
       begin
@@ -7085,7 +7085,7 @@ package body Exp_Aggr is
          Byte_Size : constant Int := UI_To_Int (Component_Size (Packed_Array));
          --  The packed array type is a byte array
 
-         Packed_Num : Int;
+         Packed_Num : Nat;
          --  Number of components accumulated in current byte
 
          Comps : List_Id;
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 04f28a6..daa5f91 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -6227,7 +6227,7 @@ package body Exp_Ch7 is
 
       procedure Preprocess_Components
         (Comps     : Node_Id;
-         Num_Comps : out Int;
+         Num_Comps : out Nat;
          Has_POC   : out Boolean);
       --  Examine all components in component list Comps, count all controlled
       --  components and determine whether at least one of them is per-object
@@ -6265,7 +6265,7 @@ package body Exp_Ch7 is
             Decl_Id   : Entity_Id;
             Decl_Typ  : Entity_Id;
             Has_POC   : Boolean;
-            Num_Comps : Int;
+            Num_Comps : Nat;
 
             procedure Process_Component_For_Adjust (Decl : Node_Id);
             --  Process the declaration of a single controlled component
@@ -6679,7 +6679,7 @@ package body Exp_Ch7 is
             Jump_Block : Node_Id;
             Label      : Node_Id;
             Label_Id   : Entity_Id;
-            Num_Comps  : Int;
+            Num_Comps  : Nat;
             Stmts      : List_Id;
 
             procedure Process_Component_For_Finalize
@@ -7236,7 +7236,7 @@ package body Exp_Ch7 is
 
       procedure Preprocess_Components
         (Comps     : Node_Id;
-         Num_Comps : out Int;
+         Num_Comps : out Nat;
          Has_POC   : out Boolean)
       is
          Decl : Node_Id;
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 11b614b..faa1d8c 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -10590,7 +10590,7 @@ package body Exp_Ch9 is
       End_Lab        : Node_Id;
       Index          : Pos := 1;
       Lab            : Node_Id;
-      Num_Alts       : Int;
+      Num_Alts       : Nat;
       Num_Accept     : Nat := 0;
       Proc           : Node_Id;
       Time_Type      : Entity_Id;
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index c317949..123f909 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -974,13 +974,13 @@ begin
                declare
                   Slen    : constant Natural := Natural (String_Length (S));
                   Options : String (1 .. Slen);
-                  J       : Natural;
-                  Ptr     : Natural;
+                  J       : Positive;
+                  Ptr     : Positive;
 
                begin
                   J := 1;
                   loop
-                     C := Get_String_Char (S, Int (J));
+                     C := Get_String_Char (S, Pos (J));
 
                      if not In_Character_Range (C) then
                         OK := False;
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 17f06f3..fa44c1d 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -6041,7 +6041,7 @@ package body Sem_Attr is
 
                Start_String;
                for J in 1 .. String_Length (Full_Name) - 1 loop
-                  Store_String_Char (Get_String_Char (Full_Name, Int (J)));
+                  Store_String_Char (Get_String_Char (Full_Name, Pos (J)));
                end loop;
 
                Store_String_Chars ("'Type_Key");
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 40433fd..084335c 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -15117,7 +15117,7 @@ package body Sem_Ch12 is
       T       : constant Entity_Id := Entity (Prefix (Def));
       Is_Fun  : constant Boolean := (Ekind (Nam) = E_Function);
       F       : Entity_Id;
-      Num_F   : Int;
+      Num_F   : Nat;
       OK      : Boolean;
 
    begin
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index f41b8e9..f2e1115 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -13871,8 +13871,8 @@ package body Sem_Ch3 is
       --  Inherit the discriminants of the parent type
 
       Add_Discriminants : declare
-         Num_Disc : Int;
-         Num_Gird : Int;
+         Num_Disc : Nat;
+         Num_Gird : Nat;
 
       begin
          Num_Disc := 0;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index e965976..289cfc8 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -21242,12 +21242,12 @@ package body Sem_Prag is
                   declare
                      Slen    : constant Natural := Natural (String_Length (S));
                      Options : String (1 .. Slen);
-                     J       : Natural;
+                     J       : Positive;
 
                   begin
                      J := 1;
                      loop
-                        C := Get_String_Char (S, Int (J));
+                        C := Get_String_Char (S, Pos (J));
                         exit when not In_Character_Range (C);
                         Options (J) := Get_Character (C);
 
@@ -22592,14 +22592,14 @@ package body Sem_Prag is
                   declare
                      Slen    : constant Natural := Natural (String_Length (S));
                      Options : String (1 .. Slen);
-                     J       : Natural;
+                     J       : Positive;
 
                   begin
                      --  Couldn't we use a for loop here over Options'Range???
 
                      J := 1;
                      loop
-                        C := Get_String_Char (S, Int (J));
+                        C := Get_String_Char (S, Pos (J));
 
                         --  This is a weird test, it skips setting validity
                         --  checks entirely if any element of S is out of
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 0bac1eb..85bf0c4 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6820,13 +6820,6 @@ package body Sem_Res is
       --  Determine whether node Context denotes an assignment statement or an
       --  object declaration whose expression is node Expr.
 
-      function Is_OK_Volatile_Context
-        (Context : Node_Id;
-         Obj_Ref : Node_Id) return Boolean;
-      --  Determine whether node Context denotes a "non-interfering context"
-      --  (as defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref
-      --  can safely reside.
-
       ----------------------------------------
       -- Is_Assignment_Or_Object_Expression --
       ----------------------------------------
@@ -6869,254 +6862,6 @@ package body Sem_Res is
          end if;
       end Is_Assignment_Or_Object_Expression;
 
-      ----------------------------
-      -- Is_OK_Volatile_Context --
-      ----------------------------
-
-      function Is_OK_Volatile_Context
-        (Context : Node_Id;
-         Obj_Ref : Node_Id) return Boolean
-      is
-         function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean;
-         --  Determine whether an arbitrary node denotes a call to a protected
-         --  entry, function or procedure in prefixed form where the prefix is
-         --  Obj_Ref.
-
-         function Within_Check (Nod : Node_Id) return Boolean;
-         --  Determine whether an arbitrary node appears in a check node
-
-         function Within_Subprogram_Call (Nod : Node_Id) return Boolean;
-         --  Determine whether an arbitrary node appears in a subprogram call
-
-         function Within_Volatile_Function (Id : Entity_Id) return Boolean;
-         --  Determine whether an arbitrary entity appears in a volatile
-         --  function.
-
-         ---------------------------------
-         -- Is_Protected_Operation_Call --
-         ---------------------------------
-
-         function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean is
-            Pref : Node_Id;
-            Subp : Node_Id;
-
-         begin
-            --  A call to a protected operations retains its selected component
-            --  form as opposed to other prefixed calls that are transformed in
-            --  expanded names.
-
-            if Nkind (Nod) = N_Selected_Component then
-               Pref := Prefix (Nod);
-               Subp := Selector_Name (Nod);
-
-               return
-                 Pref = Obj_Ref
-                   and then Present (Etype (Pref))
-                   and then Is_Protected_Type (Etype (Pref))
-                   and then Is_Entity_Name (Subp)
-                   and then Present (Entity (Subp))
-                   and then Ekind_In (Entity (Subp), E_Entry,
-                                                     E_Entry_Family,
-                                                     E_Function,
-                                                     E_Procedure);
-            else
-               return False;
-            end if;
-         end Is_Protected_Operation_Call;
-
-         ------------------
-         -- Within_Check --
-         ------------------
-
-         function Within_Check (Nod : Node_Id) return Boolean is
-            Par : Node_Id;
-
-         begin
-            --  Climb the parent chain looking for a check node
-
-            Par := Nod;
-            while Present (Par) loop
-               if Nkind (Par) in N_Raise_xxx_Error then
-                  return True;
-
-               --  Prevent the search from going too far
-
-               elsif Is_Body_Or_Package_Declaration (Par) then
-                  exit;
-               end if;
-
-               Par := Parent (Par);
-            end loop;
-
-            return False;
-         end Within_Check;
-
-         ----------------------------
-         -- Within_Subprogram_Call --
-         ----------------------------
-
-         function Within_Subprogram_Call (Nod : Node_Id) return Boolean is
-            Par : Node_Id;
-
-         begin
-            --  Climb the parent chain looking for a function or procedure call
-
-            Par := Nod;
-            while Present (Par) loop
-               if Nkind_In (Par, N_Function_Call,
-                                 N_Procedure_Call_Statement,
-                                 N_Entry_Call_Statement)
-               then
-                  return True;
-
-               --  Prevent the search from going too far
-
-               elsif Is_Body_Or_Package_Declaration (Par) then
-                  exit;
-               end if;
-
-               Par := Parent (Par);
-            end loop;
-
-            return False;
-         end Within_Subprogram_Call;
-
-         ------------------------------
-         -- Within_Volatile_Function --
-         ------------------------------
-
-         function Within_Volatile_Function (Id : Entity_Id) return Boolean is
-            Func_Id : Entity_Id;
-
-         begin
-            --  Traverse the scope stack looking for a [generic] function
-
-            Func_Id := Id;
-            while Present (Func_Id) and then Func_Id /= Standard_Standard loop
-               if Ekind_In (Func_Id, E_Function, E_Generic_Function) then
-                  return Is_Volatile_Function (Func_Id);
-               end if;
-
-               Func_Id := Scope (Func_Id);
-            end loop;
-
-            return False;
-         end Within_Volatile_Function;
-
-         --  Local variables
-
-         Obj_Id : Entity_Id;
-
-      --  Start of processing for Is_OK_Volatile_Context
-
-      begin
-         --  The volatile object appears on either side of an assignment
-
-         if Nkind (Context) = N_Assignment_Statement then
-            return True;
-
-         --  The volatile object is part of the initialization expression of
-         --  another object.
-
-         elsif Nkind (Context) = N_Object_Declaration
-           and then Present (Expression (Context))
-           and then Expression (Context) = Obj_Ref
-         then
-            Obj_Id := Defining_Entity (Context);
-
-            --  The volatile object acts as the initialization expression of an
-            --  extended return statement. This is valid context as long as the
-            --  function is volatile.
-
-            if Is_Return_Object (Obj_Id) then
-               return Within_Volatile_Function (Obj_Id);
-
-            --  Otherwise this is a normal object initialization
-
-            else
-               return True;
-            end if;
-
-         --  The volatile object acts as the name of a renaming declaration
-
-         elsif Nkind (Context) = N_Object_Renaming_Declaration
-           and then Name (Context) = Obj_Ref
-         then
-            return True;
-
-         --  The volatile object appears as an actual parameter in a call to an
-         --  instance of Unchecked_Conversion whose result is renamed.
-
-         elsif Nkind (Context) = N_Function_Call
-           and then Is_Entity_Name (Name (Context))
-           and then Is_Unchecked_Conversion_Instance (Entity (Name (Context)))
-           and then Nkind (Parent (Context)) = N_Object_Renaming_Declaration
-         then
-            return True;
-
-         --  The volatile object is actually the prefix in a protected entry,
-         --  function, or procedure call.
-
-         elsif Is_Protected_Operation_Call (Context) then
-            return True;
-
-         --  The volatile object appears as the expression of a simple return
-         --  statement that applies to a volatile function.
-
-         elsif Nkind (Context) = N_Simple_Return_Statement
-           and then Expression (Context) = Obj_Ref
-         then
-            return
-              Within_Volatile_Function (Return_Statement_Entity (Context));
-
-         --  The volatile object appears as the prefix of a name occurring
-         --  in a non-interfering context.
-
-         elsif Nkind_In (Context, N_Attribute_Reference,
-                                  N_Explicit_Dereference,
-                                  N_Indexed_Component,
-                                  N_Selected_Component,
-                                  N_Slice)
-           and then Prefix (Context) = Obj_Ref
-           and then Is_OK_Volatile_Context
-                      (Context => Parent (Context),
-                       Obj_Ref => Context)
-         then
-            return True;
-
-         --  The volatile object appears as the expression of a type conversion
-         --  occurring in a non-interfering context.
-
-         elsif Nkind_In (Context, N_Type_Conversion,
-                                  N_Unchecked_Type_Conversion)
-           and then Expression (Context) = Obj_Ref
-           and then Is_OK_Volatile_Context
-                      (Context => Parent (Context),
-                       Obj_Ref => Context)
-         then
-            return True;
-
-         --  Allow references to volatile objects in various checks. This is
-         --  not a direct SPARK 2014 requirement.
-
-         elsif Within_Check (Context) then
-            return True;
-
-         --  Assume that references to effectively volatile objects that appear
-         --  as actual parameters in a subprogram call are always legal. A full
-         --  legality check is done when the actuals are resolved.
-
-         elsif Within_Subprogram_Call (Context) then
-            return True;
-
-         --  Otherwise the context is not suitable for an effectively volatile
-         --  object.
-
-         else
-            return False;
-         end if;
-      end Is_OK_Volatile_Context;
-
       --  Local variables
 
       E   : constant Entity_Id := Entity (N);
diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb
index eddc54b..a648bfa 100644
--- a/gcc/ada/sem_type.adb
+++ b/gcc/ada/sem_type.adb
@@ -3029,7 +3029,7 @@ package body Sem_Type is
       Op_Name     : constant Name_Id   := Chars (Op);
       T           : constant Entity_Id := Etype (New_S);
       New_F       : Entity_Id;
-      Num         : Int;
+      Num         : Nat;
       Old_F       : Entity_Id;
       T1          : Entity_Id;
       T2          : Entity_Id;
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 29d2e42..d4a276c 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -13010,6 +13010,253 @@ package body Sem_Util is
       end if;
    end Is_OK_Variable_For_Out_Formal;
 
+   ----------------------------
+   -- Is_OK_Volatile_Context --
+   ----------------------------
+
+   function Is_OK_Volatile_Context
+     (Context : Node_Id;
+      Obj_Ref : Node_Id) return Boolean
+   is
+      function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean;
+      --  Determine whether an arbitrary node denotes a call to a protected
+      --  entry, function or procedure in prefixed form where the prefix is
+      --  Obj_Ref.
+
+      function Within_Check (Nod : Node_Id) return Boolean;
+      --  Determine whether an arbitrary node appears in a check node
+
+      function Within_Subprogram_Call (Nod : Node_Id) return Boolean;
+      --  Determine whether an arbitrary node appears in a procedure call
+
+      function Within_Volatile_Function (Id : Entity_Id) return Boolean;
+      --  Determine whether an arbitrary entity appears in a volatile function
+
+      ---------------------------------
+      -- Is_Protected_Operation_Call --
+      ---------------------------------
+
+      function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean is
+         Pref : Node_Id;
+         Subp : Node_Id;
+
+      begin
+         --  A call to a protected operations retains its selected component
+         --  form as opposed to other prefixed calls that are transformed in
+         --  expanded names.
+
+         if Nkind (Nod) = N_Selected_Component then
+            Pref := Prefix (Nod);
+            Subp := Selector_Name (Nod);
+
+            return
+              Pref = Obj_Ref
+              and then Present (Etype (Pref))
+              and then Is_Protected_Type (Etype (Pref))
+              and then Is_Entity_Name (Subp)
+              and then Present (Entity (Subp))
+              and then Ekind_In (Entity (Subp), E_Entry,
+                                 E_Entry_Family,
+                                 E_Function,
+                                 E_Procedure);
+         else
+            return False;
+         end if;
+      end Is_Protected_Operation_Call;
+
+      ------------------
+      -- Within_Check --
+      ------------------
+
+      function Within_Check (Nod : Node_Id) return Boolean is
+         Par : Node_Id;
+
+      begin
+         --  Climb the parent chain looking for a check node
+
+         Par := Nod;
+         while Present (Par) loop
+            if Nkind (Par) in N_Raise_xxx_Error then
+               return True;
+
+               --  Prevent the search from going too far
+
+            elsif Is_Body_Or_Package_Declaration (Par) then
+               exit;
+            end if;
+
+            Par := Parent (Par);
+         end loop;
+
+         return False;
+      end Within_Check;
+
+      ----------------------------
+      -- Within_Subprogram_Call --
+      ----------------------------
+
+      function Within_Subprogram_Call (Nod : Node_Id) return Boolean is
+         Par : Node_Id;
+
+      begin
+         --  Climb the parent chain looking for a function or procedure call
+
+         Par := Nod;
+         while Present (Par) loop
+            if Nkind_In (Par, N_Function_Call,
+                              N_Procedure_Call_Statement,
+                              N_Entry_Call_Statement)
+            then
+               return True;
+
+               --  Prevent the search from going too far
+
+            elsif Is_Body_Or_Package_Declaration (Par) then
+               exit;
+            end if;
+
+            Par := Parent (Par);
+         end loop;
+
+         return False;
+      end Within_Subprogram_Call;
+
+      ------------------------------
+      -- Within_Volatile_Function --
+      ------------------------------
+
+      function Within_Volatile_Function (Id : Entity_Id) return Boolean is
+         Func_Id : Entity_Id;
+
+      begin
+         --  Traverse the scope stack looking for a [generic] function
+
+         Func_Id := Id;
+         while Present (Func_Id) and then Func_Id /= Standard_Standard loop
+            if Ekind_In (Func_Id, E_Function, E_Generic_Function) then
+               return Is_Volatile_Function (Func_Id);
+            end if;
+
+            Func_Id := Scope (Func_Id);
+         end loop;
+
+         return False;
+      end Within_Volatile_Function;
+
+      --  Local variables
+
+      Obj_Id : Entity_Id;
+
+   --  Start of processing for Is_OK_Volatile_Context
+
+   begin
+      --  The volatile object appears on either side of an assignment
+
+      if Nkind (Context) = N_Assignment_Statement then
+         return True;
+
+         --  The volatile object is part of the initialization expression of
+         --  another object.
+
+      elsif Nkind (Context) = N_Object_Declaration
+        and then Present (Expression (Context))
+        and then Expression (Context) = Obj_Ref
+      then
+         Obj_Id := Defining_Entity (Context);
+
+         --  The volatile object acts as the initialization expression of an
+         --  extended return statement. This is valid context as long as the
+         --  function is volatile.
+
+         if Is_Return_Object (Obj_Id) then
+            return Within_Volatile_Function (Obj_Id);
+
+            --  Otherwise this is a normal object initialization
+
+         else
+            return True;
+         end if;
+
+         --  The volatile object acts as the name of a renaming declaration
+
+      elsif Nkind (Context) = N_Object_Renaming_Declaration
+        and then Name (Context) = Obj_Ref
+      then
+         return True;
+
+         --  The volatile object appears as an actual parameter in a call to an
+         --  instance of Unchecked_Conversion whose result is renamed.
+
+      elsif Nkind (Context) = N_Function_Call
+        and then Is_Entity_Name (Name (Context))
+        and then Is_Unchecked_Conversion_Instance (Entity (Name (Context)))
+        and then Nkind (Parent (Context)) = N_Object_Renaming_Declaration
+      then
+         return True;
+
+         --  The volatile object is actually the prefix in a protected entry,
+         --  function, or procedure call.
+
+      elsif Is_Protected_Operation_Call (Context) then
+         return True;
+
+         --  The volatile object appears as the expression of a simple return
+         --  statement that applies to a volatile function.
+
+      elsif Nkind (Context) = N_Simple_Return_Statement
+        and then Expression (Context) = Obj_Ref
+      then
+         return
+           Within_Volatile_Function (Return_Statement_Entity (Context));
+
+         --  The volatile object appears as the prefix of a name occurring in a
+         --  non-interfering context.
+
+      elsif Nkind_In (Context, N_Attribute_Reference,
+                      N_Explicit_Dereference,
+                      N_Indexed_Component,
+                      N_Selected_Component,
+                      N_Slice)
+        and then Prefix (Context) = Obj_Ref
+        and then Is_OK_Volatile_Context
+          (Context => Parent (Context),
+           Obj_Ref => Context)
+      then
+         return True;
+
+         --  The volatile object appears as the expression of a type conversion
+         --  occurring in a non-interfering context.
+
+      elsif Nkind_In (Context, N_Type_Conversion,
+                      N_Unchecked_Type_Conversion)
+        and then Expression (Context) = Obj_Ref
+        and then Is_OK_Volatile_Context
+          (Context => Parent (Context),
+           Obj_Ref => Context)
+      then
+         return True;
+
+         --  Allow references to volatile objects in various checks. This is
+         --  not a direct SPARK 2014 requirement.
+
+      elsif Within_Check (Context) then
+         return True;
+
+         --  Assume that references to effectively volatile objects that appear
+         --  as actual parameters in a subprogram call are always legal. A full
+         --  legality check is done when the actuals are resolved.
+
+      elsif Within_Subprogram_Call (Context) then
+         return True;
+
+         --  Otherwise the context is not suitable for an effectively volatile
+         --  object.
+
+      else
+         return False;
+      end if;
+   end Is_OK_Volatile_Context;
+
    ------------------------------------
    -- Is_Package_Contract_Annotation --
    ------------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index df475cc..4575077 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1474,6 +1474,13 @@ package Sem_Util is
    --  the Is_Variable sense) with an untagged type target are considered view
    --  conversions and hence variables.
 
+   function Is_OK_Volatile_Context
+     (Context : Node_Id;
+      Obj_Ref : Node_Id) return Boolean;
+   --  Determine whether node Context denotes a "non-interfering context" (as
+   --  defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref can
+   --  safely reside.
+
    function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean;
    --  Determine whether aspect specification or pragma Item is one of the
    --  following package contract annotations: