2016-07-04 Gary Dismukes <dismukes@adacore.com>

	* sem_ch12.ads, freeze.adb: Minor reformatting and typo fixes.

2016-07-04  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb (New_Stream_Subprogram): If the attribute
	definition clause comes from an aspect specification, place the
	generated subprogram renaming in the freeze actions of the type.

2016-07-04  Philippe Gil  <gil@adacore.com>

	* g-debpoo.adb (Dump.Do_Report) - add space prefix to backtrace
	address dump - avoid new line sent directly to stdout.

2016-07-04  Arnaud Charlet  <charlet@adacore.com>

	* gnat1drv.adb, sem_ch12.adb, sem_elab.adb, sem_prag.adb, sem_res.adb:
	Relax elaboration checks in SPARK_Mode so that we rely on the
	static elaboration model (if used). We'll have a more precise
	check performed in flow analysis of gnat2why.



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

10 files changed, 56 insertions, 46 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8672bdc301f..680902f1f82 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,25 @@
+2016-07-04  Gary Dismukes  <dismukes@adacore.com>
+
+	* sem_ch12.ads, freeze.adb: Minor reformatting and typo fixes.
+
+2016-07-04  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (New_Stream_Subprogram): If the attribute
+	definition clause comes from an aspect specification, place the
+	generated subprogram renaming in the freeze actions of the type.
+
+2016-07-04  Philippe Gil  <gil@adacore.com>
+
+	* g-debpoo.adb (Dump.Do_Report) - add space prefix to backtrace
+	address dump - avoid new line sent directly to stdout.
+
+2016-07-04  Arnaud Charlet  <charlet@adacore.com>
+
+	* gnat1drv.adb, sem_ch12.adb, sem_elab.adb, sem_prag.adb, sem_res.adb:
+	Relax elaboration checks in SPARK_Mode so that we rely on the
+	static elaboration model (if used). We'll have a more precise
+	check performed in flow analysis of gnat2why.
+
 2016-07-04  Ed Schonberg  <schonberg@adacore.com>
 
 	* ghost.adb (Prune_Node): A freeze node for an ignored ghost
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 173eae8a5e9..cfb20f4f495 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -4413,9 +4413,9 @@ package body Freeze is
 
            --  We want to implicitly pack if the specified size of the record
            --  is less than the sum of the object sizes (no point in packing
-           --  if this is not the case) if we can compute it, i.e. if we have
+           --  if this is not the case), if we can compute it, i.e. if we have
            --  only elementary components. Otherwise, we have at least one
-           --  composite component and we want to implicit pack only if bit
+           --  composite component and we want to implicitly pack only if bit
            --  packing is required for it, as we are sure in this case that
            --  the back end cannot do the expected layout without packing.
 
diff --git a/gcc/ada/g-debpoo.adb b/gcc/ada/g-debpoo.adb
index c5664a9939d..567bb758a41 100644
--- a/gcc/ada/g-debpoo.adb
+++ b/gcc/ada/g-debpoo.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --
@@ -1908,7 +1908,7 @@ package body GNAT.Debug_Pools is
          --  Sorted array for the biggest memory users
 
       begin
-         New_Line;
+         Put_Line ("");
          case Sort is
             when Memory_Usage | All_Reports  =>
                Put_Line (Size'Img & " biggest memory users at this time:");
@@ -2010,10 +2010,10 @@ package body GNAT.Debug_Pools is
             end;
 
             for J in Max (M).Traceback'Range loop
-               Put (Image_C (PC_For (Max (M).Traceback (J))));
+               Put (" " & Image_C (PC_For (Max (M).Traceback (J))));
             end loop;
 
-            New_Line;
+            Put_Line ("");
          end loop;
       end Do_Report;
 
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 702545a1718..2ade204e6ab 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -415,11 +415,6 @@ procedure Gnat1drv is
 
          Suppress_Options.Suppress := (others => False);
 
-         --  Turn off dynamic elaboration checks. SPARK mode depends on the
-         --  use of the static elaboration mode.
-
-         Dynamic_Elaboration_Checks := False;
-
          --  Detect overflow on unconstrained floating-point types, such as
          --  the predefined types Float, Long_Float and Long_Long_Float from
          --  package Standard. Not necessary if float overflows are checked
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index ae04a9d23a3..1b4807746e4 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -4356,10 +4356,6 @@ package body Sem_Ch12 is
       SPARK_Mode_Pragma        := Save_SMP;
       Style_Check              := Save_Style_Check;
 
-      if SPARK_Mode = On then
-         Dynamic_Elaboration_Checks := False;
-      end if;
-
       --  Check that if N is an instantiation of System.Dim_Float_IO or
       --  System.Dim_Integer_IO, the formal type has a dimension system.
 
@@ -4396,10 +4392,6 @@ package body Sem_Ch12 is
          SPARK_Mode               := Save_SM;
          SPARK_Mode_Pragma        := Save_SMP;
          Style_Check              := Save_Style_Check;
-
-         if SPARK_Mode = On then
-            Dynamic_Elaboration_Checks := False;
-         end if;
    end Analyze_Package_Instantiation;
 
    --------------------------
@@ -5328,10 +5320,6 @@ package body Sem_Ch12 is
          Ignore_Pragma_SPARK_Mode := Save_IPSM;
          SPARK_Mode               := Save_SM;
          SPARK_Mode_Pragma        := Save_SMP;
-
-         if SPARK_Mode = On then
-            Dynamic_Elaboration_Checks := False;
-         end if;
       end if;
 
    <<Leave>>
@@ -5352,10 +5340,6 @@ package body Sem_Ch12 is
          Ignore_Pragma_SPARK_Mode := Save_IPSM;
          SPARK_Mode               := Save_SM;
          SPARK_Mode_Pragma        := Save_SMP;
-
-         if SPARK_Mode = On then
-            Dynamic_Elaboration_Checks := False;
-         end if;
    end Analyze_Subprogram_Instantiation;
 
    -------------------------
@@ -15247,12 +15231,6 @@ package body Sem_Ch12 is
 
          SPARK_Mode := Save_SPARK_Mode;
          SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma;
-
-         --  Make sure dynamic elaboration checks are off in SPARK Mode
-
-         if SPARK_Mode = On then
-            Dynamic_Elaboration_Checks := False;
-         end if;
       end if;
 
       Current_Instantiated_Parent :=
diff --git a/gcc/ada/sem_ch12.ads b/gcc/ada/sem_ch12.ads
index 8365ac482c3..82a093afae3 100644
--- a/gcc/ada/sem_ch12.ads
+++ b/gcc/ada/sem_ch12.ads
@@ -181,9 +181,9 @@ package Sem_Ch12 is
    --  establishes a new source file entry representing the inherited pragma
    --  as an instantiation, marked as an inherited pragma (so that errout can
    --  distinguish cases for generating error messages, otherwise the treatment
-   --  is identical). In this call N is the subprogram declaration from
+   --  is identical). In this call, N is the subprogram declaration from
    --  which the pragma is inherited and E is the defining identifier of
