[multiple changes]

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

	* g-forstr.adb: Minor code reorganization (use J rather than I
	as a variable name).
	* gnat_rm.texi, sem_prag.adb, sem_util.adb, sem_ch13.adb,
	g-forstr.ads: Minor reformatting.

2014-07-30  Eric Botcazou  <ebotcazou@adacore.com>

	* sprint.adb (Set_Debug_Sloc): Also reset the end location if
	we are debugging the generated code.

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

	* sinput.ads, sinput.adb (Comes_From_Inlined_Body): New function that
	returns True for source pointer for an inlined body.

2014-07-30  Javier Miranda  <miranda@adacore.com>

	* exp_ch4.adb (Apply_Accessibility_Check): Add
	missing calls to Base_Address().

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

	* sem_ch6.adb (Hanalyze_Subprogram_Body_Helper): In GNATprove
	mode, subprogram bodies without a previous declaration are also
	candidates for front-end inlining.

From-SVN: r213242

12 files changed, 254 insertions, 119 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 18caba4..4721dc8 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,31 @@
+2014-07-30  Robert Dewar  <dewar@adacore.com>
+
+	* g-forstr.adb: Minor code reorganization (use J rather than I
+	as a variable name).
+	* gnat_rm.texi, sem_prag.adb, sem_util.adb, sem_ch13.adb,
+	g-forstr.ads: Minor reformatting.
+
+2014-07-30  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* sprint.adb (Set_Debug_Sloc): Also reset the end location if
+	we are debugging the generated code.
+
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* sinput.ads, sinput.adb (Comes_From_Inlined_Body): New function that
+	returns True for source pointer for an inlined body.
+
+2014-07-30  Javier Miranda  <miranda@adacore.com>
+
+	* exp_ch4.adb (Apply_Accessibility_Check): Add
+	missing calls to Base_Address().
+
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Hanalyze_Subprogram_Body_Helper): In GNATprove
+	mode, subprogram bodies without a previous declaration are also
+	candidates for front-end inlining.
+
 2014-07-30  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* aspects.ads Aspects Async_Readers, Async_Writers,
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 1712a7d..10cf558 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -758,6 +758,25 @@ package body Exp_Ch4 is
                Obj_Ref := New_Occurrence_Of (Ref, Loc);
             end if;
 
+            --  For access to interface types we must generate code to displace
+            --  the pointer to the base of the object since the subsequent code
+            --  references components located in the TSD of the object (which
+            --  is associated with the primary dispatch table --see a-tags.ads)
+            --  and also generates code invoking Free, which requires also a
+            --  reference to the base of the unallocated object.
+
+            if Is_Interface (DesigT) then
+               Obj_Ref :=
+                 Unchecked_Convert_To (Etype (Obj_Ref),
+                   Make_Function_Call (Loc,
+                     Name =>
+                       New_Occurrence_Of
+                         (RTE (RE_Base_Address), Loc),
+                     Parameter_Associations => New_List (
+                       Unchecked_Convert_To (RTE (RE_Address),
+                         New_Copy_Tree (Obj_Ref)))));
+            end if;
+
             --  Step 1: Create the object clean up code
 
             Stmts := New_List;
@@ -831,26 +850,13 @@ package body Exp_Ch4 is
 
             --  Step 2: Create the accessibility comparison
 
-            --  Reference the tag: for a renaming of an access to an interface
-            --  object Obj_Ref already references the tag of the secondary
-            --  dispatch table.
-
-            if Nkind (Obj_Ref) in N_Has_Entity
-              and then Present (Entity (Obj_Ref))
-              and then Present (Renamed_Object (Entity (Obj_Ref)))
-              and then Is_Interface (DesigT)
-            then
-               null;
-
             --  Generate:
             --    Ref'Tag
 
-            else
-               Obj_Ref :=
-                 Make_Attribute_Reference (Loc,
-                   Prefix         => Obj_Ref,
-                   Attribute_Name => Name_Tag);
-            end if;
+            Obj_Ref :=
+              Make_Attribute_Reference (Loc,
+                Prefix         => Obj_Ref,
+                Attribute_Name => Name_Tag);
 
             --  For tagged types, determine the accessibility level by looking
             --  at the type specific data of the dispatch table. Generate:
