mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-03-19 00:01:21 +08:00
Code Issues Packages Projects Releases Wiki Activity

2015-01-07 Hristian Kirtchev <kirtchev@adacore.com>

Browse Source 
* alloc.ads Alphabetize several declarations. Add constants
	Ignored_Ghost_Units_Initial and Ignored_Ghost_Units_Increment.
	* atree.adb Add with and use clauses for Opt.
	(Allocate_Initialize_Node): Mark a node as ignored Ghost
	if it is created in an ignored Ghost region.
	(Ekind_In): New variant.
	(Is_Ignored_Ghost_Node): New routine.
	(Set_Is_Ignored_Ghost_Node): New routine.
	* atree.adb Aplhabetize several subprograms declarations. Flag
	Spare0 is now known as Is_Ignored_Ghost_Node.
	(Ekind_In): New variant.
	(Is_Ignored_Ghost_Node): New routine.
	(Set_Is_Ignored_Ghost_Node): New routine.
	* einfo.adb: Flag 279 is now known as Contains_Ignored_Ghost_Code.
	(Contains_Ignored_Ghost_Code): New routine.
	(Set_Contains_Ignored_Ghost_Code): New routine.
	(Set_Is_Checked_Ghost_Entity, Set_Is_Ignored_Ghost_Entity):
	It is now possible to set this property on an unanalyzed entity.
	(Write_Entity_Flags): Output the status of flag
	Contains_Ignored_Ghost_Code.
	* einfo.ads New attribute Contains_Ignored_Ghost_Code along with
	usage in nodes.
	(Contains_Ignored_Ghost_Code): New routine
	along with pragma Inline.
	(Set_Contains_Ignored_Ghost_Code): New routine along with pragma Inline.
	* exp_ch3.adb Add with and use clauses for Ghost.
	(Freeze_Type): Capture/restore the value of Ghost_Mode on entry/exit.
	Set the Ghost_Mode in effect.
	(Restore_Globals): New routine.
	* exp_ch7.adb (Process_Declarations): Do not process a context
	that invoves an ignored Ghost entity.
	* exp_dbug.adb (Qualify_All_Entity_Names): Skip an ignored Ghost
	construct that has been rewritten as a null statement.
	* exp_disp.adb Add with and use clauses for Ghost.
	(Make_DT): Capture/restore the value of Ghost_Mode on entry/exit. Set
	the Ghost_Mode in effect.
	(Restore_Globals): New routine.
	* exp_util.adb (Requires_Cleanup_Actions): An ignored Ghost entity
	does not require any clean up. Add two missing cases that deal
	with block statements.
	* freeze.adb Add with and use clauses for Ghost.
	(Freeze_Entity): Capture/restore the value of Ghost_Mode on entry/exit.
	Set the Ghost_Mode in effect.
	(Restore_Globals): New routine.
	* frontend.adb Add with and use clauses for Ghost. Remove any
	ignored Ghost code from all units that qualify.
	* ghost.adb New unit.
	* ghost.ads New unit.
	* gnat1drv.adb Add with clause for Ghost. Initialize and lock
	the table in package Ghost.
	* lib.ads: Alphabetize several subprogram declarations.
	* lib-xref.adb (Output_References): Do not generate reference
	information for ignored Ghost entities.
	* opt.ads Add new type Ghost_Mode_Type and new global variable
	Ghost_Mode.
	* rtsfind.adb (Load_RTU): Provide a clean environment when
	loading a runtime unit.
	* sem.adb (Analyze): Capture/restore the value of Ghost_Mode on
	entry/exit as the node may set a different mode.
	(Do_Analyze):
	Capture/restore the value of Ghost_Mode on entry/exit as the
	unit may be withed from a unit with a different Ghost mode.
	* sem_ch3.adb Add with and use clauses for Ghost.
	(Analyze_Full_Type_Declaration, Analyze_Incomplete_Type_Decl,
	Analyze_Number_Declaration, Analyze_Private_Extension_Declaration,
	Analyze_Subtype_Declaration): Set the Ghost_Mode in effect. Mark
	the entity as Ghost when there is a Ghost_Mode in effect.
	(Array_Type_Declaration): The implicit base type inherits the
	"ghostness" from the array type.
	(Derive_Subprogram): The
	alias inherits the "ghostness" from the parent subprogram.
	(Make_Implicit_Base): The implicit base type inherits the
	"ghostness" from the parent type.
	* sem_ch5.adb Add with and use clauses for Ghost.
	(Analyze_Assignment): Set the Ghost_Mode in effect.
	* sem_ch6.adb Add with and use clauses for Ghost.
	(Analyze_Abstract_Subprogram_Declaration, Analyze_Procedure_Call,
	Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Declaration):
	Set the Ghost_Mode in effect. Mark the entity as Ghost when
	there is a Ghost_Mode in effect.
	* sem_ch7.adb Add with and use clauses for Ghost.
	(Analyze_Package_Body_Helper, Analyze_Package_Declaration,
	Analyze_Private_Type_Declaration): Set the Ghost_Mode in
	effect. Mark the entity as Ghost when there is a Ghost_Mode
	in effect.
	* sem_ch8.adb Add with and use clauses for Ghost.
	(Analyze_Exception_Renaming, Analyze_Generic_Renaming,
	Analyze_Object_Renaming, Analyze_Package_Renaming,
	Analyze_Subprogram_Renaming): Set the Ghost_Mode in effect. Mark
	the entity as Ghost when there is a Ghost_Mode in effect.
	(Find_Type): Check the Ghost context of a type.
	* sem_ch11.adb Add with and use clauses for Ghost.
	(Analyze_Exception_Declaration): Set the Ghost_Mode in
	effect. Mark the entity as Ghost when there is a Ghost_Mode
	in effect.
	* sem_ch12.adb Add with and use clauses for Ghost.
	(Analyze_Generic_Package_Declaration,
	Analyze_Generic_Subprogram_Declaration): Set the Ghost_Mode in effect.
	Mark the entity as Ghost when there is a Ghost_Mode in effect.
	* sem_prag.adb Add with and use clauses for Ghost.
	(Analyze_Pragma): Ghost-related checks are triggered when there
	is a Ghost mode in effect.
	(Create_Abstract_State): Mark the
	entity as Ghost when there is a Ghost_Mode in effect.
	* sem_res.adb Add with and use clauses for Ghost.
	(Check_Ghost_Context): Removed.
	* sem_util.adb (Check_Ghost_Completion): Removed.
	(Check_Ghost_Derivation): Removed.
	(Incomplete_Or_Partial_View):
	Add a guard in case the entity has not been analyzed yet
	and does carry a scope.
	(Is_Declaration): New routine.
	(Is_Ghost_Entity): Removed.
	(Is_Ghost_Statement_Or_Pragma):
	Removed.
	(Is_Subject_To_Ghost): Removed.
	(Set_Is_Ghost_Entity):
	Removed.
	(Within_Ghost_Scope): Removed.
	* sem_util.adb (Check_Ghost_Completion): Removed.
	(Check_Ghost_Derivation): Removed.
	(Is_Declaration): New routine.
	(Is_Ghost_Entity): Removed.
	(Is_Ghost_Statement_Or_Pragma): Removed.
	(Is_Subject_To_Ghost): Removed.
	(Set_Is_Ghost_Entity): Removed.
	(Within_Ghost_Scope): Removed.
	* sinfo.ads Add a section on Ghost mode.
	* treepr.adb (Print_Header_Flag): New routine.
	(Print_Node_Header): Factor out code. Output flag
	Is_Ignored_Ghost_Node.
	* gcc-interface/Make-lang.in: Add dependency for unit Ghost.

From-SVN: r219280
This commit is contained in:
Hristian Kirtchev 2015-01-07 08:41:47 +00:00 committed by Arnaud Charlet
parent 4a9a42abc4
commit 8636f52f7b
35 changed files with 2282 additions and 1000 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
gcc/ada/ChangeLog
View File

@ -1,3 +1,138 @@
2015-01-07 Hristian Kirtchev <kirtchev@adacore.com>
* alloc.ads Alphabetize several declarations. Add constants
Ignored_Ghost_Units_Initial and Ignored_Ghost_Units_Increment.
* atree.adb Add with and use clauses for Opt.
(Allocate_Initialize_Node): Mark a node as ignored Ghost
if it is created in an ignored Ghost region.
(Ekind_In): New variant.
(Is_Ignored_Ghost_Node): New routine.
(Set_Is_Ignored_Ghost_Node): New routine.
* atree.adb Aplhabetize several subprograms declarations. Flag
Spare0 is now known as Is_Ignored_Ghost_Node.
(Ekind_In): New variant.
(Is_Ignored_Ghost_Node): New routine.
(Set_Is_Ignored_Ghost_Node): New routine.
* einfo.adb: Flag 279 is now known as Contains_Ignored_Ghost_Code.
(Contains_Ignored_Ghost_Code): New routine.
(Set_Contains_Ignored_Ghost_Code): New routine.
(Set_Is_Checked_Ghost_Entity, Set_Is_Ignored_Ghost_Entity):
It is now possible to set this property on an unanalyzed entity.
(Write_Entity_Flags): Output the status of flag
Contains_Ignored_Ghost_Code.
* einfo.ads New attribute Contains_Ignored_Ghost_Code along with
usage in nodes.
(Contains_Ignored_Ghost_Code): New routine
along with pragma Inline.
(Set_Contains_Ignored_Ghost_Code): New routine along with pragma Inline.
* exp_ch3.adb Add with and use clauses for Ghost.
(Freeze_Type): Capture/restore the value of Ghost_Mode on entry/exit.
Set the Ghost_Mode in effect.
(Restore_Globals): New routine.
* exp_ch7.adb (Process_Declarations): Do not process a context
that invoves an ignored Ghost entity.
* exp_dbug.adb (Qualify_All_Entity_Names): Skip an ignored Ghost
construct that has been rewritten as a null statement.
* exp_disp.adb Add with and use clauses for Ghost.
(Make_DT): Capture/restore the value of Ghost_Mode on entry/exit. Set
the Ghost_Mode in effect.
(Restore_Globals): New routine.
* exp_util.adb (Requires_Cleanup_Actions): An ignored Ghost entity
does not require any clean up. Add two missing cases that deal
with block statements.
* freeze.adb Add with and use clauses for Ghost.
(Freeze_Entity): Capture/restore the value of Ghost_Mode on entry/exit.
Set the Ghost_Mode in effect.
(Restore_Globals): New routine.
* frontend.adb Add with and use clauses for Ghost. Remove any
ignored Ghost code from all units that qualify.
* ghost.adb New unit.
* ghost.ads New unit.
* gnat1drv.adb Add with clause for Ghost. Initialize and lock
the table in package Ghost.
* lib.ads: Alphabetize several subprogram declarations.
* lib-xref.adb (Output_References): Do not generate reference
information for ignored Ghost entities.
* opt.ads Add new type Ghost_Mode_Type and new global variable
Ghost_Mode.
* rtsfind.adb (Load_RTU): Provide a clean environment when
loading a runtime unit.
* sem.adb (Analyze): Capture/restore the value of Ghost_Mode on
entry/exit as the node may set a different mode.
(Do_Analyze):
Capture/restore the value of Ghost_Mode on entry/exit as the
unit may be withed from a unit with a different Ghost mode.
* sem_ch3.adb Add with and use clauses for Ghost.
(Analyze_Full_Type_Declaration, Analyze_Incomplete_Type_Decl,
Analyze_Number_Declaration, Analyze_Private_Extension_Declaration,
Analyze_Subtype_Declaration): Set the Ghost_Mode in effect. Mark
the entity as Ghost when there is a Ghost_Mode in effect.
(Array_Type_Declaration): The implicit base type inherits the
"ghostness" from the array type.
(Derive_Subprogram): The
alias inherits the "ghostness" from the parent subprogram.
(Make_Implicit_Base): The implicit base type inherits the
"ghostness" from the parent type.
* sem_ch5.adb Add with and use clauses for Ghost.
(Analyze_Assignment): Set the Ghost_Mode in effect.
* sem_ch6.adb Add with and use clauses for Ghost.
(Analyze_Abstract_Subprogram_Declaration, Analyze_Procedure_Call,
Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Declaration):
Set the Ghost_Mode in effect. Mark the entity as Ghost when
there is a Ghost_Mode in effect.
* sem_ch7.adb Add with and use clauses for Ghost.
(Analyze_Package_Body_Helper, Analyze_Package_Declaration,
Analyze_Private_Type_Declaration): Set the Ghost_Mode in
effect. Mark the entity as Ghost when there is a Ghost_Mode
in effect.
* sem_ch8.adb Add with and use clauses for Ghost.
(Analyze_Exception_Renaming, Analyze_Generic_Renaming,
Analyze_Object_Renaming, Analyze_Package_Renaming,
Analyze_Subprogram_Renaming): Set the Ghost_Mode in effect. Mark
the entity as Ghost when there is a Ghost_Mode in effect.
(Find_Type): Check the Ghost context of a type.
* sem_ch11.adb Add with and use clauses for Ghost.
(Analyze_Exception_Declaration): Set the Ghost_Mode in
effect. Mark the entity as Ghost when there is a Ghost_Mode
in effect.
* sem_ch12.adb Add with and use clauses for Ghost.
(Analyze_Generic_Package_Declaration,
Analyze_Generic_Subprogram_Declaration): Set the Ghost_Mode in effect.
Mark the entity as Ghost when there is a Ghost_Mode in effect.
* sem_prag.adb Add with and use clauses for Ghost.
(Analyze_Pragma): Ghost-related checks are triggered when there
is a Ghost mode in effect.
(Create_Abstract_State): Mark the
entity as Ghost when there is a Ghost_Mode in effect.
* sem_res.adb Add with and use clauses for Ghost.
(Check_Ghost_Context): Removed.
* sem_util.adb (Check_Ghost_Completion): Removed.
(Check_Ghost_Derivation): Removed.
(Incomplete_Or_Partial_View):
Add a guard in case the entity has not been analyzed yet
and does carry a scope.
(Is_Declaration): New routine.
(Is_Ghost_Entity): Removed.
(Is_Ghost_Statement_Or_Pragma):
Removed.
(Is_Subject_To_Ghost): Removed.
(Set_Is_Ghost_Entity):
Removed.
(Within_Ghost_Scope): Removed.
* sem_util.adb (Check_Ghost_Completion): Removed.
(Check_Ghost_Derivation): Removed.
(Is_Declaration): New routine.
(Is_Ghost_Entity): Removed.
(Is_Ghost_Statement_Or_Pragma): Removed.
(Is_Subject_To_Ghost): Removed.
(Set_Is_Ghost_Entity): Removed.
(Within_Ghost_Scope): Removed.
* sinfo.ads Add a section on Ghost mode.
* treepr.adb (Print_Header_Flag): New routine.
(Print_Node_Header): Factor out code. Output flag
Is_Ignored_Ghost_Node.
* gcc-interface/Make-lang.in: Add dependency for unit Ghost.
2015-01-06 Eric Botcazou <ebotcazou@adacore.com>
* freeze.adb (Freeze_Array_Type) <Complain_CS>: Remove always

13
gcc/ada/alloc.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2012, 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- --
@ -64,14 +64,17 @@ package Alloc is
File_Name_Chars_Initial : constant := 10_000; -- Osint
File_Name_Chars_Increment : constant := 100;
Inlined_Bodies_Initial : constant := 50; -- Inline
Inlined_Bodies_Increment : constant := 200;
In_Out_Warnings_Initial : constant := 100; -- Sem_Warn
In_Out_Warnings_Increment : constant := 100;
Ignored_Ghost_Units_Initial : constant := 20; -- Sem_Util
Ignored_Ghost_Units_Increment : constant := 50;
Inlined_Initial : constant := 100; -- Inline
Inlined_Increment : constant := 100;
In_Out_Warnings_Initial : constant := 100; -- Sem_Warn
In_Out_Warnings_Increment : constant := 100;
Inlined_Bodies_Initial : constant := 50; -- Inline
Inlined_Bodies_Increment : constant := 200;
Interp_Map_Initial : constant := 200; -- Sem_Type
Interp_Map_Increment : constant := 100;

72
gcc/ada/atree.adb
View File

