Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 235481)
+++ sem_res.adb	(working copy)
@@ -3107,6 +3107,10 @@
       --  interpretation, but the form of the actual can only be determined
       --  once the primitive operation is identified.
 
+      procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id);
+      --  Emit an error concerning the illegal usage of an effectively volatile
+      --  object in interfering context (SPARK RM 7.13(12)).
+
       procedure Insert_Default;
       --  If the actual is missing in a call, insert in the actuals list
       --  an instance of the default expression. The insertion is always
@@ -3360,6 +3364,55 @@
          end if;
       end Check_Prefixed_Call;
 
+      ---------------------------------------
+      -- Flag_Effectively_Volatile_Objects --
+      ---------------------------------------
+
+      procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is
+         function Flag_Object (N : Node_Id) return Traverse_Result;
+         --  Determine whether arbitrary node N denotes an effectively volatile
+         --  object and if it does, emit an error.
+
+         -----------------
+         -- Flag_Object --
+         -----------------
+
+         function Flag_Object (N : Node_Id) return Traverse_Result is
+            Id : Entity_Id;
+
+         begin
+            --  Do not consider nested function calls because they have already
+            --  been processed during their own resolution.
+
+            if Nkind (N) = N_Function_Call then
+               return Skip;
+
+            elsif Is_Entity_Name (N) and then Present (Entity (N)) then
+               Id := Entity (N);
+
+               if Is_Object (Id)
+                 and then Is_Effectively_Volatile (Id)
+                 and then (Async_Writers_Enabled (Id)
+                            or else Effective_Reads_Enabled (Id))
+               then
+                  Error_Msg_N
+                    ("volatile object cannot appear in this context (SPARK "
+                     & "RM 7.1.3(11))", N);
+                  return Skip;
+               end if;
+            end if;
+
+            return OK;
+         end Flag_Object;
+
+         procedure Flag_Objects is new Traverse_Proc (Flag_Object);
+
+      --  Start of processing for Flag_Effectively_Volatile_Objects
+
+      begin
+         Flag_Objects (Expr);
+      end Flag_Effectively_Volatile_Objects;
+
       --------------------
       -- Insert_Default --
       --------------------
@@ -3461,7 +3514,6 @@
             then
                Set_Is_Controlling_Actual (Actval);
             end if;
-
          end if;
 
          --  If the default expression raises constraint error, then just
@@ -4473,10 +4525,8 @@
             --  they are not standard Ada legality rule. Internally generated
             --  temporaries are ignored.
 
-            if SPARK_Mode = On
-              and then Comes_From_Source (A)
-              and then Is_Effectively_Volatile_Object (A)
-            then
+            if SPARK_Mode = On and then Comes_From_Source (A) then
+
                --  An effectively volatile object may act as an actual when the
                --  corresponding formal is of a non-scalar effectively volatile
                --  type (SPARK RM 7.1.3(11)).
@@ -4493,10 +4543,23 @@
                elsif Is_Unchecked_Conversion_Instance (Nam) then
                   null;
 
-               else
+               --  The actual denotes an object
+
+               elsif Is_Effectively_Volatile_Object (A) then
                   Error_Msg_N
                     ("volatile object cannot act as actual in a call (SPARK "
                      & "RM 7.1.3(11))", A);
+
+               --  Otherwise the actual denotes an expression. Inspect the
+               --  expression and flag each effectively volatile object with
+               --  enabled property Async_Writers or Effective_Reads as illegal
+               --  because it apprears within an interfering context. Note that
+               --  this is usually done in Resolve_Entity_Name, but when the
+               --  effectively volatile object appears as an actual in a call,
+               --  the call must be resolved first.
+
+               else
+                  Flag_Effectively_Volatile_Objects (A);
                end if;
 
                --  Detect an external variable with an enabled property that
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 235491)
+++ sem_util.adb	(working copy)
@@ -9314,7 +9314,7 @@
            Has_Default_Aspect (Typ)
              or else Has_Full_Default_Initialization (Component_Type (Typ));
 
-      --  A protected type, record type or type extension is fully default
+      --  A protected type, record type, or type extension is fully default
       --  initialized if all its components either carry an initialization
       --  expression or have a type that is fully default initialized. The
       --  parent type of a type extension must be fully default initialized.
