2014-07-29 Robert Dewar <dewar@adacore.com>

	* sinfo.ads, inline.adb, inline.ads, sem_ch6.adb: Minor reformatting.
	* snames.ads-tmpl: Minor reformatting.
	* xsnamest.adb (XSnamesT): Remove special casing of Name_Error
	to give <Error>.  Not clear why this was there, but the compiler
	sources do not reference Name_Error, and this interfered with
	the circuits for pragma Unevaluated_Use_Of_Old.

2014-07-29  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Process_Atomic_Shared_Volatile): Allow volatile
	types in SPARK 2014 (again).
	* sem_res.adb (Is_OK_Volatile_Context): New routine.
	(Resolve_Entity_Name): Ensure that a volatile object with
	enabled properties Async_Writers or Effectire_Reads appears in
	a non-interfering context.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@213180 138bc75d-0d04-0410-961f-82ee72b054a4

9 files changed, 223 insertions, 178 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 835e8346a0e..1543bdc167a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,21 @@
+2014-07-29  Robert Dewar  <dewar@adacore.com>
+
+	* sinfo.ads, inline.adb, inline.ads, sem_ch6.adb: Minor reformatting.
+	* snames.ads-tmpl: Minor reformatting.
+	* xsnamest.adb (XSnamesT): Remove special casing of Name_Error
+	to give <Error>.  Not clear why this was there, but the compiler
+	sources do not reference Name_Error, and this interfered with
+	the circuits for pragma Unevaluated_Use_Of_Old.
+
+2014-07-29  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Process_Atomic_Shared_Volatile): Allow volatile
+	types in SPARK 2014 (again).
+	* sem_res.adb (Is_OK_Volatile_Context): New routine.
+	(Resolve_Entity_Name): Ensure that a volatile object with
+	enabled properties Async_Writers or Effectire_Reads appears in
+	a non-interfering context.
+
 2014-07-29  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch6.adb: Move Build_Body_To_Inline,
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 9d244bbf27f..2dc8be7359c 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -108,9 +108,9 @@ package body Inline is
       Next : Succ_Index;
    end record;
 
-   --  The following table stores list elements for the successor lists.
-   --  These lists cannot be chained directly through entries in the Inlined
-   --  table, because a given subprogram can appear in several such lists.
+   --  The following table stores list elements for the successor lists. These
+   --  lists cannot be chained directly through entries in the Inlined table,
+   --  because a given subprogram can appear in several such lists.
 
    package Successors is new Table.Table (
       Table_Component_Type => Succ_Info,
@@ -143,8 +143,8 @@ package body Inline is
 
    function Get_Code_Unit_Entity (E : Entity_Id) return Entity_Id;
    pragma Inline (Get_Code_Unit_Entity);
-   --  Return the entity node for the unit containing E. Always return
-   --  the spec for a package.
+   --  Return the entity node for the unit containing E. Always return the spec
+   --  for a package.
 
    function In_Main_Unit_Or_Subunit (E : Entity_Id) return Boolean;
    --  Return True if E is in the main unit or its spec or in a subunit
@@ -163,12 +163,11 @@ package body Inline is
    --  non-trivial initialization procedures, they are not worth inlining.
 
    function Is_Nested (E : Entity_Id) return Boolean;
-   --  If the function is nested inside some other function, it will
-   --  always be compiled if that function is, so don't add it to the
-   --  inline list. We cannot compile a nested function outside the
-   --  scope of the containing function anyway. This is also the case if
-   --  the function is defined in a task body or within an entry (for
-   --  example, an initialization procedure).
+   --  If the function is nested inside some other function, it will always
+   --  be compiled if that function is, so don't add it to the inline list.
+   --  We cannot compile a nested function outside the scope of the containing
+   --  function anyway. This is also the case if the function is defined in a
+   --  task body or within an entry (for example, an initialization procedure).
 
    procedure Add_Inlined_Subprogram (Index : Subp_Index);
    --  Add the subprogram to the list of inlined subprogram for the unit
@@ -178,12 +177,12 @@ package body Inline is
    ------------------------------
 
    --  The cleanup actions for scopes that contain instantiations is delayed
-   --  until after expansion of those instantiations, because they may
-   --  contain finalizable objects or tasks that affect the cleanup code.
-   --  A scope that contains instantiations only needs to be finalized once,
-   --  even if it contains more than one instance. We keep a list of scopes
-   --  that must still be finalized, and call cleanup_actions after all the
-   --  instantiations have been completed.
+   --  until after expansion of those instantiations, because they may contain
+   --  finalizable objects or tasks that affect the cleanup code. A scope
+   --  that contains instantiations only needs to be finalized once, even
+   --  if it contains more than one instance. We keep a list of scopes
+   --  that must still be finalized, and call cleanup_actions after all
+   --  the instantiations have been completed.
 
    To_Clean : Elist_Id;
 
@@ -299,9 +298,7 @@ package body Inline is
          while Scope (Scop) /= Standard_Standard
            and then not Is_Child_Unit (Scop)
          loop
-            if Is_Overloadable (Scop)
-              and then Is_Inlined (Scop)
-            then
+            if Is_Overloadable (Scop) and then Is_Inlined (Scop) then
                Add_Call (E, Scop);
 
                if Inline_Level = 1 then
@@ -430,9 +427,9 @@ package body Inline is
          end if;
 
          if Present
-          (Exception_Handlers
-            (Handled_Statement_Sequence
-              (Unit_Declaration_Node (Corresponding_Body (Decl)))))
+              (Exception_Handlers
+                 (Handled_Statement_Sequence
+                    (Unit_Declaration_Node (Corresponding_Body (Decl)))))
          then
             return True;
          end if;
@@ -462,8 +459,8 @@ package body Inline is
 
       if Is_Inlined (E)
         and then (Is_Inlined (Pack)
-                    or else Is_Generic_Instance (Pack)
-                    or else Is_Internal (E))
+                   or else Is_Generic_Instance (Pack)
+                   or else Is_Internal (E))
         and then not In_Main_Unit_Or_Subunit (E)
         and then not Is_Nested (E)
         and then not Has_Initialized_Type (E)