@ -39,6 +39,7 @@ pragma Style_Checks (All_Checks);
with Aspects; use Aspects;
with Debug; use Debug;
with Nlists; use Nlists;
with Opt; use Opt;
with Output; use Output;
with Sinput; use Sinput;
with Tree_IO; use Tree_IO;
@ -569,10 +570,10 @@ package body Atree is
then
New_Id := Src;
else
-- We are allocating a new node, or extending a node
-- other than Nodes.Last.
-- We are allocating a new node, or extending a node other than
-- Nodes.Last.
else
if Present (Src) then
Nodes.Append (Nodes.Table (Src));
Flags.Append (Flags.Table (Src));
@ -586,6 +587,13 @@ package body Atree is
Node_Count := Node_Count + 1;
end if;
-- Mark the node as ignored Ghost if it is created in an ignored Ghost
-- region.
if Ghost_Mode = Ignore then
Set_Is_Ignored_Ghost_Node (New_Id);
end if;
-- Specifically copy Paren_Count to deal with creating new table entry
-- if the parentheses count is at the maximum possible value already.
@ -1079,6 +1087,30 @@ package body Atree is
T = V8;
end Ekind_In;
function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
V2 : Entity_Kind;
V3 : Entity_Kind;
V4 : Entity_Kind;
V5 : Entity_Kind;
V6 : Entity_Kind;
V7 : Entity_Kind;
V8 : Entity_Kind;
V9 : Entity_Kind) return Boolean
is
begin
return T = V1 or else
T = V2 or else
T = V3 or else
T = V4 or else
T = V5 or else
T = V6 or else
T = V7 or else
T = V8 or else
T = V9;
end Ekind_In;
function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
@ -1163,6 +1195,22 @@ package body Atree is
return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8);
end Ekind_In;
function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
V2 : Entity_Kind;
V3 : Entity_Kind;
V4 : Entity_Kind;
V5 : Entity_Kind;
V6 : Entity_Kind;
V7 : Entity_Kind;
V8 : Entity_Kind;
V9 : Entity_Kind) return Boolean
is
begin
return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9);
end Ekind_In;
------------------------
-- Set_Reporting_Proc --
------------------------
@ -1382,6 +1430,15 @@ package body Atree is
Set_Error_Posted (Error, True);
end Initialize;
---------------------------
-- Is_Ignored_Ghost_Node --
---------------------------
function Is_Ignored_Ghost_Node (N : Node_Id) return Boolean is
begin
return Flags.Table (N).Is_Ignored_Ghost_Node;
end Is_Ignored_Ghost_Node;
--------------------------
-- Is_Rewrite_Insertion --
--------------------------
@ -2031,6 +2088,15 @@ package body Atree is
Nodes.Table (N).Has_Aspects := Val;
end Set_Has_Aspects;
-------------------------------
-- Set_Is_Ignored_Ghost_Node --
-------------------------------
procedure Set_Is_Ignored_Ghost_Node (N : Node_Id; Val : Boolean := True) is
begin
Flags.Table (N).Is_Ignored_Ghost_Node := Val;
end Set_Is_Ignored_Ghost_Node;
-----------------------
-- Set_Original_Node --
-----------------------

104
gcc/ada/atree.ads
View File

@ -605,42 +605,46 @@ package Atree is
-- The following functions return the contents of the indicated field of
-- the node referenced by the argument, which is a Node_Id.
function Nkind (N : Node_Id) return Node_Kind;
pragma Inline (Nkind);
function Analyzed (N : Node_Id) return Boolean;
pragma Inline (Analyzed);
function Has_Aspects (N : Node_Id) return Boolean;
pragma Inline (Has_Aspects);
function Comes_From_Source (N : Node_Id) return Boolean;
pragma Inline (Comes_From_Source);
function Error_Posted (N : Node_Id) return Boolean;
pragma Inline (Error_Posted);
function Sloc (N : Node_Id) return Source_Ptr;
pragma Inline (Sloc);
function Has_Aspects (N : Node_Id) return Boolean;
pragma Inline (Has_Aspects);
function Paren_Count (N : Node_Id) return Nat;
pragma Inline (Paren_Count);
function Is_Ignored_Ghost_Node
(N : Node_Id) return Boolean;
pragma Inline (Is_Ignored_Ghost_Node);
function Parent (N : Node_Id) return Node_Id;
pragma Inline (Parent);
-- Returns the parent of a node if the node is not a list member, or else
-- the parent of the list containing the node if the node is a list member.
function Nkind (N : Node_Id) return Node_Kind;
pragma Inline (Nkind);
function No (N : Node_Id) return Boolean;
pragma Inline (No);
-- Tests given Id for equality with the Empty node. This allows notations
-- like "if No (Variant_Part)" as opposed to "if Variant_Part = Empty".
function Parent (N : Node_Id) return Node_Id;
pragma Inline (Parent);
-- Returns the parent of a node if the node is not a list member, or else
-- the parent of the list containing the node if the node is a list member.
function Paren_Count (N : Node_Id) return Nat;
pragma Inline (Paren_Count);
function Present (N : Node_Id) return Boolean;
pragma Inline (Present);
-- Tests given Id for inequality with the Empty node. This allows notations
-- like "if Present (Statement)" as opposed to "if Statement /= Empty".
function Sloc (N : Node_Id) return Source_Ptr;
pragma Inline (Sloc);
---------------------
-- Node_Kind Tests --
---------------------
@ -784,6 +788,18 @@ package Atree is
V7 : Entity_Kind;
V8 : Entity_Kind) return Boolean;
function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
V2 : Entity_Kind;
V3 : Entity_Kind;
V4 : Entity_Kind;
V5 : Entity_Kind;
V6 : Entity_Kind;
V7 : Entity_Kind;
V8 : Entity_Kind;
V9 : Entity_Kind) return Boolean;
function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
@ -840,6 +856,18 @@ package Atree is
V7 : Entity_Kind;
V8 : Entity_Kind) return Boolean;
function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
V2 : Entity_Kind;
V3 : Entity_Kind;
V4 : Entity_Kind;
V5 : Entity_Kind;
V6 : Entity_Kind;
V7 : Entity_Kind;
V8 : Entity_Kind;
V9 : Entity_Kind) return Boolean;
pragma Inline (Ekind_In);
-- Inline all above functions
@ -865,39 +893,42 @@ package Atree is
-- to be set in the specified field. Note that Set_Nkind is in the next
-- section, since its use is restricted.
procedure Set_Sloc (N : Node_Id; Val : Source_Ptr);
pragma Inline (Set_Sloc);
procedure Set_Paren_Count (N : Node_Id; Val : Nat);
pragma Inline (Set_Paren_Count);
procedure Set_Parent (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Parent);
procedure Set_Analyzed (N : Node_Id; Val : Boolean := True);
procedure Set_Analyzed (N : Node_Id; Val : Boolean := True);
pragma Inline (Set_Analyzed);
procedure Set_Comes_From_Source (N : Node_Id; Val : Boolean);
pragma Inline (Set_Comes_From_Source);
-- Note that this routine is very rarely used, since usually the default
-- mechanism provided sets the right value, but in some unusual cases, the
-- value needs to be reset (e.g. when a source node is copied, and the copy
-- must not have Comes_From_Source set).
procedure Set_Error_Posted (N : Node_Id; Val : Boolean := True);
pragma Inline (Set_Error_Posted);
procedure Set_Comes_From_Source (N : Node_Id; Val : Boolean);
pragma Inline (Set_Comes_From_Source);
-- Note that this routine is very rarely used, since usually the
-- default mechanism provided sets the right value, but in some
-- unusual cases, the value needs to be reset (e.g. when a source
-- node is copied, and the copy must not have Comes_From_Source set).
procedure Set_Has_Aspects (N : Node_Id; Val : Boolean := True);
pragma Inline (Set_Has_Aspects);
procedure Set_Is_Ignored_Ghost_Node (N : Node_Id; Val : Boolean := True);
pragma Inline (Set_Is_Ignored_Ghost_Node);
procedure Set_Original_Node (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Original_Node);
-- Note that this routine is used only in very peculiar cases. In normal
-- cases, the Original_Node link is set by calls to Rewrite. We currently
-- use it in ASIS mode to manually set the link from pragma expressions
-- to their aspect original source expressions, so that the original source
-- use it in ASIS mode to manually set the link from pragma expressions to
-- their aspect original source expressions, so that the original source
-- expressions accessed by ASIS are also semantically analyzed.
procedure Set_Parent (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Parent);
procedure Set_Paren_Count (N : Node_Id; Val : Nat);
pragma Inline (Set_Paren_Count);
procedure Set_Sloc (N : Node_Id; Val : Source_Ptr);
pragma Inline (Set_Sloc);
------------------------------
-- Entity Update Procedures --
------------------------------
@ -4007,7 +4038,12 @@ package Atree is
Flag1 : Boolean;
Flag2 : Boolean;
Flag3 : Boolean;
Spare0 : Boolean;
Is_Ignored_Ghost_Node : Boolean;
-- Flag denothing whether the node is subject to pragma Ghost with
-- policy Ignore. The name of the flag should be Flag4, however this
-- requires changing the names of all remaining 300+ flags.
Spare1 : Boolean;
Spare2 : Boolean;
Spare3 : Boolean;

45
gcc/ada/einfo.adb
View File

@ -574,8 +574,8 @@ package body Einfo is
-- No_Dynamic_Predicate_On_Actual Flag276
-- Is_Checked_Ghost_Entity Flag277
-- Is_Ignored_Ghost_Entity Flag278
-- Contains_Ignored_Ghost_Code Flag279
-- (unused) Flag279
-- (unused) Flag280
-- (unused) Flag281
@ -1117,6 +1117,21 @@ package body Einfo is
return Node18 (Id);
end Entry_Index_Constant;
function Contains_Ignored_Ghost_Code (Id : E) return B is
begin
pragma Assert
(Ekind_In (Id, E_Block,
E_Function,
E_Generic_Function,
E_Generic_Package,
E_Generic_Procedure,
E_Package,
E_Package_Body,
E_Procedure,
E_Subprogram_Body));
return Flag279 (Id);
end Contains_Ignored_Ghost_Code;
function Contract (Id : E) return N is
begin
pragma Assert
@ -3609,6 +3624,21 @@ package body Einfo is
Set_Node20 (Id, V);
end Set_Component_Type;
procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True) is
begin
pragma Assert
(Ekind_In (Id, E_Block,
E_Function,
E_Generic_Function,
E_Generic_Package,
E_Generic_Procedure,
E_Package,
E_Package_Body,
E_Procedure,
E_Subprogram_Body));
Set_Flag279 (Id, V);
end Set_Contains_Ignored_Ghost_Code;
procedure Set_Contract (Id : E; V : N) is
begin
pragma Assert
@ -4747,7 +4777,11 @@ package body Einfo is
or else Ekind (Id) = E_Discriminant
or else Ekind (Id) = E_Exception
or else Ekind (Id) = E_Package_Body
or else Ekind (Id) = E_Subprogram_Body);
or else Ekind (Id) = E_Subprogram_Body
-- Allow this attribute to appear on non-analyzed entities
or else Ekind (Id) = E_Void);
Set_Flag277 (Id, V);
end Set_Is_Checked_Ghost_Entity;
@ -4942,7 +4976,11 @@ package body Einfo is
or else Ekind (Id) = E_Discriminant
or else Ekind (Id) = E_Exception
or else Ekind (Id) = E_Package_Body
or else Ekind (Id) = E_Subprogram_Body);
or else Ekind (Id) = E_Subprogram_Body
-- Allow this attribute to appear on non-analyzed entities
or else Ekind (Id) = E_Void);
Set_Flag278 (Id, V);
end Set_Is_Ignored_Ghost_Entity;
@ -8371,6 +8409,7 @@ package body Einfo is
W ("C_Pass_By_Copy", Flag125 (Id));
W ("Can_Never_Be_Null", Flag38 (Id));
W ("Checks_May_Be_Suppressed", Flag31 (Id));
W ("Contains_Ignored_Ghost_Code", Flag279 (Id));
W ("Debug_Info_Off", Flag166 (Id));
W ("Default_Expressions_Processed", Flag108 (Id));
W ("Delay_Cleanups", Flag114 (Id));

21
gcc/ada/einfo.ads
View File

@ -661,6 +661,11 @@ package Einfo is
-- Component_Type (Node20) [implementation base type only]
-- Defined in array types and string types. References component type.
-- Contains_Ignored_Ghost_Code (Flag279)
-- Defined in blocks, packages and their bodies, subprograms and their
-- bodies. Set if the entity contains any ignored Ghost code in the form
-- of declaration, procedure call, assignment statement or pragma.
-- Corresponding_Concurrent_Type (Node18)
-- Defined in record types that are constructed by the expander to
-- represent task and protected types (Is_Concurrent_Record_Type flag
@ -5458,6 +5463,7 @@ package Einfo is
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Entry_Cancel_Parameter (Node23)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
-- Has_Master_Entity (Flag21)
@ -5531,8 +5537,8 @@ package Einfo is
-- Has_Biased_Representation (Flag139)
-- Has_Completion (Flag26) (constants only)
-- Has_Independent_Components (Flag34)
-- Has_Thunks (Flag228) (constants only)
-- Has_Size_Clause (Flag29)
-- Has_Thunks (Flag228) (constants only)
-- Has_Up_Level_Access (Flag215)
-- Has_Volatile_Components (Flag87)
-- Is_Atomic (Flag85)
@ -5709,11 +5715,12 @@ package Einfo is
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Body_Needed_For_SAL (Flag40)
-- Elaboration_Entity_Required (Flag174)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Default_Expressions_Processed (Flag108)
-- Delay_Cleanups (Flag114)
-- Delay_Subprogram_Descriptors (Flag50)
-- Discard_Names (Flag88)
-- Elaboration_Entity_Required (Flag174)
-- Has_Anonymous_Master (Flag253)
-- Has_Completion (Flag26)
-- Has_Controlling_Result (Flag98)
@ -5921,6 +5928,7 @@ package Einfo is
-- Contract (Node34)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Discard_Names (Flag88)
-- Elaboration_Entity_Required (Flag174)
-- Elaborate_Body_Desirable (Flag210) (non-generic case only)
@ -5955,6 +5963,7 @@ package Einfo is
-- SPARK_Aux_Pragma (Node33)
-- SPARK_Pragma (Node32)
-- Contract (Node34)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
-- Has_Anonymous_Master (Flag253)
-- SPARK_Aux_Pragma_Inherited (Flag266)
@ -6005,6 +6014,7 @@ package Einfo is
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Body_Needed_For_SAL (Flag40)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
-- Elaboration_Entity_Required (Flag174)
@ -6174,8 +6184,9 @@ package Einfo is
-- Scope_Depth_Value (Uint22)
-- Extra_Formals (Node28)
-- SPARK_Pragma (Node32)
-- SPARK_Pragma_Inherited (Flag265)
-- Contract (Node34)
-- Contains_Ignored_Ghost_Code (Flag279)
-- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
-- E_Subprogram_Type
@ -6527,6 +6538,7 @@ package Einfo is
function Component_Clause (Id : E) return N;
function Component_Size (Id : E) return U;
function Component_Type (Id : E) return E;
function Contains_Ignored_Ghost_Code (Id : E) return B;
function Contract (Id : E) return N;
function Corresponding_Concurrent_Type (Id : E) return E;
function Corresponding_Discriminant (Id : E) return E;
@ -7168,6 +7180,7 @@ package Einfo is
procedure Set_Component_Clause (Id : E; V : N);
procedure Set_Component_Size (Id : E; V : U);
procedure Set_Component_Type (Id : E; V : E);
procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True);
procedure Set_Contract (Id : E; V : N);
procedure Set_Corresponding_Concurrent_Type (Id : E; V : E);
procedure Set_Corresponding_Discriminant (Id : E; V : E);
@ -7924,6 +7937,7 @@ package Einfo is
pragma Inline (Component_Clause);
pragma Inline (Component_Size);
pragma Inline (Component_Type);
pragma Inline (Contains_Ignored_Ghost_Code);
pragma Inline (Contract);
pragma Inline (Corresponding_Concurrent_Type);
pragma Inline (Corresponding_Discriminant);
@ -8413,6 +8427,7 @@ package Einfo is
pragma Inline (Set_Component_Clause);
pragma Inline (Set_Component_Size);
pragma Inline (Set_Component_Type);
pragma Inline (Set_Contains_Ignored_Ghost_Code);
pragma Inline (Set_Contract);
pragma Inline (Set_Corresponding_Concurrent_Type);
pragma Inline (Set_Corresponding_Discriminant);

30
gcc/ada/exp_ch3.adb
View File

@ -43,6 +43,7 @@ with Exp_Strm; use Exp_Strm;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
@ -7427,11 +7428,37 @@ package body Exp_Ch3 is
-- node using Append_Freeze_Actions.
function Freeze_Type (N : Node_Id) return Boolean is
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Save the current Ghost mode in effect in case the type being frozen
-- sets a different mode.
procedure Restore_Globals;
-- Restore the values of all saved global variables
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-- Local variables
Def_Id : constant Entity_Id := Entity (N);
RACW_Seen : Boolean := False;
Result : Boolean := False;
-- Start of processing for Freeze_Type
begin
-- The type being frozen may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- freezing are properly flagged as ignored Ghost.
Set_Ghost_Mode_For_Freeze (Def_Id, N);
-- Process associated access types needing special processing
if Present (Access_Types_To_Process (N)) then
@ -7750,10 +7777,13 @@ package body Exp_Ch3 is
end if;
Freeze_Stream_Operations (N, Def_Id);
Restore_Globals;
return Result;
exception
when RE_Not_Available =>
Restore_Globals;
return False;
end Freeze_Type;

63
gcc/ada/exp_ch7.adb
View File

