[multiple changes]

2014-07-30  Gary Dismukes  <dismukes@adacore.com>

	* exp_prag.adb, a-tags.ads: Minor typo fixes.

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

	* a-excach.adb, a-excach-cert.adb, a-except-2005.ads,
	a-except.ads, g-traceb.adb, memtrack.adb,
	s-traceb.adb, s-traceb.ads, s-traceb-hpux.adb, s-traceb-mastop.adb:
	Cleanup: Make the three versions of System.Traceback.Call_Chain
	have the same interface. Use an array for the Traceback parameter
	instead of an Address.	This will enable reduction in code
	duplication.

2014-07-30  Pat Rogers  <rogers@adacore.com>

	* gnat_ugn.texi: Corrected minor textual error in description
	of switch -gnatwl.

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

	* Makefile.rtl: Sort file names.

2014-07-30  Arnaud Charlet  <charlet@adacore.com>

	* a-tasatt.adb: Complete previous change: kill spurious warning
	on e.g. sparc, and make sure we only use the fast path when the
	alignment is compatible.

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

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Mark new Spec_Id as
	coming from source.

From-SVN: r213275

16 files changed, 156 insertions, 38 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e64b7ba..3ca141d 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,37 @@
+2014-07-30  Gary Dismukes  <dismukes@adacore.com>
+
+	* exp_prag.adb, a-tags.ads: Minor typo fixes.
+
+2014-07-30  Bob Duff  <duff@adacore.com>
+
+	* a-excach.adb, a-excach-cert.adb, a-except-2005.ads,
+	a-except.ads, g-traceb.adb, memtrack.adb,
+	s-traceb.adb, s-traceb.ads, s-traceb-hpux.adb, s-traceb-mastop.adb:
+	Cleanup: Make the three versions of System.Traceback.Call_Chain
+	have the same interface. Use an array for the Traceback parameter
+	instead of an Address.	This will enable reduction in code
+	duplication.
+
+2014-07-30  Pat Rogers  <rogers@adacore.com>
+
+	* gnat_ugn.texi: Corrected minor textual error in description
+	of switch -gnatwl.
+
+2014-07-30  Bob Duff  <duff@adacore.com>
+
+	* Makefile.rtl: Sort file names.
+
+2014-07-30  Arnaud Charlet  <charlet@adacore.com>
+
+	* a-tasatt.adb: Complete previous change: kill spurious warning
+	on e.g. sparc, and make sure we only use the fast path when the
+	alignment is compatible.
+
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Mark new Spec_Id as
+	coming from source.
+
 2014-07-30  Yannick Moy  <moy@adacore.com>
 
 	* inline.adb (Build_Body_To_Inline): Issue more precise messages
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index a959d3c..98b7429 100644
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -99,12 +99,12 @@ GNATRTL_NONTASKING_OBJS= \
   a-calend$(objext) \
   a-calfor$(objext) \
   a-catizo$(objext) \
+  a-cbdlli$(objext) \
   a-cbhama$(objext) \
   a-cbhase$(objext) \
-  a-cborse$(objext) \
-  a-cbdlli$(objext) \
   a-cbmutr$(objext) \
   a-cborma$(objext) \
+  a-cborse$(objext) \
   a-cbprqu$(objext) \
   a-cbsyqu$(objext) \
   a-cdlili$(objext) \
@@ -121,8 +121,8 @@ GNATRTL_NONTASKING_OBJS= \
   a-charac$(objext) \
   a-chlat1$(objext) \
   a-chlat9$(objext) \
-  a-chtgbo$(objext) \
   a-chtgbk$(objext) \
+  a-chtgbo$(objext) \
   a-chtgke$(objext) \
   a-chtgop$(objext) \
   a-chzla1$(objext) \
@@ -130,10 +130,13 @@ GNATRTL_NONTASKING_OBJS= \
   a-cidlli$(objext) \
   a-cihama$(objext) \
   a-cihase$(objext) \
+  a-cimutr$(objext) \
   a-ciorma$(objext) \
   a-ciormu$(objext) \
   a-ciorse$(objext) \
   a-clrefi$(objext) \
+  a-cobove$(objext) \
+  a-cofove$(objext) \
   a-cogeso$(objext) \
   a-cohama$(objext) \
   a-cohase$(objext) \