@@ -848,9 +845,9 @@ package body Inline is
       --  elementary statements, as a measure of acceptable size.
 
       function Has_Pending_Instantiation return Boolean;
-      --  If some enclosing body contains instantiations that appear before the
-      --  corresponding generic body, the enclosing body has a freeze node so
-      --  that it can be elaborated after the generic itself. This might
+      --  If some enclosing body contains instantiations that appear before
+      --  the corresponding generic body, the enclosing body has a freeze node
+      --  so that it can be elaborated after the generic itself. This might
       --  conflict with subsequent inlinings, so that it is unsafe to try to
       --  inline in such a case.
 
@@ -919,7 +916,7 @@ package body Inline is
          D := First (Decls);
          while Present (D) loop
             if (Nkind (D) = N_Function_Instantiation
-                  and then not Is_Unchecked_Conversion (D))
+                 and then not Is_Unchecked_Conversion (D))
               or else Nkind_In (D, N_Protected_Type_Declaration,
                                    N_Package_Declaration,
                                    N_Package_Instantiation,
@@ -972,10 +969,10 @@ package body Inline is
                elsif Present (Handled_Statement_Sequence (S))
                   and then
                     (Present
-                      (Exception_Handlers (Handled_Statement_Sequence (S)))
-                     or else
-                       Has_Excluded_Statement
-                         (Statements (Handled_Statement_Sequence (S))))
+                       (Exception_Handlers (Handled_Statement_Sequence (S)))
+                      or else
+                        Has_Excluded_Statement
+                          (Statements (Handled_Statement_Sequence (S))))
                then
                   return True;
                end if;
@@ -1019,9 +1016,10 @@ package body Inline is
 
             elsif Nkind (S) = N_Extended_Return_Statement then
                if Has_Excluded_Statement
-                  (Statements (Handled_Statement_Sequence (S)))
-                 or else Present
-                   (Exception_Handlers (Handled_Statement_Sequence (S)))
+                    (Statements (Handled_Statement_Sequence (S)))
+                 or else
+                   Present
+                     (Exception_Handlers (Handled_Statement_Sequence (S)))
                then
                   return True;
                end if;
@@ -1251,9 +1249,9 @@ package body Inline is
                First (Exception_Handlers (Handled_Statement_Sequence (N))),
                Subp);
             return;
+
          elsif
-           Has_Excluded_Statement
-             (Statements (Handled_Statement_Sequence (N)))
+           Has_Excluded_Statement (Statements (Handled_Statement_Sequence (N)))
          then
             return;
          end if;