@ -1741,13 +1741,19 @@ package body Exp_Ch7 is
if Nkind (Decl) = N_Full_Type_Declaration then
Typ := Defining_Identifier (Decl);
if Is_Tagged_Type (Typ)
-- Ignored Ghost types do not need any cleanup actions because
-- they will not appear in the final tree.
if Is_Ignored_Ghost_Entity (Typ) then
null;
elsif Is_Tagged_Type (Typ)
and then Is_Library_Level_Entity (Typ)
and then Convention (Typ) = Convention_Ada
and then Present (Access_Disp_Table (Typ))
and then RTE_Available (RE_Register_Tag)
and then not No_Run_Time_Mode
and then not Is_Abstract_Type (Typ)
and then not No_Run_Time_Mode
then
Processing_Actions;
end if;
@ -1773,6 +1779,12 @@ package body Exp_Ch7 is
elsif Is_Processed_Transient (Obj_Id) then
null;
-- Ignored Ghost objects do not need any cleanup actions
-- because they will not appear in the final tree.
elsif Is_Ignored_Ghost_Entity (Obj_Id) then
null;
-- The object is of the form:
-- Obj : Typ [:= Expr];
@ -1880,6 +1892,12 @@ package body Exp_Ch7 is
if For_Package and then Finalize_Storage_Only (Obj_Typ) then
null;
-- Ignored Ghost object renamings do not need any cleanup
-- actions because they will not appear in the final tree.
elsif Is_Ignored_Ghost_Entity (Obj_Id) then
null;
-- Return object of a build-in-place function. This case is
-- recognized and marked by the expansion of an extended return
-- statement (see Expand_N_Extended_Return_Statement).
@ -1921,11 +1939,17 @@ package body Exp_Ch7 is
then
Typ := Entity (Decl);
if (Is_Access_Type (Typ)
and then not Is_Access_Subprogram_Type (Typ)
and then Needs_Finalization
(Available_View (Designated_Type (Typ))))
or else (Is_Type (Typ) and then Needs_Finalization (Typ))
-- Freeze nodes for ignored Ghost types do not need cleanup
-- actions because they will never appear in the final tree.
if Is_Ignored_Ghost_Entity (Typ) then
null;
elsif (Is_Access_Type (Typ)
and then not Is_Access_Subprogram_Type (Typ)
and then Needs_Finalization
(Available_View (Designated_Type (Typ))))
or else (Is_Type (Typ) and then Needs_Finalization (Typ))
then
Old_Counter_Val := Counter_Val;
@ -1950,14 +1974,16 @@ package body Exp_Ch7 is
-- Nested package declarations, avoid generics
elsif Nkind (Decl) = N_Package_Declaration then
Spec := Specification (Decl);
Pack_Id := Defining_Unit_Name (Spec);
Pack_Id := Defining_Entity (Decl);
Spec := Specification (Decl);
if Nkind (Pack_Id) = N_Defining_Program_Unit_Name then
Pack_Id := Defining_Identifier (Pack_Id);
end if;
-- Do not inspect an ignored Ghost package because all code
-- found within will not appear in the final tree.
if Ekind (Pack_Id) /= E_Generic_Package then
if Is_Ignored_Ghost_Entity (Pack_Id) then
null;
elsif Ekind (Pack_Id) /= E_Generic_Package then
Old_Counter_Val := Counter_Val;
Process_Declarations
(Private_Declarations (Spec), Preprocess);
@ -1980,9 +2006,16 @@ package body Exp_Ch7 is
-- Nested package bodies, avoid generics
elsif Nkind (Decl) = N_Package_Body then
Spec := Corresponding_Spec (Decl);
if Ekind (Spec) /= E_Generic_Package then
-- Do not inspect an ignored Ghost package body because all
-- code found within will not appear in the final tree.
if Is_Ignored_Ghost_Entity (Defining_Entity (Decl)) then
null;
elsif Ekind (Corresponding_Spec (Decl)) /=
E_Generic_Package
then
Old_Counter_Val := Counter_Val;
Process_Declarations (Declarations (Decl), Preprocess);

16
gcc/ada/exp_dbug.adb
View File

@ -1101,10 +1101,21 @@ package body Exp_Dbug is
procedure Qualify_All_Entity_Names is
E : Entity_Id;
Ent : Entity_Id;
Nod : Node_Id;
begin
for J in Name_Qualify_Units.First .. Name_Qualify_Units.Last loop
E := Defining_Entity (Name_Qualify_Units.Table (J));
Nod := Name_Qualify_Units.Table (J);
-- When a scoping construct is ignored Ghost, it is rewritten as
-- a null statement. Skip such constructs as they no longer carry
-- names.
if Nkind (Nod) = N_Null_Statement then
goto Continue;
end if;
E := Defining_Entity (Nod);
Reset_Buffers;
Qualify_Entity_Name (E);
@ -1128,6 +1139,9 @@ package body Exp_Dbug is
exit when Ent = E;
end loop;
end if;
<<Continue>>
null;
end loop;
end Qualify_All_Entity_Names;

30
gcc/ada/exp_disp.adb
View File

@ -36,6 +36,7 @@ with Exp_Dbug; use Exp_Dbug;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Itypes; use Itypes;
with Layout; use Layout;
with Nlists; use Nlists;
@ -3663,6 +3664,10 @@ package body Exp_Disp is
-- end;
function Make_DT (Typ : Entity_Id; N : Node_Id := Empty) return List_Id is
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Save the current Ghost mode in effect in case the tagged type sets a
-- different mode.
Loc : constant Source_Ptr := Sloc (Typ);
Max_Predef_Prims : constant Int :=
@ -3725,6 +3730,9 @@ package body Exp_Disp is
-- this secondary dispatch table by Make_Tags when its unique external
-- name was generated.
procedure Restore_Globals;
-- Restore the values of all saved global variables
------------------------------
-- Check_Premature_Freezing --
------------------------------
@ -4409,6 +4417,15 @@ package body Exp_Disp is
Append_Elmt (Iface_DT, DT_Decl);
end Make_Secondary_DT;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-- Local variables
Elab_Code : constant List_Id := New_List;
@ -4479,6 +4496,13 @@ package body Exp_Disp is
begin
pragma Assert (Is_Frozen (Typ));
-- The tagged type for which the dispatch table is being build may be
-- subject to pragma Ghost with policy Ignore. Set the mode now to
-- ensure that any nodes generated during freezing are properly flagged
-- as ignored Ghost.
Set_Ghost_Mode_For_Freeze (Typ, Typ);
-- Handle cases in which there is no need to build the dispatch table
if Has_Dispatch_Table (Typ)
@ -4487,10 +4511,12 @@ package body Exp_Disp is
or else Convention (Typ) = Convention_CIL
or else Convention (Typ) = Convention_Java
then
Restore_Globals;
return Result;
elsif No_Run_Time_Mode then
Error_Msg_CRT ("tagged types", Typ);
Restore_Globals;
return Result;
elsif not RTE_Available (RE_Tag) then
@ -4506,6 +4532,7 @@ package body Exp_Disp is
Analyze_List (Result, Suppress => All_Checks);
Error_Msg_CRT ("tagged types", Typ);
Restore_Globals;
return Result;
end if;
@ -4516,12 +4543,14 @@ package body Exp_Disp is
if RTE_Available (RE_Interface_Data) then
if Max_Predef_Prims /= 15 then
Error_Msg_N ("run-time library configuration error", Typ);
Restore_Globals;
return Result;
end if;
else
if Max_Predef_Prims /= 9 then
Error_Msg_N ("run-time library configuration error", Typ);
Error_Msg_CRT ("tagged types", Typ);
Restore_Globals;
return Result;
end if;
end if;
@ -6242,6 +6271,7 @@ package body Exp_Disp is
Register_CG_Node (Typ);
Restore_Globals;
return Result;
end Make_DT;

84
gcc/ada/exp_util.adb
View File

@ -7830,13 +7830,19 @@ package body Exp_Util is
if Nkind (Decl) = N_Full_Type_Declaration then
Typ := Defining_Identifier (Decl);
if Is_Tagged_Type (Typ)
-- Ignored Ghost types do not need any cleanup actions because
-- they will not appear in the final tree.
if Is_Ignored_Ghost_Entity (Typ) then
null;
elsif Is_Tagged_Type (Typ)
and then Is_Library_Level_Entity (Typ)
and then Convention (Typ) = Convention_Ada
and then Present (Access_Disp_Table (Typ))
and then RTE_Available (RE_Unregister_Tag)
and then not No_Run_Time_Mode
and then not Is_Abstract_Type (Typ)
and then not No_Run_Time_Mode
then
return True;
end if;
@ -7862,6 +7868,12 @@ package body Exp_Util is
elsif Is_Processed_Transient (Obj_Id) then
null;
-- Ignored Ghost objects do not need any cleanup actions because
-- they will not appear in the final tree.
elsif Is_Ignored_Ghost_Entity (Obj_Id) then
null;
-- The object is of the form:
-- Obj : Typ [:= Expr];
--
@ -7940,6 +7952,12 @@ package body Exp_Util is
if Lib_Level and then Finalize_Storage_Only (Obj_Typ) then
null;
-- Ignored Ghost object renamings do not need any cleanup actions
-- because they will not appear in the final tree.
elsif Is_Ignored_Ghost_Entity (Obj_Id) then
null;
-- Return object of a build-in-place function. This case is
-- recognized and marked by the expansion of an extended return
-- statement (see Expand_N_Extended_Return_Statement).
@ -7981,11 +7999,17 @@ package body Exp_Util is
then
Typ := Entity (Decl);
if ((Is_Access_Type (Typ)
and then not Is_Access_Subprogram_Type (Typ)
and then Needs_Finalization
(Available_View (Designated_Type (Typ))))
or else (Is_Type (Typ) and then Needs_Finalization (Typ)))
-- Freeze nodes for ignored Ghost types do not need cleanup
-- actions because they will never appear in the final tree.
if Is_Ignored_Ghost_Entity (Typ) then
null;
elsif ((Is_Access_Type (Typ)
and then not Is_Access_Subprogram_Type (Typ)
and then Needs_Finalization
(Available_View (Designated_Type (Typ))))
or else (Is_Type (Typ) and then Needs_Finalization (Typ)))
and then Requires_Cleanup_Actions
(Actions (Decl), Lib_Level, Nested_Constructs)
then
@ -7997,15 +8021,17 @@ package body Exp_Util is
elsif Nested_Constructs
and then Nkind (Decl) = N_Package_Declaration
then
Pack_Id := Defining_Unit_Name (Specification (Decl));
Pack_Id := Defining_Entity (Decl);
if Nkind (Pack_Id) = N_Defining_Program_Unit_Name then
Pack_Id := Defining_Identifier (Pack_Id);
end if;
-- Do not inspect an ignored Ghost package because all code found
-- within will not appear in the final tree.
if Ekind (Pack_Id) /= E_Generic_Package
and then
Requires_Cleanup_Actions (Specification (Decl), Lib_Level)
if Is_Ignored_Ghost_Entity (Pack_Id) then
null;
elsif Ekind (Pack_Id) /= E_Generic_Package
and then Requires_Cleanup_Actions
(Specification (Decl), Lib_Level)
then
return True;
end if;
@ -8013,13 +8039,39 @@ package body Exp_Util is
-- Nested package bodies
elsif Nested_Constructs and then Nkind (Decl) = N_Package_Body then
Pack_Id := Corresponding_Spec (Decl);
if Ekind (Pack_Id) /= E_Generic_Package
-- Do not inspect an ignored Ghost package body because all code
-- found within will not appear in the final tree.
if Is_Ignored_Ghost_Entity (Defining_Entity (Decl)) then
null;
elsif Ekind (Corresponding_Spec (Decl)) /= E_Generic_Package
and then Requires_Cleanup_Actions (Decl, Lib_Level)
then
return True;
end if;
elsif Nkind (Decl) = N_Block_Statement
and then
-- Handle a rare case caused by a controlled transient variable
-- created as part of a record init proc. The variable is wrapped
-- in a block, but the block is not associated with a transient
-- scope.
(Inside_Init_Proc
-- Handle the case where the original context has been wrapped in
-- a block to avoid interference between exception handlers and
-- At_End handlers. Treat the block as transparent and process its
-- contents.
or else Is_Finalization_Wrapper (Decl))
then
if Requires_Cleanup_Actions (Decl, Lib_Level) then
return True;
end if;
end if;
Next (Decl);

57
gcc/ada/freeze.adb
View File

@ -36,6 +36,7 @@ with Exp_Disp; use Exp_Disp;
with Exp_Pakd; use Exp_Pakd;
with Exp_Util; use Exp_Util;
with Exp_Tss; use Exp_Tss;
with Ghost; use Ghost;
with Layout; use Layout;
with Lib; use Lib;
with Namet; use Namet;
@ -1862,12 +1863,16 @@ package body Freeze is
-------------------
function Freeze_Entity (E : Entity_Id; N : Node_Id) return List_Id is
Loc : constant Source_Ptr := Sloc (N);
Comp : Entity_Id;
F_Node : Node_Id;
Indx : Node_Id;
Formal : Entity_Id;
Atype : Entity_Id;
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Save the current Ghost mode in effect in case the entity being frozen
-- sets a different mode.
Loc : constant Source_Ptr := Sloc (N);
Atype : Entity_Id;
Comp : Entity_Id;
F_Node : Node_Id;
Formal : Entity_Id;
Indx : Node_Id;
Test_E : Entity_Id := E;
-- This could use a comment ???
@ -1929,6 +1934,9 @@ package body Freeze is
-- call, but rather must go in the package holding the function, so that
-- the backend can process it in the proper context.
procedure Restore_Globals;
-- Restore the values of all saved global variables
procedure Wrap_Imported_Subprogram (E : Entity_Id);
-- If E is an entity for an imported subprogram with pre/post-conditions
-- then this procedure will create a wrapper to ensure that proper run-
@ -4125,6 +4133,15 @@ package body Freeze is
Append_List (Result, Decls);
end Late_Freeze_Subprogram;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
------------------------------
-- Wrap_Imported_Subprogram --
------------------------------
@ -4271,6 +4288,12 @@ package body Freeze is
-- Start of processing for Freeze_Entity
begin
-- The entity being frozen may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- freezing are properly flagged as ignored Ghost.
Set_Ghost_Mode_For_Freeze (E, N);
-- We are going to test for various reasons why this entity need not be
-- frozen here, but in the case of an Itype that's defined within a
-- record, that test actually applies to the record.
@ -4286,6 +4309,7 @@ package body Freeze is
-- Do not freeze if already frozen since we only need one freeze node
if Is_Frozen (E) then
Restore_Globals;
return No_List;
-- It is improper to freeze an external entity within a generic because
@ -4300,6 +4324,7 @@ package body Freeze is
Analyze_Aspects_At_Freeze_Point (E);
end if;
Restore_Globals;
return No_List;
-- AI05-0213: A formal incomplete type does not freeze the actual. In
@ -4310,16 +4335,19 @@ package body Freeze is
and then No (Full_View (Base_Type (E)))
and then Ada_Version >= Ada_2012
then
Restore_Globals;
return No_List;
-- Formal subprograms are never frozen
elsif Is_Formal_Subprogram (E) then
Restore_Globals;
return No_List;
-- Generic types are never frozen as they lack delayed semantic checks
elsif Is_Generic_Type (E) then
Restore_Globals;
return No_List;
-- Do not freeze a global entity within an inner scope created during
@ -4353,6 +4381,7 @@ package body Freeze is
then
exit;
else
Restore_Globals;
return No_List;
end if;
end if;
@ -4388,12 +4417,16 @@ package body Freeze is
end loop;
if No (S) then
Restore_Globals;
return No_List;
end if;
end;
elsif Ekind (E) = E_Generic_Package then
return Freeze_Generic_Entities (E);
Result := Freeze_Generic_Entities (E);
Restore_Globals;
return Result;
end if;
-- Add checks to detect proper initialization of scalars that may appear
@ -4475,6 +4508,7 @@ package body Freeze is
if not Is_Internal (E) then
if not Freeze_Profile (E) then
Restore_Globals;
return Result;
end if;
end if;
@ -4499,6 +4533,7 @@ package body Freeze is
if Late_Freezing then
Late_Freeze_Subprogram (E);
Restore_Globals;
return No_List;
end if;
@ -4830,6 +4865,7 @@ package body Freeze is
and then not Has_Delayed_Freeze (E))
then
Check_Compile_Time_Size (E);
Restore_Globals;
return No_List;
end if;
@ -5102,6 +5138,7 @@ package body Freeze is
if not Is_Frozen (Root_Type (E)) then
Set_Is_Frozen (E, False);
Restore_Globals;
return Result;
end if;
@ -5237,6 +5274,7 @@ package body Freeze is
and then not Present (Full_View (E))
then
Set_Is_Frozen (E, False);
Restore_Globals;
return Result;
-- Case of full view present
@ -5328,6 +5366,7 @@ package body Freeze is
Set_RM_Size (E, RM_Size (Full_View (E)));
end if;
Restore_Globals;
return Result;
-- Case of underlying full view present
@ -5357,6 +5396,7 @@ package body Freeze is
Check_Debug_Info_Needed (E);
Restore_Globals;
return Result;
-- Case of no full view present. If entity is derived or subtype,
@ -5370,6 +5410,7 @@ package body Freeze is
else
Set_Is_Frozen (E, False);
Restore_Globals;
return No_List;
end if;
@ -5418,6 +5459,7 @@ package body Freeze is
-- generic processing), so we never need freeze nodes for them.
if Is_Generic_Type (E) then
Restore_Globals;
return Result;
end if;
@ -6033,6 +6075,7 @@ package body Freeze is
end if;
end if;
Restore_Globals;
return Result;
end Freeze_Entity;

10
gcc/ada/frontend.adb
View File

@ -33,6 +33,7 @@ with Elists;
with Exp_Dbug;
with Fmap;
with Fname.UF;
with Ghost; use Ghost;
with Inline; use Inline;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
@ -421,14 +422,19 @@ begin
Analyze_Inlined_Bodies;
end if;
-- Remove entities from program that do not have any
-- execution time references.
-- Remove entities from program that do not have any execution
-- time references.
if Debug_Flag_UU then
Collect_Garbage_Entities;
end if;
Check_Elab_Calls;
-- Remove any ignored Ghost code as it must not appear in the
-- executable.
Remove_Ignored_Ghost_Code;
end if;
-- List library units if requested

1
gcc/ada/gcc-interface/Make-lang.in
View File

@ -297,6 +297,7 @@ GNAT_ADA_OBJS = \
ada/g-u3spch.o \
ada/get_spark_xrefs.o \
ada/get_targ.o \
ada/ghost.o \
ada/gnat.o \
ada/gnatvsn.o \
ada/hostparm.o \

