[multiple changes]

2014-07-30  Bob Duff  <duff@adacore.com>

	* g-exctra.adb, g-exctra.ads, s-exctra.adb, s-exctra.ads, Makefile.rtl,
	g-trasym.adb, g-trasym.ads, s-trasym.adb, s-trasym.ads: Move
	GNAT.Traceback.Symbolic and GNAT.Exception_Traces into the System
	hierarchy (System.Traceback.Symbolic and System.Exception_Traces), so
	we can call them from the runtimes. Leave renamings in place under GNAT.

2014-07-30  Yannick Moy  <moy@adacore.com>

	* inline.adb (Check_And_Build_Body_To_Inline): Include code for
	inlining in GNATprove mode.

2014-07-30  Ed Schonberg  <schonberg@adacore.com>

	* a-cohase.adb, a-cohase.ads (Generic_Keys): Add a
	Reference_Control_Type to generic package, to keep additional
	information for Reference_Types that manipulate keys. Add Adjust and
	Finalize procedures for this type.
	(Delete_Node): New procedure called when finalizing a
	Reference_Control_Type, to remove a node whose element has been
	improperly updated through a Reference.
	(Insert): Detect tampering.
	(Reference_Preserving_Key): Build proper Reference_Control_Type,
	and update Busy and Lock bits to detect tampering.

2014-07-30  Bob Duff  <duff@adacore.com>

	* exp_intr.ads: Minor comment fix.

From-SVN: r213276

14 files changed, 717 insertions, 296 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3ca141d..d216f82 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,33 @@
+2014-07-30  Bob Duff  <duff@adacore.com>
+
+	* g-exctra.adb, g-exctra.ads, s-exctra.adb, s-exctra.ads, Makefile.rtl,
+	g-trasym.adb, g-trasym.ads, s-trasym.adb, s-trasym.ads: Move
+	GNAT.Traceback.Symbolic and GNAT.Exception_Traces into the System
+	hierarchy (System.Traceback.Symbolic and System.Exception_Traces), so
+	we can call them from the runtimes. Leave renamings in place under GNAT.
+
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* inline.adb (Check_And_Build_Body_To_Inline): Include code for
+	inlining in GNATprove mode.
+
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* a-cohase.adb, a-cohase.ads (Generic_Keys): Add a
+	Reference_Control_Type to generic package, to keep additional
+	information for Reference_Types that manipulate keys. Add Adjust and
+	Finalize procedures for this type.
+	(Delete_Node): New procedure called when finalizing a
+	Reference_Control_Type, to remove a node whose element has been
+	improperly updated through a Reference.
+	(Insert): Detect tampering.
+	(Reference_Preserving_Key): Build proper Reference_Control_Type,
+	and update Busy and Lock bits to detect tampering.
+
+2014-07-30  Bob Duff  <duff@adacore.com>
+
+	* exp_intr.ads: Minor comment fix.
+
 2014-07-30  Gary Dismukes  <dismukes@adacore.com>
 
 	* exp_prag.adb, a-tags.ads: Minor typo fixes.
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index 98b7429..4798864 100644
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -408,6 +408,7 @@ GNATRTL_NONTASKING_OBJS= \
   g-excact$(objext) \
   g-except$(objext) \
   g-exctra$(objext) \
+  s-exctra$(objext) \
   g-expect$(objext) \
   g-exptty$(objext) \
   g-flocon$(objext) \
@@ -458,6 +459,7 @@ GNATRTL_NONTASKING_OBJS= \
   g-timsta$(objext) \
   g-traceb$(objext) \
   g-trasym$(objext) \
+  s-trasym$(objext) \
   g-tty$(objext) \
   g-u3spch$(objext) \
   g-utf_32$(objext) \
diff --git a/gcc/ada/a-cohase.adb b/gcc/ada/a-cohase.adb
index 1c3db68..421ac3e 100644
--- a/gcc/ada/a-cohase.adb
+++ b/gcc/ada/a-cohase.adb
@@ -132,6 +132,16 @@ package body Ada.Containers.Hashed_Sets is
    procedure Write_Nodes is
       new HT_Ops.Generic_Write (Write_Node);
 
+   procedure Delete_Node
+     (C    : in out Set;
+      Indx : Hash_Type;
+      X    : in out Node_Access);
+
+   --  Delete a node whose bucket position is known. Used to remove a node
+   --  whose element has been modified through a key_preserving reference.
+   --  We cannot use the value of the element precisely because the current
+   --  value does not correspond to the hash code that determines the bucket.
+
    ---------
    -- "=" --
    ---------
@@ -328,6 +338,48 @@ package body Ada.Containers.Hashed_Sets is
       Position.Container := null;
    end Delete;
 
+   procedure Delete_Node
+     (C    : in out Set;
+      Indx : Hash_Type;
+      X    : in out Node_Access)
+   is
+      HT   : Hash_Table_Type renames C.HT;
+      Prev : Node_Access;
+      Curr : Node_Access;
+
+   begin
+      Prev := HT.Buckets (Indx);
+      if Prev = X then
+         HT.Buckets (Indx) := Next (Prev);
+         HT.Length := HT.Length - 1;
+         Free (X);
+         return;
+      end if;
+
+      if HT.Length = 1 then
+         raise Program_Error with
+           "attempt to delete node not in its proper hash bucket";
+      end if;
+
+      loop
+         Curr := Next (Prev);
+
+         if Curr = null then
+            raise Program_Error with
+              "attempt to delete node not in its proper hash bucket";
+         end if;
+
+         if Curr = X then
+            Set_Next (Node => Prev, Next => Next (Curr));
+            HT.Length := HT.Length - 1;
+            Free (X);
+            return;
+         end if;
+         Prev := Curr;
+      end loop;
+
+   end Delete_Node;
+
    ----------------
    -- Difference --
    ----------------