-   --  the overridding subprogram (when the subprogram is redefined) or the
+   --  the overriding subprogram (when the subprogram is redefined) or the
    --  defining identifier of the extension type (when the subprogram is
    --  inherited). The resulting Sloc adjustment factor is saved as part of the
    --  internal state of the Sem_Ch12 package for use in subsequent calls to
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index b631b9c9417..aaa8576ee26 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -11941,7 +11941,9 @@ package body Sem_Ch13 is
       --  at the freeze point, and we must generate only a completion of this
       --  declaration. We do the same for private types, because the full view
       --  might be tagged. Otherwise we generate a declaration at the point of
-      --  the attribute definition clause.
+      --  the attribute definition clause. If the attribute definition comes
+      --  from an aspect specification the declaration is part of the freeze
+      --  actions of the type.
 
       function Build_Spec return Node_Id;
       --  Used for declaration and renaming declaration, so that this is
@@ -12033,8 +12035,16 @@ package body Sem_Ch13 is
              Object_Definition   => New_Occurrence_Of (Standard_Boolean, Loc));
       end if;
 
-      Insert_Action (N, Subp_Decl);
-      Set_Entity (N, Subp_Id);
+      if not Defer_Declaration
+        and then From_Aspect_Specification (N)
+        and then Has_Delayed_Freeze (Ent)
+      then
+         Append_Freeze_Action (Ent, Subp_Decl);
+
+      else
+         Insert_Action (N, Subp_Decl);
+         Set_Entity (N, Subp_Id);
+      end if;
 
       Subp_Decl :=
         Make_Subprogram_Renaming_Declaration (Loc,
@@ -12043,8 +12053,15 @@ package body Sem_Ch13 is
 
       if Defer_Declaration then
          Set_TSS (Base_Type (Ent), Subp_Id);
+
       else
-         Insert_Action (N, Subp_Decl);
+         if From_Aspect_Specification (N) then
+            Append_Freeze_Action (Ent, Subp_Decl);
+
+         else
+            Insert_Action (N, Subp_Decl);
+         end if;
+
          Copy_TSS (Subp_Id, Base_Type (Ent));
       end if;
    end New_Stream_Subprogram;
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index d963def7980..8e82d281795 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -1018,7 +1018,9 @@ package body Sem_Elab is
       --  expression, which in turn may have side effects.
 
       Issue_In_SPARK :=
-        SPARK_Mode = On and (Comes_From_Source (Ent) or Is_DIC_Proc);
+        SPARK_Mode = On
+          and then Dynamic_Elaboration_Checks
+          and then (Comes_From_Source (Ent) or Is_DIC_Proc);
 
       --  Now check if an Elaborate_All (or dynamic check) is needed
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 3a14fdffe94..f603e317af4 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -14489,8 +14489,7 @@ package body Sem_Prag is
             --  checks in SPARK mode).
 
             Dynamic_Elaboration_Checks :=
-              (Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic)
-                and then SPARK_Mode /= On;
+              Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic;
 
          ---------------
          -- Eliminate --
@@ -21200,10 +21199,6 @@ package body Sem_Prag is
             begin
                SPARK_Mode := Mode_Id;
                SPARK_Mode_Pragma := N;
-
-               if SPARK_Mode = On then
-                  Dynamic_Elaboration_Checks := False;
-               end if;
             end Set_SPARK_Context;
 
             --  Local variables
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index ffd2ea15fbd..06e9f06303d 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7119,6 +7119,7 @@ package body Sem_Res is
             --  read as it simply establishes an alias.
 
             if Ekind (E) = E_Variable
+              and then Dynamic_Elaboration_Checks
               and then Nkind (Par) /= N_Object_Renaming_Declaration
             then
                Check_Elab_Call (N);