@@ -1293,11 +1291,11 @@ package body Inline is
 
       --  We need to capture references to the formals in order to substitute
       --  the actuals at the point of inlining, i.e. instantiation. To treat
-      --  the formals as globals to the body to inline, we nest it within
-      --  a dummy parameterless subprogram, declared within the real one.
-      --  To avoid generating an internal name (which is never public, and
-      --  which affects serial numbers of other generated names), we use
-      --  an internal symbol that cannot conflict with user declarations.
+      --  the formals as globals to the body to inline, we nest it within a
+      --  dummy parameterless subprogram, declared within the real one. To
+      --  avoid generating an internal name (which is never public, and which
+      --  affects serial numbers of other generated names), we use an internal
+      --  symbol that cannot conflict with user declarations.
 
       Set_Parameter_Specifications (Specification (Original_Body), No_List);
       Set_Defining_Unit_Name
@@ -1421,7 +1419,7 @@ package body Inline is
                   Gen_P : constant Entity_Id := Generic_Parent (Parent (Subp));
                begin
                   if Is_Predefined_File_Name
-                    (Unit_File_Name (Get_Source_Unit (Gen_P)))
+                       (Unit_File_Name (Get_Source_Unit (Gen_P)))
                   then
                      Set_Is_Inlined (Subp, False);
                      Error_Msg_NE (Msg & "p?", N, Subp);
@@ -1681,7 +1679,7 @@ package body Inline is
             D := First (Decls);
             while Present (D) loop
                if (Nkind (D) = N_Function_Instantiation
-                   and then not Is_Unchecked_Conversion (D))
+                    and then not Is_Unchecked_Conversion (D))
                  or else Nkind_In (D, N_Protected_Type_Declaration,
                                    N_Package_Declaration,
                                    N_Package_Instantiation,
@@ -1734,17 +1732,17 @@ package body Inline is
 
                   elsif Present (Handled_Statement_Sequence (S)) then
                      if Present
-                       (Exception_Handlers (Handled_Statement_Sequence (S)))
+                          (Exception_Handlers (Handled_Statement_Sequence (S)))
                      then
                         Cannot_Inline
                           ("cannot inline& (exception handler)?",
                            First (Exception_Handlers
-                             (Handled_Statement_Sequence (S))),
+                                    (Handled_Statement_Sequence (S))),
                            Subp);
                         return True;
 
                      elsif Has_Excluded_Statement
-                       (Statements (Handled_Statement_Sequence (S)))
+                             (Statements (Handled_Statement_Sequence (S)))
                      then
                         return True;
                      end if;
@@ -1797,7 +1795,7 @@ package body Inline is
                   elsif Present (Handled_Statement_Sequence (S))
                     and then
                       Present (Exception_Handlers
-                               (Handled_Statement_Sequence (S)))
+                                (Handled_Statement_Sequence (S)))
                   then
                      Cannot_Inline
                        ("cannot inline& (exception handler)?",
@@ -1824,9 +1822,7 @@ package body Inline is
          begin
             S := Current_Scope;
             while Present (S) loop
-               if Is_Compilation_Unit (S)
-                 or else Is_Child_Unit (S)
-               then
+               if Is_Compilation_Unit (S) or else Is_Child_Unit (S) then
                   return False;
 
                elsif Ekind (S) = E_Package
@@ -1862,12 +1858,12 @@ package body Inline is
                   if Present (Expression (N)) then
                      declare
                         Orig_Expr : constant Node_Id :=
-                          Original_Node (Expression (N));
+                                      Original_Node (Expression (N));
 
                      begin
                         if Nkind_In (Orig_Expr, N_Integer_Literal,
-                                     N_Real_Literal,
-                                     N_Character_Literal)
+                                                N_Real_Literal,
+                                                N_Character_Literal)
                         then
                            return OK;
 
@@ -2060,14 +2056,12 @@ package body Inline is
             then
                Cannot_Inline
                  ("cannot inline& (exception handler)?",
-                  First
-                    (Exception_Handlers (Handled_Statement_Sequence (N))),
+                  First (Exception_Handlers (Handled_Statement_Sequence (N))),
                   Subp);
-
                return False;
 
             elsif Has_Excluded_Statement
-              (Statements (Handled_Statement_Sequence (N)))
+                    (Statements (Handled_Statement_Sequence (N)))
             then
                return False;
             end if;