949
gcc/ada/ghost.adb Normal file
View File

@ -0,0 +1,949 @@
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- G H O S T --
-- --
-- B o d y --
-- --
-- Copyright (C) 2014-2015, 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- --
-- 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. See the GNU General Public License --
-- for more details. You should have received a copy of the GNU General --
-- Public License distributed with GNAT; see file COPYING3. If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
with Alloc; use Alloc;
with Aspects; use Aspects;
with Atree; use Atree;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Opt; use Opt;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Eval; use Sem_Eval;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Snames; use Snames;
with Table;
package body Ghost is
-- The following table contains the N_Compilation_Unit node for a unit that
-- is either subject to pragma Ghost with policy Ignore or contains ignored
-- Ghost code. The table is used in the removal of ignored Ghost code from
-- units.
package Ignored_Ghost_Units is new Table.Table (
Table_Component_Type => Node_Id,
Table_Index_Type => Int,
Table_Low_Bound => 0,
Table_Initial => Alloc.Ignored_Ghost_Units_Initial,
Table_Increment => Alloc.Ignored_Ghost_Units_Increment,
Table_Name => "Ignored_Ghost_Units");
-----------------------
-- Local Subprograms --
-----------------------
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
-- Subsidiary to Set_Ghost_Mode_xxx. Signal all enclosing scopes that they
-- now contain ignored Ghost code. Add the compilation unit containing N to
-- table Ignored_Ghost_Units for post processing.
----------------------------
-- Add_Ignored_Ghost_Unit --
----------------------------
procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is
begin
pragma Assert (Nkind (Unit) = N_Compilation_Unit);
-- Avoid duplicates in the table as pruning the same unit more than once
-- is wasteful. Since ignored Ghost code tends to be grouped up, check
-- the contents of the table in reverse.
for Index in reverse Ignored_Ghost_Units.First ..
Ignored_Ghost_Units.Last
loop
-- The unit is already present in the table, do not add it again
if Unit = Ignored_Ghost_Units.Table (Index) then
return;
end if;
end loop;
-- If we get here, then this is the first time the unit is being added
Ignored_Ghost_Units.Append (Unit);
end Add_Ignored_Ghost_Unit;
----------------------------
-- Check_Ghost_Completion --
----------------------------
procedure Check_Ghost_Completion
(Partial_View : Entity_Id;
Full_View : Entity_Id)
is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Partial_View)
and then Policy = Name_Ignore
then
Error_Msg_Sloc := Sloc (Full_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Check", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
end if;
end Check_Ghost_Completion;
-------------------------
-- Check_Ghost_Context --
-------------------------
procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
-- Verify that the Ghost policy at the point of declaration of entity Id
-- matches the policy at the point of reference. If this is not the case
-- emit an error at Err_N.
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
-- Determine whether node Context denotes a Ghost-friendly context where
-- a Ghost entity can safely reside.
-------------------------
-- Is_OK_Ghost_Context --
-------------------------
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
-- Determine whether node Decl is a Ghost declaration or appears
-- within a Ghost declaration.
function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
-- Determine whether statement or pragma N is Ghost or appears within
-- a Ghost statement or pragma. To qualify as such, N must either
-- 1) Occur within a ghost subprogram or package
-- 2) Denote a call to a ghost procedure
-- 3) Denote an assignment statement whose target is a ghost
-- variable.
-- 4) Denote a pragma that mentions a ghost entity
--------------------------
-- Is_Ghost_Declaration --
--------------------------
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
Par : Node_Id;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
begin
-- Climb the parent chain looking for an object declaration
Par := Decl;
while Present (Par) loop
if Is_Declaration (Par) then
-- A declaration is Ghost when it appears within a Ghost
-- package or subprogram.
if Ghost_Mode > None then
return True;
-- Otherwise the declaration may not have been analyzed yet,
-- determine whether it is subject to aspect/pragma Ghost.
else
return Is_Subject_To_Ghost (Par);
end if;
-- Special cases
-- A reference to a Ghost entity may appear as the default
-- expression of a formal parameter of a subprogram body. This
-- context must be treated as suitable because the relation
-- between the spec and the body has not been established and
-- the body is not marked as Ghost yet. The real check was
-- performed on the spec.
elsif Nkind (Par) = N_Parameter_Specification
and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
then
return True;
-- References to Ghost entities may be relocated in internally
-- generated bodies.
elsif Nkind (Par) = N_Subprogram_Body
and then not Comes_From_Source (Par)
then
Subp_Id := Corresponding_Spec (Par);
-- The original context is an expression function that has
-- been split into a spec and a body. The context is OK as
-- long as the the initial declaration is Ghost.
if Present (Subp_Id) then
Subp_Decl :=
Original_Node (Unit_Declaration_Node (Subp_Id));
if Nkind (Subp_Decl) = N_Expression_Function then
return Is_Subject_To_Ghost (Subp_Decl);
end if;
end if;
-- Otherwise this is either an internal body or an internal
-- completion. Both are OK because the real check was done
-- before expansion activities.
return True;
end if;
-- Prevent the search from going too far
if Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Par := Parent (Par);
end loop;
return False;
end Is_Ghost_Declaration;
----------------------------------
-- Is_Ghost_Statement_Or_Pragma --
----------------------------------
function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a reference to a
-- Ghost entity.
-------------------------------
-- Is_Ghost_Entity_Reference --
-------------------------------
function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
Ref : Node_Id;
begin
Ref := N;
-- When the reference extracts a subcomponent, recover the
-- related object (SPARK RM 6.9(1)).
while Nkind_In (Ref, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Ref := Prefix (Ref);
end loop;
return
Is_Entity_Name (Ref)
and then Present (Entity (Ref))
and then Is_Ghost_Entity (Entity (Ref));
end Is_Ghost_Entity_Reference;
-- Local variables
Arg : Node_Id;
Stmt : Node_Id;
-- Start of processing for Is_Ghost_Statement_Or_Pragma
begin
if Nkind (N) = N_Pragma then
-- A pragma is Ghost when it appears within a Ghost package or
-- subprogram.
if Ghost_Mode > None then
return True;
end if;
-- A pragma is Ghost when it mentions a Ghost entity
Arg := First (Pragma_Argument_Associations (N));
while Present (Arg) loop
if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
return True;
end if;
Next (Arg);
end loop;
end if;
Stmt := N;
while Present (Stmt) loop
if Is_Statement (Stmt) then
-- A statement is Ghost when it appears within a Ghost
-- package or subprogram.
if Ghost_Mode > None then
return True;
-- An assignment statement or a procedure call is Ghost when
-- the name denotes a Ghost entity.
elsif Nkind_In (Stmt, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
return Is_Ghost_Entity_Reference (Name (Stmt));
end if;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Stmt) then
return False;
end if;
Stmt := Parent (Stmt);
end loop;
return False;
end Is_Ghost_Statement_Or_Pragma;
-- Start of processing for Is_OK_Ghost_Context
begin
-- The Ghost entity appears within an assertion expression
if In_Assertion_Expr > 0 then
return True;
-- The Ghost entity is part of a declaration or its completion
elsif Is_Ghost_Declaration (Context) then
return True;
-- The Ghost entity is referenced within a Ghost statement
elsif Is_Ghost_Statement_Or_Pragma (Context) then
return True;
-- Routine Expand_Record_Extension creates a parent subtype without
-- inserting it into the tree. There is no good way of recognizing
-- this special case as there is no parent. Try to approximate the
-- context.
elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
return True;
else
return False;
end if;
end Is_OK_Ghost_Context;
------------------------
-- Check_Ghost_Policy --
------------------------
procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- The Ghost policy in effect a the point of declaration and at the
-- point of use must match (SPARK RM 6.9(14)).
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
end if;
end Check_Ghost_Policy;
-- Start of processing for Check_Ghost_Context
begin
-- Once it has been established that the reference to the Ghost entity
-- is within a suitable context, ensure that the policy at the point of
-- declaration and at the point of use match.
if Is_OK_Ghost_Context (Ghost_Ref) then
Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
-- Otherwise the Ghost entity appears in a non-Ghost context and affects
-- its behavior or value.
else
Error_Msg_N
("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
Ghost_Ref);
end if;
end Check_Ghost_Context;
----------------------------
-- Check_Ghost_Derivation --
----------------------------
procedure Check_Ghost_Derivation (Typ : Entity_Id) is
Parent_Typ : constant Entity_Id := Etype (Typ);
Iface : Entity_Id;
Iface_Elmt : Elmt_Id;
begin
-- Allow untagged derivations from predefined types such as Integer as
-- those are not Ghost by definition.
if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
null;
-- The parent type of a Ghost type extension must be Ghost
elsif not Is_Ghost_Entity (Parent_Typ) then
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
return;
end if;
-- All progenitors (if any) must be Ghost as well
if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
Iface_Elmt := First_Elmt (Interfaces (Typ));
while Present (Iface_Elmt) loop
Iface := Node (Iface_Elmt);
if not Is_Ghost_Entity (Iface) then
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
return;
end if;
Next_Elmt (Iface_Elmt);
end loop;
end if;
end Check_Ghost_Derivation;
--------------------------------
-- Implements_Ghost_Interface --
--------------------------------
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
Iface_Elmt : Elmt_Id;
begin
-- Traverse the list of interfaces looking for a Ghost interface
if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
Iface_Elmt := First_Elmt (Interfaces (Typ));
while Present (Iface_Elmt) loop
if Is_Ghost_Entity (Node (Iface_Elmt)) then
return True;
end if;
Next_Elmt (Iface_Elmt);
end loop;
end if;
return False;
end Implements_Ghost_Interface;
----------------
-- Initialize --
----------------
procedure Initialize is
begin
Ignored_Ghost_Units.Init;
end Initialize;
---------------------
-- Is_Ghost_Entity --
---------------------
function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
begin
return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
end Is_Ghost_Entity;
-------------------------
-- Is_Subject_To_Ghost --
-------------------------
function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
function Enables_Ghostness (Arg : Node_Id) return Boolean;
-- Determine whether aspect or pragma argument Arg enables "ghostness"
-----------------------
-- Enables_Ghostness --
-----------------------
function Enables_Ghostness (Arg : Node_Id) return Boolean is
Expr : Node_Id;
begin
Expr := Arg;
if Nkind (Expr) = N_Pragma_Argument_Association then
Expr := Get_Pragma_Arg (Expr);
end if;
-- Determine whether the expression of the aspect is static and
-- denotes True.
if Present (Expr) then
Preanalyze_And_Resolve (Expr);
return
Is_OK_Static_Expression (Expr)
and then Is_True (Expr_Value (Expr));
-- Otherwise Ghost defaults to True
else
return True;
end if;
end Enables_Ghostness;
-- Local variables
Id : constant Entity_Id := Defining_Entity (N);
Asp : Node_Id;
Decl : Node_Id;
Prev_Id : Entity_Id;
-- Start of processing for Is_Subject_To_Ghost
begin
-- The related entity of the declaration has not been analyzed yet, do
-- not inspect its attributes.
if Ekind (Id) = E_Void then
null;
elsif Is_Ghost_Entity (Id) then
return True;
-- The completion of a type or a constant is not fully analyzed when the
-- reference to the Ghost entity is resolved. Because the completion is
-- not marked as Ghost yet, inspect the partial view.
elsif Is_Record_Type (Id)
or else Ekind (Id) = E_Constant
or else (Nkind (N) = N_Object_Declaration
and then Constant_Present (N))
then
Prev_Id := Incomplete_Or_Partial_View (Id);
if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
return True;
end if;
end if;
-- Examine the aspect specifications (if any) looking for aspect Ghost
if Permits_Aspect_Specifications (N) then
Asp := First (Aspect_Specifications (N));
while Present (Asp) loop
if Chars (Identifier (Asp)) = Name_Ghost then
return Enables_Ghostness (Expression (Asp));
end if;
Next (Asp);
end loop;
end if;
Decl := Empty;
-- When the context is a [generic] package declaration, pragma Ghost
-- resides in the visible declarations.
if Nkind_In (N, N_Generic_Package_Declaration,
N_Package_Declaration)
then
Decl := First (Visible_Declarations (Specification (N)));
-- When the context is a package or a subprogram body, pragma Ghost
-- resides in the declarative part.
elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
Decl := First (Declarations (N));
-- Otherwise pragma Ghost appears in the declarations following N
elsif Is_List_Member (N) then
Decl := Next (N);
end if;
while Present (Decl) loop
if Nkind (Decl) = N_Pragma
and then Pragma_Name (Decl) = Name_Ghost
then
return
Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
-- A source construct ends the region where pragma Ghost may appear,
-- stop the traversal.
elsif Comes_From_Source (Decl) then
exit;
end if;
Next (Decl);
end loop;
return False;
end Is_Subject_To_Ghost;
----------
-- Lock --
----------
procedure Lock is
begin
Ignored_Ghost_Units.Locked := True;
Ignored_Ghost_Units.Release;
end Lock;
----------------------------------
-- Propagate_Ignored_Ghost_Code --
----------------------------------
procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is
Nod : Node_Id;
Scop : Entity_Id;
begin
-- Traverse the parent chain looking for blocks, packages and
-- subprograms or their respective bodies.
Nod := Parent (N);
while Present (Nod) loop
Scop := Empty;
if Nkind (Nod) = N_Block_Statement then
Scop := Entity (Identifier (Nod));
elsif Nkind_In (Nod, N_Package_Body,
N_Package_Declaration,
N_Subprogram_Body,
N_Subprogram_Declaration)
then
Scop := Defining_Entity (Nod);
end if;
-- The current node denotes a scoping construct
if Present (Scop) then
-- Stop the traversal when the scope already contains ignored
-- Ghost code as all enclosing scopes have already been marked.
if Contains_Ignored_Ghost_Code (Scop) then
exit;
-- Otherwise mark this scope and keep climbing
else
Set_Contains_Ignored_Ghost_Code (Scop);
end if;
end if;
Nod := Parent (Nod);
end loop;
-- The unit containing the ignored Ghost code must be post processed
-- before invoking the back end.
Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N)));
end Propagate_Ignored_Ghost_Code;
-------------------------------
-- Remove_Ignored_Ghost_Code --
-------------------------------
procedure Remove_Ignored_Ghost_Code is
procedure Prune_Tree (Root : Node_Id);
-- Remove all code marked as ignored Ghost from the tree of denoted by
-- Root.
----------------
-- Prune_Tree --
----------------
procedure Prune_Tree (Root : Node_Id) is
procedure Prune (N : Node_Id);
-- Remove a given node from the tree by rewriting it into null
function Prune_Node (N : Node_Id) return Traverse_Result;
-- Determine whether node N denotes an ignored Ghost construct. If
-- this is the case, rewrite N as a null statement. See the body for
-- special cases.
-----------
-- Prune --
-----------
procedure Prune (N : Node_Id) is
begin
-- Destroy any aspects that may be associated with the node
if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
Remove_Aspects (N);
end if;
Rewrite (N, Make_Null_Statement (Sloc (N)));
end Prune;
----------------
-- Prune_Node --
----------------
function Prune_Node (N : Node_Id) return Traverse_Result is
Id : Entity_Id;
begin
-- The node is either declared as ignored Ghost or is a byproduct
-- of expansion. Destroy it and stop the traversal on this branch.
if Is_Ignored_Ghost_Node (N) then
Prune (N);
return Skip;
-- Scoping constructs such as blocks, packages, subprograms and
-- bodies offer some flexibility with respect to pruning.
elsif Nkind_In (N, N_Block_Statement,
N_Package_Body,
N_Package_Declaration,
N_Subprogram_Body,
N_Subprogram_Declaration)
then
if Nkind (N) = N_Block_Statement then
Id := Entity (Identifier (N));
else
Id := Defining_Entity (N);
end if;
-- The scoping construct contains both living and ignored Ghost
-- code, let the traversal prune all relevant nodes.
if Contains_Ignored_Ghost_Code (Id) then
return OK;
-- Otherwise the construct contains only living code and should
-- not be pruned.
else
return Skip;
end if;
-- Otherwise keep searching for ignored Ghost nodes
else
return OK;
end if;
end Prune_Node;
procedure Prune_Nodes is new Traverse_Proc (Prune_Node);
-- Start of processing for Prune_Tree
begin
Prune_Nodes (Root);
end Prune_Tree;
-- Start of processing for Remove_Ignored_Ghost_Code
begin
for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
end loop;
end Remove_Ignored_Ghost_Code;
--------------------
-- Set_Ghost_Mode --
--------------------
procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
-- Set the value of global variable Ghost_Mode depending on the mode of
-- entity Id.
procedure Set_Ghost_Mode_From_Policy;
-- Set the value of global variable Ghost_Mode depending on the current
-- Ghost policy in effect.
--------------------------------
-- Set_Ghost_Mode_From_Entity --
--------------------------------
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
begin
if Is_Checked_Ghost_Entity (Id) then
Ghost_Mode := Check;
elsif Is_Ignored_Ghost_Entity (Id) then
Ghost_Mode := Ignore;
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_From_Entity;
--------------------------------
-- Set_Ghost_Mode_From_Policy --
--------------------------------
procedure Set_Ghost_Mode_From_Policy is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
if Policy = Name_Check then
Ghost_Mode := Check;
elsif Policy = Name_Ignore then
Ghost_Mode := Ignore;
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_From_Policy;
-- Local variables
Nam : Node_Id;
-- Start of processing for Set_Ghost_Mode
begin
-- The input node denotes one of the many declaration kinds that may be
-- subject to pragma Ghost.
if Is_Declaration (N) then
if Is_Subject_To_Ghost (N) then
Set_Ghost_Mode_From_Policy;
-- The declaration denotes the completion of a deferred constant,
-- pragma Ghost appears on the partial declaration.
elsif Nkind (N) = N_Object_Declaration
and then Constant_Present (N)
and then Present (Prev_Id)
then
Set_Ghost_Mode_From_Entity (Prev_Id);
-- The declaration denotes the full view of a private type, pragma
-- Ghost appears on the partial declaration.
elsif Nkind (N) = N_Full_Type_Declaration
and then Is_Private_Type (Defining_Entity (N))
and then Present (Prev_Id)
then
Set_Ghost_Mode_From_Entity (Prev_Id);
end if;
-- The input denotes an assignment or a procedure call. In this case
-- the Ghost mode is dictated by the name of the construct.
elsif Nkind_In (N, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
Nam := Name (N);
-- When the reference extracts a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
while Nkind_In (Nam, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Nam := Prefix (Nam);
end loop;
if Is_Entity_Name (Nam)
and then Present (Entity (Nam))
then
Set_Ghost_Mode_From_Entity (Entity (Nam));
end if;
-- The input denotes a package or subprogram body
elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id))
or else Is_Subject_To_Ghost (N)
then
Set_Ghost_Mode_From_Policy;
end if;
end if;
end Set_Ghost_Mode;
-------------------------------
-- Set_Ghost_Mode_For_Freeze --
-------------------------------
procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is
begin
if Is_Checked_Ghost_Entity (Id) then
Ghost_Mode := Check;
elsif Is_Ignored_Ghost_Entity (Id) then
Ghost_Mode := Ignore;
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_For_Freeze;
-------------------------
-- Set_Is_Ghost_Entity --
-------------------------
procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
if Policy = Name_Check then
Set_Is_Checked_Ghost_Entity (Id);
elsif Policy = Name_Ignore then
Set_Is_Ignored_Ghost_Entity (Id);
end if;
end Set_Is_Ghost_Entity;
end Ghost;