@@ -824,6 +876,11 @@ package body Ada.Containers.Hashed_Sets is
          HT_Ops.Reserve_Capacity (HT, 1);
       end if;
 
+      if HT.Busy > 0 then
+         raise Program_Error with
+           "attempt tp tamper with cursors (set is busy)";
+      end if;
+
       Local_Insert (HT, New_Item, Node, Inserted);
 
       if Inserted
@@ -1921,6 +1978,24 @@ package body Ada.Containers.Hashed_Sets is
       -- Local Subprograms --
       -----------------------
 
+      ------------
+      -- Adjust --
+      ------------
+
+      procedure Adjust (Control : in out Reference_Control_Type) is
+      begin
+         if Control.Container /= null then
+            declare
+               HT : Hash_Table_Type renames Control.Container.all.HT;
+               B : Natural renames HT.Busy;
+               L : Natural renames HT.Lock;
+            begin
+               B := B + 1;
+               L := L + 1;
+            end;
+         end if;
+      end Adjust;
+
       function Equivalent_Key_Node
         (Key  : Key_Type;
          Node : Node_Access) return Boolean;
@@ -2046,6 +2121,33 @@ package body Ada.Containers.Hashed_Sets is
          Free (X);
       end Exclude;
 
+      --------------
+      -- Finalize --
+      --------------
+
+      procedure Finalize (Control : in out Reference_Control_Type) is
+      begin
+         if Control.Container /= null then
+            declare
+               HT : Hash_Table_Type renames Control.Container.all.HT;
+               B : Natural renames HT.Busy;
+               L : Natural renames HT.Lock;
+            begin
+               B := B - 1;
+               L := L - 1;
+            end;
+
+            if Hash (Key (Element (Control.Old_Pos))) /= Control.Old_Hash
+            then
+               Delete_Node
+                (Control.Container.all, Control.Index,  Control.Old_Pos.Node);
+               raise Program_Error with "key not preserved in reference";
+            end if;
+
+            Control.Container := null;
+         end if;
+      end Finalize;
+
       ----------
       -- Find --
       ----------
@@ -2115,11 +2217,24 @@ package body Ada.Containers.Hashed_Sets is
            (Vet (Position),
             "bad cursor in function Reference_Preserving_Key");
 