@@ -2096,7 +2090,6 @@ package body Inline is
             Cannot_Inline
               ("cannot inline& (forward instance within enclosing body)?",
                N, Subp);
-
             return False;
          end if;
 
@@ -2318,21 +2311,26 @@ package body Inline is
          --  Build a procedure containing the statements found in the extended
          --  return statement of the unconstrained function body N.
 
+         ---------------------
+         -- Build_Procedure --
+         ---------------------
+
          procedure Build_Procedure
            (Proc_Id   : out Entity_Id;
             Decl_List : out List_Id)
          is
-            Formal      : Entity_Id;
-            Formal_List : constant List_Id := New_List;
-            Proc_Spec   : Node_Id;
-            Proc_Body   : Node_Id;
-            Subp_Name   : constant Name_Id := New_Internal_Name ('F');
+            Formal         : Entity_Id;
+            Formal_List    : constant List_Id := New_List;
+            Proc_Spec      : Node_Id;
+            Proc_Body      : Node_Id;
+            Subp_Name      : constant Name_Id := New_Internal_Name ('F');
             Body_Decl_List : List_Id := No_List;
-            Param_Type  : Node_Id;
+            Param_Type     : Node_Id;
 
          begin
             if Nkind (Object_Definition (Ret_Obj)) = N_Identifier then
-               Param_Type := New_Copy (Object_Definition (Ret_Obj));
+               Param_Type :=
+                 New_Copy (Object_Definition (Ret_Obj));
             else
                Param_Type :=
                  New_Copy (Subtype_Mark (Object_Definition (Ret_Obj)));
@@ -2340,39 +2338,38 @@ package body Inline is
 
             Append_To (Formal_List,
               Make_Parameter_Specification (Loc,
-                Defining_Identifier =>
+                Defining_Identifier    =>
                   Make_Defining_Identifier (Loc,
                     Chars => Chars (Defining_Identifier (Ret_Obj))),
-                In_Present  => False,
-                Out_Present => True,
+                In_Present             => False,
+                Out_Present            => True,
                 Null_Exclusion_Present => False,
-                Parameter_Type => Param_Type));
+                Parameter_Type         => Param_Type));
 
             Formal := First_Formal (Spec_Id);
             while Present (Formal) loop
                Append_To (Formal_List,
                  Make_Parameter_Specification (Loc,
-                   Defining_Identifier =>
+                   Defining_Identifier    =>
                      Make_Defining_Identifier (Sloc (Formal),
                        Chars => Chars (Formal)),
-                   In_Present  => In_Present (Parent (Formal)),
-                   Out_Present => Out_Present (Parent (Formal)),
+                   In_Present             => In_Present (Parent (Formal)),
+                   Out_Present            => Out_Present (Parent (Formal)),
                    Null_Exclusion_Present =>
                      Null_Exclusion_Present (Parent (Formal)),
-                   Parameter_Type =>
+                   Parameter_Type         =>
                      New_Occurrence_Of (Etype (Formal), Loc),
-                   Expression =>
+                   Expression             =>
                      Copy_Separate_Tree (Expression (Parent (Formal)))));
 
                Next_Formal (Formal);
             end loop;
 
-            Proc_Id :=
-              Make_Defining_Identifier (Loc, Chars => Subp_Name);
+            Proc_Id := Make_Defining_Identifier (Loc, Chars => Subp_Name);
 
             Proc_Spec :=
               Make_Procedure_Specification (Loc,
-                Defining_Unit_Name => Proc_Id,
+                Defining_Unit_Name       => Proc_Id,
                 Parameter_Specifications => Formal_List);
 
             Decl_List := New_List;
@@ -2434,7 +2431,7 @@ package body Inline is
 
       begin
          --  Build the associated procedure, analyze it and insert it before
-         --  the function body N
+         --  the function body N.
 
          declare
             Scope     : constant Entity_Id := Current_Scope;
@@ -2468,7 +2465,7 @@ package body Inline is
 
             Proc_Call :=
               Make_Procedure_Call_Statement (Loc,
-                Name => New_Occurrence_Of (Proc_Id, Loc),
+                Name                   => New_Occurrence_Of (Proc_Id, Loc),
                 Parameter_Associations => Actual_List);
          end;
 