@@ -13159,7 +13159,7 @@
             when N_Function_Call =>
                return Etype (N) /= Standard_Void_Type;
 
-            --  Attributes 'Input, 'Loop_Entry, 'Old and 'Result produce
+            --  Attributes 'Input, 'Loop_Entry, 'Old, and 'Result produce
             --  objects.
 
             when N_Attribute_Reference =>
@@ -13346,14 +13346,15 @@
    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
+      --  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
+      --  Determine whether an arbitrary node appears in an entry, function, or
+      --  procedure call.
 
       function Within_Volatile_Function (Id : Entity_Id) return Boolean;
       --  Determine whether an arbitrary entity appears in a volatile function
@@ -13405,7 +13406,7 @@
             if Nkind (Par) in N_Raise_xxx_Error then
                return True;
 
-               --  Prevent the search from going too far
+            --  Prevent the search from going too far
 
             elsif Is_Body_Or_Package_Declaration (Par) then
                exit;
@@ -13435,7 +13436,7 @@
             then
                return True;
 
-               --  Prevent the search from going too far
+            --  Prevent the search from going too far
 
             elsif Is_Body_Or_Package_Declaration (Par) then
                exit;
@@ -13481,8 +13482,8 @@
       if Nkind (Context) = N_Assignment_Statement then
          return True;
 
-         --  The volatile object is part of the initialization expression of
-         --  another object.
+      --  The volatile object is part of the initialization expression of
+      --  another object.
 
       elsif Nkind (Context) = N_Object_Declaration
         and then Present (Expression (Context))
@@ -13497,21 +13498,21 @@
          if Is_Return_Object (Obj_Id) then
             return Within_Volatile_Function (Obj_Id);
 
-            --  Otherwise this is a normal object initialization
+         --  Otherwise this is a normal object initialization
 
          else
             return True;
          end if;
 
-         --  The volatile object acts as the name of a renaming declaration
+      --  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.
+      --  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))
@@ -13520,14 +13521,14 @@
       then
          return True;
 
-         --  The volatile object is actually the prefix in a protected entry,
-         --  function, or procedure call.
+      --  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.
+      --  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
@@ -13535,8 +13536,8 @@
          return
            Within_Volatile_Function (Return_Statement_Entity (Context));
 
-         --  The volatile object appears as the prefix of a name occurring in a
-         --  non-interfering 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,
@@ -13550,8 +13551,8 @@
       then
          return True;
 
-         --  The volatile object appears as the expression of a type conversion
-         --  occurring in a non-interfering context.
+      --  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)
@@ -13562,21 +13563,22 @@
       then
          return True;
 
-         --  Allow references to volatile objects in various checks. This is
-         --  not a direct SPARK 2014 requirement.
+      --  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.
+      --  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 (see routine
+      --  Resolve_Actuals).
 
       elsif Within_Subprogram_Call (Context) then
          return True;
 
-         --  Otherwise the context is not suitable for an effectively volatile
-         --  object.
+      --  Otherwise the context is not suitable for an effectively volatile
+      --  object.
 
       else
          return False;
@@ -13888,7 +13890,7 @@
 
    begin
       --  Verify that prefix is analyzed and has the proper form. Note that
-      --  the attributes Elab_Spec, Elab_Body and Elab_Subp_Body which also
+      --  the attributes Elab_Spec, Elab_Body, and Elab_Subp_Body, which also
       --  produce the address of an entity, do not analyze their prefix
       --  because they denote entities that are not necessarily visible.
       --  Neither of them can apply to a protected type.
@@ -16034,7 +16036,7 @@
 
       procedure Copy_Itype_With_Replacement (New_Itype : Entity_Id) is
       begin
-         --  Translate Next_Entity, Scope and Etype fields, in case they
+         --  Translate Next_Entity, Scope, and Etype fields, in case they
          --  reference entities that have been mapped into copies.
 
          Set_Next_Entity (New_Itype, Assoc (Next_Entity (New_Itype)));
@@ -19986,8 +19988,8 @@
          return False;
       end if;
 
-      --  Check that the size of the component is 8, 16, 32 or 64 bits and that
-      --  Typ is properly aligned.
+      --  Check that the size of the component is 8, 16, 32, or 64 bits and
+      --  that Typ is properly aligned.
 
       case Size is
          when 8 | 16 | 32 | 64 =>