-         --  Some form of finalization will be required in order to actually
-         --  check that the key-part of the element designated by Position has
-         --  not changed.  ???
-
-         return (Element => Position.Node.Element'Access);
+         declare
+            HT : Hash_Table_Type renames Position.Container.all.HT;
+            B : Natural renames HT.Busy;
+            L : Natural renames HT.Lock;
+         begin
+            return R : constant Reference_Type :=
+                (Element  => Position.Node.Element'Access,
+                  Control  =>
+                    (Controlled with
+                       Container'Unrestricted_Access,
+                       Index  => HT_Ops.Index (HT, Position.Node),
+                       Old_Pos => Position,
+                       Old_Hash => Hash (Key (Position))))
+            do
+               B := B + 1;
+               L := L + 1;
+            end return;
+         end;
       end Reference_Preserving_Key;
 
       function Reference_Preserving_Key
@@ -2133,11 +2248,25 @@ package body Ada.Containers.Hashed_Sets is
             raise Constraint_Error with "Key not in set";
          end if;
 
-         --  Some form of finalization will be required in order to actually
-         --  check that the key-part of the element designated by Key has not
-         --  changed.  ???
-
-         return (Element => Node.Element'Access);
+         declare
+            HT : Hash_Table_Type renames Container.HT;
+            B : Natural renames HT.Busy;
+            L : Natural renames HT.Lock;
+            P : constant Cursor := Find (Container, Key);
+         begin
+            return R : constant Reference_Type :=
+              (Element  => Node.Element'Access,
+               Control  =>
+                 (Controlled with
+                   Container'Unrestricted_Access,
+                   Index  => HT_Ops.Index (HT, P.Node),
+                   Old_Pos => P,
+                   Old_Hash => Hash (Key)))
+            do
+               B := B + 1;
+               L := L + 1;
+            end return;
+         end;
       end Reference_Preserving_Key;
 
       -------------
diff --git a/gcc/ada/a-cohase.ads b/gcc/ada/a-cohase.ads
index 9c112fa..9e40f0e 100644
--- a/gcc/ada/a-cohase.ads
+++ b/gcc/ada/a-cohase.ads
@@ -35,7 +35,7 @@ with Ada.Iterator_Interfaces;
 
 private with Ada.Containers.Hash_Tables;
 private with Ada.Streams;
-private with Ada.Finalization;
+with Ada.Finalization;
 
 generic
    type Element_Type is private;
@@ -433,10 +433,44 @@ package Ada.Containers.Hashed_Sets is
          Key       : Key_Type) return Reference_Type;
 
    private
-      type Reference_Type (Element : not null access Element_Type)
-         is null record;
-
       use Ada.Streams;
+      type Set_Access is access all Set;
+      for Set_Access'Storage_Size use 0;
+
+      --  Key_Preserving references must carry information to allow removal
+      --  of elements whose value may have been altered improperly, i.e. have
+      --  been given values incompatible with the hash-code of the previous
+      --  value, and are thus in the wrong bucket. (RM 18.7 (96.6/3))
+
+      --  We cannot store the key directly because it is an unconstrained type.
+      --  To avoid using additional dynamic allocation we store the old cursor
+      --  which simplifies possible removal. This is not possible for some
+      --  other set types.
+
+      --  The mechanism is different for Update_Element_Preserving_Key, as
+      --  in that case the check that buckets have not changed is performed
+      --  at the time of the update, not when the reference is finalized.
+
+      type Reference_Control_Type is
+         new Ada.Finalization.Controlled with
+      record
+         Container : Set_Access;
+         Index     : Hash_Type;
+         Old_Pos   : Cursor;
+         Old_Hash  : Hash_Type;
+      end record;
+
+      overriding procedure
+         Adjust (Control : in out Reference_Control_Type);
+      pragma Inline (Adjust);
+
+      overriding procedure
+         Finalize (Control : in out Reference_Control_Type);
+      pragma Inline (Finalize);
+
+      type Reference_Type (Element : not null access Element_Type) is record
+         Control  : Reference_Control_Type;
+      end record;
 
       procedure Read
         (Stream : not null access Root_Stream_Type'Class;
@@ -449,7 +483,6 @@ package Ada.Containers.Hashed_Sets is
          Item   : Reference_Type);
 
       for Reference_Type'Write use Write;
-
    end Generic_Keys;
 
 private
@@ -498,6 +531,10 @@ private
       Node      : Node_Access;
    end record;
 
+   type Reference_Control_Type is new Ada.Finalization.Controlled with record
+      Container : Set_Access;
+   end record;
+
    procedure Write
      (Stream : not null access Root_Stream_Type'Class;
       Item   : Cursor);
@@ -510,11 +547,6 @@ private
 
    for Cursor'Read use Read;
 
-   type Reference_Control_Type is
-      new Controlled with record
-         Container : Set_Access;
-      end record;
-
    overriding procedure Adjust (Control : in out Reference_Control_Type);
    pragma Inline (Adjust);
 
diff --git a/gcc/ada/exp_intr.ads b/gcc/ada/exp_intr.ads
index a9d8a39..1285f4f 100644
--- a/gcc/ada/exp_intr.ads
+++ b/gcc/ada/exp_intr.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, 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- --
@@ -32,9 +32,9 @@ package Exp_Intr is
    procedure Expand_Intrinsic_Call (N : Node_Id; E : Entity_Id);
    --  N is either a function call node, a procedure call statement node, or
    --  an operator where the corresponding subprogram is intrinsic (i.e. was
-   --  the subject of a Import or Interface pragma specifying the subprogram
-   --  as intrinsic.  The effect is to replace the call with appropriate
-   --  specialized nodes.  The second argument is the entity for the
+   --  the subject of an Import or Interface pragma specifying the subprogram
+   --  as intrinsic. The effect is to replace the call with appropriate
+   --  specialized nodes. The second argument is the entity for the
    --  subprogram spec.
 
 end Exp_Intr;
diff --git a/gcc/ada/g-exctra.adb b/gcc/ada/g-exctra.adb
index 1ac24ce..8844fcf 100644
--- a/gcc/ada/g-exctra.adb
+++ b/gcc/ada/g-exctra.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 2000-2010, AdaCore                     --
+--                     Copyright (C) 2000-2014, AdaCore                     --
 --                                                                          --
 -- 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- --
@@ -29,89 +29,8 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with System.Standard_Library; use System.Standard_Library;
-with System.Soft_Links;       use System.Soft_Links;
+--  This package does not require a body, since it is a package renaming. We
+--  provide a dummy file containing a No_Body pragma so that previous versions
+--  of the body (which did exist) will not interfere.
 
-package body GNAT.Exception_Traces is
-
-   --  Calling the decorator directly from where it is needed would require
-   --  introducing nasty dependencies upon the spec of this package (typically
-   --  in a-except.adb). We also have to deal with the fact that the traceback
-   --  array within an exception occurrence and the one the decorator shall
-   --  accept are of different types. These are two reasons for which a wrapper
-   --  with a System.Address argument is indeed used to call the decorator
-   --  provided by the user of this package. This wrapper is called via a
-   --  soft-link, which either is null when no decorator is in place or "points
-   --  to" the following function otherwise.
-
-   function Decorator_Wrapper
-     (Traceback : System.Address;
-      Len       : Natural) return String;
-   --  The wrapper to be called when a decorator is in place for exception
-   --  backtraces.
-   --
-   --  Traceback is the address of the call chain array as stored in the
-   --  exception occurrence and Len is the number of significant addresses
-   --  contained in this array.
-
-   Current_Decorator : Traceback_Decorator := null;
-   --  The decorator to be called by the wrapper when it is not null, as set
-   --  by Set_Trace_Decorator. When this access is null, the wrapper is null
-   --  also and shall then not be called.
-
-   -----------------------
-   -- Decorator_Wrapper --
-   -----------------------
-
-   function Decorator_Wrapper
-     (Traceback : System.Address;
-      Len       : Natural) return String
-   is
-      Decorator_Traceback : Tracebacks_Array (1 .. Len);
-      for Decorator_Traceback'Address use Traceback;
-
-      --  Handle the "transition" from the array stored in the exception
-      --  occurrence to the array expected by the decorator.
-
-      pragma Import (Ada, Decorator_Traceback);
-
-   begin
-      return Current_Decorator.all (Decorator_Traceback);
-   end Decorator_Wrapper;
-
-   -------------------------
-   -- Set_Trace_Decorator --
-   -------------------------
-
-   procedure Set_Trace_Decorator (Decorator : Traceback_Decorator) is
-   begin
-      Current_Decorator := Decorator;
-      Traceback_Decorator_Wrapper :=
-        (if Current_Decorator /= null
-         then Decorator_Wrapper'Access else null);
-   end Set_Trace_Decorator;
-
-   ---------------
-   -- Trace_Off --
-   ---------------
-
-   procedure Trace_Off is
-   begin
-      Exception_Trace := RM_Convention;
-   end Trace_Off;
-
-   --------------
-   -- Trace_On --
-   --------------
-
-   procedure Trace_On (Kind : Trace_Kind) is
-   begin
-      case Kind is
-         when Every_Raise =>
-            Exception_Trace := Every_Raise;
-         when Unhandled_Raise =>
-            Exception_Trace := Unhandled_Raise;
-      end case;
-   end Trace_On;
-
-end GNAT.Exception_Traces;
+pragma No_Body;
diff --git a/gcc/ada/g-exctra.ads b/gcc/ada/g-exctra.ads
index 83bc339..aa264ba 100644
--- a/gcc/ada/g-exctra.ads
+++ b/gcc/ada/g-exctra.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---                     Copyright (C) 2000-2010, AdaCore                     --
+--                     Copyright (C) 2000-2014, AdaCore                     --
 --                                                                          --
 -- 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- --
@@ -31,66 +31,9 @@
 
 --  This package provides an interface allowing to control *automatic* output
 --  to standard error upon exception occurrences (as opposed to explicit
---  generation of traceback information using GNAT.Traceback).
+--  generation of traceback information using System.Traceback).
 
---  This output includes the basic information associated with the exception
---  (name, message) as well as a backtrace of the call chain at the point
---  where the exception occurred. This backtrace is only output if the call
---  chain information is available, depending if the binder switch dedicated
---  to that purpose has been used or not.
+--  See file s-exctra.ads for full documentation of the interface
 
---  The default backtrace is in the form of absolute code locations which may
---  be converted to corresponding source locations using the addr2line utility
---  or from within GDB. Please refer to GNAT.Traceback for information about
---  what is necessary to be able to exploit this possibility.
-
---  The backtrace output can also be customized by way of a "decorator" which
---  may return any string output in association with a provided call chain.
---  The decorator replaces the default backtrace mentioned above.
-
-with GNAT.Traceback; use GNAT.Traceback;
-
-package GNAT.Exception_Traces is
-
-   --  The following defines the exact situations in which raises will
-   --  cause automatic output of trace information.
-
-   type Trace_Kind is
-     (Every_Raise,
-      --  Denotes the initial raise event for any exception occurrence, either
-      --  explicit or due to a specific language rule, within the context of a
-      --  task or not.
-
-      Unhandled_Raise
-      --  Denotes the raise events corresponding to exceptions for which there
-      --  is no user defined handler, in particular, when a task dies due to an
-      --  unhandled exception.
-     );
-
-   --  The following procedures can be used to activate and deactivate
-   --  traces identified by the above trace kind values.
-
-   procedure Trace_On (Kind : Trace_Kind);
-   --  Activate the traces denoted by Kind
-
-   procedure Trace_Off;
-   --  Stop the tracing requested by the last call to Trace_On.
-   --  Has no effect if no such call has ever occurred.
-
-   --  The following provide the backtrace decorating facilities
-
-   type Traceback_Decorator is access
-     function (Traceback : Tracebacks_Array) return String;
-   --  A backtrace decorator is a function which returns the string to be
-   --  output for a call chain provided by way of a tracebacks array.
-
-   procedure Set_Trace_Decorator (Decorator : Traceback_Decorator);
-   --  Set the decorator to be used for future automatic outputs. Restore
-   --  the default behavior (output of raw addresses) if the provided
-   --  access value is null.
-   --
-   --  Note: GNAT.Traceback.Symbolic.Symbolic_Traceback may be used as the
-   --  Decorator, to get a symbolic traceback. This will cause a significant
-   --  cpu and memory overhead.
-
-end GNAT.Exception_Traces;
+with System.Exception_Traces;
+package GNAT.Exception_Traces renames System.Exception_Traces;
diff --git a/gcc/ada/g-trasym.adb b/gcc/ada/g-trasym.adb
index 35d4020..3fdfd1ad 100644
--- a/gcc/ada/g-trasym.adb
+++ b/gcc/ada/g-trasym.adb
@@ -29,51 +29,8 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This is the default implementation for platforms where the full capability
---  is not supported. It returns tracebacks as lists of LF separated strings of
---  the form "0x..." corresponding to the addresses.
+--  This package does not require a body, since it is a package renaming. We
+--  provide a dummy file containing a No_Body pragma so that previous versions
+--  of the body (which did exist) will not interfere.
 
-with Ada.Exceptions.Traceback; use Ada.Exceptions.Traceback;
-with System.Address_Image;
-
-package body GNAT.Traceback.Symbolic is
-
-   ------------------------
-   -- Symbolic_Traceback --
-   ------------------------
-
-   function Symbolic_Traceback (Traceback : Tracebacks_Array) return String is
-   begin
-      if Traceback'Length = 0 then
-         return "";
-
-      else
-         declare
-            Img : String := System.Address_Image (Traceback (Traceback'First));
-
-            Result : String (1 .. (Img'Length + 3) * Traceback'Length);
-            Last   : Natural := 0;
-
-         begin
-            for J in Traceback'Range loop
-               Img := System.Address_Image (Traceback (J));
-               Result (Last + 1 .. Last + 2) := "0x";
-               Last := Last + 2;
-               Result (Last + 1 .. Last + Img'Length) := Img;
-               Last := Last + Img'Length + 1;
-               Result (Last) := ASCII.LF;
-            end loop;
-
-            return Result (1 .. Last);
-         end;
-      end if;
-   end Symbolic_Traceback;
-
-   function Symbolic_Traceback
-     (E : Ada.Exceptions.Exception_Occurrence) return String
-   is
-   begin
-      return Symbolic_Traceback (Tracebacks (E));
-   end Symbolic_Traceback;
-
-end GNAT.Traceback.Symbolic;
+pragma No_Body;
diff --git a/gcc/ada/g-trasym.ads b/gcc/ada/g-trasym.ads
index a3ac108..1d9b3f7 100644
--- a/gcc/ada/g-trasym.ads
+++ b/gcc/ada/g-trasym.ads
@@ -31,71 +31,7 @@
 
 --  Run-time symbolic traceback support
 
---  The full capability is currently supported on the following targets:
+--  See file s-trasym.ads for full documentation of the interface
 
---     HP-UX ia64
---     GNU/Linux x86, x86_64, ia64
---     FreeBSD x86, x86_64
---     Solaris sparc and x86
---     OpenVMS Alpha and ia64
---     Windows
-
---  Note: on targets other than those listed above, a dummy implementation of
---  the body returns a series of LF separated strings of the form "0x..."
---  corresponding to the addresses.
-
---  The routines provided in this package assume that your application has
---  been compiled with debugging information turned on, since this information
---  is used to build a symbolic traceback.
-
---  If you want to retrieve tracebacks from exception occurrences, it is also
---  necessary to invoke the binder with -E switch. Please refer to the gnatbind
---  documentation for more information.
-
---  Note that it is also possible (and often recommended) to compute symbolic
---  traceback outside the program execution, which in addition allows you
---  to distribute the executable with no debug info:
---
---  - build your executable with debug info
---  - archive this executable
---  - strip a copy of the executable and distribute/deploy this version
---  - at run time, compute absolute traceback (-bargs -E) from your
---    executable and log it using Ada.Exceptions.Exception_Information
---  - off line, compute the symbolic traceback using the executable archived
---    with debug info and addr2line or gdb (using info line *<addr>) on the
---    absolute addresses logged by your application.
-
---  In order to retrieve symbolic information, functions in this package will
---  read on disk all the debug information of the executable file (found via
---  Argument (0), and looked in the PATH if needed) or shared libraries using
---  OS facilities, and load them in memory, causing a significant cpu and
---  memory overhead.
-
---  Symbolic traceback from shared libraries is only supported for VMS, Windows
---  and GNU/Linux. On other targets symbolic tracebacks are only supported for
---  the main executable. You should consider using gdb to obtain symbolic
---  traceback in such cases.
-
---  On VMS, there is no restriction on using this facility with shared
---  libraries. However, the OS should be at least v7.3-1 and OS patch
---  VMS731_TRACE-V0100 must be applied in order to use this package.
-
---  On platforms where the full capability is not supported, function
---  Symbolic_Traceback return a list of addresses expressed as "0x..."
---  separated by line feed.
-
-with Ada.Exceptions;
-
-package GNAT.Traceback.Symbolic is
-   pragma Elaborate_Body;
-
-   function Symbolic_Traceback (Traceback : Tracebacks_Array) return String;
-   --  Build a string containing a symbolic traceback of the given call chain.
-   --  Note: This procedure may be installed by Set_Trace_Decorator, to get a
-   --  symbolic traceback on all exceptions raised (see GNAT.Exception_Traces).
-
-   function Symbolic_Traceback
-     (E : Ada.Exceptions.Exception_Occurrence) return String;
-   --  Build string containing symbolic traceback of given exception occurrence
-
-end GNAT.Traceback.Symbolic;
+with System.Traceback.Symbolic;
+package GNAT.Traceback.Symbolic renames System.Traceback.Symbolic;
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 65fec71..315a21d 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1938,6 +1938,11 @@ package body Inline is
          --  Return True if some enclosing body contains instantiations that
          --  appear before the corresponding generic body.
 
+         function Has_Single_Return_In_GNATprove_Mode return Boolean;
+         --  This function is called only in GNATprove mode, and it returns
+         --  True if the subprogram has no or a single return statement as
+         --  last statement.
+
          function Returns_Compile_Time_Constant (N : Node_Id) return Boolean;
          --  Return True if all the return statements of the function body N
          --  are simple return statements and return a compile time constant
@@ -1999,18 +2004,48 @@ package body Inline is
          begin
             D := First (Decls);
             while Present (D) loop
-               if (Nkind (D) = N_Function_Instantiation
-                    and then not Is_Unchecked_Conversion (D))
-                 or else Nkind_In (D, N_Protected_Type_Declaration,
-                                   N_Package_Declaration,
-                                   N_Package_Instantiation,
-                                   N_Subprogram_Body,
-                                   N_Procedure_Instantiation,
-                                   N_Task_Type_Declaration)
+               if Nkind (D) = N_Function_Instantiation
+                 and then not Is_Unchecked_Conversion (D)
                then
                   Cannot_Inline
-                    ("cannot inline & (non-allowed declaration)?", D, Subp);
+                    ("cannot inline & (nested function instantiation)?",
+                     D, Subp);
+                  return True;
+
+               elsif Nkind (D) = N_Protected_Type_Declaration then
+                  Cannot_Inline
+                    ("cannot inline & (nested protected type declaration)?",
+                     D, Subp);
+                  return True;
+
+               elsif Nkind (D) = N_Package_Declaration then
+                  Cannot_Inline
+                    ("cannot inline & (nested package declaration)?",
+                     D, Subp);
+                  return True;
 
+               elsif Nkind (D) = N_Package_Instantiation then
+                  Cannot_Inline
+                    ("cannot inline & (nested package instantiation)?",
+                     D, Subp);
+                  return True;
+
+               elsif Nkind (D) = N_Subprogram_Body then
+                  Cannot_Inline
+                    ("cannot inline & (nested subprogram)?",
+                     D, Subp);
+                  return True;
+
+               elsif Nkind (D) = N_Procedure_Instantiation then
+                  Cannot_Inline
+                    ("cannot inline & (nested procedure instantiation)?",
+                     D, Subp);
+                  return True;
+
+               elsif Nkind (D) = N_Task_Type_Declaration then
+                  Cannot_Inline
+                    ("cannot inline & (nested task type declaration)?",
+                     D, Subp);
                   return True;
                end if;
 
@@ -2158,6 +2193,58 @@ package body Inline is
             return False;
          end Has_Pending_Instantiation;
 
+         -----------------------------------------
+         -- Has_Single_Return_In_GNATprove_Mode --
+         -----------------------------------------
+
+         function Has_Single_Return_In_GNATprove_Mode return Boolean is
+            Last_Statement : Node_Id := Empty;
+
+            function Check_Return (N : Node_Id) return Traverse_Result;
+            --  Returns OK on node N if this is not a return statement
+            --  different from the last statement in the subprogram.
+
+            ------------------
+            -- Check_Return --
+            ------------------
+
+            function Check_Return (N : Node_Id) return Traverse_Result is
+            begin
+               if Nkind_In (N, N_Simple_Return_Statement,
+                            N_Extended_Return_Statement)
+               then
+                  if N = Last_Statement then
+                     return OK;
+                  else
+                     return Abandon;
+                  end if;
+
+               else
+                  return OK;
+               end if;
+            end Check_Return;
+
+            function Check_All_Returns is new Traverse_Func (Check_Return);
+
+         --  Start of processing for Has_Single_Return_In_GNATprove_Mode
+
+         begin
+            --  Retrieve last statement inside possible block statements
+
+            Last_Statement :=
+              Last (Statements (Handled_Statement_Sequence (N)));
+
+            while Nkind (Last_Statement) = N_Block_Statement loop
+               Last_Statement := Last
+                 (Statements (Handled_Statement_Sequence (Last_Statement)));
+            end loop;
+
+            --  Check that the last statement is the only possible return
+            --  statement in the subprogram.
+
+            return Check_All_Returns (N) = OK;
+         end Has_Single_Return_In_GNATprove_Mode;
+
          ------------------------------------
          --  Returns_Compile_Time_Constant --
          ------------------------------------
@@ -2356,6 +2443,16 @@ package body Inline is
          elsif Present (Body_To_Inline (Decl)) then
             return False;
 
+         --  Subprograms that have return statements in the middle of the
+         --  body are inlined with gotos. GNATprove does not currently
+         --  support gotos, so we prevent such inlining.
+
+         elsif GNATprove_Mode
+           and then not Has_Single_Return_In_GNATprove_Mode
+         then
+            Cannot_Inline ("cannot inline & (multiple returns)?", N, Subp);
+            return False;
+
          --  No action needed if the subprogram does not fulfill the minimum
          --  conditions to be inlined by the frontend
 
@@ -2396,7 +2493,8 @@ package body Inline is
          --  on inlining (forbidden declarations, handlers, etc).
 
          if Front_End_Inlining
-           and then not Has_Pragma_Inline_Always (Subp)
+           and then
+             not (Has_Pragma_Inline_Always (Subp) or else GNATprove_Mode)
            and then Stat_Count > Max_Size
          then
             Cannot_Inline ("cannot inline& (body too large)?", N, Subp);
diff --git a/gcc/ada/s-exctra.adb b/gcc/ada/s-exctra.adb
new file mode 100644
index 0000000..234b726
--- /dev/null
+++ b/gcc/ada/s-exctra.adb
@@ -0,0 +1,117 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT RUN-TIME COMPONENTS                         --
+--                                                                          --
+--                S Y S T E M . E X C E P T I O N _ T R A C E S             --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--                     Copyright (C) 2000-2014, AdaCore                     --
+--                                                                          --
+-- 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- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+with System.Standard_Library; use System.Standard_Library;
+with System.Soft_Links;       use System.Soft_Links;
+
+package body System.Exception_Traces is
+
+   --  Calling the decorator directly from where it is needed would require
+   --  introducing nasty dependencies upon the spec of this package (typically
+   --  in a-except.adb). We also have to deal with the fact that the traceback
+   --  array within an exception occurrence and the one the decorator shall
+   --  accept are of different types. These are two reasons for which a wrapper
+   --  with a System.Address argument is indeed used to call the decorator
+   --  provided by the user of this package. This wrapper is called via a
+   --  soft-link, which either is null when no decorator is in place or "points
+   --  to" the following function otherwise.
+
+   function Decorator_Wrapper
+     (Traceback : System.Address;
+      Len       : Natural) return String;
+   --  The wrapper to be called when a decorator is in place for exception
+   --  backtraces.
+   --
+   --  Traceback is the address of the call chain array as stored in the
+   --  exception occurrence and Len is the number of significant addresses
+   --  contained in this array.
+
+   Current_Decorator : Traceback_Decorator := null;
+   --  The decorator to be called by the wrapper when it is not null, as set
+   --  by Set_Trace_Decorator. When this access is null, the wrapper is null
+   --  also and shall then not be called.
+
+   -----------------------
+   -- Decorator_Wrapper --
+   -----------------------
+
+   function Decorator_Wrapper
+     (Traceback : System.Address;
+      Len       : Natural) return String
+   is
+      Decorator_Traceback : Traceback_Entries.Tracebacks_Array (1 .. Len);
+      for Decorator_Traceback'Address use Traceback;
+
+      --  Handle the "transition" from the array stored in the exception
+      --  occurrence to the array expected by the decorator.
+
+      pragma Import (Ada, Decorator_Traceback);
+
+   begin
+      return Current_Decorator.all (Decorator_Traceback);
+   end Decorator_Wrapper;
+
+   -------------------------
+   -- Set_Trace_Decorator --
+   -------------------------
+
+   procedure Set_Trace_Decorator (Decorator : Traceback_Decorator) is
+   begin
+      Current_Decorator := Decorator;
+      Traceback_Decorator_Wrapper :=
+        (if Current_Decorator /= null
+         then Decorator_Wrapper'Access else null);
+   end Set_Trace_Decorator;
+
+   ---------------
+   -- Trace_Off --
+   ---------------
+
+   procedure Trace_Off is
+   begin
+      Exception_Trace := RM_Convention;
+   end Trace_Off;
+
+   --------------
+   -- Trace_On --
+   --------------
+
+   procedure Trace_On (Kind : Trace_Kind) is
+   begin
+      case Kind is
+         when Every_Raise =>
+            Exception_Trace := Every_Raise;
+         when Unhandled_Raise =>
+            Exception_Trace := Unhandled_Raise;
+      end case;
+   end Trace_On;
+
+end System.Exception_Traces;
diff --git a/gcc/ada/s-exctra.ads b/gcc/ada/s-exctra.ads
new file mode 100644
index 0000000..956f531
--- /dev/null
+++ b/gcc/ada/s-exctra.ads
@@ -0,0 +1,96 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT RUN-TIME COMPONENTS                         --
+--                                                                          --
+--                S Y S T E M . E X C E P T I O N _ T R A C E S             --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--                     Copyright (C) 2000-2014, AdaCore                     --
+--                                                                          --
+-- 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- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package provides an interface allowing to control *automatic* output
+--  to standard error upon exception occurrences (as opposed to explicit
+--  generation of traceback information using System.Traceback).
+
+--  This output includes the basic information associated with the exception
+--  (name, message) as well as a backtrace of the call chain at the point
+--  where the exception occurred. This backtrace is only output if the call
+--  chain information is available, depending if the binder switch dedicated
+--  to that purpose has been used or not.
+
+--  The default backtrace is in the form of absolute code locations which may
+--  be converted to corresponding source locations using the addr2line utility
+--  or from within GDB. Please refer to System.Traceback for information about
+--  what is necessary to be able to exploit this possibility.
+
+--  The backtrace output can also be customized by way of a "decorator" which
+--  may return any string output in association with a provided call chain.
+--  The decorator replaces the default backtrace mentioned above.
+
+with System.Traceback_Entries;
+
+package System.Exception_Traces is
+
+   --  The following defines the exact situations in which raises will
+   --  cause automatic output of trace information.
+
+   type Trace_Kind is
+     (Every_Raise,
+      --  Denotes the initial raise event for any exception occurrence, either
+      --  explicit or due to a specific language rule, within the context of a
+      --  task or not.
+
+      Unhandled_Raise
+      --  Denotes the raise events corresponding to exceptions for which there
+      --  is no user defined handler, in particular, when a task dies due to an
+      --  unhandled exception.
+     );
+
+   --  The following procedures can be used to activate and deactivate
+   --  traces identified by the above trace kind values.
+
+   procedure Trace_On (Kind : Trace_Kind);
+   --  Activate the traces denoted by Kind
+
+   procedure Trace_Off;
+   --  Stop the tracing requested by the last call to Trace_On.
+   --  Has no effect if no such call has ever occurred.
+
+   --  The following provide the backtrace decorating facilities
+
+   type Traceback_Decorator is access
+     function (Traceback : Traceback_Entries.Tracebacks_Array) return String;
+   --  A backtrace decorator is a function which returns the string to be
+   --  output for a call chain provided by way of a tracebacks array.
+
+   procedure Set_Trace_Decorator (Decorator : Traceback_Decorator);
+   --  Set the decorator to be used for future automatic outputs. Restore
+   --  the default behavior (output of raw addresses) if the provided
+   --  access value is null.
+   --
+   --  Note: System.Traceback.Symbolic.Symbolic_Traceback may be used as the
+   --  Decorator, to get a symbolic traceback. This will cause a significant
+   --  cpu and memory overhead.
+
+end System.Exception_Traces;
diff --git a/gcc/ada/s-trasym.adb b/gcc/ada/s-trasym.adb
new file mode 100644
index 0000000..ad55887
--- /dev/null
+++ b/gcc/ada/s-trasym.adb
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT RUN-TIME COMPONENTS                         --
+--                                                                          --
+--           S Y S T E M . T R A C E B A C K . S Y M B O L I C              --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--                     Copyright (C) 1999-2014, AdaCore                     --
+--                                                                          --
+-- 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- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This is the default implementation for platforms where the full capability
+--  is not supported. It returns tracebacks as lists of LF separated strings of
+--  the form "0x..." corresponding to the addresses.
+
+with Ada.Exceptions.Traceback; use Ada.Exceptions.Traceback;
+with System.Address_Image;
+
+package body System.Traceback.Symbolic is
+
+   ------------------------
+   -- Symbolic_Traceback --
+   ------------------------
+
+   function Symbolic_Traceback
+     (Traceback : System.Traceback_Entries.Tracebacks_Array) return String
+   is
+   begin
+      if Traceback'Length = 0 then
+         return "";
+
+      else
+         declare
+            Img : String := System.Address_Image (Traceback (Traceback'First));
+
+            Result : String (1 .. (Img'Length + 3) * Traceback'Length);
+            Last   : Natural := 0;
+
+         begin
+            for J in Traceback'Range loop
+               Img := System.Address_Image (Traceback (J));
+               Result (Last + 1 .. Last + 2) := "0x";
+               Last := Last + 2;
+               Result (Last + 1 .. Last + Img'Length) := Img;
+               Last := Last + Img'Length + 1;
+               Result (Last) := ASCII.LF;
+            end loop;
+
+            return Result (1 .. Last);
+         end;
+      end if;
+   end Symbolic_Traceback;
+
+   function Symbolic_Traceback
+     (E : Ada.Exceptions.Exception_Occurrence) return String
+   is
+   begin
+      return Symbolic_Traceback (Ada.Exceptions.Traceback.Tracebacks (E));
+   end Symbolic_Traceback;
+
+end System.Traceback.Symbolic;
diff --git a/gcc/ada/s-trasym.ads b/gcc/ada/s-trasym.ads
new file mode 100644
index 0000000..ea0b46b
--- /dev/null
+++ b/gcc/ada/s-trasym.ads
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT RUN-TIME COMPONENTS                         --
+--                                                                          --
+--           S Y S T E M . T R A C E B A C K . S Y M B O L I C              --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--                     Copyright (C) 1999-2014, AdaCore                     --
+--                                                                          --
+-- 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- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  Run-time symbolic traceback support
+
+--  The routines provided in this package assume that your application has
+--  been compiled with debugging information turned on, since this information
+--  is used to build a symbolic traceback.
+
+--  If you want to retrieve tracebacks from exception occurrences, it is also
+--  necessary to invoke the binder with -E switch. Please refer to the gnatbind
+--  documentation for more information.
+
+--  Note that it is also possible (and often recommended) to compute symbolic
+--  traceback outside the program execution, which in addition allows you
+--  to distribute the executable with no debug info:
+--
+--  - build your executable with debug info
+--  - archive this executable
+--  - strip a copy of the executable and distribute/deploy this version
+--  - at run time, compute absolute traceback (-bargs -E) from your
+--    executable and log it using Ada.Exceptions.Exception_Information
+--  - off line, compute the symbolic traceback using the executable archived
+--    with debug info and addr2line or gdb (using info line *<addr>) on the
+--    absolute addresses logged by your application.
+
+--  In order to retrieve symbolic information, functions in this package will
+--  read on disk all the debug information of the executable file (found via
+--  Argument (0), and looked in the PATH if needed) or shared libraries using
+--  OS facilities, and load them in memory, causing a significant cpu and
+--  memory overhead.
+
+--  On platforms where the full capability is not supported, function
+--  Symbolic_Traceback return a list of addresses expressed as "0x..."
+--  separated by line feed.
+
+with Ada.Exceptions;
+
+package System.Traceback.Symbolic is
+   pragma Elaborate_Body;
+
+   function Symbolic_Traceback
+     (Traceback : System.Traceback_Entries.Tracebacks_Array) return String;
+   --  Build a string containing a symbolic traceback of the given call chain.
+   --  Note: This procedure may be installed by Set_Trace_Decorator, to get a
+   --  symbolic traceback on all exceptions raised (see
+   --  System.Exception_Traces).
+
+   function Symbolic_Traceback
+     (E : Ada.Exceptions.Exception_Occurrence) return String;
+   --  Build string containing symbolic traceback of given exception occurrence
+
+end System.Traceback.Symbolic;