@@ -2483,7 +2480,7 @@ package body Inline is
 
          Blk_Stmt :=
            Make_Block_Statement (Loc,
-             Declarations => New_List (New_Obj),
+             Declarations               => New_List (New_Obj),
              Handled_Statement_Sequence =>
                Make_Handled_Sequence_Of_Statements (Loc,
                  Statements => New_List (
@@ -2501,14 +2498,14 @@ package body Inline is
    --  Start of processing for Check_And_Build_Body_To_Inline
 
    begin
-      --  Do not inline any subprogram that contains nested subprograms, since
-      --  the backend inlining circuit seems to generate uninitialized
+      --  Do not inline any subprogram that contains nested subprograms,
+      --  since the backend inlining circuit seems to generate uninitialized
       --  references in this case. We know this happens in the case of front
-      --  end ZCX support, but it also appears it can happen in other cases as
-      --  well. The backend often rejects attempts to inline in the case of
-      --  nested procedures anyway, so little if anything is lost by this.
-      --  Note that this is test is for the benefit of the back-end. There is
-      --  a separate test for front-end inlining that also rejects nested
+      --  end ZCX support, but it also appears it can happen in other cases
+      --  as well. The backend often rejects attempts to inline in the case
+      --  of nested procedures anyway, so little if anything is lost by this.
+      --  Note that this is test is for the benefit of the back-end. There
+      --  is a separate test for front-end inlining that also rejects nested
       --  subprograms.
 
       --  Do not do this test if errors have been detected, because in some
@@ -2517,7 +2514,7 @@ package body Inline is
 
       if Comes_From_Source (Body_Id)
         and then (Has_Pragma_Inline_Always (Spec_Id)
-                    or else Optimization_Level > 0)
+                   or else Optimization_Level > 0)
         and then Serious_Errors_Detected = 0
       then
          declare
@@ -2561,6 +2558,7 @@ package body Inline is
          end if;
       end if;
    end Check_And_Build_Body_To_Inline;
+
    -----------------------------
    -- Check_Body_For_Inlining --
    -----------------------------
@@ -2635,7 +2633,7 @@ package body Inline is
                                  Ent := First_Entity (P);
                                  while Present (Ent) loop
                                     if Is_Type (Ent)
-                                       and then Has_Completion_In_Body (Ent)
+                                      and then Has_Completion_In_Body (Ent)
                                     then
                                        Set_Full_View (Ent, Empty);
 
@@ -2692,12 +2690,12 @@ package body Inline is
            and then Is_Protected_Type (Scope (Scop))
            and then Present (Protected_Body_Subprogram (Scop))
          then
-            --  If a protected operation contains an instance, its
-            --  cleanup operations have been delayed, and the subprogram
-            --  has been rewritten in the expansion of the enclosing
-            --  protected body. It is the corresponding subprogram that
-            --  may require the cleanup operations, so propagate the
-            --  information that triggers cleanup activity.
+            --  If a protected operation contains an instance, its cleanup
+            --  operations have been delayed, and the subprogram has been
+            --  rewritten in the expansion of the enclosing protected body. It
+            --  is the corresponding subprogram that may require the cleanup
+            --  operations, so propagate the information that triggers cleanup
+            --  activity.
 
             Set_Uses_Sec_Stack
               (Protected_Body_Subprogram (Scop),
@@ -2712,9 +2710,9 @@ package body Inline is
          else
             Decl := Unit_Declaration_Node (Scop);
 
-            if Nkind (Decl) = N_Subprogram_Declaration
-              or else Nkind (Decl) = N_Task_Type_Declaration
-              or else Nkind (Decl) = N_Subprogram_Body_Stub
+            if Nkind_In (Decl, N_Subprogram_Declaration,
+                               N_Task_Type_Declaration,
+                               N_Subprogram_Body_Stub)
             then
                Decl := Unit_Declaration_Node (Corresponding_Body (Decl));
             end if;
@@ -2739,15 +2737,15 @@ package body Inline is
    is
       Loc       : constant Source_Ptr := Sloc (N);
       Is_Predef : constant Boolean :=
-                   Is_Predefined_File_Name
-                     (Unit_File_Name (Get_Source_Unit (Subp)));
+                    Is_Predefined_File_Name
+                      (Unit_File_Name (Get_Source_Unit (Subp)));
       Orig_Bod  : constant Node_Id :=
                     Body_To_Inline (Unit_Declaration_Node (Subp));
 
       Blk      : Node_Id;
       Decl     : Node_Id;
       Decls    : constant List_Id := New_List;
-      Exit_Lab : Entity_Id := Empty;
+      Exit_Lab : Entity_Id        := Empty;
       F        : Entity_Id;
       A        : Node_Id;
       Lab_Decl : Node_Id;
@@ -2823,8 +2821,8 @@ package body Inline is
             Exit_Lab := Make_Label (Loc, Lab_Id);
             Lab_Decl :=
               Make_Implicit_Label_Declaration (Loc,
-                Defining_Identifier  => Lab_Ent,
-                Label_Construct      => Exit_Lab);
+                Defining_Identifier => Lab_Ent,
+                Label_Construct     => Exit_Lab);
          end if;
       end Make_Exit_Label;
 
@@ -2922,7 +2920,7 @@ package body Inline is
                   Ret :=
                     Make_Qualified_Expression (Sloc (N),
                       Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
-                      Expression => Relocate_Node (Expression (N)));
+                      Expression   => Relocate_Node (Expression (N)));
                else
                   Ret :=
                     Unchecked_Convert_To
@@ -3333,7 +3331,7 @@ package body Inline is
             Bod := Copy_Generic_Node (Orig_Bod, Empty, Instantiating => True);
             Blk :=
               Make_Block_Statement (Loc,
-                Declarations => Declarations (Bod),
+                Declarations               => Declarations (Bod),
                 Handled_Statement_Sequence =>
                   Handled_Statement_Sequence (Bod));
 
@@ -3386,9 +3384,9 @@ package body Inline is
                  Copy_Generic_Node (Orig_Bod, Empty, Instantiating => True);
                Blk :=
                  Make_Block_Statement (Loc,
-                                       Declarations => Declarations (Bod),
-                                       Handled_Statement_Sequence =>
-                                         Handled_Statement_Sequence (Bod));
+                   Declarations               => Declarations (Bod),
+                   Handled_Statement_Sequence =>
+                     Handled_Statement_Sequence (Bod));
 
             --  Inline a call to a function that returns an unconstrained type.
             --  The semantic analyzer checked that frontend-inlined functions