diff --git a/gcc/ada/g-forstr.adb b/gcc/ada/g-forstr.adb
index bcb0fff..a6ebc91 100644
--- a/gcc/ada/g-forstr.adb
+++ b/gcc/ada/g-forstr.adb
@@ -64,7 +64,7 @@ package body GNAT.Formatted_String is
 
    type F_Base is (None, C_Style, Ada_Style) with Default_Value => None;
 
-   Unset    : constant Integer := -1;
+   Unset : constant Integer := -1;
 
    type F_Data is record
       Kind         : F_Kind;
@@ -78,12 +78,16 @@ package body GNAT.Formatted_String is
    end record;
 
    procedure Next_Format
-     (Format : Formatted_String; F_Spec : out F_Data; Start : out Positive);
+     (Format : Formatted_String;
+      F_Spec : out F_Data;
+      Start  : out Positive);
    --  Parse the next format specifier, a format specifier has the following
    --  syntax: %[flags][width][.precision][length]specifier
 
    function Get_Formatted
-     (F_Spec : F_Data; Value : String; Len : Positive) return String;
+     (F_Spec : F_Data;
+      Value  : String;
+      Len    : Positive) return String;
    --  Returns Value formatted given the information in F_Spec
 
    procedure Raise_Wrong_Format (Format : Formatted_String) with No_Return;
@@ -98,7 +102,8 @@ package body GNAT.Formatted_String is
          Aft  : Text_IO.Field;
          Exp  : Text_IO.Field);
    function P_Flt_Format
-     (Format : Formatted_String; Var : Flt) return Formatted_String;
+     (Format : Formatted_String;
+      Var    : Flt) return Formatted_String;
    --  Generic routine which handles all floating point numbers
 
    generic
@@ -113,7 +118,8 @@ package body GNAT.Formatted_String is
          Item : Int;
          Base : Text_IO.Number_Base);
    function P_Int_Format
-     (Format : Formatted_String; Var : Int) return Formatted_String;
+     (Format : Formatted_String;
+      Var    : Int) return Formatted_String;
    --  Generic routine which handles all the integer numbers
 
    ---------
@@ -134,24 +140,25 @@ package body GNAT.Formatted_String is
 
    function "-" (Format : Formatted_String) return String is
       F : String renames Format.D.Format;
-      I : Natural renames Format.D.Index;
+      J : Natural renames Format.D.Index;
       R : Unbounded_String := Format.D.Result;
+
    begin
       --  Make sure we get the remaining character up to the next unhandled
       --  format specifier.
 