115
gcc/ada/ghost.ads Normal file
View File

@ -0,0 +1,115 @@
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- G H O S T --
-- --
-- S p e c --
-- --
-- Copyright (C) 2014-2015, 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- --
-- 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. See the GNU General Public License --
-- for more details. You should have received a copy of the GNU General --
-- Public License distributed with GNAT; see file COPYING3. If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
-- This package contains routines that deal with the static and runtime
-- semantics of Ghost entities.
with Types; use Types;
package Ghost is
procedure Add_Ignored_Ghost_Unit (Unit : Node_Id);
-- Add a single ignored Ghost compilation unit to the internal table for
-- post processing.
procedure Check_Ghost_Completion
(Partial_View : Entity_Id;
Full_View : Entity_Id);
-- Verify that the Ghost policy of a full view or a completion is the same
-- as the Ghost policy of the partial view. Emit an error if this is not
-- the case.
procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
procedure Check_Ghost_Derivation (Typ : Entity_Id);
-- Verify that the parent type and all progenitors of derived type or type
-- extension Typ are Ghost. If this is not the case, issue an error.
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
procedure Initialize;
-- Initialize internal tables
function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
-- Determine whether entity Id is Ghost. To qualify as such, the entity
-- must be subject to pragma Ghost.
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
-- Determine whether declarative node N is subject to aspect or pragma
-- Ghost. Use this routine in cases where [source] pragma Ghost has not
-- been analyzed yet, but the context needs to establish the "ghostness"
-- of N.
procedure Lock;
-- Lock internal tables before calling backend
procedure Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
-- units.
--
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty);
-- Set the value of global variable Ghost_Mode depending on the following
-- scenarios:
--
-- If N is a declaration, determine whether N is subject to pragma Ghost.
-- If this is the case, the Ghost_Mode is set based on the current Ghost
-- policy in effect. Special cases:
--
-- N is the completion of a deferred constant, Prev_Id denotes the
-- entity of the partial declaration.
--
-- N is the full view of a private type, Prev_Id denotes the entity
-- of the partial declaration.
--
-- If N is an assignment statement or a procedure call, determine whether
-- the name of N denotes a reference to a Ghost entity. If this is the
-- case, the Global_Mode is set based on the mode of the name.
--
-- If N denotes a package or a subprogram body, determine whether the
-- corresponding spec Prev_Id is a Ghost entity or the body is subject
-- to pragma Ghost. If this is the case, the Global_Mode is set based on
-- the current Ghost policy in effect.
--
-- WARNING: the caller must save and restore the value of Ghost_Mode in a
-- a stack-like fasion as this routine may override the existing value.
procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id);
-- Set the value of global variable Ghost_Mode depending on the mode of
-- entity Id. N denotes the context of the freeze.
--
-- WARNING: the caller must save and restore the value of Ghost_Mode in a
-- a stack-like fasion as this routine may override the existing value.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant ghost attribute of entity Id depending on the current
-- Ghost assertion policy in effect.
end Ghost;

6
gcc/ada/gnat1drv.adb
View File

@ -36,6 +36,7 @@ with Fmap;
with Fname; use Fname;
with Fname.UF; use Fname.UF;
with Frontend;
with Ghost;
with Gnatvsn; use Gnatvsn;
with Inline;
with Lib; use Lib;
@ -863,7 +864,6 @@ begin
Lib.Xref.Initialize;
Scan_Compiler_Arguments;
Osint.Add_Default_Search_Dirs;
Atree.Initialize;
Nlists.Initialize;
Sinput.Initialize;
@ -876,6 +876,7 @@ begin
SCOs.Initialize;
Snames.Initialize;
Stringt.Initialize;
Ghost.Initialize;
Inline.Initialize;
Par_SCO.Initialize;
Sem_Ch8.Initialize;
@ -1291,12 +1292,13 @@ begin
Atree.Lock;
Elists.Lock;
Fname.UF.Lock;
Ghost.Lock;
Inline.Lock;
Lib.Lock;
Namet.Lock;
Nlists.Lock;
Sem.Lock;
Sinput.Lock;
Namet.Lock;
Stringt.Lock;
-- Here we call the back end to generate the output code

20
gcc/ada/lib-xref.adb
View File

@ -1662,6 +1662,15 @@ package body Lib.Xref is
J := 1;
while J <= Xrefs.Last loop
Ent := Xrefs.Table (J).Key.Ent;
-- Do not generate reference information for an ignored Ghost
-- entity because neither the entity nor its references will
-- appear in the final tree.
if Is_Ignored_Ghost_Entity (Ent) then
goto Orphan_Continue;
end if;
Get_Type_Reference (Ent, Tref, L, R);
if Present (Tref)
@ -1744,6 +1753,7 @@ package body Lib.Xref is
end;
end if;
<<Orphan_Continue>>
J := J + 1;
end loop;
end Handle_Orphan_Type_References;
@ -1752,7 +1762,6 @@ package body Lib.Xref is
-- references, so we can sort them, and output them.
Output_Refs : declare
Nrefs : constant Nat := Xrefs.Last;
-- Number of references in table
@ -2114,6 +2123,15 @@ package body Lib.Xref is
begin
Ent := XE.Key.Ent;
-- Do not generate reference information for an ignored Ghost
-- entity because neither the entity nor its references will
-- appear in the final tree.
if Is_Ignored_Ghost_Entity (Ent) then
goto Continue;
end if;
Ctyp := Xref_Entity_Letters (Ekind (Ent));
-- Skip reference if it is the only reference to an entity,

240
gcc/ada/lib.ads
View File