@@ -3402,18 +3400,14 @@ package body Inline is
                pragma Assert
                  (Nkind
                    (First
-                     (Statements (Handled_Statement_Sequence (Orig_Bod))))
-                  = N_Block_Statement);
+                     (Statements (Handled_Statement_Sequence (Orig_Bod)))) =
+                                                         N_Block_Statement);
 
                declare
                   Blk_Stmt    : constant Node_Id :=
-                    First
-                      (Statements
-                        (Handled_Statement_Sequence (Orig_Bod)));
+                    First (Statements (Handled_Statement_Sequence (Orig_Bod)));
                   First_Stmt  : constant Node_Id :=
-                    First
-                      (Statements
-                        (Handled_Statement_Sequence (Blk_Stmt)));
+                    First (Statements (Handled_Statement_Sequence (Blk_Stmt)));
                   Second_Stmt : constant Node_Id := Next (First_Stmt);
 
                begin
@@ -3652,8 +3646,7 @@ package body Inline is
             --  eventually be possible to remove that temporary and use the
             --  result variable directly.
 
-            if Is_Unc
-              and then Nkind (Parent (N)) /= N_Assignment_Statement
+            if Is_Unc and then Nkind (Parent (N)) /= N_Assignment_Statement
             then
                Decl :=
                  Make_Object_Declaration (Loc,
@@ -3857,6 +3850,7 @@ package body Inline is
          Next_Formal (F);
       end loop;
    end Expand_Inlined_Call;
+
    --------------------------
    -- Get_Code_Unit_Entity --
    --------------------------
@@ -3887,7 +3881,6 @@ package body Inline is
       else
          Decl := First (Declarations (E_Body));
          while Present (Decl) loop
-
             if Nkind (Decl) = N_Full_Type_Declaration
               and then Present (Init_Proc (Defining_Identifier (Decl)))
             then
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index e6bab07fe86..4c1dbf92fe9 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -35,12 +35,12 @@
 --  of them uses a workpile algorithm, but they are called independently from
 --  Frontend, and thus are not mutually recursive.
 
---  Front-end inlining for subprograms marked Inline_Always. This is primarily
---  an expansion activity that is performed for performance reasons, and when
---  the target does not use the gcc backend.  Inline_Always can also be used
---  in the context of GNATprove, to perform source transformations to simplify
---  proof obligations. The machinery used in both cases is similar, but there
---  are fewer restrictions on the source of subprograms in the latter case.
+--  c) Front-end inlining for Inline_Always subprograms. This is primarily an
+--  expansion activity that is performed for performance reasons, and when the
+--  target does not use the gcc backend. Inline_Always can also be used in the
+--  context of GNATprove, to perform source transformations to simplify proof
+--  obligations. The machinery used in both cases is similar, but there are
+--  fewer restrictions on the source of subprograms in the latter case.
 
 with Alloc;
 with Opt;    use Opt;