@@ -143,10 +146,9 @@ GNATRTL_NONTASKING_OBJS= \
   a-colien$(objext) \
   a-colire$(objext) \
   a-comlin$(objext) \
+  a-comutr$(objext) \
   a-contai$(objext) \
   a-convec$(objext) \
-  a-cobove$(objext) \
-  a-cofove$(objext) \
   a-coorma$(objext) \
   a-coormu$(objext) \
   a-coorse$(objext) \
@@ -156,8 +158,6 @@ GNATRTL_NONTASKING_OBJS= \
   a-crbtgk$(objext) \
   a-crbtgo$(objext) \
   a-crdlli$(objext) \
-  a-comutr$(objext) \
-  a-cimutr$(objext) \
   a-csquin$(objext) \
   a-cuprqu$(objext) \
   a-cusyqu$(objext) \
@@ -207,12 +207,12 @@ GNATRTL_NONTASKING_OBJS= \
   a-nlcoar$(objext) \
   a-nlcoty$(objext) \
   a-nlelfu$(objext) \
-  a-nlrear$(objext) \
   a-nllcar$(objext) \
   a-nllcef$(objext) \
   a-nllcty$(objext) \
   a-nllefu$(objext) \
   a-nllrar$(objext) \
+  a-nlrear$(objext) \
   a-nscefu$(objext) \
   a-nscoty$(objext) \
   a-nselfu$(objext) \
@@ -224,8 +224,8 @@ GNATRTL_NONTASKING_OBJS= \
   a-numaux$(objext) \
   a-numeri$(objext) \
   a-nurear$(objext) \
-  a-rbtgbo$(objext) \
   a-rbtgbk$(objext) \
+  a-rbtgbo$(objext) \
   a-rbtgso$(objext) \
   a-sbecin$(objext) \
   a-sbhcin$(objext) \
@@ -511,8 +511,8 @@ GNATRTL_NONTASKING_OBJS= \
   s-crc32$(objext)  \
   s-crtl$(objext)   \
   s-diflio$(objext) \
-  s-dim$(objext)    \
   s-diinio$(objext) \
+  s-dim$(objext)    \
   s-dimkio$(objext) \
   s-dimmks$(objext) \
   s-direio$(objext) \
diff --git a/gcc/ada/a-excach.adb b/gcc/ada/a-excach.adb
index ab82920..b1cc22b 100644
--- a/gcc/ada/a-excach.adb
+++ b/gcc/ada/a-excach.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          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- --
@@ -63,7 +63,7 @@ begin
       --  outside the AAA/ZZZ range.
 
       System.Traceback.Call_Chain