@ -440,18 +440,25 @@ package Lib is
-- do not have an entry for each possible field, since some of the fields
-- can only be set by specialized interfaces (defined below).
function Version_Get (U : Unit_Number_Type) return Word_Hex_String;
-- Returns the version as a string with 8 hex digits (upper case letters)
function Compilation_Switches_Last return Nat;
-- Return the count of stored compilation switches
function Last_Unit return Unit_Number_Type;
-- Unit number of last allocated unit
procedure Disable_Switch_Storing;
-- Disable registration of switches by Store_Compilation_Switch. Used to
-- avoid registering switches added automatically by the gcc driver at the
-- end of the command line.
function Num_Units return Nat;
-- Number of units currently in unit table
function Earlier_In_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
-- Given two Sloc values for which In_Same_Extended_Unit is true, determine
-- if S1 appears before S2. Returns True if S1 appears before S2, and False
-- otherwise. The result is undefined if S1 and S2 are not in the same
-- extended unit. Note: this routine will not give reliable results if
-- called after Sprint has been called with -gnatD set.
procedure Remove_Unit (U : Unit_Number_Type);
-- Remove unit U from unit table. Currently this is effective only
-- if U is the last unit currently stored in the unit table.
procedure Enable_Switch_Storing;
-- Enable registration of switches by Store_Compilation_Switch. Used to
-- avoid registering switches added automatically by the gcc driver at the
-- beginning of the command line.
function Entity_Is_In_Main_Unit (E : Entity_Id) return Boolean;
-- Returns True if the entity E is declared in the main unit, or, in
@ -459,6 +466,45 @@ package Lib is
-- within generic instantiations return True if the instantiation is
-- itself "in the main unit" by this definition. Otherwise False.
function Exact_Source_Name (Loc : Source_Ptr) return String;
-- Return name of entity at location Loc exactly as written in the source.
-- this includes copying the wide character encodings exactly as they were
-- used in the source, so the caller must be aware of the possibility of
-- such encodings.
function Get_Compilation_Switch (N : Pos) return String_Ptr;
-- Return the Nth stored compilation switch, or null if less than N
-- switches have been stored. Used by ASIS and back ends written in Ada.
function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean;
-- Generic units must be separately compiled. Since we always use
-- macro substitution for generics, the resulting object file is a dummy
-- one with no code, but the ALI file has the normal form, and we need
-- this ALI file so that the binder can work out a correct order of
-- elaboration.
--
-- However, ancient versions of GNAT used to not generate code or ALI
-- files for generic units, and this would yield complex order of
-- elaboration issues. These were fixed in GNAT 3.10. The support for not
-- compiling language-defined library generics was retained nonetheless
-- to facilitate bootstrap. Specifically, it is convenient to have
-- the same list of files to be compiled for all stages. So, if the
-- bootstrap compiler does not generate code for a given file, then
-- the stage1 compiler (and binder) also must deal with the case of
-- that file not being compiled. The predicate Generic_May_Lack_ALI is
-- True for those generic units for which missing ALI files are allowed.
function Get_Cunit_Unit_Number (N : Node_Id) return Unit_Number_Type;
-- Return unit number of the unit whose N_Compilation_Unit node is the
-- one passed as an argument. This must always succeed since the node
-- could not have been built without making a unit table entry.
function Get_Cunit_Entity_Unit_Number
(E : Entity_Id) return Unit_Number_Type;
-- Return unit number of the unit whose compilation unit spec entity is
-- the one passed as an argument. This must always succeed since the
-- entity could not have been built without making a unit table entry.
function Get_Source_Unit (N : Node_Or_Entity_Id) return Unit_Number_Type;
pragma Inline (Get_Source_Unit);
function Get_Source_Unit (S : Source_Ptr) return Unit_Number_Type;
@ -478,34 +524,6 @@ package Lib is
-- template, so it returns the unit number containing the code that
-- corresponds to the node N, or the source location S.
function In_Same_Source_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Source_Unit);
-- Determines if the two nodes or entities N1 and N2 are in the same
-- source unit, the criterion being that Get_Source_Unit yields the
-- same value for each argument.
function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Code_Unit);
-- Determines if the two nodes or entities N1 and N2 are in the same
-- code unit, the criterion being that Get_Code_Unit yields the same
-- value for each argument.
function In_Same_Extended_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Extended_Unit);
-- Determines if two nodes or entities N1 and N2 are in the same
-- extended unit, where an extended unit is defined as a unit and all
-- its subunits (considered recursively, i.e. subunits of subunits are
-- included). Returns true if S1 and S2 are in the same extended unit
-- and False otherwise.
function In_Same_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
pragma Inline (In_Same_Extended_Unit);
-- Determines if the two source locations S1 and S2 are in the same
-- extended unit, where an extended unit is defined as a unit and all
-- its subunits (considered recursively, i.e. subunits of subunits are
-- included). Returns true if S1 and S2 are in the same extended unit
-- and False otherwise.
function In_Extended_Main_Code_Unit
(N : Node_Or_Entity_Id) return Boolean;
-- Return True if the node is in the generated code of the extended main
@ -550,48 +568,67 @@ package Lib is
function In_Predefined_Unit (S : Source_Ptr) return Boolean;
-- Same function as above but argument is a source pointer
function Earlier_In_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
-- Given two Sloc values for which In_Same_Extended_Unit is true, determine
-- if S1 appears before S2. Returns True if S1 appears before S2, and False
-- otherwise. The result is undefined if S1 and S2 are not in the same
-- extended unit. Note: this routine will not give reliable results if
-- called after Sprint has been called with -gnatD set.
function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Code_Unit);
-- Determines if the two nodes or entities N1 and N2 are in the same
-- code unit, the criterion being that Get_Code_Unit yields the same
-- value for each argument.
function Exact_Source_Name (Loc : Source_Ptr) return String;
-- Return name of entity at location Loc exactly as written in the source.
-- this includes copying the wide character encodings exactly as they were
-- used in the source, so the caller must be aware of the possibility of
-- such encodings.
function In_Same_Extended_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Extended_Unit);
-- Determines if two nodes or entities N1 and N2 are in the same
-- extended unit, where an extended unit is defined as a unit and all
-- its subunits (considered recursively, i.e. subunits of subunits are
-- included). Returns true if S1 and S2 are in the same extended unit
-- and False otherwise.
function Compilation_Switches_Last return Nat;
-- Return the count of stored compilation switches
function In_Same_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
pragma Inline (In_Same_Extended_Unit);
-- Determines if the two source locations S1 and S2 are in the same
-- extended unit, where an extended unit is defined as a unit and all
-- its subunits (considered recursively, i.e. subunits of subunits are
-- included). Returns true if S1 and S2 are in the same extended unit
-- and False otherwise.
function Get_Compilation_Switch (N : Pos) return String_Ptr;
-- Return the Nth stored compilation switch, or null if less than N
-- switches have been stored. Used by ASIS and back ends written in Ada.
function Get_Cunit_Unit_Number (N : Node_Id) return Unit_Number_Type;
-- Return unit number of the unit whose N_Compilation_Unit node is the
-- one passed as an argument. This must always succeed since the node
-- could not have been built without making a unit table entry.
function Get_Cunit_Entity_Unit_Number
(E : Entity_Id) return Unit_Number_Type;
-- Return unit number of the unit whose compilation unit spec entity is
-- the one passed as an argument. This must always succeed since the
-- entity could not have been built without making a unit table entry.
function In_Same_Source_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Source_Unit);
-- Determines if the two nodes or entities N1 and N2 are in the same
-- source unit, the criterion being that Get_Source_Unit yields the
-- same value for each argument.
function Increment_Serial_Number return Nat;
-- Increment Serial_Number field for current unit, and return the
-- incremented value.
procedure Synchronize_Serial_Number;
-- This function increments the Serial_Number field for the current unit
-- but does not return the incremented value. This is used when there
-- is a situation where one path of control increments a serial number
-- (using Increment_Serial_Number), and the other path does not and it is
-- important to keep the serial numbers synchronized in the two cases (e.g.
-- when the references in a package and a client must be kept consistent).
procedure Initialize;
-- Initialize internal tables
function Is_Loaded (Uname : Unit_Name_Type) return Boolean;
-- Determines if unit with given name is already loaded, i.e. there is
-- already an entry in the file table with this unit name for which the
-- corresponding file was found and parsed. Note that the Fatal_Error flag
-- of this entry must be checked before proceeding with further processing.
function Last_Unit return Unit_Number_Type;
-- Unit number of last allocated unit
procedure List (File_Names_Only : Boolean := False);
-- Lists units in active library (i.e. generates output consisting of a
-- sorted listing of the units represented in File table, except for the
-- main unit). If File_Names_Only is set to True, then the list includes
-- only file names, and no other information. Otherwise the unit name and
-- time stamp are also output. File_Names_Only also restricts the list to
-- exclude any predefined files.
procedure Lock;
-- Lock internal tables before calling back end
function Num_Units return Nat;
-- Number of units currently in unit table
procedure Remove_Unit (U : Unit_Number_Type);
-- Remove unit U from unit table. Currently this is effective only if U is
-- the last unit currently stored in the unit table.
procedure Replace_Linker_Option_String
(S : String_Id;
@ -604,16 +641,6 @@ package Lib is
-- which may influence the generated output file(s). Switch is the text of
-- the switch to store (except that -fRTS gets changed back to --RTS).
procedure Enable_Switch_Storing;
-- Enable registration of switches by Store_Compilation_Switch. Used to
-- avoid registering switches added automatically by the gcc driver at the
-- beginning of the command line.
procedure Disable_Switch_Storing;
-- Disable registration of switches by Store_Compilation_Switch. Used to
-- avoid registering switches added automatically by the gcc driver at the
-- end of the command line.
procedure Store_Linker_Option_String (S : String_Id);
-- This procedure is called to register the string from a pragma
-- Linker_Option. The argument is the Id of the string to register.
@ -622,14 +649,13 @@ package Lib is
-- This procedure is called to register a pragma N for which a notes
-- entry is required.
procedure Initialize;
-- Initialize internal tables
procedure Lock;
-- Lock internal tables before calling back end
procedure Unlock;
-- Unlock internal tables, in cases where the back end needs to modify them
procedure Synchronize_Serial_Number;
-- This function increments the Serial_Number field for the current unit
-- but does not return the incremented value. This is used when there
-- is a situation where one path of control increments a serial number
-- (using Increment_Serial_Number), and the other path does not and it is
-- important to keep the serial numbers synchronized in the two cases (e.g.
-- when the references in a package and a client must be kept consistent).
procedure Tree_Read;
-- Initializes internal tables from current tree file using the relevant
@ -639,43 +665,17 @@ package Lib is
-- Writes out internal tables to current tree file using the relevant
-- Table.Tree_Write routines.
function Is_Loaded (Uname : Unit_Name_Type) return Boolean;
-- Determines if unit with given name is already loaded, i.e. there is
-- already an entry in the file table with this unit name for which the
-- corresponding file was found and parsed. Note that the Fatal_Error flag
-- of this entry must be checked before proceeding with further processing.
procedure Unlock;
-- Unlock internal tables, in cases where the back end needs to modify them
function Version_Get (U : Unit_Number_Type) return Word_Hex_String;
-- Returns the version as a string with 8 hex digits (upper case letters)
procedure Version_Referenced (S : String_Id);
-- This routine is called from Exp_Attr to register the use of a Version
-- or Body_Version attribute. The argument is the external name used to
-- access the version string.
procedure List (File_Names_Only : Boolean := False);
-- Lists units in active library (i.e. generates output consisting of a
-- sorted listing of the units represented in File table, except for the
-- main unit). If File_Names_Only is set to True, then the list includes
-- only file names, and no other information. Otherwise the unit name and
-- time stamp are also output. File_Names_Only also restricts the list to
-- exclude any predefined files.
function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean;
-- Generic units must be separately compiled. Since we always use
-- macro substitution for generics, the resulting object file is a dummy
-- one with no code, but the ALI file has the normal form, and we need
-- this ALI file so that the binder can work out a correct order of
-- elaboration.
--
-- However, ancient versions of GNAT used to not generate code or ALI
-- files for generic units, and this would yield complex order of
-- elaboration issues. These were fixed in GNAT 3.10. The support for not
-- compiling language-defined library generics was retained nonetheless
-- to facilitate bootstrap. Specifically, it is convenient to have
-- the same list of files to be compiled for all stages. So, if the
-- bootstrap compiler does not generate code for a given file, then
-- the stage1 compiler (and binder) also must deal with the case of
-- that file not being compiled. The predicate Generic_May_Lack_ALI is
-- True for those generic units for which missing ALI files are allowed.
procedure Write_Unit_Info
(Unit_Num : Unit_Number_Type;
Item : Node_Id;

8
gcc/ada/opt.ads
View File

@ -724,6 +724,14 @@ package Opt is
-- True if the frontend finished its work and has called the backend to
-- process the tree and generate the object file.
type Ghost_Mode_Type is (None, Check, Ignore);
-- Possible legal modes that can be set by aspect/pragma Ghost as well as
-- value None, which indicates that no such aspect/pragma applies.
Ghost_Mode : Ghost_Mode_Type := None;
-- GNAT
-- Current Ghost mode setting
Global_Discard_Names : Boolean := False;
-- GNAT, GNATBIND
-- True if a pragma Discard_Names appeared as a configuration pragma for

14
gcc/ada/rtsfind.adb
View File

@ -923,6 +923,12 @@ package body Rtsfind is
end loop;
end Save_Private_Visibility;
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Save the current Ghost mode in effect to ensure a clean environment
-- when analyzing the unit.
-- Start of processing for Load_RTU
begin
@ -932,6 +938,10 @@ package body Rtsfind is
return;
end if;
-- Provide a clean environment for the unit
Ghost_Mode := None;
-- Note if secondary stack is used
if U_Id = System_Secondary_Stack then
@ -1032,6 +1042,10 @@ package body Rtsfind is
if Use_Setting then
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
-- Restore the original Ghost mode now that analysis has taken place
Ghost_Mode := GM;
end Load_RTU;
--------------------

217
gcc/ada/sem.adb
View File

@ -95,6 +95,10 @@ package body Sem is
-------------
procedure Analyze (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Save the current Ghost mode in effect in case the construct sets a
-- different mode.
begin
Debug_A_Entry ("analyzing ", N);
@ -108,7 +112,6 @@ package body Sem is
-- Otherwise processing depends on the node kind
case Nkind (N) is
when N_Abort_Statement =>
Analyze_Abort_Statement (N);
@ -622,10 +625,9 @@ package body Sem is
-- the call to analyze them is generated when the full list is
-- analyzed.
when
N_SCIL_Dispatch_Table_Tag_Init |
N_SCIL_Dispatching_Call |
N_SCIL_Membership_Test =>
when N_SCIL_Dispatch_Table_Tag_Init |
N_SCIL_Dispatching_Call |
N_SCIL_Membership_Test =>
null;
-- For the remaining node types, we generate compiler abort, because
@ -635,65 +637,63 @@ package body Sem is
-- node appears only in the context of a type declaration, and is
-- processed by the analyze routine for type declarations.
when
N_Abortable_Part |
N_Access_Definition |
N_Access_Function_Definition |
N_Access_Procedure_Definition |
N_Access_To_Object_Definition |
N_Aspect_Specification |
N_Case_Expression_Alternative |
N_Case_Statement_Alternative |
N_Compilation_Unit_Aux |
N_Component_Association |
N_Component_Clause |
N_Component_Definition |
N_Component_List |
N_Constrained_Array_Definition |
N_Contract |
N_Decimal_Fixed_Point_Definition |
N_Defining_Character_Literal |
N_Defining_Identifier |
N_Defining_Operator_Symbol |
N_Defining_Program_Unit_Name |
N_Delta_Constraint |
N_Derived_Type_Definition |
N_Designator |
N_Digits_Constraint |
N_Discriminant_Association |
N_Discriminant_Specification |
N_Elsif_Part |
N_Entry_Call_Statement |
N_Enumeration_Type_Definition |
N_Exception_Handler |
N_Floating_Point_Definition |
N_Formal_Decimal_Fixed_Point_Definition |
N_Formal_Derived_Type_Definition |
N_Formal_Discrete_Type_Definition |
N_Formal_Floating_Point_Definition |
N_Formal_Modular_Type_Definition |
N_Formal_Ordinary_Fixed_Point_Definition |
N_Formal_Private_Type_Definition |
N_Formal_Incomplete_Type_Definition |
N_Formal_Signed_Integer_Type_Definition |
N_Function_Specification |
N_Generic_Association |
N_Index_Or_Discriminant_Constraint |
N_Iteration_Scheme |
N_Mod_Clause |
N_Modular_Type_Definition |
N_Ordinary_Fixed_Point_Definition |
N_Parameter_Specification |
N_Pragma_Argument_Association |
N_Procedure_Specification |
N_Real_Range_Specification |
N_Record_Definition |
N_Signed_Integer_Type_Definition |
N_Unconstrained_Array_Definition |
N_Unused_At_Start |
N_Unused_At_End |
N_Variant =>
when N_Abortable_Part |
N_Access_Definition |
N_Access_Function_Definition |
N_Access_Procedure_Definition |
N_Access_To_Object_Definition |
N_Aspect_Specification |
N_Case_Expression_Alternative |
N_Case_Statement_Alternative |
N_Compilation_Unit_Aux |
N_Component_Association |
N_Component_Clause |
N_Component_Definition |
N_Component_List |
N_Constrained_Array_Definition |
N_Contract |
N_Decimal_Fixed_Point_Definition |
N_Defining_Character_Literal |
N_Defining_Identifier |
N_Defining_Operator_Symbol |
N_Defining_Program_Unit_Name |
N_Delta_Constraint |
N_Derived_Type_Definition |
N_Designator |
N_Digits_Constraint |
N_Discriminant_Association |
N_Discriminant_Specification |
N_Elsif_Part |
N_Entry_Call_Statement |
N_Enumeration_Type_Definition |
N_Exception_Handler |
N_Floating_Point_Definition |
N_Formal_Decimal_Fixed_Point_Definition |
N_Formal_Derived_Type_Definition |
N_Formal_Discrete_Type_Definition |
N_Formal_Floating_Point_Definition |
N_Formal_Modular_Type_Definition |
N_Formal_Ordinary_Fixed_Point_Definition |
N_Formal_Private_Type_Definition |
N_Formal_Incomplete_Type_Definition |
N_Formal_Signed_Integer_Type_Definition |
N_Function_Specification |
N_Generic_Association |
N_Index_Or_Discriminant_Constraint |
N_Iteration_Scheme |
N_Mod_Clause |
N_Modular_Type_Definition |
N_Ordinary_Fixed_Point_Definition |
N_Parameter_Specification |
N_Pragma_Argument_Association |
N_Procedure_Specification |
N_Real_Range_Specification |
N_Record_Definition |
N_Signed_Integer_Type_Definition |
N_Unconstrained_Array_Definition |
N_Unused_At_Start |
N_Unused_At_End |
N_Variant =>
raise Program_Error;
end case;
@ -719,6 +719,11 @@ package body Sem is
then
Expand (N);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze;
-- Version with check(s) suppressed
@ -1297,6 +1302,51 @@ package body Sem is
---------------
procedure Semantics (Comp_Unit : Node_Id) is
procedure Do_Analyze;
-- Perform the analysis of the compilation unit
----------------
-- Do_Analyze --
----------------
procedure Do_Analyze is
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Save the current Ghost mode in effect in case the compilation unit
-- is withed from a unit with a different Ghost mode.
List : Elist_Id;
begin
List := Save_Scope_Stack;
Push_Scope (Standard_Standard);
-- Set up a clean environment before analyzing
Ghost_Mode := None;
Outer_Generic_Scope := Empty;
Scope_Suppress := Suppress_Options;
Scope_Stack.Table
(Scope_Stack.Last).Component_Alignment_Default := Calign_Default;
Scope_Stack.Table
(Scope_Stack.Last).Is_Active_Stack_Base := True;
-- Now analyze the top level compilation unit node
Analyze (Comp_Unit);
-- Check for scope mismatch on exit from compilation
pragma Assert (Current_Scope = Standard_Standard
or else Comp_Unit = Cunit (Main_Unit));
-- Then pop entry for Standard, and pop implicit types
Pop_Scope;
Restore_Scope_Stack (List);
Ghost_Mode := GM;
end Do_Analyze;
-- Local variables
-- The following locations save the corresponding global flags and
-- variables so that they can be restored on completion. This is needed
@ -1315,6 +1365,8 @@ package body Sem is
S_Outer_Gen_Scope : constant Entity_Id := Outer_Generic_Scope;
S_Style_Check : constant Boolean := Style_Check;
Already_Analyzed : constant Boolean := Analyzed (Comp_Unit);
Curunit : constant Unit_Number_Type := Get_Cunit_Unit_Number (Comp_Unit);
-- New value of Current_Sem_Unit
@ -1344,43 +1396,6 @@ package body Sem is
-- unit. All with'ed units are analyzed with config restrictions reset
-- and we need to restore these saved values at the end.
procedure Do_Analyze;
-- Procedure to analyze the compilation unit
----------------
-- Do_Analyze --
----------------
procedure Do_Analyze is
List : Elist_Id;
begin
List := Save_Scope_Stack;
Push_Scope (Standard_Standard);
Scope_Suppress := Suppress_Options;
Scope_Stack.Table
(Scope_Stack.Last).Component_Alignment_Default := Calign_Default;
Scope_Stack.Table
(Scope_Stack.Last).Is_Active_Stack_Base := True;
Outer_Generic_Scope := Empty;
-- Now analyze the top level compilation unit node
Analyze (Comp_Unit);
-- Check for scope mismatch on exit from compilation
pragma Assert (Current_Scope = Standard_Standard
or else Comp_Unit = Cunit (Main_Unit));
-- Then pop entry for Standard, and pop implicit types
Pop_Scope;
Restore_Scope_Stack (List);
end Do_Analyze;
Already_Analyzed : constant Boolean := Analyzed (Comp_Unit);
-- Start of processing for Semantics
begin

12
gcc/ada/sem_ch11.adb
View File

@ -27,6 +27,7 @@ with Atree; use Atree;
with Checks; use Checks;
with Einfo; use Einfo;
with Errout; use Errout;
with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
@ -56,7 +57,14 @@ package body Sem_Ch11 is
procedure Analyze_Exception_Declaration (N : Node_Id) is
Id : constant Entity_Id := Defining_Identifier (N);
PF : constant Boolean := Is_Pure (Current_Scope);
begin
-- The exception declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Generate_Definition (Id);
Enter_Name (Id);
Set_Ekind (Id, E_Exception);
@ -64,10 +72,10 @@ package body Sem_Ch11 is
Set_Is_Statically_Allocated (Id);
Set_Is_Pure (Id, PF);
-- An exception declared within a Ghost scope is automatically Ghost
-- An exception declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;

20
gcc/ada/sem_ch12.adb
View File

@ -33,6 +33,7 @@ with Exp_Disp; use Exp_Disp;
with Fname; use Fname;
with Fname.UF; use Fname.UF;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Itypes; use Itypes;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
@ -2991,6 +2992,11 @@ package body Sem_Ch12 is
Decl : Node_Id;
begin
-- The generic package declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic is not allowed", N);
-- We introduce a renaming of the enclosing package, to have a usable
@ -3050,10 +3056,10 @@ package body Sem_Ch12 is
Set_Etype (Id, Standard_Void_Type);
Set_Contract (Id, Make_Contract (Sloc (Id)));
-- A generic package declared within a Ghost scope is rendered Ghost
-- A generic package declared within a Ghost region is rendered Ghost
-- (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
@ -3152,6 +3158,12 @@ package body Sem_Ch12 is
Typ : Entity_Id;
begin
-- The generic subprogram declaration may be subject to pragma Ghost
-- with policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged as
-- ignored Ghost.
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic is not allowed", N);
-- Create copy of generic unit, and save for instantiation. If the unit
@ -3259,10 +3271,10 @@ package body Sem_Ch12 is
Set_Etype (Id, Standard_Void_Type);
end if;
-- A generic subprogram declared within a Ghost scope is rendered Ghost
-- A generic subprogram declared within a Ghost region is rendered Ghost
-- (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;

141
gcc/ada/sem_ch3.adb
View File

@ -39,6 +39,7 @@ with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Itypes; use Itypes;
with Layout; use Layout;
with Lib; use Lib;
@ -532,8 +533,8 @@ package body Sem_Ch3 is
function Find_Type_Of_Object
(Obj_Def : Node_Id;
Related_Nod : Node_Id) return Entity_Id;
-- Get type entity for object referenced by Obj_Def, attaching the
-- implicit types generated to Related_Nod
-- Get type entity for object referenced by Obj_Def, attaching the implicit
-- types generated to Related_Nod.
procedure Floating_Point_Type_Declaration (T : Entity_Id; Def : Node_Id);
-- Create a new float and apply the constraint to obtain subtype of it
@ -2552,9 +2553,15 @@ package body Sem_Ch3 is
begin
Prev := Find_Type_Name (N);
-- The full view, if present, now points to the current type
-- If there is an incomplete partial view, set a link to it, to
-- simplify the retrieval of primitive operations of the type.
-- The type declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N, Prev);
-- The full view, if present, now points to the current type. If there
-- is an incomplete partial view, set a link to it, to simplify the
-- retrieval of primitive operations of the type.
-- Ada 2005 (AI-50217): If the type was previously decorated when
-- imported through a LIMITED WITH clause, it appears as incomplete
@ -2704,10 +2711,10 @@ package body Sem_Ch3 is
Check_SPARK_05_Restriction ("controlled type is not allowed", N);
end if;
-- A type declared within a Ghost scope is automatically Ghost
-- A type declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Comes_From_Source (T) and then Within_Ghost_Scope then
if Comes_From_Source (T) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (T);
end if;
@ -2856,10 +2863,10 @@ package body Sem_Ch3 is
Set_Is_First_Subtype (T, True);
Set_Etype (T, T);
-- An incomplete type declared within a Ghost scope is automatically
-- An incomplete type declared within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (T);
end if;
@ -2970,13 +2977,19 @@ package body Sem_Ch3 is
It : Interp;
begin
-- The number declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Generate_Definition (Id);
Enter_Name (Id);
-- A number declared within a Ghost scope is automatically Ghost
-- A number declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
@ -3393,6 +3406,12 @@ package body Sem_Ch3 is
end if;
end if;
-- The object declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N, Prev_Entity);
if Present (Prev_Entity) then
Constant_Redeclaration (Id, N, T);
@ -3917,10 +3936,10 @@ package body Sem_Ch3 is
Set_Ekind (Id, E_Variable);
end if;
-- An object declared within a Ghost scope is automatically
-- An object declared within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
if Comes_From_Source (Id) and then Within_Ghost_Scope then
if Comes_From_Source (Id) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
-- The Ghost policy in effect at the point of declaration
@ -4098,16 +4117,13 @@ package body Sem_Ch3 is
Init_Esize (Id);
Set_Optimize_Alignment_Flags (Id);
-- An object declared within a Ghost scope is automatically Ghost
-- (SPARK RM 6.9(2)). This property is also inherited when its type
-- is Ghost or the previous declaration of the deferred constant is
-- Ghost.
-- An object declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Comes_From_Source (Id)
and then (Is_Ghost_Entity (T)
and then (Ghost_Mode > None
or else (Present (Prev_Entity)
and then Is_Ghost_Entity (Prev_Entity))
or else Within_Ghost_Scope)
and then Is_Ghost_Entity (Prev_Entity)))
then
Set_Is_Ghost_Entity (Id);
@ -4353,6 +4369,12 @@ package body Sem_Ch3 is
Parent_Base : Entity_Id;
begin
-- The private extension declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Ada 2005 (AI-251): Decorate all names in list of ancestor interfaces
if Is_Non_Empty_List (Interface_List (N)) then
@ -4581,6 +4603,12 @@ package body Sem_Ch3 is
R_Checks : Check_Result;
begin
-- The subtype declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Generate_Definition (Id);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
Init_Size_Align (Id);
@ -5456,12 +5484,13 @@ package body Sem_Ch3 is
-- The constrained array type is a subtype of the unconstrained one
Set_Ekind (T, E_Array_Subtype);
Init_Size_Align (T);
Set_Etype (T, Implicit_Base);
Set_Scope (T, Current_Scope);
Set_Is_Constrained (T, True);
Set_First_Index (T, First (Discrete_Subtype_Definitions (Def)));
Set_Ekind (T, E_Array_Subtype);
Init_Size_Align (T);
Set_Etype (T, Implicit_Base);
Set_Scope (T, Current_Scope);
Set_Is_Constrained (T);
Set_First_Index (T,
First (Discrete_Subtype_Definitions (Def)));
Set_Has_Delayed_Freeze (T);
-- Complete setup of implicit base type
@ -5472,13 +5501,17 @@ package body Sem_Ch3 is
Set_Has_Protected (Implicit_Base, Has_Protected (Element_Type));
Set_Component_Size (Implicit_Base, Uint_0);
Set_Packed_Array_Impl_Type (Implicit_Base, Empty);
Set_Has_Controlled_Component
(Implicit_Base,
Has_Controlled_Component (Element_Type)
or else Is_Controlled (Element_Type));
Set_Finalize_Storage_Only
(Implicit_Base, Finalize_Storage_Only
(Element_Type));
Set_Has_Controlled_Component (Implicit_Base,
Has_Controlled_Component (Element_Type)
or else Is_Controlled (Element_Type));
Set_Finalize_Storage_Only (Implicit_Base,
Finalize_Storage_Only (Element_Type));
-- Inherit the "ghostness" from the constrained array type
if Is_Ghost_Entity (T) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Implicit_Base);
end if;
-- Unconstrained array case
@ -5945,6 +5978,12 @@ package body Sem_Ch3 is
Copy_Array_Base_Type_Attributes (Implicit_Base, Parent_Base);
Set_Has_Delayed_Freeze (Implicit_Base, True);
-- Inherit the "ghostness" from the parent base type
if Is_Ghost_Entity (Parent_Base) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Implicit_Base);
end if;
end Make_Implicit_Base;
-- Start of processing for Build_Derived_Array_Type
@ -7720,34 +7759,6 @@ package body Sem_Ch3 is
Derived_Type : Entity_Id;
Derive_Subps : Boolean := True)
is
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
--------------------------------
-- Implements_Ghost_Interface --
--------------------------------
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
Iface_Elmt : Elmt_Id;
begin
-- Traverse the list of interfaces looking for a Ghost interface
if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
Iface_Elmt := First_Elmt (Interfaces (Typ));
while Present (Iface_Elmt) loop
if Is_Ghost_Entity (Node (Iface_Elmt)) then
return True;
end if;
Next_Elmt (Iface_Elmt);
end loop;
end if;
return False;
end Implements_Ghost_Interface;
-- Local variables
Discriminant_Specs : constant Boolean :=
Present (Discriminant_Specifications (N));
Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type);
@ -7775,8 +7786,6 @@ package body Sem_Ch3 is
-- An empty Discs list means that there were no constraints in the
-- subtype indication or that there was an error processing it.
-- Start of processing for Build_Derived_Record_Type
begin
if Ekind (Parent_Type) = E_Record_Type_With_Private
and then Present (Full_View (Parent_Type))
@ -14630,6 +14639,12 @@ package body Sem_Ch3 is
Set_Alias (New_Subp, Actual_Subp);
end if;
-- Inherit the "ghostness" from the parent subprogram
if Is_Ghost_Entity (Alias (New_Subp)) then
Set_Is_Ghost_Entity (New_Subp);
end if;
-- Derived subprograms of a tagged type must inherit the convention
-- of the parent subprogram (a requirement of AI-117). Derived
-- subprograms of untagged types simply get convention Ada by default.