@@ -133,7 +133,7 @@ package Inline is
    Backend_Calls : Elist_Id := No_Elist;
    --  List of frontend inlined calls and inline calls passed to the backend
 
------------------
+   -----------------
    -- Subprograms --
    -----------------
 
@@ -168,7 +168,7 @@ package Inline is
    --  that cannot be inlined, the offending construct is flagged accordingly.
 
    procedure Cannot_Inline
-      (Msg        : String;
+     (Msg        : String;
       N          : Node_Id;
       Subp       : Entity_Id;
       Is_Serious : Boolean := False);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index b452124be58..8caf19c49a6 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1942,7 +1942,7 @@ package body Sem_Ch6 is
                   if From_Limited_With (Typ) and then In_Package_Body then
                      Error_Msg_NE
                        ("invalid use of incomplete type&",
-                          Result_Definition (N), Typ);
+                        Result_Definition (N), Typ);
 
                   elsif Is_Tagged_Type (Typ) then
                      null;
@@ -3960,7 +3960,8 @@ package body Sem_Ch6 is
                   Error_Msg_N
                     ("interface procedure % must be abstract or null", N);
                else
-                  Error_Msg_N ("interface function % must be abstract", N);
+                  Error_Msg_N
+                    ("interface function % must be abstract", N);
                end if;
             end if;
          end;
@@ -4168,9 +4169,9 @@ package body Sem_Ch6 is
          --  the check is applied later (see Analyze_Subprogram_Declaration).
 
          if not Nkind_In (Original_Node (Parent (N)),
-                            N_Subprogram_Renaming_Declaration,
-                            N_Abstract_Subprogram_Declaration,
-                            N_Formal_Abstract_Subprogram_Declaration)
+                          N_Subprogram_Renaming_Declaration,
+                          N_Abstract_Subprogram_Declaration,
+                          N_Formal_Abstract_Subprogram_Declaration)
          then
             if Is_Abstract_Type (Etype (Designator))
               and then not Is_Interface (Etype (Designator))
@@ -4188,7 +4189,7 @@ package body Sem_Ch6 is
               and then Ada_Version >= Ada_2012
             then
                Error_Msg_N ("function whose access result designates "
-                 & "abstract type must be abstract", N);
+                            & "abstract type must be abstract", N);
             end if;
          end if;
       end if;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 16b93ab6d53..f33f268732a 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -6317,14 +6317,6 @@ package body Sem_Prag is
             Set_Treat_As_Volatile (E);
             Set_Treat_As_Volatile (Underlying_Type (E));
 
-            --  The following check is only relevant when SPARK_Mode is on as
-            --  this is not a standard Ada legality rule. Volatile types are
-            --  not allowed (SPARK RM C.6(1)).
-
-            if SPARK_Mode = On and then Prag_Id = Pragma_Volatile then
-               Error_Msg_N ("volatile type not allowed", E);
-            end if;
-
          elsif K = N_Object_Declaration
            or else (K = N_Component_Declaration
                      and then Original_Record_Component (E) = E)
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index ca4cc59a6ee..9f304eedb8b 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6420,6 +6420,13 @@ package body Sem_Res is
       function Appears_In_Check (Nod : Node_Id) return Boolean;
       --  Denote whether an arbitrary node Nod appears in a check node
 
+      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(13)) where volatile reference Obj_Ref
+      --  can safely reside.
+
       ----------------------
       -- Appears_In_Check --
       ----------------------
@@ -6447,6 +6454,64 @@ package body Sem_Res is
          return False;
       end Appears_In_Check;
 
