[multiple changes]

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.

From-SVN: r237968
This commit is contained in:
Arnaud Charlet 2016-07-04 12:38:22 +02:00
parent 7c14db4032
commit d4b56371aa
10 changed files with 56 additions and 46 deletions

View File

@ -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

View File

@ -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.

View File

@ -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;

View File

@ -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

View File

@ -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 :=

View File

@ -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

View File

@ -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;

View File

@ -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

View File

@ -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

View File

@ -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);