8
gcc/ada/sem_ch5.adb
View File

@ -32,6 +32,7 @@ with Expander; use Expander;
with Exp_Ch6; use Exp_Ch6;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
@ -278,6 +279,13 @@ package body Sem_Ch5 is
-- proper use of a Ghost entity need to know the enclosing context.
Analyze (Lhs);
-- The left hand side of an assignment may reference an entity subject
-- to pragma Ghost with policy Ignore. Set the mode now to ensure that
-- any nodes generated during analysis and expansion are properly
-- flagged as ignored Ghost.
Set_Ghost_Mode (N);
Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as

63
gcc/ada/sem_ch6.adb
View File

@ -40,6 +40,7 @@ with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib.Xref; use Lib.Xref;
@ -213,6 +214,12 @@ package body Sem_Ch6 is
Scop : constant Entity_Id := Current_Scope;
begin
-- The abstract subprogram declaration may be subject to pragma Ghost
-- with policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged as
-- ignored Ghost.
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Designator);
@ -223,10 +230,10 @@ package body Sem_Ch6 is
Set_Categorization_From_Scope (Designator, Scop);
-- An abstract subprogram declared within a Ghost scope is automatically
-- An abstract subprogram declared within a Ghost region is rendered
-- Ghost (SPARK RM 6.9(2)).
if Comes_From_Source (Designator) and then Within_Ghost_Scope then
if Comes_From_Source (Designator) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Designator);
end if;
@ -1257,7 +1264,7 @@ package body Sem_Ch6 is
-- property is not directly inherited as the body may be subject
-- to a different Ghost assertion policy.
if Is_Ghost_Entity (Gen_Id) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Gen_Id) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at
@ -1606,6 +1613,13 @@ package body Sem_Ch6 is
return;
end if;
-- The name of the procedure call may reference an entity subject to
-- pragma Ghost with policy Ignore. Set the mode now to ensure that any
-- nodes generated during analysis and expansion are properly flagged as
-- ignored Ghost.
Set_Ghost_Mode (N);
-- Otherwise analyze the parameters
if Present (Actuals) then
@ -3113,6 +3127,13 @@ package body Sem_Ch6 is
then
if Is_Generic_Subprogram (Prev_Id) then
Spec_Id := Prev_Id;
-- The corresponding spec may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged
-- as ignored Ghost.
Set_Ghost_Mode (N, Spec_Id);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id));
@ -3150,9 +3171,24 @@ package body Sem_Ch6 is
then
if Is_Private_Concurrent_Primitive (Body_Id) then
Spec_Id := Disambiguate_Spec;
-- The corresponding spec may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged
-- as ignored Ghost.
Set_Ghost_Mode (N, Spec_Id);
else
Spec_Id := Find_Corresponding_Spec (N);
-- The corresponding spec may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged
-- as ignored Ghost.
Set_Ghost_Mode (N, Spec_Id);
-- 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
@ -3294,6 +3330,13 @@ package body Sem_Ch6 is
else
Spec_Id := Corresponding_Spec (N);
-- The corresponding spec may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged
-- as ignored Ghost.
Set_Ghost_Mode (N, Spec_Id);
end if;
end if;
@ -3387,7 +3430,7 @@ package body Sem_Ch6 is
-- property is not directly inherited as the body may be subject
-- to a different Ghost assertion policy.
if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and
@ -4261,6 +4304,12 @@ package body Sem_Ch6 is
-- Indicates whether a null procedure declaration is a completion
begin
-- The subprogram declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Null procedures are not allowed in SPARK
if Nkind (Specification (N)) = N_Procedure_Specification
@ -4294,12 +4343,12 @@ package body Sem_Ch6 is
-- explicit pragma).
Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Designator, True);
Set_SPARK_Pragma_Inherited (Designator);
-- A subprogram declared within a Ghost scope is automatically Ghost
-- A subprogram declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Comes_From_Source (Designator) and then Within_Ghost_Scope then
if Comes_From_Source (Designator) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Designator);
end if;

26
gcc/ada/sem_ch7.adb
View File

@ -37,6 +37,7 @@ with Errout; use Errout;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
with Exp_Dbug; use Exp_Dbug;
with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
@ -634,6 +635,13 @@ package body Sem_Ch7 is
end if;
end if;
-- The corresponding spec of the package body may be subject to pragma
-- Ghost with policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged as
-- ignored Ghost.
Set_Ghost_Mode (N, Spec_Id);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Style.Check_Identifier (Body_Id, Spec_Id);
@ -731,7 +739,7 @@ package body Sem_Ch7 is
-- property is not directly inherited as the body may be subject to a
-- different Ghost assertion policy.
if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at the
@ -1001,6 +1009,12 @@ package body Sem_Ch7 is
Indent;
end if;
-- The package declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Generate_Definition (Id);
Enter_Name (Id);
Set_Ekind (Id, E_Package);
@ -1762,6 +1776,12 @@ package body Sem_Ch7 is
Id : constant Entity_Id := Defining_Identifier (N);
begin
-- The private type declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Generate_Definition (Id);
Set_Is_Pure (Id, PF);
Init_Size_Align (Id);
@ -1775,10 +1795,10 @@ package body Sem_Ch7 is
New_Private_Type (N, Id, N);
Set_Depends_On_Private (Id);
-- A type declared within a Ghost scope is automatically Ghost
-- A type declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;

46
gcc/ada/sem_ch8.adb
View File

@ -32,6 +32,7 @@ with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Impunit; use Impunit;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
@ -552,6 +553,12 @@ package body Sem_Ch8 is
Nam : constant Node_Id := Name (N);
begin
-- The exception renaming declaration may be subject to pragma Ghost
-- with policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged as
-- ignored Ghost.
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("exception renaming is not allowed", N);
Enter_Name (Id);
@ -575,7 +582,7 @@ package body Sem_Ch8 is
-- An exception renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
end if;
@ -665,6 +672,11 @@ package body Sem_Ch8 is
return;
end if;
-- The generic renaming declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic renaming is not allowed", N);
Generate_Definition (New_P);
@ -711,7 +723,7 @@ package body Sem_Ch8 is
-- An generic renaming is Ghost if the renamed entity is Ghost or the
-- construct appears within a Ghost scope.
if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_P);
end if;
@ -850,6 +862,11 @@ package body Sem_Ch8 is
return;
end if;
-- The object renaming declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("object renaming is not allowed", N);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
@ -1315,7 +1332,7 @@ package body Sem_Ch8 is
if (Is_Entity_Name (Nam)
and then Is_Ghost_Entity (Entity (Nam)))
or else Within_Ghost_Scope
or else Ghost_Mode > None
then
Set_Is_Ghost_Entity (Id);
end if;
@ -1371,6 +1388,12 @@ package body Sem_Ch8 is
return;
end if;
-- The package renaming declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Check for Text_IO special unit (we may be renaming a Text_IO child)
Check_Text_IO_Special_Unit (Name (N));
@ -1437,7 +1460,7 @@ package body Sem_Ch8 is
-- A package renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_P);
end if;
@ -2559,6 +2582,13 @@ package body Sem_Ch8 is
-- Start of processing for Analyze_Subprogram_Renaming
begin
-- The subprogram renaming declaration may be subject to pragma Ghost
-- with policy Ignore. Set the mode now to ensure that any nodes
-- generated during analysis and expansion are properly flagged as
-- ignored Ghost.
Set_Ghost_Mode (N);
-- We must test for the attribute renaming case before the Analyze
-- call because otherwise Sem_Attr will complain that the attribute
-- is missing an argument when it is analyzed.
@ -3027,7 +3057,7 @@ package body Sem_Ch8 is
-- A subprogram renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then
if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_S);
end if;
@ -7184,6 +7214,12 @@ package body Sem_Ch8 is
elsif Is_Floating_Point_Type (Etype (N)) then
Check_Restriction (No_Floating_Point, N);
end if;
-- A Ghost type must appear in a specific context
if Is_Ghost_Entity (Etype (N)) then
Check_Ghost_Context (Etype (N), N);
end if;
end if;
end Find_Type;

16
gcc/ada/sem_prag.adb
View File

@ -41,6 +41,7 @@ with Errout; use Errout;
with Exp_Dist; use Exp_Dist;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Writ; use Lib.Writ;
with Lib.Xref; use Lib.Xref;
@ -8412,7 +8413,7 @@ package body Sem_Prag is
-- If previous error, avoid cascaded errors
Check_Error_Detected;
Applies := True;
Applies := True;
else
Make_Inline (Subp);
@ -8434,8 +8435,7 @@ package body Sem_Prag is
end if;
if not Applies then
Error_Pragma_Arg
("inappropriate argument for pragma%", Assoc);
Error_Pragma_Arg ("inappropriate argument for pragma%", Assoc);
end if;
Next (Assoc);
@ -10212,10 +10212,10 @@ package body Sem_Prag is
Set_Refinement_Constituents (State_Id, New_Elmt_List);
Set_Part_Of_Constituents (State_Id, New_Elmt_List);
-- An abstract state declared within a Ghost scope becomes
-- An abstract state declared within a Ghost region becomes
-- Ghost (SPARK RM 6.9(2)).
if Within_Ghost_Scope then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (State_Id);
end if;
@ -11907,7 +11907,7 @@ package body Sem_Prag is
-- Pragma Check_Policy specifying a Ghost policy cannot
-- occur within a ghost subprogram or package.
if Within_Ghost_Scope then
if Ghost_Mode > None then
Error_Pragma
("pragma % cannot appear within ghost subprogram or "
& "package");
@ -14377,7 +14377,7 @@ package body Sem_Prag is
-- region (SPARK RM 6.9(7)).
if Is_False (Expr_Value (Expr))
and then Within_Ghost_Scope
and then Ghost_Mode > None
then
Error_Pragma
("pragma % with value False cannot appear in enabled "
@ -14941,7 +14941,7 @@ package body Sem_Prag is
-- Independent_Components --
----------------------------
-- pragma Independent_Components (array_or_record_LOCAL_NAME);
-- pragma Atomic_Components (array_or_record_LOCAL_NAME);
when Pragma_Independent_Components => Independent_Components : declare
E_Id : Node_Id;

192
gcc/ada/sem_res.adb
View File

@ -37,6 +37,7 @@ with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib; use Lib;
@ -110,10 +111,6 @@ package body Sem_Res is
Pref : Node_Id);
-- Check that the type of the prefix of a dereference is not incomplete
procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
function Check_Infinite_Recursion (N : Node_Id) return Boolean;
-- Given a call node, N, which is known to occur immediately within the
-- subprogram being called, determines whether it is a detectable case of
@ -694,193 +691,6 @@ package body Sem_Res is
end if;
end Check_Fully_Declared_Prefix;
-------------------------
-- Check_Ghost_Context --
-------------------------
procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
-- Verify that the Ghost policy at the point of declaration of entity Id
-- matches the policy at the point of reference. If this is not the case
-- emit an error at Err_N.
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
-- Determine whether node Context denotes a Ghost-friendly context where
-- a Ghost entity can safely reside.
-------------------------
-- Is_OK_Ghost_Context --
-------------------------
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
-- Determine whether node Decl is a Ghost declaration or appears
-- within a Ghost declaration.
--------------------------
-- Is_Ghost_Declaration --
--------------------------
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
Par : Node_Id;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
begin
-- Climb the parent chain looking for an object declaration
Par := Decl;
while Present (Par) loop
case Nkind (Par) is
when N_Abstract_Subprogram_Declaration |
N_Exception_Declaration |
N_Exception_Renaming_Declaration |
N_Full_Type_Declaration |
N_Generic_Function_Renaming_Declaration |
N_Generic_Package_Declaration |
N_Generic_Package_Renaming_Declaration |
N_Generic_Procedure_Renaming_Declaration |
N_Generic_Subprogram_Declaration |
N_Number_Declaration |
N_Object_Declaration |
N_Object_Renaming_Declaration |
N_Package_Declaration |
N_Package_Renaming_Declaration |
N_Private_Extension_Declaration |
N_Private_Type_Declaration |
N_Subprogram_Declaration |
N_Subprogram_Renaming_Declaration |
N_Subtype_Declaration =>
return Is_Subject_To_Ghost (Par);
when others =>
null;
end case;
-- Special cases
-- A reference to a Ghost entity may appear as the default
-- expression of a formal parameter of a subprogram body. This
-- context must be treated as suitable because the relation
-- between the spec and the body has not been established and
-- the body is not marked as Ghost yet. The real check was
-- performed on the spec.
if Nkind (Par) = N_Parameter_Specification
and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
then
return True;
-- References to Ghost entities may be relocated in internally
-- generated bodies.
elsif Nkind (Par) = N_Subprogram_Body
and then not Comes_From_Source (Par)
then
Subp_Id := Corresponding_Spec (Par);
-- The original context is an expression function that has
-- been split into a spec and a body. The context is OK as
-- long as the the initial declaration is Ghost.
if Present (Subp_Id) then
Subp_Decl :=
Original_Node (Unit_Declaration_Node (Subp_Id));
if Nkind (Subp_Decl) = N_Expression_Function then
return Is_Subject_To_Ghost (Subp_Decl);
end if;
end if;
-- Otherwise this is either an internal body or an internal
-- completion. Both are OK because the real check was done
-- before expansion activities.
return True;
end if;
-- Prevent the search from going too far
if Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Par := Parent (Par);
end loop;
return False;
end Is_Ghost_Declaration;
-- Start of processing for Is_OK_Ghost_Context
begin
-- The Ghost entity appears within an assertion expression
if In_Assertion_Expr > 0 then
return True;
-- The Ghost entity is part of a declaration or its completion
elsif Is_Ghost_Declaration (Context) then
return True;
-- The Ghost entity is referenced within a Ghost statement
elsif Is_Ghost_Statement_Or_Pragma (Context) then
return True;
else
return False;
end if;
end Is_OK_Ghost_Context;
------------------------
-- Check_Ghost_Policy --
------------------------
procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- The Ghost policy in effect a the point of declaration and at the
-- point of use must match (SPARK RM 6.9(14)).
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
end if;
end Check_Ghost_Policy;
-- Start of processing for Check_Ghost_Context
begin
-- Once it has been established that the reference to the Ghost entity
-- is within a suitable context, ensure that the policy at the point of
-- declaration and at the point of use match.
if Is_OK_Ghost_Context (Ghost_Ref) then
Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
-- Otherwise the Ghost entity appears in a non-Ghost context and affects
-- its behavior or value.
else
Error_Msg_N
("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
Ghost_Ref);
end if;
end Check_Ghost_Context;
------------------------------
-- Check_Infinite_Recursion --
------------------------------