-      while (I <= F'Length and then F (I) /= '%')
-        or else (I < F'Length - 1 and then F (I + 1) = '%')
+      while (J <= F'Length and then F (J) /= '%')
+        or else (J < F'Length - 1 and then F (J + 1) = '%')
       loop
-         Append (R, F (I));
+         Append (R, F (J));
 
          --  If we have two consecutive %, skip the second one
 
-         if F (I) = '%' and then I < F'Length - 1 and then F (I + 1) = '%' then
-            I := I + 1;
+         if F (J) = '%' and then J < F'Length - 1 and then F (J + 1) = '%' then
+            J := J + 1;
          end if;
 
-         I := I + 1;
+         J := J + 1;
       end loop;
 
       return To_String (R);
@@ -167,6 +174,7 @@ package body GNAT.Formatted_String is
    is
       F     : F_Data;
       Start : Positive;
+
    begin
       Next_Format (Format, F, Start);
 
@@ -190,6 +198,7 @@ package body GNAT.Formatted_String is
    is
       F     : F_Data;
       Start : Positive;
+
    begin
       Next_Format (Format, F, Start);
 
@@ -282,6 +291,7 @@ package body GNAT.Formatted_String is
       A_Img : constant String := System.Address_Image (Var);
       F     : F_Data;
       Start : Positive;
+
    begin
       Next_Format (Format, F, Start);
 
@@ -337,11 +347,11 @@ package body GNAT.Formatted_String is
    --------------
 
    overriding procedure Finalize (F : in out Formatted_String) is
-
       procedure Unchecked_Free is
         new Unchecked_Deallocation (Data, Data_Access);
 
       D : Data_Access := F.D;
+
    begin
       F.D := null;
 
@@ -391,8 +401,9 @@ package body GNAT.Formatted_String is
 
       Res : Unbounded_String;
       S   : Positive := Value'First;
+
    begin
-      --  Let's hanfles the flags
+      --  Handle the flags
 
       if F_Spec.Kind in Is_Number then
          if F_Spec.Sign = Forced and then Value (Value'First) /= '-' then
@@ -442,10 +453,14 @@ package body GNAT.Formatted_String is
      (Format : Formatted_String;
       Var    : Int) return Formatted_String
    is
-      function Sign (Var : Int) return Sign_Kind
-      is (if Var < 0 then Neg elsif Var = 0 then Zero else Pos);
-      function To_Integer (Var : Int) return Integer is (Integer (Var));
+      function Sign (Var : Int) return Sign_Kind is
+        (if Var < 0 then Neg elsif Var = 0 then Zero else Pos);
+
+      function To_Integer (Var : Int) return Integer is
+        (Integer (Var));
+
       function Int_Format is new P_Int_Format (Int, To_Integer, Sign, Put);
+
    begin
       return Int_Format (Format, Var);
    end Int_Format;
@@ -458,10 +473,14 @@ package body GNAT.Formatted_String is
      (Format : Formatted_String;
       Var    : Int) return Formatted_String
    is
-      function Sign (Var : Int) return Sign_Kind
-        is (if Var < 0 then Neg elsif Var = 0 then Zero else Pos);
-      function To_Integer (Var : Int) return Integer is (Integer (Var));
+      function Sign (Var : Int) return Sign_Kind is
+        (if Var < 0 then Neg elsif Var = 0 then Zero else Pos);
+
+      function To_Integer (Var : Int) return Integer is
+        (Integer (Var));
+
       function Int_Format is new P_Int_Format (Int, To_Integer, Sign, Put);
+
    begin
       return Int_Format (Format, Var);
    end Mod_Format;
@@ -475,111 +494,119 @@ package body GNAT.Formatted_String is
       F_Spec : out F_Data;
       Start  : out Positive)
    is
-      F              : String renames Format.D.Format;
-      I              : Natural renames Format.D.Index;
+      F              : String  renames Format.D.Format;
+      J              : Natural renames Format.D.Index;
       S              : Natural;
       Width_From_Var : Boolean := False;
+
    begin
       Format.D.Current := Format.D.Current + 1;
       F_Spec.Value_Needed := 0;
 
       --  Got to next %
 
-      while (I <= F'Last and then F (I) /= '%')
-        or else (I < F'Last - 1 and then F (I + 1) = '%')
+      while (J <= F'Last and then F (J) /= '%')
+        or else (J < F'Last - 1 and then F (J + 1) = '%')
       loop
-         Append (Format.D.Result, F (I));
+         Append (Format.D.Result, F (J));
 
          --  If we have two consecutive %, skip the second one
 
-         if F (I) = '%' and then I < F'Last - 1 and then F (I + 1) = '%' then
-            I := I + 1;
+         if F (J) = '%' and then J < F'Last - 1 and then F (J + 1) = '%' then
+            J := J + 1;
          end if;
 
-         I := I + 1;
+         J := J + 1;
       end loop;
 
-      if F (I) /= '%' or else I = F'Last then
+      if F (J) /= '%' or else J = F'Last then
          raise Format_Error with "no format specifier found for parameter"
            & Positive'Image (Format.D.Current);
       end if;
 
-      Start := I;
+      Start := J;
 
-      I := I + 1;
+      J := J + 1;
 
       --  Check for any flags
 
-      Flags_Check : while I < F'Last loop
-         if F (I) = '-' then
+      Flags_Check : while J < F'Last loop
+         if F (J) = '-' then
             F_Spec.Left_Justify := True;
-         elsif F (I) = '+' then
-            F_Spec.Sign := Forced;
-         elsif F (I) = ' ' then
-            F_Spec.Sign := Space;
-         elsif F (I) = '#' then
-            F_Spec.Base := C_Style;
-         elsif F (I) = '~' then
-            F_Spec.Base := Ada_Style;
-         elsif F (I) = '0' then
-            F_Spec.Zero_Pad := True;
+         elsif F (J) = '+' then
+            F_Spec.Sign         := Forced;
+         elsif F (J) = ' ' then
+            F_Spec.Sign         := Space;
+         elsif F (J) = '#' then
+            F_Spec.Base         := C_Style;
+         elsif F (J) = '~' then
+            F_Spec.Base         := Ada_Style;
+         elsif F (J) = '0' then
+            F_Spec.Zero_Pad     := True;
          else
             exit Flags_Check;
          end if;
 
-         I := I + 1;
+         J := J + 1;
       end loop Flags_Check;
 
       --  Check width if any
 
-      if F (I) in '0' .. '9' then
+      if F (J) in '0' .. '9' then
+
          --  We have a width parameter
 
-         S := I;
+         S := J;
 
-         while I < F'Last and then F (I + 1) in '0' .. '9' loop
-            I := I + 1;
+         while J < F'Last and then F (J + 1) in '0' .. '9' loop
+            J := J + 1;
          end loop;
 
-         F_Spec.Width := Natural'Value (F (S .. I));
+         F_Spec.Width := Natural'Value (F (S .. J));
+
+         J := J + 1;
 
-         I := I + 1;
+      elsif F (J) = '*' then
 
-      elsif F (I) = '*' then
          --  The width will be taken from the integer parameter
 
          F_Spec.Value_Needed := 1;
          Width_From_Var := True;
 
-         I := I + 1;
+         J := J + 1;
       end if;
 
-      if F (I) = '.' then
+      if F (J) = '.' then
+
          --  We have a precision parameter
 
-         I := I + 1;
+         J := J + 1;
 
-         if F (I) in '0' .. '9' then
-            S := I;
+         if F (J) in '0' .. '9' then
+            S := J;
 
-            while I < F'Length and then F (I + 1) in '0' .. '9' loop
-               I := I + 1;
+            while J < F'Length and then F (J + 1) in '0' .. '9' loop
+               J := J + 1;
             end loop;
 
-            if F (I) = '.' then
+            if F (J) = '.' then
+
                --  No precision, 0 is assumed
+
                F_Spec.Precision := 0;
+
             else
-               F_Spec.Precision := Natural'Value (F (S .. I));
+               F_Spec.Precision := Natural'Value (F (S .. J));
             end if;
 
-            I := I + 1;
+            J := J + 1;
+
+         elsif F (J) = '*' then
 
-         elsif F (I) = '*' then
             --  The prevision will be taken from the integer parameter
 
             F_Spec.Value_Needed := F_Spec.Value_Needed + 1;
-            I := I + 1;
+            J := J + 1;
          end if;
       end if;
 
@@ -587,19 +614,19 @@ package body GNAT.Formatted_String is
       --  but yet for compatibility reason it is handled.
 
       Length_Check :
-      while I <= F'Last
-        and then F (I) in 'h' | 'l' | 'j' | 'z' | 't' | 'L'
+      while J <= F'Last
+        and then F (J) in 'h' | 'l' | 'j' | 'z' | 't' | 'L'
       loop
-         I := I + 1;
+         J := J + 1;
       end loop Length_Check;
 
-      if I > F'Last then
+      if J > F'Last then
          Raise_Wrong_Format (Format);
       end if;
 
       --  Read next character which should be the expected type
 
-      case F (I) is
+      case F (J) is
          when 'c'       => F_Spec.Kind := Char;
          when 's'       => F_Spec.Kind := Str;
          when 'd' | 'i' => F_Spec.Kind := Decimal_Int;
@@ -618,7 +645,7 @@ package body GNAT.Formatted_String is
               & Positive'Image (Format.D.Current);
       end case;
 
-      I := I + 1;
+      J := J + 1;
 
       if F_Spec.Value_Needed > 0
         and then F_Spec.Value_Needed = Format.D.Stored_Value
@@ -650,6 +677,7 @@ package body GNAT.Formatted_String is
       S, E   : Positive := 1;
       Start  : Positive;
       Aft    : Text_IO.Field;
+
    begin
       Next_Format (Format, F, Start);
 
@@ -682,6 +710,7 @@ package body GNAT.Formatted_String is
             end if;
 
          when Shortest_Decimal_Float | Shortest_Decimal_Float_Up =>
+
             --  Without exponent
 
             Put (Buffer, Var, Aft, Exp => 0);
@@ -693,6 +722,7 @@ package body GNAT.Formatted_String is
             declare
                Buffer2 : String (1 .. 50);
                S2, E2  : Positive;
+
             begin
                Put (Buffer2, Var, Aft, Exp => 3);
                S2 := Strings.Fixed.Index_Non_Blank (Buffer2);
@@ -717,7 +747,7 @@ package body GNAT.Formatted_String is
       end case;
 
       Append (Format.D.Result,
-              Get_Formatted (F, Buffer (S .. E), Buffer (S .. E)'Length));
+        Get_Formatted (F, Buffer (S .. E), Buffer (S .. E)'Length));
 
       return Format;
    end P_Flt_Format;
@@ -730,7 +760,6 @@ package body GNAT.Formatted_String is
      (Format : Formatted_String;
       Var    : Int) return Formatted_String
    is
-
       function Handle_Precision return Boolean;
       --  Return True if nothing else to do
 
@@ -761,6 +790,8 @@ package body GNAT.Formatted_String is
          return False;
       end Handle_Precision;
 
+   --  Start of processing for P_Int_Format
+
    begin
       Next_Format (Format, F, Start);
 
@@ -868,8 +899,7 @@ package body GNAT.Formatted_String is
       --  Then add base if needed
 
       declare
-         N : String :=
-               Get_Formatted (F, Buffer (S .. E), E - S + 1 + Len);
+         N : String := Get_Formatted (F, Buffer (S .. E), E - S + 1 + Len);
          P : constant Positive :=
                (if F.Left_Justify
                 then N'First
@@ -915,9 +945,8 @@ package body GNAT.Formatted_String is
                      N (N'First .. N'First + 1) := "8#";
                      N (N'Last) := '#';
 
-                  when Unsigned_Hexadecimal_Int
-                    | Unsigned_Hexadecimal_Int_Up
-                    =>
+                  when Unsigned_Hexadecimal_Int    |
+                       Unsigned_Hexadecimal_Int_Up =>
                      if F.Left_Justify then
                         N (N'First + 3 .. N'Last) := N (N'First .. N'Last - 3);
                      else
@@ -944,7 +973,8 @@ package body GNAT.Formatted_String is
 
    procedure Raise_Wrong_Format (Format : Formatted_String) is
    begin
-      raise Format_Error with "wrong format specified for parameter"
+      raise Format_Error with
+        "wrong format specified for parameter"
         & Positive'Image (Format.D.Current);
    end Raise_Wrong_Format;
 
diff --git a/gcc/ada/g-forstr.ads b/gcc/ada/g-forstr.ads
index c0e0049..94c295c 100644
--- a/gcc/ada/g-forstr.ads
+++ b/gcc/ada/g-forstr.ads
@@ -30,9 +30,9 @@
 ------------------------------------------------------------------------------
 
 --  This package add support for formatted string as supported by C printf().
---
+
 --  A simple usage is:
---
+
 --     declare
 --        F : Formatted_String := +"['%c' ; %10d]";
 --        C : Character := 'v';
@@ -40,16 +40,14 @@
 --     begin
 --        F := F & C & I;
 --        Put_Line (-F);
---
 --     end;
---
+
 --  Which will display:
---
+
 --     ['v' ;         98]
---
---
+
 --  Each format specifier is: %[flags][width][.precision][length]specifier
---
+
 --  Specifiers:
 --    d or i    Signed decimal integer
 --    u         Unsigned decimal integer
@@ -66,29 +64,37 @@
 --    s         String of characters
 --    p         Pointer address
 --    %         A % followed by another % character will write a single %
---
+
 --  Flags:
+
 --    -         Left-justify within the given field width;
---              Right justification is the default
+--              Right justification is the default.
+
 --    +         Forces to preceed the result with a plus or minus sign (+ or -)
 --              even for positive numbers. By default, only negative numbers
 --              are preceded with a - sign.
+
 --    (space)   If no sign is going to be written, a blank space is inserted
 --              before the value.
+
 --    #         Used with o, x or X specifiers the value is preceeded with
 --              0, 0x or 0X respectively for values different than zero.
 --              Used with a, A, e, E, f, F, g or G it forces the written
 --              output to contain a decimal point even if no more digits
 --              follow. By default, if no digits follow, no decimal point is
 --              written.
+
 --    ~         As above, but using Ada style based <base>#<number>#
+
 --    0         Left-pads the number with zeroes (0) instead of spaces when
 --              padding is specified.
+
 --  Width:
 --    number    Minimum number of characters to be printed. If the value to
 --              be printed is shorter than this number, the result is padded
 --              with blank spaces. The value is not truncated even if the
 --              result is larger.
+
 --    *         The width is not specified in the format string, but as an
 --              additional integer value argument preceding the argument that
 --              has to be formatted.
@@ -99,15 +105,19 @@
 --              leading zeros. The value is not truncated even if the result
 --              is longer. A precision of 0 means that no character is written
 --              for the value 0.
+
 --              For e, E, f and F specifiers: this is the number of digits to
 --              be printed after the decimal point (by default, this is 6).
 --              For g and G specifiers: This is the maximum number of
 --              significant digits to be printed.
+
 --              For s: this is the maximum number of characters to be printed.
 --              By default all characters are printed until the ending null
 --              character is encountered.
+
 --              If the period is specified without an explicit value for
 --              precision, 0 is assumed.
+
 --    .*        The precision is not specified in the format string, but as an
 --              additional integer value argument preceding the argument that
 --              has to be formatted.
@@ -119,7 +129,6 @@ private with Ada.Finalization;
 private with Ada.Strings.Unbounded;
 
 package GNAT.Formatted_String is
-
    use Ada;
 
    type Formatted_String (<>) is private;
@@ -249,11 +258,11 @@ package GNAT.Formatted_String is
    generic
       type Enum is (<>);
    function Enum_Format
-     (Format : Formatted_String; Var : Enum) return Formatted_String;
+     (Format : Formatted_String;
+      Var    : Enum) return Formatted_String;
    --  As for String above, output the string representation of the enumeration
 
 private
-
    use Ada.Strings.Unbounded;
 
    type I_Vars is array (Positive range 1 .. 2) of Integer;
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index fa18f8a..4d93d0c 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -19868,7 +19868,7 @@ in this package can be used to reestablish the required mode.
 @cindex Formatted String
 
 @noindent
-Provides support for C/C++ printf() formatted string. The format is
+Provides support for C/C++ printf() formatted strings. The format is
 copied from the printf() routine and should therefore gives identical
 output. Some generic routines are provided to be able to use types
 derived from Integer, Float or enumerations as values for the
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 6a8f336..cb3b105 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -2909,10 +2909,10 @@ package body Sem_Ch13 is
                   --  their pragmas must contain two arguments, the second
                   --  being the optional Boolean expression.
 
-                  if A_Id = Aspect_Async_Readers
-                    or else A_Id = Aspect_Async_Writers
-                    or else A_Id = Aspect_Effective_Reads
-                    or else A_Id = Aspect_Effective_Writes
+                  if A_Id = Aspect_Async_Readers   or else
+                     A_Id = Aspect_Async_Writers   or else
+                     A_Id = Aspect_Effective_Reads or else
+                     A_Id = Aspect_Effective_Writes
                   then
                      declare
                         Args : List_Id;
@@ -2921,9 +2921,10 @@ package body Sem_Ch13 is
                         --  The first argument of the external property pragma
                         --  is the related object.
 
-                        Args := New_List (
-                          Make_Pragma_Argument_Association (Sloc (Ent),
-                            Expression => Ent));
+                        Args :=
+                          New_List (
+                            Make_Pragma_Argument_Association (Sloc (Ent),
+                              Expression => Ent));
 
                         --  The second argument is the optional Boolean
                         --  expression which must be propagated even if it
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 8919a4a..f182051 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2952,6 +2952,42 @@ package body Sem_Ch6 is
                Spec_Id := Disambiguate_Spec;
             else
                Spec_Id := Find_Corresponding_Spec (N);
+
+               --  In GNATprove mode, if the body has no previous spec, create
+               --  one so that the inlining machinery can operate properly.
+               --  Transfer aspects, if any, to the new spec, so that they
+               --  are legal and can be processed ahead of the body.
+               --  We make two copies of the given spec, one for the new
+               --  declaration, and one for the body.
+
+               --  This cannot be done for a compilation unit, which is not
+               --  in a context where we can insert a new spec.
+
+               if No (Spec_Id)
+                 and then GNATprove_Mode
+                 and then Debug_Flag_QQ
+                 and then Full_Analysis
+                 and then Comes_From_Source (Body_Id)
+                 and then Is_List_Member (N)
+               then
+                  declare
+                     Body_Spec : constant Node_Id :=
+                       Copy_Separate_Tree (Specification (N));
+                     New_Decl : constant Node_Id :=
+                       Make_Subprogram_Declaration
+                        (Loc, Copy_Separate_Tree (Specification (N)));
+
+                  begin
+                     Insert_Before (N, New_Decl);
+                     Move_Aspects (From => N, To => New_Decl);
+                     Analyze (New_Decl);
+                     Spec_Id := Defining_Entity (New_Decl);
+
+                     Set_Specification (N, Body_Spec);
+                     Body_Id := Analyze_Subprogram_Specification (Body_Spec);
+                     Set_Corresponding_Spec (N, Spec_Id);
+                  end;
+               end if;
             end if;
 
             --  If this is a duplicate body, no point in analyzing it
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 158304d..714512e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1845,7 +1845,7 @@ package body Sem_Prag is
       --  than a formal subprogram parameter (SPARK RM 7.1.3(2)). The check
       --  is performed at the end of the declarative region due to a possible
       --  out-of-order arrangement of pragmas:
-      --
+
       --    Obj : ...;
       --    pragma Async_Readers (Obj);
       --    pragma Volatile (Obj);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 9395c7b..7043b79 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7698,8 +7698,7 @@ package body Sem_Util is
             or else (Present (Full_View (Etype (Typ)))
                       and then Full_View (Etype (Typ)) = Typ)
 
-            --  Protect the frontend against wrong source with cyclic
-            --  derivations
+            --  Protect frontend against wrong sources with cyclic derivations
 
             or else Etype (Typ) = T;
 
diff --git a/gcc/ada/sinput.adb b/gcc/ada/sinput.adb
index 70d4481..640e277 100644
--- a/gcc/ada/sinput.adb
+++ b/gcc/ada/sinput.adb
@@ -302,6 +302,17 @@ package body Sinput is
       end case;
    end Check_For_BOM;
 
+   -----------------------------
+   -- Comes_From_Inlined_Body --
+   -----------------------------
+
+   function Comes_From_Inlined_Body (S : Source_Ptr) return Boolean is
+      SIE : Source_File_Record renames
+        Source_File.Table (Get_Source_File_Index (S));
+   begin
+      return SIE.Inlined_Body;
+   end Comes_From_Inlined_Body;
+
    -----------------------
    -- Get_Column_Number --
    -----------------------
diff --git a/gcc/ada/sinput.ads b/gcc/ada/sinput.ads
index 899bead..3d36903 100644
--- a/gcc/ada/sinput.ads
+++ b/gcc/ada/sinput.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, 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- --
@@ -638,6 +638,13 @@ package Sinput is
    --  value of the instantiation if this location is within an instance.
    --  If S is not within an instance, then this returns No_Location.
 
+   function Comes_From_Inlined_Body (S : Source_Ptr) return Boolean;
+   pragma Inline (Comes_From_Inlined_Body);
+   --  Given a source pointer S, returns whether it comes from an inlined body.
+   --  This allows distinguishing these source pointers from those that come
+   --  from instantiation of generics, since Instantiation_Location returns a
+   --  valid location in both cases.
+
    function Top_Level_Location (S : Source_Ptr) return Source_Ptr;
    --  Given a source pointer S, returns the argument unchanged if it is
    --  not in an instantiation. If S is in an instantiation, then it returns
diff --git a/gcc/ada/sprint.adb b/gcc/ada/sprint.adb
index 19d3432..98a923a 100644
--- a/gcc/ada/sprint.adb
+++ b/gcc/ada/sprint.adb
@@ -513,6 +513,14 @@ package body Sprint is
    begin
       if Debug_Generated_Code and then Present (Dump_Node) then
          Set_Sloc (Dump_Node, Debug_Sloc + Source_Ptr (Column - 1));
+
+         --  We do not know the actual end location in the generated code and
+         --  it could be much closer than in the source code, so play safe.
+
+         if Nkind_In (Dump_Node, N_Case_Statement, N_If_Statement) then
+            Set_End_Location (Dump_Node, Debug_Sloc + Source_Ptr (Column - 1));
+         end if;
+
          Dump_Node := Empty;
       end if;
    end Set_Debug_Sloc;