-        (Traceback   => Excep.Tracebacks'Address,
+        (Traceback   => Excep.Tracebacks,
          Max_Len     => Max_Tracebacks,
          Len         => Excep.Num_Tracebacks,
          Exclude_Min => Code_Address_For_AAA,
diff --git a/gcc/ada/a-except-2005.ads b/gcc/ada/a-except-2005.ads
index 90c952c..7bf20dc 100644
--- a/gcc/ada/a-except-2005.ads
+++ b/gcc/ada/a-except-2005.ads
@@ -291,7 +291,7 @@ private
    Max_Tracebacks : constant := 50;
    --  Maximum number of trace backs stored in exception occurrence
 
-   type Tracebacks_Array is array (1 .. Max_Tracebacks) of TBE.Traceback_Entry;
+   subtype Tracebacks_Array is TBE.Tracebacks_Array (1 .. Max_Tracebacks);
    --  Traceback array stored in exception occurrence
 
    type Exception_Occurrence is record
diff --git a/gcc/ada/a-except.ads b/gcc/ada/a-except.ads
index 1228bf5..183bd58 100644
--- a/gcc/ada/a-except.ads
+++ b/gcc/ada/a-except.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.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -265,7 +265,7 @@ private
    Max_Tracebacks : constant := 50;
    --  Maximum number of trace backs stored in exception occurrence
 
-   type Tracebacks_Array is array (1 .. Max_Tracebacks) of TBE.Traceback_Entry;
+   subtype Tracebacks_Array is TBE.Tracebacks_Array (1 .. Max_Tracebacks);
    --  Traceback array stored in exception occurrence
 
    type Exception_Occurrence is record
diff --git a/gcc/ada/a-tags.ads b/gcc/ada/a-tags.ads
index f8d92b0..53a541b 100644
--- a/gcc/ada/a-tags.ads
+++ b/gcc/ada/a-tags.ads
@@ -49,12 +49,12 @@
 --    Descendant_Tag (when used with a library-level tagged type),
 --    Internal_Tag (when used with a library-level tagged type).
 
---  The following subprograms of the public part of this package take non
---  constant time (in terms of sources line executed):
+--  The following subprograms of the public part of this package execute in
+--  time that is not constant (in terms of sources line executed):
 
 --    Internal_Tag (when used with a locally defined tagged type), because in
---    such case this routine processes the external tag, extract from it an
---    address available there, and convert it into the tag value returned by
+--    such cases this routine processes the external tag, extracts from it an
+--    address available there, and converts it into the tag value returned by
 --    this function. The number of instructions executed is not constant since
 --    it depends on the length of the external tag string.
 
diff --git a/gcc/ada/a-tasatt.adb b/gcc/ada/a-tasatt.adb
index c127fe0..6e35d26 100644
--- a/gcc/ada/a-tasatt.adb
+++ b/gcc/ada/a-tasatt.adb
@@ -115,11 +115,13 @@ package body Ada.Task_Attributes is
 
    Fast_Path : constant Boolean :=
                  Attribute'Size <= Atomic_Address'Size
+                   and then Attribute'Alignment <= Atomic_Address'Alignment
                    and then To_Address (Initial_Value) = 0;
-   --  If the attribute fits in an Atomic_Address and Initial_Value is 0 (or
-   --  null), then we will map the attribute directly into
-   --  ATCB.Attributes (Index), otherwise we will create a level of indirection
-   --  and instead use Attributes (Index) as a Real_Attribute_Access.
+   --  If the attribute fits in an Atomic_Address (both size and alignment)
+   --  and Initial_Value is 0 (or null), then we will map the attribute
+   --  directly into ATCB.Attributes (Index), otherwise we will create a level
+   --  of indirection and instead use Attributes (Index) as a
+   --  Real_Attribute_Access.
 
    Index : constant Integer :=
              Next_Index (Require_Finalization => not Fast_Path);
@@ -203,7 +205,11 @@ package body Ada.Task_Attributes is
       end if;
 
       if Fast_Path then
+         --  Kill warning about possible alignment mismatch. If this happens,
+         --  Fast_Path will be False anyway
+         pragma Warnings (Off);
          return To_Handle (TT.Attributes (Index)'Address);
+         pragma Warnings (On);
       else
          Self_Id := STPO.Self;
          Task_Lock (Self_Id);
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index c48f3d2..417a76d 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -441,7 +441,7 @@ package body Exp_Prag is
                --  Generate a temporary to capture the value of the prefix:
                --    Temp : <Pref type>;
                --  Place that temporary at the beginning of declarations, to
-               --  prevent anomolies in the GNATprove flow analysis pass in
+               --  prevent anomalies in the GNATprove flow-analysis pass in
                --  the precondition procedure that follows.
 
                Decl :=
diff --git a/gcc/ada/g-traceb.adb b/gcc/ada/g-traceb.adb
index 790115f..157d8b6 100644
--- a/gcc/ada/g-traceb.adb
+++ b/gcc/ada/g-traceb.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                      Copyright (C) 1999-2010, AdaCore                    --
+--                      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- --
@@ -44,7 +44,7 @@ package body GNAT.Traceback is
       Len       : out Natural)
    is
    begin
-      System.Traceback.Call_Chain (Traceback'Address, Traceback'Length, Len);
+      System.Traceback.Call_Chain (Traceback, Traceback'Length, Len);
    end Call_Chain;
 
 end GNAT.Traceback;
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index 0c08f0e..bd8be55 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -5424,8 +5424,8 @@ is defined in package Standard.
 @emph{Activate warnings for elaboration pragmas.}
 @cindex @option{-gnatwl} (@command{gcc})
 @cindex Elaboration, warnings
-This switch activates warnings on missing
-for possible elaboration problems, including suspicious use
+This switch activates warnings for possible elaboration problems,
+including suspicious use
 of @code{Elaborate} pragmas, when using the static elaboration model, and
 possible situations that may raise @code{Program_Error} when using the
 dynamic elaboration model.
diff --git a/gcc/ada/memtrack.adb b/gcc/ada/memtrack.adb
index 2499bb7..be510f5 100644
--- a/gcc/ada/memtrack.adb
+++ b/gcc/ada/memtrack.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2001-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-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- --
@@ -132,7 +132,7 @@ package body System.Memory is
    Max_Call_Stack : constant := 200;
    --  Maximum number of frames supported
 
-   Tracebk   : aliased array (0 .. Max_Call_Stack) of Traceback_Entry;
+   Tracebk   : Tracebacks_Array (1 .. Max_Call_Stack);
    Num_Calls : aliased Integer := 0;
 
    Gmemfname : constant String := "gmem.out" & ASCII.NUL;
@@ -196,7 +196,7 @@ package body System.Memory is
          end if;
 
          Timestamp := System.OS_Primitives.Clock;
-         Call_Chain (Tracebk'Address, Max_Call_Stack, Num_Calls,
+         Call_Chain (Tracebk, Max_Call_Stack, Num_Calls,
                      Skip_Frames => 2);
          fputc (Character'Pos ('A'), Gmemfile);
          fwrite (Result'Address, Address_Size, 1, Gmemfile);
@@ -262,7 +262,7 @@ package body System.Memory is
             Gmem_Initialize;
          end if;
 
-         Call_Chain (Tracebk'Address, Max_Call_Stack, Num_Calls,
+         Call_Chain (Tracebk, Max_Call_Stack, Num_Calls,
                      Skip_Frames => 2);
          Timestamp := System.OS_Primitives.Clock;
          fputc (Character'Pos ('D'), Gmemfile);
@@ -345,7 +345,7 @@ package body System.Memory is
          if Needs_Init then
             Gmem_Initialize;
          end if;
-         Call_Chain (Tracebk'Address, Max_Call_Stack, Num_Calls,
+         Call_Chain (Tracebk, Max_Call_Stack, Num_Calls,
                      Skip_Frames => 2);
          Timestamp := System.OS_Primitives.Clock;
          fputc (Character'Pos ('D'), Gmemfile);
diff --git a/gcc/ada/s-traceb-hpux.adb b/gcc/ada/s-traceb-hpux.adb
index 734f0f4..92e36ca 100644
--- a/gcc/ada/s-traceb-hpux.adb
+++ b/gcc/ada/s-traceb-hpux.adb
@@ -7,7 +7,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---           Copyright (C) 2009-2011, Free Software Foundation, Inc.        --
+--           Copyright (C) 2009-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- --
@@ -262,6 +262,15 @@ package body System.Traceback is
    --  but it is not usable when frames with dynamically allocated space are
    --  on the way.
 
+   procedure Call_Chain
+     (Traceback   : System.Address;
+      Max_Len     : Natural;
+      Len         : out Natural;
+      Exclude_Min : System.Address := System.Null_Address;
+      Exclude_Max : System.Address := System.Null_Address;
+      Skip_Frames : Natural := 1);
+   --  Same as the exported version, but takes Traceback as an Address
+
    ------------------
    -- C_Call_Chain --
    ------------------
@@ -598,4 +607,18 @@ package body System.Traceback is
       Len := J - 1;
    end Call_Chain;
 
+   procedure Call_Chain
+     (Traceback   : in out System.Traceback_Entries.Tracebacks_Array;
+      Max_Len     : Natural;
+      Len         : out Natural;
+      Exclude_Min : System.Address := System.Null_Address;
+      Exclude_Max : System.Address := System.Null_Address;
+      Skip_Frames : Natural := 1)
+   is
+   begin
+      Call_Chain
+        (Traceback'Address, Max_Len, Len,
+         Exclude_Min, Exclude_Max, Skip_Frames);
+   end Call_Chain;
+
 end System.Traceback;
diff --git a/gcc/ada/s-traceb-mastop.adb b/gcc/ada/s-traceb-mastop.adb
index 4b5a177..f7da807 100644
--- a/gcc/ada/s-traceb-mastop.adb
+++ b/gcc/ada/s-traceb-mastop.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 1999-2010, AdaCore                     --
+--                     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- --
@@ -37,6 +37,15 @@ package body System.Traceback is
 
    use System.Machine_State_Operations;
 
+   procedure Call_Chain
+     (Traceback   : System.Address;
+      Max_Len     : Natural;
+      Len         : out Natural;
+      Exclude_Min : System.Address := System.Null_Address;
+      Exclude_Max : System.Address := System.Null_Address;
+      Skip_Frames : Natural := 1);
+   --  Same as the exported version, but takes Traceback as an Address
+
    ----------------
    -- Call_Chain --
    ----------------
@@ -93,6 +102,20 @@ package body System.Traceback is
       Free_Machine_State (M);
    end Call_Chain;
 
+   procedure Call_Chain
+     (Traceback   : in out System.Traceback_Entries.Tracebacks_Array;
+      Max_Len     : Natural;
+      Len         : out Natural;
+      Exclude_Min : System.Address := System.Null_Address;
+      Exclude_Max : System.Address := System.Null_Address;
+      Skip_Frames : Natural := 1)
+   is
+   begin
+      Call_Chain
+        (Traceback'Address, Max_Len, Len,
+         Exclude_Min, Exclude_Max, Skip_Frames);
+   end Call_Chain;
+
    ------------------
    -- C_Call_Chain --
    ------------------
diff --git a/gcc/ada/s-traceb.adb b/gcc/ada/s-traceb.adb
index b32e2a1..0c55cfc 100644
--- a/gcc/ada/s-traceb.adb
+++ b/gcc/ada/s-traceb.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1999-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1999-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- --
@@ -38,6 +38,15 @@ pragma Compiler_Unit_Warning;
 
 package body System.Traceback is
 
+   procedure Call_Chain
+     (Traceback   : System.Address;
+      Max_Len     : Natural;
+      Len         : out Natural;
+      Exclude_Min : System.Address := System.Null_Address;
+      Exclude_Max : System.Address := System.Null_Address;
+      Skip_Frames : Natural := 1);
+   --  Same as the exported version, but takes Traceback as an Address
+
    ------------------
    -- C_Call_Chain --
    ------------------
@@ -90,4 +99,18 @@ package body System.Traceback is
                         Skip_Frames => Skip_Frames + 1);
    end Call_Chain;
 
+   procedure Call_Chain
+     (Traceback   : in out System.Traceback_Entries.Tracebacks_Array;
+      Max_Len     : Natural;
+      Len         : out Natural;
+      Exclude_Min : System.Address := System.Null_Address;
+      Exclude_Max : System.Address := System.Null_Address;
+      Skip_Frames : Natural := 1)
+   is
+   begin
+      Call_Chain
+        (Traceback'Address, Max_Len, Len,
+         Exclude_Min, Exclude_Max, Skip_Frames);
+   end Call_Chain;
+
 end System.Traceback;
diff --git a/gcc/ada/s-traceb.ads b/gcc/ada/s-traceb.ads
index fc5cfb2..b149268 100644
--- a/gcc/ada/s-traceb.ads
+++ b/gcc/ada/s-traceb.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1999-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1999-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- --
@@ -39,6 +39,8 @@ pragma Polling (Off);
 --  We must turn polling off for this unit, because otherwise we get
 --  elaboration circularities with System.Exception_Tables.
 
+with System.Traceback_Entries;
+
 package System.Traceback is
 
    ----------------
@@ -46,7 +48,7 @@ package System.Traceback is
    ----------------
 
    procedure Call_Chain
-     (Traceback   : System.Address;
+     (Traceback   : in out System.Traceback_Entries.Tracebacks_Array;
       Max_Len     : Natural;
       Len         : out Natural;
       Exclude_Min : System.Address := System.Null_Address;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index d98c7c2..a5dda11 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3104,6 +3104,13 @@ package body Sem_Ch6 is
 
                      Spec_Id := Defining_Entity (New_Decl);
 
+                     --  As Body_Id originally comes from source, mark the new
+                     --  Spec_Id as such, which is required so that calls to
+                     --  this subprogram are registered in the local effects
+                     --  stored in ALI files for GNATprove.
+
+                     Set_Comes_From_Source (Spec_Id, True);
+
                      --  If aspect SPARK_Mode was specified on the body, it
                      --  needs to be repeated on the generated decl and the
                      --  body. Since the original aspect was moved to the