+      ----------------------------
+      -- Is_OK_Volatile_Context --
+      ----------------------------
+
+      function Is_OK_Volatile_Context
+        (Context : Node_Id;
+         Obj_Ref : Node_Id) return Boolean
+      is
+      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. Ensure that the climb of the parent chain came
+         --  from the expression side and not from the name side.
+
+         elsif Nkind (Context) = N_Object_Declaration
+           and then Present (Expression (Context))
+           and then Expression (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_Unchecked_Conversion_Instance (Entity (Name (Context)))
+           and then Nkind (Parent (Context)) = N_Object_Renaming_Declaration
+         then
+            return True;
+
+         --  The volatile object appears as the prefix of a name occurring
+         --  in a non-interfering context.
+
+         elsif Nkind_In (Context, N_Attribute_Reference,
+                                  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;
+
+         --  Allow references to volatile objects in various checks. This is
+         --  not a direct SPARK 2014 requirement.
+
+         elsif Appears_In_Check (Context) then
+            return True;
+
+         else
+            return False;
+         end if;
+      end Is_OK_Volatile_Context;
+
       --  Local variables
 
       E   : constant Entity_Id := Entity (N);
@@ -6568,28 +6633,10 @@ package body Sem_Res is
         and then
           (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
       then
-         --  The volatile object can appear on either side of an assignment
+         --  The volatile objects appears in a "non-interfering context" as
+         --  defined in SPARK RM 7.1.3(13).
 
-         if Nkind (Par) = N_Assignment_Statement then
-            null;
-
-         --  The volatile object is part of the initialization expression of
-         --  another object. Ensure that the climb of the parent chain came
-         --  from the expression side and not from the name side.
-
-         elsif Nkind (Par) = N_Object_Declaration
-           and then Present (Expression (Par))
-           and then N = Expression (Par)
-         then
-            null;
-
-         --  The volatile object appears as an actual parameter in a call to an
-         --  instance of Unchecked_Conversion whose result is renamed.
-
-         elsif Nkind (Par) = N_Function_Call
-           and then Is_Unchecked_Conversion_Instance (Entity (Name (Par)))
-           and then Nkind (Parent (Par)) = N_Object_Renaming_Declaration
-         then
+         if Is_OK_Volatile_Context (Par, N) then
             null;
 
          --  Assume that references to volatile objects that appear as actual
@@ -6599,10 +6646,8 @@ package body Sem_Res is
          elsif Nkind (Par) = N_Procedure_Call_Statement then
             null;
 
-         --  Allow references to volatile objects in various checks
-
-         elsif Appears_In_Check (Par) then
-            null;
+         --  Otherwise the context causes a side effect with respect to the
+         --  volatile object.
 
          else
             Error_Msg_N
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 13d1d599bb8..5c085410571 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -1851,9 +1851,9 @@ package Sinfo is
    --    to assist in detecting this illegal use of Unrestricted_Access.
 
    --  Null_Excluding_Subtype (Flag16)
-   --   Present in N_Access_To_Object_Definition. Indicates that the subtype
-   --   indication carries a null-exclusion indicator, which is distinct from
-   --   the null-exclusion indicator that may precede the access keyword.
+   --    Present in N_Access_To_Object_Definition. Indicates that the subtype
+   --    indication carries a null-exclusion indicator, which is distinct from
+   --    the null-exclusion indicator that may precede the access keyword.
 
    --  Original_Discriminant (Node2-Sem)
    --    Present in identifiers. Used in references to discriminants that
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 8315566a155..e6ee6f1e1de 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -56,8 +56,8 @@ package Snames is
 
    --  First we have the one character names used to optimize the lookup
    --  process for one character identifiers (to avoid the hashing in this
-   --  case) There are a full 256 of these, but only the entries for lower case
-   --  and upper case letters have identifiers
+   --  case) There are a full 256 of these, but only the entries for lower
+   --  case and upper case letters have identifiers
 
    --  The lower case letter entries are used for one character identifiers
    --  appearing in the source, for example in pragma Interface (C).
diff --git a/gcc/ada/xsnamest.adb b/gcc/ada/xsnamest.adb
index a22eec02aa7..a7fbb2ad649 100644
--- a/gcc/ada/xsnamest.adb
+++ b/gcc/ada/xsnamest.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -255,10 +255,6 @@ begin
                Name0 := 'O' & Translate (Name0, Lower_Case_Map);
             end if;
 
-            if Name0 = "error" then
-               Name0 := V ("<error>");
-            end if;
-
             if not Match (Name0, Chk_Low) then
                Put_Line (OutB, "     """ & Name0 & "#"" &");
             end if;