386
gcc/ada/sem_util.adb
View File

@ -70,7 +70,7 @@ with GNAT.HTable; use GNAT.HTable;
package body Sem_Util is
----------------------------------------
-- Global_Variables for New_Copy_Tree --
-- Global Variables for New_Copy_Tree --
----------------------------------------
-- These global variables are used by New_Copy_Tree. See description of the
@ -110,12 +110,6 @@ package body Sem_Util is
-- and Build_Discriminal_Subtype_Of_Component. C is a list of constraints,
-- Loc is the source location, T is the original subtype.
function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean;
-- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type
-- with discriminants whose default values are static, examine only the
-- components in the selected variant to determine whether all of them
-- have a default.
function Has_Enabled_Property
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean;
@ -127,6 +121,12 @@ package body Sem_Util is
-- T is a derived tagged type. Check whether the type extension is null.
-- If the parent type is fully initialized, T can be treated as such.
function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean;
-- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type
-- with discriminants whose default values are static, examine only the
-- components in the selected variant to determine whether all of them
-- have a default.
------------------------------
-- Abstract_Interface_List --
------------------------------
@ -2676,82 +2676,6 @@ package body Sem_Util is
end if;
end Check_Function_Writable_Actuals;
----------------------------
-- Check_Ghost_Completion --
----------------------------
procedure Check_Ghost_Completion
(Partial_View : Entity_Id;
Full_View : Entity_Id)
is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Partial_View)
and then Policy = Name_Ignore
then
Error_Msg_Sloc := Sloc (Full_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Check", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
end if;
end Check_Ghost_Completion;
----------------------------
-- Check_Ghost_Derivation --
----------------------------
procedure Check_Ghost_Derivation (Typ : Entity_Id) is
Parent_Typ : constant Entity_Id := Etype (Typ);
Iface : Entity_Id;
Iface_Elmt : Elmt_Id;
begin
-- Allow untagged derivations from predefined types such as Integer as
-- those are not Ghost by definition.
if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
null;
-- The parent type of a Ghost type extension must be Ghost
elsif not Is_Ghost_Entity (Parent_Typ) then
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
return;
end if;
-- All progenitors (if any) must be Ghost as well
if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
Iface_Elmt := First_Elmt (Interfaces (Typ));
while Present (Iface_Elmt) loop
Iface := Node (Iface_Elmt);
if not Is_Ghost_Entity (Iface) then
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
return;
end if;
Next_Elmt (Iface_Elmt);
end loop;
end if;
end Check_Ghost_Derivation;
--------------------------------
-- Check_Implicit_Dereference --
--------------------------------
@ -9498,7 +9422,7 @@ package body Sem_Util is
Pkg_Decl : Node_Id := Pkg;
begin
if Ekind (Pkg) = E_Package then
if Present (Pkg) and then Ekind (Pkg) = E_Package then
while Nkind (Pkg_Decl) /= N_Package_Specification loop
Pkg_Decl := Parent (Pkg_Decl);
end loop;
@ -10437,6 +10361,39 @@ package body Sem_Util is
and then Is_Imported (Entity (Name (N)));
end Is_CPP_Constructor_Call;
--------------------
-- Is_Declaration --
--------------------
function Is_Declaration (N : Node_Id) return Boolean is
begin
case Nkind (N) is
when N_Abstract_Subprogram_Declaration |
N_Exception_Declaration |
N_Exception_Renaming_Declaration |
N_Full_Type_Declaration |
N_Generic_Function_Renaming_Declaration |
N_Generic_Package_Declaration |
N_Generic_Package_Renaming_Declaration |
N_Generic_Procedure_Renaming_Declaration |
N_Generic_Subprogram_Declaration |
N_Number_Declaration |
N_Object_Declaration |
N_Object_Renaming_Declaration |
N_Package_Declaration |
N_Package_Renaming_Declaration |
N_Private_Extension_Declaration |
N_Private_Type_Declaration |
N_Subprogram_Declaration |
N_Subprogram_Renaming_Declaration |
N_Subtype_Declaration =>
return True;
when others =>
return False;
end case;
end Is_Declaration;
-----------------
-- Is_Delegate --
-----------------
@ -11209,110 +11166,6 @@ package body Sem_Util is
end if;
end Is_Fully_Initialized_Variant;
---------------------
-- Is_Ghost_Entity --
---------------------
function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
begin
return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
end Is_Ghost_Entity;
----------------------------------
-- Is_Ghost_Statement_Or_Pragma --
----------------------------------
function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a reference to a Ghost
-- entity.
-------------------------------
-- Is_Ghost_Entity_Reference --
-------------------------------
function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
Ref : Node_Id;
begin
Ref := N;
-- When the reference extracts a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
while Nkind_In (Ref, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Ref := Prefix (Ref);
end loop;
return
Is_Entity_Name (Ref)
and then Present (Entity (Ref))
and then Is_Ghost_Entity (Entity (Ref));
end Is_Ghost_Entity_Reference;
-- Local variables
Arg : Node_Id;
Stmt : Node_Id;
-- Start of processing for Is_Ghost_Statement_Or_Pragma
begin
if Nkind (N) = N_Pragma then
-- A pragma is Ghost when it appears within a Ghost package or
-- subprogram.
if Within_Ghost_Scope then
return True;
end if;
-- A pragma is Ghost when it mentions a Ghost entity
Arg := First (Pragma_Argument_Associations (N));
while Present (Arg) loop
if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
return True;
end if;
Next (Arg);
end loop;
end if;
Stmt := N;
while Present (Stmt) loop
-- A statement is Ghost when it appears within a Ghost package or
-- subprogram.
if Is_Statement (Stmt) and then Within_Ghost_Scope then
return True;
-- An assignment statement is Ghost when the target is a Ghost
-- variable. A procedure call is Ghost when the invoked procedure
-- is Ghost.
elsif Nkind_In (Stmt, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
return Is_Ghost_Entity_Reference (Name (Stmt));
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Stmt) then
return False;
end if;
Stmt := Parent (Stmt);
end loop;
return False;
end Is_Ghost_Statement_Or_Pragma;
----------------------------
-- Is_Inherited_Operation --
----------------------------
@ -12417,123 +12270,6 @@ package body Sem_Util is
or else Nkind (N) = N_Procedure_Call_Statement;
end Is_Statement;
-------------------------
-- Is_Subject_To_Ghost --
-------------------------
function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
function Enables_Ghostness (Arg : Node_Id) return Boolean;
-- Determine whether aspect or pragma argument Arg enables "ghostness"
-----------------------
-- Enables_Ghostness --
-----------------------
function Enables_Ghostness (Arg : Node_Id) return Boolean is
Expr : Node_Id;
begin
Expr := Arg;
if Nkind (Expr) = N_Pragma_Argument_Association then
Expr := Get_Pragma_Arg (Expr);
end if;
-- Determine whether the expression of the aspect is static and
-- denotes True.
if Present (Expr) then
Preanalyze_And_Resolve (Expr);
return
Is_OK_Static_Expression (Expr)
and then Is_True (Expr_Value (Expr));
-- Otherwise Ghost defaults to True
else
return True;
end if;
end Enables_Ghostness;
-- Local variables
Id : constant Entity_Id := Defining_Entity (N);
Asp : Node_Id;
Decl : Node_Id;
Prev_Id : Entity_Id;
-- Start of processing for Is_Subject_To_Ghost
begin
if Is_Ghost_Entity (Id) then
return True;
-- The completion of a type or a constant is not fully analyzed when the
-- reference to the Ghost entity is resolved. Because the completion is
-- not marked as Ghost yet, inspect the partial view.
elsif Is_Record_Type (Id)
or else Ekind (Id) = E_Constant
or else (Nkind (N) = N_Object_Declaration
and then Constant_Present (N))
then
Prev_Id := Incomplete_Or_Partial_View (Id);
if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
return True;
end if;
end if;
-- Examine the aspect specifications (if any) looking for aspect Ghost
if Permits_Aspect_Specifications (N) then
Asp := First (Aspect_Specifications (N));
while Present (Asp) loop
if Chars (Identifier (Asp)) = Name_Ghost then
return Enables_Ghostness (Expression (Asp));
end if;
Next (Asp);
end loop;
end if;
Decl := Empty;
-- When the context is a [generic] package declaration, pragma Ghost
-- resides in the visible declarations.
if Nkind_In (N, N_Generic_Package_Declaration,
N_Package_Declaration)
then
Decl := First (Visible_Declarations (Specification (N)));
-- Otherwise pragma Ghost appears in the declarations following N
elsif Is_List_Member (N) then
Decl := Next (N);
end if;
while Present (Decl) loop
if Nkind (Decl) = N_Pragma
and then Pragma_Name (Decl) = Name_Ghost
then
return
Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
-- A source construct ends the region where pragma Ghost may appear,
-- stop the traversal.
elsif Comes_From_Source (Decl) then
exit;
end if;
Next (Decl);
end loop;
return False;
end Is_Subject_To_Ghost;
--------------------------------------------------
-- Is_Subprogram_Stub_Without_Prior_Declaration --
--------------------------------------------------
@ -17265,22 +17001,6 @@ package body Sem_Util is
Set_Entity (N, Val);
end Set_Entity_With_Checks;
-------------------------
-- Set_Is_Ghost_Entity --
-------------------------
procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
if Policy = Name_Check then
Set_Is_Checked_Ghost_Entity (Id);
elsif Policy = Name_Ignore then
Set_Is_Ignored_Ghost_Entity (Id);
end if;
end Set_Is_Ghost_Entity;
------------------------
-- Set_Name_Entity_Id --
------------------------
@ -18213,30 +17933,6 @@ package body Sem_Util is
return List_1;
end Visible_Ancestors;
------------------------
-- Within_Ghost_Scope --
------------------------
function Within_Ghost_Scope
(Id : Entity_Id := Current_Scope) return Boolean
is
S : Entity_Id;
begin
-- Climb the scope stack looking for a Ghost scope
S := Id;
while Present (S) and then S /= Standard_Standard loop
if Is_Ghost_Entity (S) then
return True;
end if;
S := Scope (S);
end loop;
return False;
end Within_Ghost_Scope;
----------------------
-- Within_Init_Proc --
----------------------

42
gcc/ada/sem_util.ads
View File

@ -285,17 +285,6 @@ package Sem_Util is
-- the one containing C2, that is known to refer to the same object (RM
-- 6.4.1(6.17/3)).
procedure Check_Ghost_Completion
(Partial_View : Entity_Id;
Full_View : Entity_Id);
-- Verify that the Ghost policy of a full view or a completion is the same
-- as the Ghost policy of the partial view. Emit an error if this is not
-- the case.
procedure Check_Ghost_Derivation (Typ : Entity_Id);
-- Verify that the parent type and all progenitors of derived type or type
-- extension Typ are Ghost. If this is not the case, issue an error.
procedure Check_Implicit_Dereference (N : Node_Id; Typ : Entity_Id);
-- AI05-139-2: Accessors and iterators for containers. This procedure
-- checks whether T is a reference type, and if so it adds an interprettion
@ -1213,6 +1202,9 @@ package Sem_Util is
-- First determine whether type T is an interface and then check whether
-- it is of protected, synchronized or task kind.
function Is_Declaration (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a declaration
function Is_Delegate (T : Entity_Id) return Boolean;
-- Returns true if type T represents a delegate. A Delegate is the CIL
-- object used to represent access-to-subprogram types. This is only
@ -1279,18 +1271,6 @@ package Sem_Util is
-- means that the result returned is not crucial, but should err on the
-- side of thinking things are fully initialized if it does not know.
function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
-- Determine whether entity Id is Ghost. To qualify as such, the entity
-- must be subject to Convention Ghost.
function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
-- Determine whether statement or pragma N is ghost. To qualify as such, N
-- must either
-- 1) Occur within a ghost subprogram or package
-- 2) Denote a call to a ghost procedure
-- 3) Denote an assignment statement whose target is a ghost variable
-- 4) Denote a pragma that mentions a ghost entity
function Is_Inherited_Operation (E : Entity_Id) return Boolean;
-- E is a subprogram. Return True is E is an implicit operation inherited
-- by a derived type declaration.
@ -1419,12 +1399,6 @@ package Sem_Util is
-- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo).
-- Note that a label is *not* a statement, and will return False.
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
-- Determine whether declarative node N is subject to aspect or pragma
-- Ghost. Use this routine in cases where [source] pragma Ghost has not
-- been analyzed yet, but the context needs to establish the "ghostness"
-- of N.
function Is_Subprogram_Stub_Without_Prior_Declaration
(N : Node_Id) return Boolean;
-- Return True if N is a subprogram stub with no prior subprogram
@ -1914,10 +1888,6 @@ package Sem_Util is
-- If restriction No_Implementation_Identifiers is set, then it checks
-- that the entity is not implementation defined.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant ghost attribute of entity Id depending on the current
-- Ghost assertion policy in effect.
procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
pragma Inline (Set_Name_Entity_Id);
-- Sets the Entity_Id value associated with the given name, which is the
@ -2045,12 +2015,6 @@ package Sem_Util is
-- generate the list of visible ancestors; otherwise their partial
-- view is added to the resulting list.
function Within_Ghost_Scope
(Id : Entity_Id := Current_Scope) return Boolean;
-- Determine whether an arbitrary entity is either a scope or within a
-- scope subject to convention Ghost or one that inherits "ghostness" from
-- an enclosing construct.
function Within_Init_Proc return Boolean;
-- Determines if Current_Scope is within an init proc

26
gcc/ada/sinfo.ads
View File

@ -521,6 +521,32 @@ package Sinfo is
-- simply ignore these nodes, since they are not relevant to the task
-- of back annotating representation information.
----------------
-- Ghost Mode --
----------------
-- When a declaration is subject to pragma Ghost, it establishes a Ghost
-- region depending on the Ghost assertion policy in effect at the point
-- of declaration. This region is temporal and starts right before the
-- analysis of the Ghost declaration and ends after its expansion. The
-- values of global variable Opt.Ghost_Mode are as follows:
-- 1. Check - All static semantics as defined in SPARK RM 6.9 are in
-- effect.
-- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI
-- files, object files as well as the final executable.
-- To achieve the runtime semantics of "Ignore", the compiler marks each
-- node created during an ignored Ghost region and signals all enclosing
-- scopes that such a node resides within. The compilation unit where the
-- node resides is also added to an auxiliary table for post processing.
-- After the analysis and expansion of all compilation units takes place
-- as well as the instantiation of all inlined [generic] bodies, the GNAT
-- driver initiates a separate pass which removes all ignored Ghost code
-- from all units stored in the auxiliary table.
--------------------
-- GNATprove Mode --
--------------------

54
gcc/ada/treepr.adb
View File

@ -1282,7 +1282,30 @@ package body Treepr is
-----------------------
procedure Print_Node_Header (N : Node_Id) is
Notes : Boolean := False;
Enumerate : Boolean := False;
-- Flag set when enumerating multiple header flags
procedure Print_Header_Flag (Flag : String);
-- Output one of the flags that appears in a node header. The routine
-- automatically handles enumeration of multiple flags.
-----------------------
-- Print_Header_Flag --
-----------------------
procedure Print_Header_Flag (Flag : String) is
begin
if Enumerate then
Print_Char (',');
else
Enumerate := True;
Print_Char ('(');
end if;
Print_Str (Flag);
end Print_Header_Flag;
-- Start of processing for Print_Node_Header
begin
Print_Node_Ref (N);
@ -1293,34 +1316,25 @@ package body Treepr is
return;
end if;
Print_Char (' ');
if Comes_From_Source (N) then
Notes := True;
Print_Str (" (source");
Print_Header_Flag ("source");
end if;
if Analyzed (N) then
if not Notes then
Notes := True;
Print_Str (" (");
else
Print_Str (",");
end if;
Print_Str ("analyzed");
Print_Header_Flag ("analyzed");
end if;
if Error_Posted (N) then
if not Notes then
Notes := True;
Print_Str (" (");
else
Print_Str (",");
end if;
Print_Str ("posted");
Print_Header_Flag ("posted");
end if;
if Notes then
if Is_Ignored_Ghost_Node (N) then
Print_Header_Flag ("ignored ghost");
end if;
if Enumerate then
Print_Char (')');
end if;