procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and restore the Ghost mode.

Browse source 
2015-05-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and
	restore the Ghost mode.
	(Expand_N_Object_Declaration): Capture, set and restore the Ghost mode.
	(Freeze_Type): Update the call to Set_Ghost_Mode.
	(Restore_Globals): New routine.
	* exp_ch5.adb Add with and use clauses for Ghost.
	(Expand_N_Assignment_Statement): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch6.adb Add with and use clauses for Ghost.
	(Expand_N_Procedure_Call_Statement): Capture, set and
	restore the Ghost mode.
	(Expand_N_Subprogram_Body):
	Code cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Subprogram_Declaration): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch7.adb Add with and use clauses for Ghost.
	(Expand_N_Package_Body): Capture, set and restore the Ghost mode.
	(Expand_N_Package_Declaration): Capture, set and restore the
	Ghost mode.
	(Wrap_HSS_In_Block): Create a proper identifier for the block.
	* exp_ch8.adb Add with and use clauses for Ghost.
	(Expand_N_Exception_Renaming_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Object_Renaming_Declaration): Capture, set and restore
	the Ghost mode.
	(Expand_N_Package_Renaming_Declaration): Capture, set and restore the
	Ghost mode.
	(Expand_N_Subprogram_Renaming_Declaration): Capture, set and
	restore the Ghost mode.
	* exp_ch11.adb (Expand_N_Exception_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	* exp_disp.adb (Make_DT): Update the call to Set_Ghost_Mode. Do
	not initialize the dispatch table slot of a Ghost subprogram.
	* exp_prag.adb Add with and use clauses for Ghost.
	(Expand_Pragma_Check): Capture, set and restore the Ghost mode.
	(Expand_Pragma_Contract_Cases): Capture, set and restore the
	Ghost mode.
	(Expand_Pragma_Initial_Condition): Capture, set and
	restore the Ghost mode.
	(Expand_Pragma_Loop_Variant): Capture,
	set and restore the Ghost mode.
	(Restore_Globals): New routine.
	* exp_util.adb Add with and use clauses for Ghost.
	(Make_Predicate_Call): Code cleanup. Capture, set and restore
	the Ghost mode.
	(Restore_Globals): New routine.
	* freeze.adb (Freeze_Entity): Code cleanup. Update the call
	to Set_Ghost_Mode.
	* ghost.adb Add with and use clause for Sem_Prag.
	(Check_Ghost_Completion): Code cleanup.
	(Check_Ghost_Overriding): New routine.
	(Check_Ghost_Policy): Code cleanup.
	(Ghost_Entity): New routine.
	(Is_Ghost_Declaration): Removed.
	(Is_Ghost_Statement_Or_Pragma): Removed.
	(Is_OK_Context): Reimplemented.
	(Is_OK_Declaration): New routine.
	(Is_OK_Pragma): New routine.
	(Is_OK_Statement): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Propagate_Ignored_Ghost_Code): Update the comment on usage.
	(Set_From_Entity): New routine.
	(Set_From_Policy): New routine.
	(Set_Ghost_Mode): This routine now handles pragmas and freeze nodes.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	(Set_Ghost_Mode_From_Policy): Removed.
	* ghost.ads (Check_Ghost_Overriding): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Set_Ghost_Mode): Update the parameter profile. Update the
	comment on usage.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	* sem_ch3.adb (Analyze_Full_Type_Declaration):
	Capture and restore the Ghost mode. Mark a type
	as Ghost regardless of whether it comes from source.
	(Analyze_Incomplete_Type_Decl): Capture, set and restore the
	Ghost mode.
	(Analyze_Number_Declaration): Capture and restore the Ghost mode.
	(Analyze_Object_Declaration): Capture and restore the Ghost mode.
	(Analyze_Private_Extension_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Subtype_Declaration): Capture and restore the Ghost mode.
	(Process_Full_View): The full view inherits all Ghost-related
	attributes from the private view.
	(Restore_Globals): New routine.
	* sem_ch5.adb (Analyze_Assignment): Capture and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
	Code cleanup. Capture and restore the Ghost mode. Mark a
	subprogram as Ghost regarless of whether it comes from source.
	(Analyze_Procedure_Call): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Body_Helper): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Declaration): Capture and restore the Ghost mode.
	(New_Overloaded_Entity): Ensure that a
	parent subprogram and an overriding subprogram have compatible
	Ghost policies.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Capture and restore
	the Ghost mode.
	(Analyze_Package_Declaration): Capture and
	restore the Ghost mode. Mark a package as Ghost when it is
	declared in a Ghost region.
	(Analyze_Private_Type_Declaration): Capture and restore the Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch8.adb (Analyze_Exception_Renaming): Code
	reformatting. Capture and restore the Ghost mode. A renaming
	becomes Ghost when its name references a Ghost entity.
	(Analyze_Generic_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Object_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Package_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Subprogram_Renaming): Capture and restore the Ghost
	mode. A renaming becomes Ghost when its name references a
	Ghost entity.
	* sem_ch11.adb (Analyze_Exception_Declaration): Capture, set
	and restore the Ghost mode.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Generic_Subprogram_Declaration):
	Capture and restore the Ghost mode.
	* sem_ch13.adb Add with and use clauses for Ghost.
	(Add_Invariant): New routine.
	(Add_Invariants): Factor out code.
	(Add_Predicate): New routine.
	(Add_Predicates): Factor out code.
	(Build_Invariant_Procedure_Declaration): Code cleanup. Capture,
	set and restore the Ghost mode.
	(Build_Invariant_Procedure): Code cleanup.
	(Build_Predicate_Functions): Capture, set and
	restore the Ghost mode. Mark the generated functions as Ghost.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_External_Property_In_Decl_Part): Capture, set and restore
	the Ghost mode.
	(Analyze_Initial_Condition_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_Pragma):
	Code cleanup. Capture, set and restore the Ghost mode. Flag
	pragmas Linker_Section, No_Return, Unmodified, Unreferenced and
	Unreferenced_Objects as illegal when it applies to both Ghost
	and living arguments. Pragma Ghost cannot apply to synchronized
	objects.
	(Check_Kind): Moved to the spec of Sem_Prag.
	(Process_Inline): Flag the pragma as illegal when it applies to
	both Ghost and living arguments.
	(Restore_Globals): New routine.
	* sem_prag.ads Add pragma Default_Initial_Condition
	to table Assertion_Expression_Pragma. Add new table
	Is_Aspect_Specifying_Pragma.
	(Check_Kind): Moved from body of Sem_Prag.
	* sem_util.adb Add with and use clauses for Ghost.
	(Build_Default_Init_Cond_Procedure_Body): Capture, set and restore
	the Ghost mode.
	(Build_Default_Init_Cond_Procedure_Declaration):
	Capture, set and restore the Ghost mode. Mark the default
	initial condition procedure as Ghost when it is declared
	in a Ghost region.
	(Is_Renaming_Declaration): New routine.
	(Policy_In_List): Account for the single argument version of
	Check_Pragma.
	* sem_util.ads (Is_Renaming_Declaration): New routine.
	* sinfo.adb (Is_Ghost_Pragma): New routine.
	(Set_Is_Ghost_Pragma): New routine.
	* sinfo.ads New attribute Is_Ghost_Pragma.
	(Is_Ghost_Pragma): New routine along with pragma Inline.
	(Set_Is_Ghost_Pragma): New routine along with pragma Inline.

From-SVN: r223684
This commit is contained in:
Hristian Kirtchev 2015-05-26 10:46:58 +00:00 • committed by Arnaud Charlet
parent 138cac6426
commit 241ebe892a
27 changed files with 2984 additions and 1070 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

178
gcc/ada/ChangeLog
View file

@ -1,3 +1,181 @@
2015-05-26 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and
restore the Ghost mode.
(Expand_N_Object_Declaration): Capture, set and restore the Ghost mode.
(Freeze_Type): Update the call to Set_Ghost_Mode.
(Restore_Globals): New routine.
* exp_ch5.adb Add with and use clauses for Ghost.
(Expand_N_Assignment_Statement): Capture, set and restore the
Ghost mode.
(Restore_Globals): New routine.
* exp_ch6.adb Add with and use clauses for Ghost.
(Expand_N_Procedure_Call_Statement): Capture, set and
restore the Ghost mode.
(Expand_N_Subprogram_Body):
Code cleanup. Capture, set and restore the Ghost mode.
(Expand_N_Subprogram_Declaration): Capture, set and restore the
Ghost mode.
(Restore_Globals): New routine.
* exp_ch7.adb Add with and use clauses for Ghost.
(Expand_N_Package_Body): Capture, set and restore the Ghost mode.
(Expand_N_Package_Declaration): Capture, set and restore the
Ghost mode.
(Wrap_HSS_In_Block): Create a proper identifier for the block.
* exp_ch8.adb Add with and use clauses for Ghost.
(Expand_N_Exception_Renaming_Declaration): Code
cleanup. Capture, set and restore the Ghost mode.
(Expand_N_Object_Renaming_Declaration): Capture, set and restore
the Ghost mode.
(Expand_N_Package_Renaming_Declaration): Capture, set and restore the
Ghost mode.
(Expand_N_Subprogram_Renaming_Declaration): Capture, set and
restore the Ghost mode.
* exp_ch11.adb (Expand_N_Exception_Declaration): Code
cleanup. Capture, set and restore the Ghost mode.
* exp_disp.adb (Make_DT): Update the call to Set_Ghost_Mode. Do
not initialize the dispatch table slot of a Ghost subprogram.
* exp_prag.adb Add with and use clauses for Ghost.
(Expand_Pragma_Check): Capture, set and restore the Ghost mode.
(Expand_Pragma_Contract_Cases): Capture, set and restore the
Ghost mode.
(Expand_Pragma_Initial_Condition): Capture, set and
restore the Ghost mode.
(Expand_Pragma_Loop_Variant): Capture,
set and restore the Ghost mode.
(Restore_Globals): New routine.
* exp_util.adb Add with and use clauses for Ghost.
(Make_Predicate_Call): Code cleanup. Capture, set and restore
the Ghost mode.
(Restore_Globals): New routine.
* freeze.adb (Freeze_Entity): Code cleanup. Update the call
to Set_Ghost_Mode.
* ghost.adb Add with and use clause for Sem_Prag.
(Check_Ghost_Completion): Code cleanup.
(Check_Ghost_Overriding): New routine.
(Check_Ghost_Policy): Code cleanup.
(Ghost_Entity): New routine.
(Is_Ghost_Declaration): Removed.
(Is_Ghost_Statement_Or_Pragma): Removed.
(Is_OK_Context): Reimplemented.
(Is_OK_Declaration): New routine.
(Is_OK_Pragma): New routine.
(Is_OK_Statement): New routine.
(Mark_Full_View_As_Ghost): New routine.
(Mark_Pragma_As_Ghost): New routine.
(Mark_Renaming_As_Ghost): New routine.
(Propagate_Ignored_Ghost_Code): Update the comment on usage.
(Set_From_Entity): New routine.
(Set_From_Policy): New routine.
(Set_Ghost_Mode): This routine now handles pragmas and freeze nodes.
(Set_Ghost_Mode_For_Freeze): Removed.
(Set_Ghost_Mode_From_Entity): New routine.
(Set_Ghost_Mode_From_Policy): Removed.
* ghost.ads (Check_Ghost_Overriding): New routine.
(Mark_Full_View_As_Ghost): New routine.
(Mark_Pragma_As_Ghost): New routine.
(Mark_Renaming_As_Ghost): New routine.
(Set_Ghost_Mode): Update the parameter profile. Update the
comment on usage.
(Set_Ghost_Mode_For_Freeze): Removed.
(Set_Ghost_Mode_From_Entity): New routine.
* sem_ch3.adb (Analyze_Full_Type_Declaration):
Capture and restore the Ghost mode. Mark a type
as Ghost regardless of whether it comes from source.
(Analyze_Incomplete_Type_Decl): Capture, set and restore the
Ghost mode.
(Analyze_Number_Declaration): Capture and restore the Ghost mode.
(Analyze_Object_Declaration): Capture and restore the Ghost mode.
(Analyze_Private_Extension_Declaration): Capture and
restore the Ghost mode.
(Analyze_Subtype_Declaration): Capture and restore the Ghost mode.
(Process_Full_View): The full view inherits all Ghost-related
attributes from the private view.
(Restore_Globals): New routine.
* sem_ch5.adb (Analyze_Assignment): Capture and restore the
Ghost mode.
(Restore_Globals): New routine.
* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
Code cleanup. Capture and restore the Ghost mode. Mark a
subprogram as Ghost regarless of whether it comes from source.
(Analyze_Procedure_Call): Capture and restore the Ghost mode.
(Analyze_Subprogram_Body_Helper): Capture and restore the Ghost mode.
(Analyze_Subprogram_Declaration): Capture and restore the Ghost mode.
(New_Overloaded_Entity): Ensure that a
parent subprogram and an overriding subprogram have compatible
Ghost policies.
* sem_ch7.adb (Analyze_Package_Body_Helper): Capture and restore
the Ghost mode.
(Analyze_Package_Declaration): Capture and
restore the Ghost mode. Mark a package as Ghost when it is
declared in a Ghost region.
(Analyze_Private_Type_Declaration): Capture and restore the Ghost mode.
(Restore_Globals): New routine.
* sem_ch8.adb (Analyze_Exception_Renaming): Code
reformatting. Capture and restore the Ghost mode. A renaming
becomes Ghost when its name references a Ghost entity.
(Analyze_Generic_Renaming): Capture and restore the Ghost mode. A
renaming becomes Ghost when its name references a Ghost entity.
(Analyze_Object_Renaming): Capture and restore the Ghost mode. A
renaming becomes Ghost when its name references a Ghost entity.
(Analyze_Package_Renaming): Capture and restore the Ghost mode. A
renaming becomes Ghost when its name references a Ghost entity.
(Analyze_Subprogram_Renaming): Capture and restore the Ghost
mode. A renaming becomes Ghost when its name references a
Ghost entity.
* sem_ch11.adb (Analyze_Exception_Declaration): Capture, set
and restore the Ghost mode.
* sem_ch12.adb (Analyze_Generic_Package_Declaration): Capture and
restore the Ghost mode.
(Analyze_Generic_Subprogram_Declaration):
Capture and restore the Ghost mode.
* sem_ch13.adb Add with and use clauses for Ghost.
(Add_Invariant): New routine.
(Add_Invariants): Factor out code.
(Add_Predicate): New routine.
(Add_Predicates): Factor out code.
(Build_Invariant_Procedure_Declaration): Code cleanup. Capture,
set and restore the Ghost mode.
(Build_Invariant_Procedure): Code cleanup.
(Build_Predicate_Functions): Capture, set and
restore the Ghost mode. Mark the generated functions as Ghost.
* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
Capture, set and restore the Ghost mode.
(Analyze_External_Property_In_Decl_Part): Capture, set and restore
the Ghost mode.
(Analyze_Initial_Condition_In_Decl_Part):
Capture, set and restore the Ghost mode.
(Analyze_Pragma):
Code cleanup. Capture, set and restore the Ghost mode. Flag
pragmas Linker_Section, No_Return, Unmodified, Unreferenced and
Unreferenced_Objects as illegal when it applies to both Ghost
and living arguments. Pragma Ghost cannot apply to synchronized
objects.
(Check_Kind): Moved to the spec of Sem_Prag.
(Process_Inline): Flag the pragma as illegal when it applies to
both Ghost and living arguments.
(Restore_Globals): New routine.
* sem_prag.ads Add pragma Default_Initial_Condition
to table Assertion_Expression_Pragma. Add new table
Is_Aspect_Specifying_Pragma.
(Check_Kind): Moved from body of Sem_Prag.
* sem_util.adb Add with and use clauses for Ghost.
(Build_Default_Init_Cond_Procedure_Body): Capture, set and restore
the Ghost mode.
(Build_Default_Init_Cond_Procedure_Declaration):
Capture, set and restore the Ghost mode. Mark the default
initial condition procedure as Ghost when it is declared
in a Ghost region.
(Is_Renaming_Declaration): New routine.
(Policy_In_List): Account for the single argument version of
Check_Pragma.
* sem_util.ads (Is_Renaming_Declaration): New routine.
* sinfo.adb (Is_Ghost_Pragma): New routine.
(Set_Is_Ghost_Pragma): New routine.
* sinfo.ads New attribute Is_Ghost_Pragma.
(Is_Ghost_Pragma): New routine along with pragma Inline.
(Set_Is_Ghost_Pragma): New routine along with pragma Inline.
2015-05-26 Robert Dewar <dewar@adacore.com>
* sem_ch3.adb, sem_aux.adb, sem_aux.ads, exp_ch6.adb, sprint.adb:

55
gcc/ada/exp_ch11.adb
View file

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- Copyright (C) 1992-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- --
@ -31,6 +31,7 @@ with Errout; use Errout;
with Exp_Ch7; use Exp_Ch7;
with Exp_Intr; use Exp_Intr;
with Exp_Util; use Exp_Util;
with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
@ -1189,14 +1190,12 @@ package body Exp_Ch11 is
-- end if;
procedure Expand_N_Exception_Declaration (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
L : List_Id := New_List;
Loc : constant Source_Ptr := Sloc (N);
Ex_Id : Entity_Id;
Flag_Id : Entity_Id;
Name_Exname : constant Name_Id := New_External_Name (Chars (Id), 'E');
Exname : constant Node_Id :=
Make_Defining_Identifier (Loc, Name_Exname);
L : List_Id := New_List;
procedure Force_Static_Allocation_Of_Referenced_Objects
(Aggregate : Node_Id);
@ -1280,18 +1279,27 @@ package body Exp_Ch11 is
return;
end if;
-- The exception declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Definition of the external name: nam : constant String := "A.B.NAME";
Ex_Id :=
Make_Defining_Identifier (Loc, New_External_Name (Chars (Id), 'E'));
Insert_Action (N,
Make_Object_Declaration (Loc,
Defining_Identifier => Exname,
Defining_Identifier => Ex_Id,
Constant_Present => True,
Object_Definition => New_Occurrence_Of (Standard_String, Loc),
Expression =>
Make_String_Literal (Loc,
Strval => Fully_Qualified_Name_String (Id))));
Set_Is_Statically_Allocated (Exname);
Set_Is_Statically_Allocated (Ex_Id);
-- Create the aggregate list for type Standard.Exception_Type:
-- Handled_By_Other component: False
@ -1309,14 +1317,14 @@ package body Exp_Ch11 is
Append_To (L,
Make_Attribute_Reference (Loc,
Prefix => New_Occurrence_Of (Exname, Loc),
Prefix => New_Occurrence_Of (Ex_Id, Loc),
Attribute_Name => Name_Length));
-- Full_Name component: Standard.A_Char!(Nam'Address)
Append_To (L, Unchecked_Convert_To (Standard_A_Char,
Make_Attribute_Reference (Loc,
Prefix => New_Occurrence_Of (Exname, Loc),
Prefix => New_Occurrence_Of (Ex_Id, Loc),
Attribute_Name => Name_Address)));
-- HTable_Ptr component: null
@ -1342,19 +1350,21 @@ package body Exp_Ch11 is
and then not Restriction_Active (No_Exception_Registration)
then
L := New_List (
Make_Procedure_Call_Statement (Loc,
Name => New_Occurrence_Of (RTE (RE_Register_Exception), Loc),
Parameter_Associations => New_List (
Unchecked_Convert_To (RTE (RE_Exception_Data_Ptr),
Make_Attribute_Reference (Loc,
Prefix => New_Occurrence_Of (Id, Loc),
Attribute_Name => Name_Unrestricted_Access)))));
Make_Procedure_Call_Statement (Loc,
Name =>
New_Occurrence_Of (RTE (RE_Register_Exception), Loc),
Parameter_Associations => New_List (
Unchecked_Convert_To (RTE (RE_Exception_Data_Ptr),
Make_Attribute_Reference (Loc,
Prefix => New_Occurrence_Of (Id, Loc),
Attribute_Name => Name_Unrestricted_Access)))));
Set_Register_Exception_Call (Id, First (L));
if not Is_Library_Level_Entity (Id) then
Flag_Id := Make_Defining_Identifier (Loc,
New_External_Name (Chars (Id), 'F'));
Flag_Id :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (Id), 'F'));
Insert_Action (N,
Make_Object_Declaration (Loc,
@ -1380,6 +1390,11 @@ package body Exp_Ch11 is
Insert_List_After_And_Analyze (N, L);
end if;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Exception_Declaration;
---------------------------------------------

46
gcc/ada/exp_ch3.adb
View file

@ -4794,12 +4794,19 @@ package body Exp_Ch3 is
Def_Id : constant Entity_Id := Defining_Identifier (N);
B_Id : constant Entity_Id := Base_Type (Def_Id);
GM : constant Ghost_Mode_Type := Ghost_Mode;
FN : Node_Id;
Par_Id : Entity_Id;
-- Start of processing for Expand_N_Full_Type_Declaration
begin
-- The type declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
if Is_Access_Type (Def_Id) then
Build_Master (Def_Id);
@ -4923,6 +4930,11 @@ package body Exp_Ch3 is
end if;
end;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Full_Type_Declaration;
---------------------------------
@ -4932,6 +4944,7 @@ package body Exp_Ch3 is
procedure Expand_N_Object_Declaration (N : Node_Id) is
Def_Id : constant Entity_Id := Defining_Identifier (N);
Expr : constant Node_Id := Expression (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Obj_Def : constant Node_Id := Object_Definition (N);
Typ : constant Entity_Id := Etype (Def_Id);
@ -4947,6 +4960,9 @@ package body Exp_Ch3 is
-- Generate all default initialization actions for object Def_Id. Any
-- new code is inserted after node After.
procedure Restore_Globals;
-- Restore the values of all saved global variables
function Rewrite_As_Renaming return Boolean;
-- Indicate whether to rewrite a declaration with initialization into an
-- object renaming declaration (see below).
@ -5377,6 +5393,15 @@ package body Exp_Ch3 is
end if;
end Default_Initialize_Object;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-------------------------
-- Rewrite_As_Renaming --
-------------------------
@ -5392,8 +5417,9 @@ package body Exp_Ch3 is
-- Local variables
Next_N : constant Node_Id := Next (N);
Id_Ref : Node_Id;
Next_N : constant Node_Id := Next (N);
Id_Ref : Node_Id;
Tag_Assign : Node_Id;
Init_After : Node_Id := N;
-- Node after which the initialization actions are to be inserted. This
@ -5401,8 +5427,6 @@ package body Exp_Ch3 is
-- which case the init proc call must be inserted only after the bodies
-- of the shared variable procedures have been seen.
Tag_Assign : Node_Id;
-- Start of processing for Expand_N_Object_Declaration
begin
@ -5421,6 +5445,12 @@ package body Exp_Ch3 is
return;
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
-- expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- First we do special processing for objects of a tagged type where
-- this is the point at which the type is frozen. The creation of the
-- dispatch table and the initialization procedure have to be deferred
@ -5589,6 +5619,7 @@ package body Exp_Ch3 is
and then Is_Build_In_Place_Function_Call (Expr_Q)
then
Make_Build_In_Place_Call_In_Object_Declaration (N, Expr_Q);
Restore_Globals;
-- The previous call expands the expression initializing the
-- built-in-place object into further code that will be analyzed
@ -5833,6 +5864,7 @@ package body Exp_Ch3 is
end;
end if;
Restore_Globals;
return;
-- Common case of explicit object initialization
@ -5948,6 +5980,7 @@ package body Exp_Ch3 is
-- to avoid its management in the backend
Set_Expression (N, Empty);
Restore_Globals;
return;
-- Handle initialization of limited tagged types
@ -6169,10 +6202,13 @@ package body Exp_Ch3 is
end;
end if;
Restore_Globals;
-- Exception on library entity not available
exception
when RE_Not_Available =>
Restore_Globals;
return;
end Expand_N_Object_Declaration;
@ -7609,7 +7645,7 @@ package body Exp_Ch3 is
-- 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);
Set_Ghost_Mode (N, Def_Id);
-- Process any remote access-to-class-wide types designating the type
-- being frozen.

41
gcc/ada/exp_ch5.adb
View file

@ -38,6 +38,7 @@ with Exp_Dbug; use Exp_Dbug;
with Exp_Pakd; use Exp_Pakd;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Ghost; use Ghost;
with Inline; use Inline;
with Namet; use Namet;
with Nlists; use Nlists;
@ -1626,14 +1627,38 @@ package body Exp_Ch5 is
-- cannot just be passed on to the back end in untransformed state.
procedure Expand_N_Assignment_Statement (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
GM : constant Ghost_Mode_Type := Ghost_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
Crep : constant Boolean := Change_Of_Representation (N);
Lhs : constant Node_Id := Name (N);
Loc : constant Source_Ptr := Sloc (N);
Rhs : constant Node_Id := Expression (N);
Typ : constant Entity_Id := Underlying_Type (Etype (Lhs));
Exp : Node_Id;
-- Start of processing for Expand_N_Assignment_Statement
begin
-- The assignment statement may be Ghost if the left hand side is Ghost.
-- Set the mode now to ensure that any nodes generated during expansion
-- are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Special case to check right away, if the Componentwise_Assignment
-- flag is set, this is a reanalysis from the expansion of the primitive
-- assignment procedure for a tagged type, and all we need to do is to
@ -1643,6 +1668,7 @@ package body Exp_Ch5 is
if Componentwise_Assignment (N) then
Expand_Assign_Record (N);
Restore_Globals;
return;
end if;
@ -1736,6 +1762,8 @@ package body Exp_Ch5 is
Rewrite (N, Call);
Analyze (N);
Restore_Globals;
return;
end if;
end;
@ -1885,6 +1913,8 @@ package body Exp_Ch5 is
Convert_Aggr_In_Assignment (N);
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
Restore_Globals;
return;
end if;
@ -2104,6 +2134,7 @@ package body Exp_Ch5 is
if not Crep then
Expand_Bit_Packed_Element_Set (N);
Restore_Globals;
return;
-- Change of representation case
@ -2155,6 +2186,7 @@ package body Exp_Ch5 is
-- Nothing to do for valuetypes
-- ??? Set_Scope_Is_Transient (False);
Restore_Globals;
return;
elsif Is_Tagged_Type (Typ)
@ -2210,6 +2242,7 @@ package body Exp_Ch5 is
-- expansion, since they would be missed in -gnatc mode ???
Error_Msg_N ("assignment not available on limited type", N);
Restore_Globals;
return;
end if;
@ -2380,6 +2413,7 @@ package body Exp_Ch5 is
-- it with all checks suppressed.
Analyze (N, Suppress => All_Checks);
Restore_Globals;
return;
end Tagged_Case;
@ -2397,6 +2431,7 @@ package body Exp_Ch5 is
end loop;
Expand_Assign_Array (N, Actual_Rhs);
Restore_Globals;
return;
end;
@ -2404,6 +2439,7 @@ package body Exp_Ch5 is
elsif Is_Record_Type (Typ) then
Expand_Assign_Record (N);
Restore_Globals;
return;
-- Scalar types. This is where we perform the processing related to the
@ -2516,8 +2552,11 @@ package body Exp_Ch5 is
end if;
end if;
Restore_Globals;
exception
when RE_Not_Available =>
Restore_Globals;
return;
end Expand_N_Assignment_Statement;

72
gcc/ada/exp_ch6.adb
View file

@ -45,6 +45,7 @@ with Exp_Tss; use Exp_Tss;
with Exp_Unst; use Exp_Unst;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Inline; use Inline;
with Lib; use Lib;
with Namet; use Namet;
@ -4916,8 +4917,20 @@ package body Exp_Ch6 is
---------------------------------------
procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
begin
-- The procedure call may be Ghost if the name is Ghost. Set the mode
-- now to ensure that any nodes generated during expansion are properly
-- flagged as ignored Ghost.
Set_Ghost_Mode (N);
Expand_Call (N);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Procedure_Call_Statement;
--------------------------------------
@ -4992,8 +5005,9 @@ package body Exp_Ch6 is
-- Wrap thread body
procedure Expand_N_Subprogram_Body (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
H : constant Node_Id := Handled_Statement_Sequence (N);
HSS : constant Node_Id := Handled_Statement_Sequence (N);
Body_Id : Entity_Id;
Except_H : Node_Id;
L : List_Id;
@ -5005,6 +5019,9 @@ package body Exp_Ch6 is
-- the latter test is not critical, it does not matter if we add a few
-- extra returns, since they get eliminated anyway later on.
procedure Restore_Globals;
-- Restore the values of all saved global variables
----------------
-- Add_Return --
----------------
@ -5038,8 +5055,8 @@ package body Exp_Ch6 is
and then not Comes_From_Source (Parent (S))
then
Loc := Sloc (Last_Stmt);
elsif Present (End_Label (H)) then
Loc := Sloc (End_Label (H));
elsif Present (End_Label (HSS)) then
Loc := Sloc (End_Label (HSS));
else
Loc := Sloc (Last_Stmt);
end if;
@ -5077,9 +5094,24 @@ package body Exp_Ch6 is
end if;
end Add_Return;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-- Start of processing for Expand_N_Subprogram_Body
begin
-- The subprogram body may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- expansion are flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Set L to either the list of declarations if present, or to the list
-- of statements if no declarations are present. This is used to insert
-- new stuff at the start.
@ -5087,7 +5119,7 @@ package body Exp_Ch6 is
if Is_Non_Empty_List (Declarations (N)) then
L := Declarations (N);
else
L := Statements (H);
L := Statements (HSS);
end if;
-- If local-exception-to-goto optimization active, insert dummy push
@ -5112,8 +5144,8 @@ package body Exp_Ch6 is
-- or to the last declaration if there are no statements present.
-- It is the node after which the pop's are generated.
if Is_Non_Empty_List (Statements (H)) then
LS := Last (Statements (H));
if Is_Non_Empty_List (Statements (HSS)) then
LS := Last (Statements (HSS));
else
LS := Last (L);
end if;
@ -5255,6 +5287,8 @@ package body Exp_Ch6 is
Set_Handled_Statement_Sequence (N,
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
Restore_Globals;
return;
end if;
end if;
@ -5295,10 +5329,10 @@ package body Exp_Ch6 is
-- the subprogram.
if Ekind_In (Spec_Id, E_Procedure, E_Generic_Procedure) then
Add_Return (Statements (H));
Add_Return (Statements (HSS));
if Present (Exception_Handlers (H)) then
Except_H := First_Non_Pragma (Exception_Handlers (H));
if Present (Exception_Handlers (HSS)) then
Except_H := First_Non_Pragma (Exception_Handlers (HSS));
while Present (Except_H) loop
Add_Return (Statements (Except_H));
Next_Non_Pragma (Except_H);
@ -5333,10 +5367,10 @@ package body Exp_Ch6 is
elsif Has_Missing_Return (Spec_Id) then
declare
Hloc : constant Source_Ptr := Sloc (H);
Hloc : constant Source_Ptr := Sloc (HSS);
Blok : constant Node_Id :=
Make_Block_Statement (Hloc,
Handled_Statement_Sequence => H);
Handled_Statement_Sequence => HSS);
Rais : constant Node_Id :=
Make_Raise_Program_Error (Hloc,
Reason => PE_Missing_Return);
@ -5389,6 +5423,8 @@ package body Exp_Ch6 is
then
Unest_Bodies.Append ((Spec_Id, N));
end if;
Restore_Globals;
end Expand_N_Subprogram_Body;
-----------------------------------
@ -5415,14 +5451,21 @@ package body Exp_Ch6 is
-- If the declaration is for a null procedure, emit null body
procedure Expand_N_Subprogram_Declaration (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Subp : constant Entity_Id := Defining_Entity (N);
Scop : constant Entity_Id := Scope (Subp);
Prot_Decl : Node_Id;
Prot_Bod : Node_Id;
Prot_Decl : Node_Id;
Prot_Id : Entity_Id;
begin
-- The subprogram declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
-- expansion are flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- In SPARK, subprogram declarations are only allowed in package
-- specifications.
@ -5523,6 +5566,11 @@ package body Exp_Ch6 is
Set_Is_Inlined (Subp, False);
end;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Subprogram_Declaration;
--------------------------------

35
gcc/ada/exp_ch7.adb
View file

@ -42,6 +42,7 @@ with Exp_Prag; use Exp_Prag;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Lib; use Lib;
with Nlists; use Nlists;
with Nmake; use Nmake;
@ -3951,8 +3952,9 @@ package body Exp_Ch7 is
-----------------------
procedure Wrap_HSS_In_Block is
Block : Node_Id;
End_Lab : Node_Id;
Block : Node_Id;
Block_Id : Entity_Id;
End_Lab : Node_Id;
begin
-- Preserve end label to provide proper cross-reference information
@ -3961,6 +3963,11 @@ package body Exp_Ch7 is
Block :=
Make_Block_Statement (Loc, Handled_Statement_Sequence => HSS);
Block_Id := New_Internal_Entity (E_Block, Current_Scope, Loc, 'B');
Set_Identifier (Block, New_Occurrence_Of (Block_Id, Loc));
Set_Etype (Block_Id, Standard_Void_Type);
Set_Block_Node (Block_Id, Identifier (Block));
-- Signal the finalization machinery that this particular block
-- contains the original context.
@ -4163,10 +4170,17 @@ package body Exp_Ch7 is
-- Encode entity names in package body
procedure Expand_N_Package_Body (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Spec_Ent : constant Entity_Id := Corresponding_Spec (N);
Fin_Id : Entity_Id;
begin
-- The package body may be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that any nodes generated during expansion
-- are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- This is done only for non-generic packages
if Ekind (Spec_Ent) = E_Package then
@ -4222,6 +4236,11 @@ package body Exp_Ch7 is
end;
end if;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Package_Body;
----------------------------------
@ -4234,6 +4253,7 @@ package body Exp_Ch7 is
-- appear.
procedure Expand_N_Package_Declaration (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Entity (N);
Spec : constant Node_Id := Specification (N);
Decls : List_Id;
@ -4277,6 +4297,12 @@ package body Exp_Ch7 is
return;
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
-- expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- For a package declaration that implies no associated body, generate
-- task activation call and RACW supporting bodies now (since we won't
-- have a specific separate compilation unit for that).
@ -4350,6 +4376,11 @@ package body Exp_Ch7 is
Set_Finalizer (Id, Fin_Id);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Package_Declaration;
-----------------------------

63
gcc/ada/exp_ch8.adb
View file

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- Copyright (C) 1992-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- --
@ -30,6 +30,7 @@ with Exp_Ch6; use Exp_Ch6;
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Namet; use Namet;
with Nmake; use Nmake;
with Nlists; use Nlists;
@ -49,11 +50,26 @@ package body Exp_Ch8 is
---------------------------------------------
procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is
Decl : constant Node_Id := Debug_Renaming_Declaration (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Decl : Node_Id;
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 expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Decl := Debug_Renaming_Declaration (N);
if Present (Decl) then
Insert_Action (N, Decl);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Exception_Renaming_Declaration;
------------------------------------------
@ -141,9 +157,19 @@ package body Exp_Ch8 is
end if;
end Evaluation_Required;
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Object_Renaming_Declaration
begin
-- The object renaming declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Perform name evaluation if required
if Evaluation_Required (Nam) then
@ -186,6 +212,11 @@ package body Exp_Ch8 is
if Present (Decl) then
Insert_Action (N, Decl);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Object_Renaming_Declaration;
-------------------------------------------
@ -193,9 +224,18 @@ package body Exp_Ch8 is
-------------------------------------------
procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is
Decl : constant Node_Id := Debug_Renaming_Declaration (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Decl : Node_Id;
begin
-- The package renaming declaration may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
Decl := Debug_Renaming_Declaration (N);
if Present (Decl) then
-- If we are in a compilation unit, then this is an outer
@ -232,6 +272,11 @@ package body Exp_Ch8 is
Insert_Action (N, Decl);
end if;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Package_Renaming_Declaration;
----------------------------------------------
@ -281,11 +326,18 @@ package body Exp_Ch8 is
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
Nam : constant Node_Id := Name (N);
-- Start of processing for Expand_N_Subprogram_Renaming_Declaration
begin
-- The subprogram renaming declaration may be subject to pragma Ghost
-- with policy Ignore. Set the mode now to ensure that any nodes created
-- during expansion are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- When the prefix of the name is a function call, we must force the
-- call to be made by removing side effects from the call, since we
-- must only call the function once.
@ -349,6 +401,11 @@ package body Exp_Ch8 is
end if;
end;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_N_Subprogram_Renaming_Declaration;
end Exp_Ch8;

36
gcc/ada/exp_disp.adb
View file

@ -4477,12 +4477,11 @@ 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.
-- The tagged type being processed may be subject to pragma Ghost with
-- policy Ignore. Set the mode now to ensure that any nodes generated
-- during dispatch table creation are properly flagged as ignored Ghost.
Set_Ghost_Mode_For_Freeze (Typ, Typ);
Set_Ghost_Mode (Declaration_Node (Typ), Typ);
-- Handle cases in which there is no need to build the dispatch table
@ -5784,21 +5783,34 @@ package body Exp_Disp is
E := Ultimate_Alias (Prim);
Prim_Pos := UI_To_Int (DT_Position (E));
-- Do not reference predefined primitives because they are
-- located in a separate dispatch table; skip entities with
-- attribute Interface_Alias because they are only required
-- to build secondary dispatch tables; skip abstract and
-- eliminated primitives; for derivations of CPP types skip
-- primitives located in the C++ part of the dispatch table
-- because their slot is initialized by the IC routine.
-- Skip predefined primitives because they are located in a
-- separate dispatch table.
if not Is_Predefined_Dispatching_Operation (Prim)
and then not Is_Predefined_Dispatching_Operation (E)
-- Skip entities with attribute Interface_Alias because
-- those are only required to build secondary dispatch
-- tables.
and then not Present (Interface_Alias (Prim))
-- Skip abstract and eliminated primitives
and then not Is_Abstract_Subprogram (E)
and then not Is_Eliminated (E)
-- For derivations of CPP types skip primitives located in
-- the C++ part of the dispatch table because their slots
-- are initialized by the IC routine.
and then (not Is_CPP_Class (Root_Type (Typ))
or else Prim_Pos > CPP_Nb_Prims)
-- Skip ignored Ghost subprograms as those will be removed
-- from the executable.
and then not Is_Ignored_Ghost_Entity (E)
then
pragma Assert
(UI_To_Int (DT_Position (Prim)) <= Nb_Prim);

80
gcc/ada/exp_prag.adb
View file

@ -32,6 +32,7 @@ with Errout; use Errout;
with Exp_Ch11; use Exp_Ch11;
with Exp_Util; use Exp_Util;
with Expander; use Expander;
with Ghost; use Ghost;
with Inline; use Inline;
with Namet; use Namet;
with Nlists; use Nlists;
@ -292,6 +293,7 @@ package body Exp_Prag is
--------------------------
procedure Expand_Pragma_Check (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Cond : constant Node_Id := Arg2 (N);
Nam : constant Name_Id := Chars (Arg1 (N));
Msg : Node_Id;
@ -317,6 +319,16 @@ package body Exp_Prag is
return;
end if;
-- Set the Ghost mode in effect from the pragma. In general both the
-- assertion policy and the Ghost policy of pragma Check must agree,
-- but there are cases where this can be circumvented. For instance,
-- a living subtype with an ignored predicate may be declared in one
-- packade, an ignored Ghost object in another and the compilation may
-- use -gnata to enable assertions.
-- ??? Ghost predicates are under redesign
Set_Ghost_Mode (N);
-- Since this check is active, we rewrite the pragma into a
-- corresponding if statement, and then analyze the statement.
@ -480,6 +492,11 @@ package body Exp_Prag is
Error_Msg_N ("?A?check will fail at run time", N);
end if;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_Pragma_Check;
---------------------------------
@ -963,9 +980,10 @@ package body Exp_Prag is
-- Local variables
Aggr : constant Node_Id :=
Expression (First
(Pragma_Argument_Associations (CCs)));
Aggr : constant Node_Id :=
Expression (First (Pragma_Argument_Associations (CCs)));
GM : constant Ghost_Mode_Type := Ghost_Mode;
Case_Guard : Node_Id;
CG_Checks : Node_Id;
CG_Stmts : List_Id;
@ -999,6 +1017,12 @@ package body Exp_Prag is
return;
end if;
-- The contract cases may be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that any nodes generated during expansion
-- are properly flagged as ignored Ghost.
Set_Ghost_Mode (CCs);
Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
-- Create the counter which tracks the number of case guards that
@ -1223,6 +1247,11 @@ package body Exp_Prag is
end if;
Append_To (Stmts, Conseq_Checks);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_Pragma_Contract_Cases;
---------------------------------------
@ -1322,6 +1351,22 @@ package body Exp_Prag is
-------------------------------------
procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_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
Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
Check : Node_Id;
Expr : Node_Id;
@ -1329,6 +1374,8 @@ package body Exp_Prag is
List : List_Id;
Pack_Id : Entity_Id;
-- Start of processing for Expand_Pragma_Initial_Condition
begin
if Nkind (Spec_Or_Body) = N_Package_Body then
Pack_Id := Corresponding_Spec (Spec_Or_Body);
@ -1367,6 +1414,12 @@ package body Exp_Prag is
Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
-- The initial condition be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that any nodes generated during expansion
-- are properly flagged as ignored Ghost.
Set_Ghost_Mode (Init_Cond);
-- The caller should check whether the package is subject to pragma
-- Initial_Condition.
@ -1379,6 +1432,7 @@ package body Exp_Prag is
-- runtime check as it will repeat the illegality.
if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
Restore_Globals;
return;
end if;
@ -1396,6 +1450,8 @@ package body Exp_Prag is
Append_To (List, Check);
Analyze (Check);
Restore_Globals;
end Expand_Pragma_Initial_Condition;
------------------------------------
@ -1524,9 +1580,8 @@ package body Exp_Prag is
-- end loop;
procedure Expand_Pragma_Loop_Variant (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Last_Var : constant Node_Id := Last (Pragma_Argument_Associations (N));
Loc : constant Source_Ptr := Sloc (N);
Curr_Assign : List_Id := No_List;
Flag_Id : Entity_Id := Empty;
@ -1743,6 +1798,10 @@ package body Exp_Prag is
end if;
end Process_Variant;
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_Pragma_Loop_Variant
begin
@ -1755,6 +1814,12 @@ package body Exp_Prag is
return;
end if;
-- The loop variant may be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that any nodes generated during expansion
-- are properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
-- Locate the enclosing loop for which this assertion applies. In the
-- case of Ada 2012 array iteration, we might be dealing with nested
-- loops. Only the outermost loop has an identifier.
@ -1777,7 +1842,6 @@ package body Exp_Prag is
Variant := First (Pragma_Argument_Associations (N));
while Present (Variant) loop
Process_Variant (Variant, Is_Last => Variant = Last_Var);
Next (Variant);
end loop;
@ -1817,6 +1881,10 @@ package body Exp_Prag is
-- corresponding declarations and statements. We leave it in the tree
-- for documentation purposes. It will be ignored by the backend.
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Expand_Pragma_Loop_Variant;
--------------------------------

63
gcc/ada/exp_util.adb
View file

@ -34,6 +34,7 @@ with Errout; use Errout;
with Exp_Aggr; use Exp_Aggr;
with Exp_Ch6; use Exp_Ch6;
with Exp_Ch7; use Exp_Ch7;
with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib; use Lib;
@ -6423,33 +6424,63 @@ package body Exp_Util is
Expr : Node_Id;
Mem : Boolean := False) return Node_Id
is
Loc : constant Source_Ptr := Sloc (Expr);
GM : constant Ghost_Mode_Type := Ghost_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
Loc : constant Source_Ptr := Sloc (Expr);
Call : Node_Id;
PFM : Entity_Id;
-- Start of processing for Make_Predicate_Call
begin
pragma Assert (Present (Predicate_Function (Typ)));
-- The related type may be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that the call is properly flagged as
-- ignored Ghost.
Set_Ghost_Mode_From_Entity (Typ);
-- Call special membership version if requested and available
if Mem then
declare
PFM : constant Entity_Id := Predicate_Function_M (Typ);
begin
if Present (PFM) then
return
Make_Function_Call (Loc,
Name => New_Occurrence_Of (PFM, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
end if;
end;
PFM := Predicate_Function_M (Typ);
if Present (PFM) then
Call :=
Make_Function_Call (Loc,
Name => New_Occurrence_Of (PFM, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
Restore_Globals;
return Call;
end if;
end if;
-- Case of calling normal predicate function
return
Make_Function_Call (Loc,
Name =>
New_Occurrence_Of (Predicate_Function (Typ), Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
Call :=
Make_Function_Call (Loc,
Name =>
New_Occurrence_Of (Predicate_Function (Typ), Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
Restore_Globals;
return Call;
end Make_Predicate_Call;
--------------------------

10
gcc/ada/freeze.adb
View file

@ -1862,8 +1862,8 @@ package body Freeze is
Formal : Entity_Id;
Indx : Node_Id;
Test_E : Entity_Id := E;
-- This could use a comment ???
Has_Default_Initialization : Boolean := False;
-- This flag gets set to true for a variable with default initialization
Late_Freezing : Boolean := False;
-- Used to detect attempt to freeze function declared in another unit
@ -1871,8 +1871,8 @@ package body Freeze is
Result : List_Id := No_List;
-- List of freezing actions, left at No_List if none
Has_Default_Initialization : Boolean := False;
-- This flag gets set to true for a variable with default initialization
Test_E : Entity_Id := E;
-- This could use a comment ???
procedure Add_To_Result (N : Node_Id);
-- N is a freezing action to be appended to the Result
@ -4632,7 +4632,7 @@ package body Freeze is
-- 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);
Set_Ghost_Mode_From_Entity (E);
-- 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

690
gcc/ada/ghost.adb
View file

@ -37,6 +37,7 @@ with Opt; use Opt;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Eval; use Sem_Eval;
with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
@ -62,10 +63,15 @@ package body Ghost is
-- Local Subprograms --
-----------------------
function Ghost_Entity (N : Node_Id) return Entity_Id;
-- Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
-- a reference to a Ghost entity. Return Empty if there is no such entity.
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.
-- Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_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 --
@ -113,18 +119,20 @@ package body Ghost is
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);
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);
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;
@ -147,213 +155,282 @@ package body Ghost is
-------------------------
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_OK_Declaration (Decl : Node_Id) return Boolean;
-- Determine whether node Decl is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Decl must either
-- 1) Be subject to pragma Ghost
-- 2) Rename a Ghost entity
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
function Is_OK_Pragma (Prag : Node_Id) return Boolean;
-- Determine whether node Prag is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Prag must either
-- 1) Be an assertion expression pragma
-- 2) Denote pragma Global, Depends, Initializes, Refined_Global,
-- Refined_Depends or Refined_State
-- 3) Specify an aspect of a Ghost entity
-- 4) Contain a reference to a Ghost entity
--------------------------
-- Is_Ghost_Declaration --
--------------------------
function Is_OK_Statement (Stmt : Node_Id) return Boolean;
-- Determine whether node Stmt is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Stmt must either
-- 1) Denote a call to a Ghost procedure
-- 2) Denote an assignment statement whose target is Ghost
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
Par : Node_Id;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
-----------------------
-- Is_OK_Declaration --
-----------------------
begin
-- Climb the parent chain looking for an object declaration
function Is_OK_Declaration (Decl : Node_Id) return Boolean is
function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
-- Determine whether node Ren_Decl denotes a renaming declaration
-- with a Ghost name.
Par := Decl;
while Present (Par) loop
if Is_Declaration (Par) then
-----------------------
-- Is_Ghost_Renaming --
-----------------------
-- 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;
function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is
Nam_Id : Entity_Id;
begin
-- When the reference extracts a subcomponent, recover the
-- related object (SPARK RM 6.9(1)).
if Is_Renaming_Declaration (Ren_Decl) then
Nam_Id := Ghost_Entity (Name (Ren_Decl));
Ref := N;
while Nkind_In (Ref, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Ref := Prefix (Ref);
end loop;
return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
end if;
return
Is_Entity_Name (Ref)
and then Present (Entity (Ref))
and then Is_Ghost_Entity (Entity (Ref));
end Is_Ghost_Entity_Reference;
return False;
end Is_Ghost_Renaming;
-- Local variables
Arg : Node_Id;
Stmt : Node_Id;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
-- Start of processing for Is_Ghost_Statement_Or_Pragma
-- Start of processing for Is_OK_Declaration
begin
if Nkind (N) = N_Pragma then
if Is_Declaration (Decl) then
-- A pragma is Ghost when it appears within a Ghost package or
-- subprogram.
-- A renaming declaration is Ghost when it renames a Ghost
-- entity.
if Ghost_Mode > None then
if Is_Ghost_Renaming (Decl) then
return True;
-- The declaration may not have been analyzed yet, determine
-- whether it is subject to pragma Ghost.
elsif Is_Subject_To_Ghost (Decl) then
return True;
-- The declaration appears within an assertion expression
elsif In_Assertion_Expr > 0 then
return True;
end if;
-- A pragma is Ghost when it mentions a Ghost entity
-- Special cases
Arg := First (Pragma_Argument_Associations (N));
while Present (Arg) loop
if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
return True;
-- 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 (Decl) = N_Parameter_Specification
and then Nkind (Parent (Parent (Decl))) = N_Subprogram_Body
then
return True;
-- References to Ghost entities may be relocated in internally
-- generated bodies.
elsif Nkind (Decl) = N_Subprogram_Body
and then not Comes_From_Source (Decl)
then
Subp_Id := Corresponding_Spec (Decl);
-- 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 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;
Next (Arg);
end loop;
-- Otherwise this is either an internal body or an internal
-- completion. Both are OK because the real check was done
-- before expansion activities.
else
return True;
end if;
end if;
Stmt := N;
while Present (Stmt) loop
if Is_Statement (Stmt) then
return False;
end Is_OK_Declaration;
-- A statement is Ghost when it appears within a Ghost
-- package or subprogram.
------------------
-- Is_OK_Pragma --
------------------
if Ghost_Mode > None then
return True;
function Is_OK_Pragma (Prag : Node_Id) return Boolean is
procedure Check_Policies (Prag_Nam : Name_Id);
-- Verify that the Ghost policy in effect is the same as the
-- assertion policy for pragma name Prag_Nam. Emit an error if
-- this is not the case.
-- An assignment statement or a procedure call is Ghost when
-- the name denotes a Ghost entity.
--------------------
-- Check_Policies --
--------------------
elsif Nkind_In (Stmt, N_Assignment_Statement,
N_Procedure_Call_Statement)
procedure Check_Policies (Prag_Nam : Name_Id) is
AP : constant Name_Id := Check_Kind (Prag_Nam);
GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- If the Ghost policy in effect at the point of a Ghost entity
-- reference is Ignore, then the assertion policy of the pragma
-- must be Ignore (SPARK RM 6.9(18)).
if GP = Name_Ignore and then AP /= Name_Ignore then
Error_Msg_N
("incompatible ghost policies in effect", Ghost_Ref);
Error_Msg_NE
("\ghost entity & has policy `Ignore`",
Ghost_Ref, Ghost_Id);
Error_Msg_Name_1 := AP;
Error_Msg_N
("\assertion expression has policy %", Ghost_Ref);
end if;
end Check_Policies;
-- Local variables
Arg : Node_Id;
Arg_Id : Entity_Id;
Prag_Id : Pragma_Id;
Prag_Nam : Name_Id;
-- Start of processing for Is_OK_Pragma
begin
if Nkind (Prag) = N_Pragma then
Prag_Id := Get_Pragma_Id (Prag);
Prag_Nam := Original_Aspect_Pragma_Name (Prag);
-- A pragma that applies to a Ghost construct or specifies an
-- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
if Is_Ghost_Pragma (Prag) then
return True;
-- An assertion expression is a Ghost pragma when it contains a
-- reference to a Ghost entity (SPARK RM 6.9(11)).
elsif Assertion_Expression_Pragma (Prag_Id) then
-- Predicates are excluded from this category when they do
-- not apply to a Ghost subtype (SPARK RM 6.9(12)).
if Nam_In (Prag_Nam, Name_Dynamic_Predicate,
Name_Predicate,
Name_Static_Predicate)
then
return Is_Ghost_Entity_Reference (Name (Stmt));
return False;
-- Otherwise ensure that the assertion policy and the Ghost
-- policy are compatible (SPARK RM 6.9(18)).
else
Check_Policies (Prag_Nam);
return True;
end if;
-- Prevent the search from going too far
-- Several pragmas that may apply to a non-Ghost entity are
-- treated as Ghost when they contain a reference to a Ghost
-- entity (SPARK RM 6.9(12)).
elsif Is_Body_Or_Package_Declaration (Stmt) then
return False;
elsif Nam_In (Prag_Nam, Name_Global,
Name_Depends,
Name_Initializes,
Name_Refined_Global,
Name_Refined_Depends,
Name_Refined_State)
then
return True;
-- Otherwise a normal pragma is Ghost when it encloses a Ghost
-- name (SPARK RM 6.9(3)).
else
Arg := First (Pragma_Argument_Associations (Prag));
while Present (Arg) loop
Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
return True;
end if;
Next (Arg);
end loop;
end if;
Stmt := Parent (Stmt);
end loop;
end if;
return False;
end Is_Ghost_Statement_Or_Pragma;
end Is_OK_Pragma;
---------------------
-- Is_OK_Statement --
---------------------
function Is_OK_Statement (Stmt : Node_Id) return Boolean is
Nam_Id : Entity_Id;
begin
-- An assignment statement or a procedure call is Ghost when the
-- name denotes a Ghost entity.
if Nkind_In (Stmt, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
Nam_Id := Ghost_Entity (Name (Stmt));
return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
-- Special cases
-- An if statement is a suitable context for a Ghost entity if it
-- is the byproduct of assertion expression expansion.
elsif Nkind (Stmt) = N_If_Statement
and then Nkind (Original_Node (Stmt)) = N_Pragma
and then Assertion_Expression_Pragma
(Get_Pragma_Id (Original_Node (Stmt)))
then
return True;
end if;
return False;
end Is_OK_Statement;
-- Local variables
Par : Node_Id;
-- Start of processing for Is_OK_Ghost_Context
begin
-- The Ghost entity appears within an assertion expression
-- The context is Ghost when it appears within a Ghost package or
-- subprogram.
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
if Ghost_Mode > None then
return True;
-- Routine Expand_Record_Extension creates a parent subtype without
@ -364,7 +441,39 @@ package body Ghost is
elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
return True;
-- Otherwise climb the parent chain looking for a suitable Ghost
-- context.
else
Par := Context;
while Present (Par) loop
if Is_Ignored_Ghost_Node (Par) then
return True;
-- A reference to a Ghost entity can appear within an aspect
-- specification (SPARK RM 6.9(11)).
elsif Nkind (Par) = N_Aspect_Specification then
return True;
elsif Is_OK_Declaration (Par) then
return True;
elsif Is_OK_Pragma (Par) then
return True;
elsif Is_OK_Statement (Par) then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Par := Parent (Par);
end loop;
return False;
end if;
end Is_OK_Ghost_Context;
@ -384,15 +493,15 @@ package body Ghost is
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);
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);
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;
@ -458,6 +567,75 @@ package body Ghost is
end if;
end Check_Ghost_Derivation;
----------------------------
-- Check_Ghost_Overriding --
----------------------------
procedure Check_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id)
is
Par_Subp : Entity_Id;
begin
if Present (Subp) and then Present (Overridden_Subp) then
Par_Subp := Ultimate_Alias (Overridden_Subp);
-- The Ghost policy in effect at the point of declaration of a parent
-- and an overriding subprogram must match (SPARK RM 6.9(17)).
if Is_Checked_Ghost_Entity (Par_Subp)
and then Is_Ignored_Ghost_Entity (Subp)
then
Error_Msg_N ("incompatible ghost policies in effect", Subp);
Error_Msg_Sloc := Sloc (Par_Subp);
Error_Msg_N ("\& declared # with ghost policy `Check`", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N ("\overridden # with ghost policy `Ignore`", Subp);
elsif Is_Ignored_Ghost_Entity (Par_Subp)
and then Is_Checked_Ghost_Entity (Subp)
then
Error_Msg_N ("incompatible ghost policies in effect", Subp);
Error_Msg_Sloc := Sloc (Par_Subp);
Error_Msg_N ("\& declared # with ghost policy `Ignore`", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N ("\overridden # with ghost policy `Check`", Subp);
end if;
end if;
end Check_Ghost_Overriding;
------------------
-- Ghost_Entity --
------------------
function Ghost_Entity (N : Node_Id) return Entity_Id is
Ref : Node_Id;
begin
-- When the reference extracts a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
Ref := N;
while Nkind_In (Ref, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Ref := Prefix (Ref);
end loop;
if Is_Entity_Name (Ref) then
return Entity (Ref);
else
return Empty;
end if;
end Ghost_Entity;
--------------------------------
-- Implements_Ghost_Interface --
--------------------------------
@ -639,6 +817,67 @@ package body Ghost is
Ignored_Ghost_Units.Release;
end Lock;
-----------------------------
-- Mark_Full_View_As_Ghost --
-----------------------------
procedure Mark_Full_View_As_Ghost
(Priv_Typ : Entity_Id;
Full_Typ : Entity_Id)
is
Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
begin
if Is_Checked_Ghost_Entity (Priv_Typ) then
Set_Is_Checked_Ghost_Entity (Full_Typ);
elsif Is_Ignored_Ghost_Entity (Priv_Typ) then
Set_Is_Ignored_Ghost_Entity (Full_Typ);
Set_Is_Ignored_Ghost_Node (Full_Decl);
Propagate_Ignored_Ghost_Code (Full_Decl);
end if;
end Mark_Full_View_As_Ghost;
--------------------------
-- Mark_Pragma_As_Ghost --
--------------------------
procedure Mark_Pragma_As_Ghost
(Prag : Node_Id;
Context_Id : Entity_Id)
is
begin
if Is_Checked_Ghost_Entity (Context_Id) then
Set_Is_Ghost_Pragma (Prag);
elsif Is_Ignored_Ghost_Entity (Context_Id) then
Set_Is_Ghost_Pragma (Prag);
Set_Is_Ignored_Ghost_Node (Prag);
Propagate_Ignored_Ghost_Code (Prag);
end if;
end Mark_Pragma_As_Ghost;
----------------------------
-- Mark_Renaming_As_Ghost --
----------------------------
procedure Mark_Renaming_As_Ghost
(Ren_Decl : Node_Id;
Nam_Id : Entity_Id)
is
Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
begin
if Is_Checked_Ghost_Entity (Nam_Id) then
Set_Is_Checked_Ghost_Entity (Ren_Id);
elsif Is_Ignored_Ghost_Entity (Nam_Id) then
Set_Is_Ignored_Ghost_Entity (Ren_Id);
Set_Is_Ignored_Ghost_Node (Ren_Decl);
Propagate_Ignored_Ghost_Code (Ren_Decl);
end if;
end Mark_Renaming_As_Ghost;
----------------------------------
-- Propagate_Ignored_Ghost_Code --
----------------------------------
@ -799,37 +1038,34 @@ package body Ghost is
-- 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);
procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty) is
procedure Set_From_Entity (Ent_Id : Entity_Id);
-- Set the value of global variable Ghost_Mode depending on the mode of
-- entity Id.
-- entity Ent_Id.
procedure Set_Ghost_Mode_From_Policy;
procedure Set_From_Policy;
-- Set the value of global variable Ghost_Mode depending on the current
-- Ghost policy in effect.
--------------------------------
-- Set_Ghost_Mode_From_Entity --
--------------------------------
---------------------
-- Set_From_Entity --
---------------------
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
procedure Set_From_Entity (Ent_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_Ghost_Mode_From_Entity (Ent_Id);
if Is_Ignored_Ghost_Entity (Ent_Id) then
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_From_Entity;
end Set_From_Entity;
--------------------------------
-- Set_Ghost_Mode_From_Policy --
--------------------------------
---------------------
-- Set_From_Policy --
---------------------
procedure Set_Ghost_Mode_From_Policy is
procedure Set_From_Policy is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
@ -842,11 +1078,11 @@ package body Ghost is
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_From_Policy;
end Set_From_Policy;
-- Local variables
Nam : Node_Id;
Nam_Id : Entity_Id;
-- Start of processing for Set_Ghost_Mode
@ -856,25 +1092,25 @@ package body Ghost is
if Is_Declaration (N) then
if Is_Subject_To_Ghost (N) then
Set_Ghost_Mode_From_Policy;
Set_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)
and then Present (Id)
then
Set_Ghost_Mode_From_Entity (Prev_Id);
Set_From_Entity (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)
and then Present (Id)
then
Set_Ghost_Mode_From_Entity (Prev_Id);
Set_From_Entity (Id);
end if;
-- The input denotes an assignment or a procedure call. In this case
@ -883,48 +1119,50 @@ package body Ghost is
elsif Nkind_In (N, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
-- When the reference extracts a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
Nam_Id := Ghost_Entity (Name (N));
Nam := Name (N);
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));
if Present (Nam_Id) then
Set_From_Entity (Nam_Id);
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))
if (Present (Id) and then Is_Ghost_Entity (Id))
or else Is_Subject_To_Ghost (N)
then
Set_Ghost_Mode_From_Policy;
Set_From_Policy;
end if;
-- The input denotes a pragma
elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
if Is_Ignored_Ghost_Node (N) then
Ghost_Mode := Ignore;
else
Ghost_Mode := Check;
end if;
-- The input denotes a freeze node
elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
Set_From_Entity (Id);
end if;
end Set_Ghost_Mode;
-------------------------------
-- Set_Ghost_Mode_For_Freeze --
-------------------------------
--------------------------------
-- Set_Ghost_Mode_From_Entity --
--------------------------------
procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is
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;
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_For_Freeze;
end Set_Ghost_Mode_From_Entity;
-------------------------
-- Set_Is_Ghost_Entity --

63
gcc/ada/ghost.ads
View file

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
-- 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- --
@ -49,6 +49,13 @@ package Ghost is
-- 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_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id);
-- Verify that the Ghost policy of parent subprogram Overridden_Subp is the
-- same as the Ghost policy of overriding subprogram Subp. Emit an error if
-- this is not the case.
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
@ -68,6 +75,24 @@ package Ghost is
procedure Lock;
-- Lock internal tables before calling backend
procedure Mark_Full_View_As_Ghost
(Priv_Typ : Entity_Id;
Full_Typ : Entity_Id);
-- Set all Ghost-related attributes of type Full_Typ depending on the Ghost
-- mode of incomplete or private type Priv_Typ.
procedure Mark_Pragma_As_Ghost
(Prag : Node_Id;
Context_Id : Entity_Id);
-- Set all Ghost-related attributes of pragma Prag if its context denoted
-- by Id is a Ghost entity.
procedure Mark_Renaming_As_Ghost
(Ren_Decl : Node_Id;
Nam_Id : Entity_Id);
-- Set all Ghost-related attributes of renaming declaration Ren_Decl if its
-- renamed name denoted by Nam_Id is a Ghost entity.
procedure Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
-- units.
@ -75,7 +100,7 @@ package Ghost is
-- 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);
procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
-- Set the value of global variable Ghost_Mode depending on the following
-- scenarios:
--
@ -83,33 +108,37 @@ package Ghost is
-- 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 completion of a deferred constant, the Ghost_Mode is set
-- based on the mode of partial declaration entity denoted by Id.
--
-- N is the full view of a private type, Prev_Id denotes the entity
-- of the partial declaration.
-- N is the full view of a private type, the Ghost_Mode is set based
-- on the mode of the partial declaration entity denoted by Id.
--
-- 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 is an assignment statement or a procedure call, the Ghost_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.
-- If N denotes a package or a subprogram body, the Ghost_Mode is set to
-- the current Ghost policy in effect if the body is subject to Ghost or
-- the corresponding spec denoted by Id is a Ghost entity.
--
-- If N is a pragma, the Ghost_Mode is set based on the mode of the
-- pragma.
--
-- If N is a freeze node, the Global_Mode is set based on the mode of
-- entity Id.
--
-- 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.
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
-- Set the valye of global variable Ghost_Mode depending on the mode of
-- entity Id.
--
-- 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
-- Set the relevant Ghost attributes of entity Id depending on the current
-- Ghost assertion policy in effect.
end Ghost;

8
gcc/ada/sem_ch11.adb
View file

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- Copyright (C) 1992-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- --
@ -55,6 +55,7 @@ package body Sem_Ch11 is
-----------------------------------
procedure Analyze_Exception_Declaration (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
PF : constant Boolean := Is_Pure (Current_Scope);
@ -82,6 +83,11 @@ package body Sem_Ch11 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Exception_Declaration;
--------------------------------

20
gcc/ada/sem_ch12.adb
View file

@ -3124,14 +3124,15 @@ package body Sem_Ch12 is
------------------------------------------
procedure Analyze_Generic_Package_Declaration (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Id : Entity_Id;
New_N : Node_Id;
Save_Parent : Node_Id;
Renaming : Node_Id;
Decls : constant List_Id :=
Visible_Declarations (Specification (N));
Decl : Node_Id;
Id : Entity_Id;
New_N : Node_Id;
Renaming : Node_Id;
Save_Parent : Node_Id;
begin
-- The generic package declaration may be subject to pragma Ghost with
@ -3290,6 +3291,11 @@ package body Sem_Ch12 is
end if;
end;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Generic_Package_Declaration;
--------------------------------------------
@ -3297,6 +3303,7 @@ package body Sem_Ch12 is
--------------------------------------------
procedure Analyze_Generic_Subprogram_Declaration (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Formals : List_Id;
Id : Entity_Id;
New_N : Node_Id;
@ -3460,6 +3467,11 @@ package body Sem_Ch12 is
Generate_Reference_To_Formals (Id);
List_Inherited_Pre_Post_Aspects (Id);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Generic_Subprogram_Declaration;
-----------------------------------

786
gcc/ada/sem_ch13.adb
View file

@ -34,6 +34,7 @@ with Exp_Disp; use Exp_Disp;
with Exp_Tss; use Exp_Tss;
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;
@ -7762,21 +7763,25 @@ package body Sem_Ch13 is
function Build_Invariant_Procedure_Declaration
(Typ : Entity_Id) return Node_Id
is
Loc : constant Source_Ptr := Sloc (Typ);
Object_Entity : constant Entity_Id :=
Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
Spec : Node_Id;
SId : Entity_Id;
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (Typ);
Decl : Node_Id;
Obj_Id : Entity_Id;
SId : Entity_Id;
begin
Set_Etype (Object_Entity, Typ);
-- Check for duplicate definiations.
-- Check for duplicate definiations
if Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)) then
return Empty;
end if;
-- The related type may be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that the predicate functions are properly
-- flagged as ignored Ghost.
Set_Ghost_Mode_From_Entity (Typ);
SId :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (Typ), "Invariant"));
@ -7786,15 +7791,31 @@ package body Sem_Ch13 is
Set_Is_Invariant_Procedure (SId);
Set_Invariant_Procedure (Typ, SId);
Spec :=
Make_Procedure_Specification (Loc,
Defining_Unit_Name => SId,
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
Defining_Identifier => Object_Entity,
Parameter_Type => New_Occurrence_Of (Typ, Loc))));
-- Mark the invariant procedure explicitly as Ghost because it does not
-- come from source.
return Make_Subprogram_Declaration (Loc, Specification => Spec);
if Ghost_Mode > None then
Set_Is_Ghost_Entity (SId);
end if;
Obj_Id := Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
Set_Etype (Obj_Id, Typ);
Decl :=
Make_Subprogram_Declaration (Loc,
Make_Procedure_Specification (Loc,
Defining_Unit_Name => SId,
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
Defining_Identifier => Obj_Id,
Parameter_Type => New_Occurrence_Of (Typ, Loc)))));
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
return Decl;
end Build_Invariant_Procedure_Declaration;
-------------------------------
@ -7813,6 +7834,9 @@ package body Sem_Ch13 is
-- end typInvariant;
procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id) is
Priv_Decls : constant List_Id := Private_Declarations (N);
Vis_Decls : constant List_Id := Visible_Declarations (N);
Loc : constant Source_Ptr := Sloc (Typ);
Stmts : List_Id;
Spec : Node_Id;
@ -7820,13 +7844,11 @@ package body Sem_Ch13 is
PDecl : Node_Id;
PBody : Node_Id;
Nam : Name_Id;
-- Name for Check pragma, usually Invariant, but might be Type_Invariant
-- if we come from a Type_Invariant aspect, we make sure to build the
-- Check pragma with the right name, so that Check_Policy works right.
Object_Entity : Node_Id;
-- The entity of the formal for the procedure
Visible_Decls : constant List_Id := Visible_Declarations (N);
Private_Decls : constant List_Id := Private_Declarations (N);
Object_Name : Name_Id;
-- Name for argument of invariant procedure
procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
-- Appends statements to Stmts for any invariants in the rep item chain
@ -7836,246 +7858,229 @@ package body Sem_Ch13 is
-- "inherited" to the exception message and generating an informational
-- message about the inheritance of an invariant.
Object_Name : Name_Id;
-- Name for argument of invariant procedure
Object_Entity : Node_Id;
-- The entity of the formal for the procedure
--------------------
-- Add_Invariants --
--------------------
procedure Add_Invariants (T : Entity_Id; Inherit : Boolean) is
Ritem : Node_Id;
Arg1 : Node_Id;
Arg2 : Node_Id;
Arg3 : Node_Id;
Exp : Node_Id;
Loc : Source_Ptr;
Assoc : List_Id;
Str : String_Id;
procedure Add_Invariant (Prag : Node_Id);
-- Create a runtime check to verify the exression of invariant pragma
-- Prag. All generated code is added to list Stmts.
procedure Replace_Type_Reference (N : Node_Id);
-- Replace a single occurrence N of the subtype name with a reference
-- to the formal of the predicate function. N can be an identifier
-- referencing the subtype, or a selected component, representing an
-- appropriately qualified occurrence of the subtype name.
-------------------
-- Add_Invariant --
-------------------
procedure Replace_Type_References is
new Replace_Type_References_Generic (Replace_Type_Reference);
-- Traverse an expression replacing all occurrences of the subtype
-- name with appropriate references to the object that is the formal
-- parameter of the predicate function. Note that we must ensure
-- that the type and entity information is properly set in the
-- replacement node, since we will do a Preanalyze call of this
-- expression without proper visibility of the procedure argument.
procedure Add_Invariant (Prag : Node_Id) is
procedure Replace_Type_Reference (N : Node_Id);
-- Replace a single occurrence N of the subtype name with a
-- reference to the formal of the predicate function. N can be an
-- identifier referencing the subtype, or a selected component,
-- representing an appropriately qualified occurrence of the
-- subtype name.
----------------------------
-- Replace_Type_Reference --
----------------------------
procedure Replace_Type_References is
new Replace_Type_References_Generic (Replace_Type_Reference);
-- Traverse an expression replacing all occurrences of the subtype
-- name with appropriate references to the formal of the predicate
-- function. Note that we must ensure that the type and entity
-- information is properly set in the replacement node, since we
-- will do a Preanalyze call of this expression without proper
-- visibility of the procedure argument.
-- Note: See comments in Add_Predicates.Replace_Type_Reference
-- regarding handling of Sloc and Comes_From_Source.
----------------------------
-- Replace_Type_Reference --
----------------------------
procedure Replace_Type_Reference (N : Node_Id) is
begin
-- Note: See comments in Add_Predicates.Replace_Type_Reference
-- regarding handling of Sloc and Comes_From_Source.
-- Add semantic information to node to be rewritten, for ASIS
-- navigation needs.
procedure Replace_Type_Reference (N : Node_Id) is
Nloc : constant Source_Ptr := Sloc (N);
if Nkind (N) = N_Identifier then
Set_Entity (N, T);
Set_Etype (N, T);
begin
-- Add semantic information to node to be rewritten, for ASIS
-- navigation needs.
elsif Nkind (N) = N_Selected_Component then
Analyze (Prefix (N));
Set_Entity (Selector_Name (N), T);
Set_Etype (Selector_Name (N), T);
end if;
if Nkind (N) = N_Identifier then
Set_Entity (N, T);
Set_Etype (N, T);
-- Invariant'Class, replace with T'Class (obj)
-- In ASIS mode, an inherited item is analyzed already, and the
-- replacement has been done, so do not repeat transformation
-- to prevent ill-formed tree.
if Class_Present (Ritem) then
if ASIS_Mode
and then Nkind (Parent (N)) = N_Attribute_Reference
and then Attribute_Name (Parent (N)) = Name_Class
then
null;
else
Rewrite (N,
Make_Type_Conversion (Sloc (N),
Subtype_Mark =>
Make_Attribute_Reference (Sloc (N),
Prefix => New_Occurrence_Of (T, Sloc (N)),
Attribute_Name => Name_Class),
Expression =>
Make_Identifier (Sloc (N), Object_Name)));
Set_Entity (Expression (N), Object_Entity);
Set_Etype (Expression (N), Typ);
elsif Nkind (N) = N_Selected_Component then
Analyze (Prefix (N));
Set_Entity (Selector_Name (N), T);
Set_Etype (Selector_Name (N), T);
end if;
-- Invariant, replace with obj
-- Invariant'Class, replace with T'Class (obj)
if Class_Present (Prag) then
-- In ASIS mode, an inherited item is already analyzed,
-- and the replacement has been done, so do not repeat
-- the transformation to prevent a malformed tree.
if ASIS_Mode
and then Nkind (Parent (N)) = N_Attribute_Reference
and then Attribute_Name (Parent (N)) = Name_Class
then
null;
else
Rewrite (N,
Make_Type_Conversion (Nloc,
Subtype_Mark =>
Make_Attribute_Reference (Nloc,
Prefix => New_Occurrence_Of (T, Nloc),
Attribute_Name => Name_Class),
Expression => Make_Identifier (Nloc, Object_Name)));
Set_Entity (Expression (N), Object_Entity);
Set_Etype (Expression (N), Typ);
end if;
-- Invariant, replace with obj
else
Rewrite (N, Make_Identifier (Nloc, Object_Name));
Set_Entity (N, Object_Entity);
Set_Etype (N, Typ);
end if;
Set_Comes_From_Source (N, True);
end Replace_Type_Reference;
-- Local variables
Asp : constant Node_Id := Corresponding_Aspect (Prag);
Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
Ploc : constant Source_Ptr := Sloc (Prag);
Arg1 : Node_Id;
Arg2 : Node_Id;
Arg3 : Node_Id;
Assoc : List_Id;
Expr : Node_Id;
Str : String_Id;
-- Start of processing for Add_Invariant
begin
-- Extract the arguments of the invariant pragma
Arg1 := First (Pragma_Argument_Associations (Prag));
Arg2 := Next (Arg1);
Arg3 := Next (Arg2);
Arg1 := Get_Pragma_Arg (Arg1);
Arg2 := Get_Pragma_Arg (Arg2);
-- The caller requests processing of all Invariant'Class pragmas,
-- but the current pragma does not fall in this category. Return
-- as there is nothing left to do.
if Inherit then
if not Class_Present (Prag) then
return;
end if;
-- Otherwise the pragma must apply to the current type
elsif Entity (Arg1) /= T then
return;
end if;
Expr := New_Copy_Tree (Arg2);
-- Replace all occurrences of the type's name with references to
-- the formal parameter of the invariant procedure.
Replace_Type_References (Expr, T);
-- If the invariant pragma comes from an aspect, replace the saved
-- expression because we need the subtype references replaced for
-- the calls to Preanalyze_Spec_Expression in Check_Aspect_At_xxx
-- routines.
if Present (Asp) then
Set_Entity (Identifier (Asp), New_Copy_Tree (Expr));
end if;
-- Preanalyze the invariant expression to capture the visibility
-- of the proper package part. In general the expression is not
-- fully analyzed until the body of the invariant procedure is
-- analyzed at the end of the private part, but that yields the
-- wrong visibility.
-- Historic note: we used to set N as the parent, but a package
-- specification as the parent of an expression is bizarre.
Set_Parent (Expr, Parent (Arg2));
Preanalyze_Assert_Expression (Expr, Any_Boolean);
-- A class-wide invariant may be inherited in a separate unit,
-- where the corresponding expression cannot be resolved by
-- visibility, because it refers to a local function. Propagate
-- semantic information to the original representation item, to
-- be used when an invariant procedure for a derived type is
-- constructed.
-- ??? Unclear how to handle class-wide invariants that are not
-- function calls.
if not Inherit
and then Class_Present (Prag)
and then Nkind (Expr) = N_Function_Call
and then Nkind (Arg2) = N_Indexed_Component
then
Rewrite (Arg2,
Make_Function_Call (Ploc,
Name =>
New_Occurrence_Of (Entity (Name (Expr)), Ploc),
Parameter_Associations =>
New_Copy_List (Expressions (Arg2))));
end if;
-- In ASIS mode, even if assertions are not enabled, we must
-- analyze the original expression in the aspect specification
-- because it is part of the original tree.
if ASIS_Mode and then Present (Asp) then
declare
Orig_Expr : constant Node_Id := Expression (Asp);
begin
Replace_Type_References (Orig_Expr, T);
Preanalyze_Assert_Expression (Orig_Expr, Any_Boolean);
end;
end if;
-- An ignored invariant must not generate a runtime check. Add a
-- null statement to ensure that the invariant procedure does get
-- a completing body.
if No (Stmts) then
Stmts := Empty_List;
end if;
if Is_Ignored (Prag) then
Append_To (Stmts, Make_Null_Statement (Ploc));
-- Otherwise the invariant is checked. Build a Check pragma to
-- verify the expression at runtime.
else
Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
Set_Entity (N, Object_Entity);
Set_Etype (N, Typ);
end if;
Assoc := New_List (
Make_Pragma_Argument_Association (Ploc,
Expression => Make_Identifier (Ploc, Nam)),
Make_Pragma_Argument_Association (Ploc,
Expression => Expr));
Set_Comes_From_Source (N, True);
end Replace_Type_Reference;
-- Start of processing for Add_Invariants
begin
Ritem := First_Rep_Item (T);
while Present (Ritem) loop
if Nkind (Ritem) = N_Pragma
and then Pragma_Name (Ritem) = Name_Invariant
then
Arg1 := First (Pragma_Argument_Associations (Ritem));
Arg2 := Next (Arg1);
Arg3 := Next (Arg2);
Arg1 := Get_Pragma_Arg (Arg1);
Arg2 := Get_Pragma_Arg (Arg2);
-- For Inherit case, ignore Invariant, process only Class case
if Inherit then
if not Class_Present (Ritem) then
goto Continue;
end if;
-- For Inherit false, process only item for right type
else
if Entity (Arg1) /= Typ then
goto Continue;
end if;
end if;
if No (Stmts) then
Stmts := Empty_List;
end if;
Exp := New_Copy_Tree (Arg2);
-- Preserve sloc of original pragma Invariant
Loc := Sloc (Ritem);
-- We need to replace any occurrences of the name of the type
-- with references to the object, converted to type'Class in
-- the case of Invariant'Class aspects.
Replace_Type_References (Exp, T);
-- If this invariant comes from an aspect, find the aspect
-- specification, and replace the saved expression because
-- we need the subtype references replaced for the calls to
-- Preanalyze_Spec_Expressin in Check_Aspect_At_Freeze_Point
-- and Check_Aspect_At_End_Of_Declarations.
if From_Aspect_Specification (Ritem) then
declare
Aitem : Node_Id;
begin
-- Loop to find corresponding aspect, note that this
-- must be present given the pragma is marked delayed.
-- Note: in practice Next_Rep_Item (Ritem) is Empty so
-- this loop does nothing. Furthermore, why isn't this
-- simply Corresponding_Aspect ???
Aitem := Next_Rep_Item (Ritem);
while Present (Aitem) loop
if Nkind (Aitem) = N_Aspect_Specification
and then Aspect_Rep_Item (Aitem) = Ritem
then
Set_Entity
(Identifier (Aitem), New_Copy_Tree (Exp));
exit;
end if;
Aitem := Next_Rep_Item (Aitem);
end loop;
end;
end if;
-- Now we need to preanalyze the expression to properly capture
-- the visibility in the visible part. The expression will not
-- be analyzed for real until the body is analyzed, but that is
-- at the end of the private part and has the wrong visibility.
Set_Parent (Exp, N);
Preanalyze_Assert_Expression (Exp, Any_Boolean);
-- A class-wide invariant may be inherited in a separate unit,
-- where the corresponding expression cannot be resolved by
-- visibility, because it refers to a local function. Propagate
-- semantic information to the original representation item, to
-- be used when an invariant procedure for a derived type is
-- constructed.
-- Unclear how to handle class-wide invariants that are not
-- function calls ???
if not Inherit
and then Class_Present (Ritem)
and then Nkind (Exp) = N_Function_Call
and then Nkind (Arg2) = N_Indexed_Component
then
Rewrite (Arg2,
Make_Function_Call (Loc,
Name =>
New_Occurrence_Of (Entity (Name (Exp)), Loc),
Parameter_Associations =>
New_Copy_List (Expressions (Arg2))));
end if;
-- In ASIS mode, even if assertions are not enabled, we must
-- analyze the original expression in the aspect specification
-- because it is part of the original tree.
if ASIS_Mode and then From_Aspect_Specification (Ritem) then
declare
Inv : constant Node_Id :=
Expression (Corresponding_Aspect (Ritem));
begin
Replace_Type_References (Inv, T);
Preanalyze_Assert_Expression (Inv, Standard_Boolean);
end;
end if;
-- Get name to be used for Check pragma. Using the original
-- name ensures that 'Class case is properly handled.
Nam := Original_Aspect_Pragma_Name (Ritem);
-- Build first two arguments for Check pragma
Assoc :=
New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Make_Identifier (Loc, Chars => Nam)),
Make_Pragma_Argument_Association (Loc,
Expression => Exp));
-- Add message if present in Invariant pragma
-- Handle the String argument (if any)
if Present (Arg3) then
Str := Strval (Get_Pragma_Arg (Arg3));
-- If inherited case, and message starts "failed invariant",
-- change it to be "failed inherited invariant".
-- When inheriting an invariant, modify the message from
-- "failed invariant" to "failed inherited invariant".
if Inherit then
String_To_Name_Buffer (Str);
@ -8087,30 +8092,45 @@ package body Sem_Ch13 is
end if;
Append_To (Assoc,
Make_Pragma_Argument_Association (Loc,
Expression => Make_String_Literal (Loc, Str)));
Make_Pragma_Argument_Association (Ploc,
Expression => Make_String_Literal (Ploc, Str)));
end if;
-- Add Check pragma to list of statements
-- Generate:
-- pragma Check (Nam, Expr, Str);
Append_To (Stmts,
Make_Pragma (Loc,
Make_Pragma (Ploc,
Pragma_Identifier =>
Make_Identifier (Loc, Name_Check),
Make_Identifier (Ploc, Name_Check),
Pragma_Argument_Associations => Assoc));
-- If Inherited case and option enabled, output info msg. Note
-- that we know this is a case of Invariant'Class.
if Inherit and Opt.List_Inherited_Aspects then
Error_Msg_Sloc := Sloc (Ritem);
Error_Msg_N
("info: & inherits `Invariant''Class` aspect from #?L?",
Typ);
end if;
end if;
<<Continue>>
-- Output an info message when inheriting an invariant and the
-- listing option is enabled.
if Inherit and Opt.List_Inherited_Aspects then
Error_Msg_Sloc := Sloc (Prag);
Error_Msg_N
("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
end if;
end Add_Invariant;
-- Local variables
Ritem : Node_Id;
-- Start of processing for Add_Invariants
begin
Ritem := First_Rep_Item (T);
while Present (Ritem) loop
if Nkind (Ritem) = N_Pragma
and then Pragma_Name (Ritem) = Name_Invariant
then
Add_Invariant (Ritem);
end if;
Next_Rep_Item (Ritem);
end loop;
end Add_Invariants;
@ -8228,13 +8248,13 @@ package body Sem_Ch13 is
-- If declaration is already analyzed, it was processed by the
-- generated pragma.
if Present (Private_Decls) then
if Present (Priv_Decls) then
-- The spec goes at the end of visible declarations, but they have
-- already been analyzed, so we need to explicitly do the analyze.
if not Analyzed (PDecl) then
Append_To (Visible_Decls, PDecl);
Append_To (Vis_Decls, PDecl);
Analyze (PDecl);
end if;
@ -8243,7 +8263,7 @@ package body Sem_Ch13 is
-- analyze call. We skip this if there are no private declarations
-- (this is an error that will be caught elsewhere);
Append_To (Private_Decls, PBody);
Append_To (Priv_Decls, PBody);
-- If the invariant appears on the full view of a type, the
-- analysis of the private part is complete, and we must
@ -8261,8 +8281,8 @@ package body Sem_Ch13 is
-- that the type is about to be frozen.
elsif not Is_Private_Type (Typ) then
Append_To (Visible_Decls, PDecl);
Append_To (Visible_Decls, PBody);
Append_To (Vis_Decls, PDecl);
Append_To (Vis_Decls, PBody);
Analyze (PDecl);
Analyze (PBody);
end if;
@ -8332,13 +8352,6 @@ package body Sem_Ch13 is
-- Inheritance of predicates for the parent type is done by calling the
-- Predicate_Function of the parent type, using Add_Call above.
function Test_RE (N : Node_Id) return Traverse_Result;
-- Used in Test_REs, tests one node for being a raise expression, and if
-- so sets Raise_Expression_Present True.
procedure Test_REs is new Traverse_Proc (Test_RE);
-- Tests to see if Expr contains any raise expressions
function Process_RE (N : Node_Id) return Traverse_Result;
-- Used in Process REs, tests if node N is a raise expression, and if
-- so, marks it to be converted to return False.
@ -8346,6 +8359,13 @@ package body Sem_Ch13 is
procedure Process_REs is new Traverse_Proc (Process_RE);
-- Marks any raise expressions in Expr_M to return False
function Test_RE (N : Node_Id) return Traverse_Result;
-- Used in Test_REs, tests one node for being a raise expression, and if
-- so sets Raise_Expression_Present True.
procedure Test_REs is new Traverse_Proc (Test_RE);
-- Tests to see if Expr contains any raise expressions
--------------
-- Add_Call --
--------------
@ -8399,128 +8419,121 @@ package body Sem_Ch13 is
--------------------
procedure Add_Predicates is
Ritem : Node_Id;
Arg1 : Node_Id;
Arg2 : Node_Id;
procedure Add_Predicate (Prag : Node_Id);
-- Concatenate the expression of predicate pragma Prag to Expr by
-- using a short circuit "and then" operator.
procedure Replace_Type_Reference (N : Node_Id);
-- Replace a single occurrence N of the subtype name with a reference
-- to the formal of the predicate function. N can be an identifier
-- referencing the subtype, or a selected component, representing an
-- appropriately qualified occurrence of the subtype name.
-------------------
-- Add_Predicate --
-------------------
procedure Replace_Type_References is
new Replace_Type_References_Generic (Replace_Type_Reference);
-- Traverse an expression changing every occurrence of an identifier
-- whose name matches the name of the subtype with a reference to
-- the formal parameter of the predicate function.
procedure Add_Predicate (Prag : Node_Id) is
procedure Replace_Type_Reference (N : Node_Id);
-- Replace a single occurrence N of the subtype name with a
-- reference to the formal of the predicate function. N can be an
-- identifier referencing the subtype, or a selected component,
-- representing an appropriately qualified occurrence of the
-- subtype name.
----------------------------
-- Replace_Type_Reference --
----------------------------
procedure Replace_Type_References is
new Replace_Type_References_Generic (Replace_Type_Reference);
-- Traverse an expression changing every occurrence of an
-- identifier whose name matches the name of the subtype with a
-- reference to the formal parameter of the predicate function.
----------------------------
-- Replace_Type_Reference --
----------------------------
procedure Replace_Type_Reference (N : Node_Id) is
begin
Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
-- Use the Sloc of the usage name, not the defining name
Set_Etype (N, Typ);
Set_Entity (N, Object_Entity);
-- We want to treat the node as if it comes from source, so
-- that ASIS will not ignore it.
Set_Comes_From_Source (N, True);
end Replace_Type_Reference;
-- Local variables
Asp : constant Node_Id := Corresponding_Aspect (Prag);
Arg1 : Node_Id;
Arg2 : Node_Id;
-- Start of processing for Add_Predicate
procedure Replace_Type_Reference (N : Node_Id) is
begin
Rewrite (N, Make_Identifier (Sloc (N), Object_Name));
-- Use the Sloc of the usage name, not the defining name
-- Extract the arguments of the pragma. The expression itself
-- is copied for use in the predicate function, to preserve the
-- original version for ASIS use.
Set_Etype (N, Typ);
Set_Entity (N, Object_Entity);
Arg1 := First (Pragma_Argument_Associations (Prag));
Arg2 := Next (Arg1);
-- We want to treat the node as if it comes from source, so that
-- ASIS will not ignore it
Arg1 := Get_Pragma_Arg (Arg1);
Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2));
Set_Comes_From_Source (N, True);
end Replace_Type_Reference;
-- When the predicate pragma applies to the current type or its
-- full view, replace all occurrences of the subtype name with
-- references to the formal parameter of the predicate function.
if Entity (Arg1) = Typ
or else Full_View (Entity (Arg1)) = Typ
then
Replace_Type_References (Arg2, Typ);
-- If the predicate pragma comes from an aspect, replace the
-- saved expression because we need the subtype references
-- replaced for the calls to Preanalyze_Spec_Expression in
-- Check_Aspect_At_xxx routines.
if Present (Asp) then
-- For ASIS use, perform semantic analysis of the original
-- predicate expression, which is otherwise not utilized.
if ASIS_Mode then
Preanalyze_And_Resolve (Expression (Asp));
end if;
Set_Entity (Identifier (Asp), New_Copy_Tree (Arg2));
end if;
-- Concatenate to the existing predicate expressions by using
-- "and then".
if Present (Expr) then
Expr :=
Make_And_Then (Loc,
Left_Opnd => Relocate_Node (Expr),
Right_Opnd => Relocate_Node (Arg2));
-- Otherwise this is the first predicate expression
else
Expr := Relocate_Node (Arg2);
end if;
end if;
end Add_Predicate;
-- Local variables
Ritem : Node_Id;
-- Start of processing for Add_Predicates
begin
Ritem := First_Rep_Item (Typ);
while Present (Ritem) loop
if Nkind (Ritem) = N_Pragma
and then Pragma_Name (Ritem) = Name_Predicate
then
-- Acquire arguments. The expression itself is copied for use
-- in the predicate function, to preserve the original version
-- for ASIS use.
Arg1 := First (Pragma_Argument_Associations (Ritem));
Arg2 := Next (Arg1);
Arg1 := Get_Pragma_Arg (Arg1);
Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2));
-- See if this predicate pragma is for the current type or for
-- its full view. A predicate on a private completion is placed
-- on the partial view beause this is the visible entity that
-- is frozen.
if Entity (Arg1) = Typ
or else Full_View (Entity (Arg1)) = Typ
then
-- We have a match, this entry is for our subtype
-- We need to replace any occurrences of the name of the
-- type with references to the object.
Replace_Type_References (Arg2, Typ);
-- If this predicate comes from an aspect, find the aspect
-- specification, and replace the saved expression because
-- we need the subtype references replaced for the calls to
-- Preanalyze_Spec_Expressin in Check_Aspect_At_Freeze_Point
-- and Check_Aspect_At_End_Of_Declarations.
if From_Aspect_Specification (Ritem) then
declare
Aitem : Node_Id;
Orig_Expr : constant Node_Id :=
Expression (Corresponding_Aspect (Ritem));
begin
-- For ASIS use, perform semantic analysis of the
-- original predicate expression, which is otherwise
-- not utilized.
if ASIS_Mode then
Preanalyze_And_Resolve (Orig_Expr);
end if;
-- Loop to find corresponding aspect, note that this
-- must be present given the pragma is marked delayed.
Aitem := Next_Rep_Item (Ritem);
loop
if Nkind (Aitem) = N_Aspect_Specification
and then Aspect_Rep_Item (Aitem) = Ritem
then
Set_Entity
(Identifier (Aitem), New_Copy_Tree (Arg2));
exit;
end if;
Aitem := Next_Rep_Item (Aitem);
end loop;
end;
end if;
-- Now we can add the expression
if No (Expr) then
Expr := Relocate_Node (Arg2);
-- There already was a predicate, so add to it
else
Expr :=
Make_And_Then (Loc,
Left_Opnd => Relocate_Node (Expr),
Right_Opnd => Relocate_Node (Arg2));
end if;
end if;
Add_Predicate (Ritem);
end if;
Next_Rep_Item (Ritem);
@ -8555,6 +8568,10 @@ package body Sem_Ch13 is
end if;
end Test_RE;
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Build_Predicate_Functions
begin
@ -8566,6 +8583,12 @@ package body Sem_Ch13 is
return;
end if;
-- The related type may be subject to pragma Ghost with policy Ignore.
-- Set the mode now to ensure that the predicate functions are properly
-- flagged as ignored Ghost.
Set_Ghost_Mode_From_Entity (Typ);
-- Prepare to construct predicate expression
Expr := Empty;
@ -8670,6 +8693,13 @@ package body Sem_Ch13 is
Set_Predicate_Function (Full_View (Typ), SId);
end if;
-- Mark the predicate function explicitly as Ghost because it does
-- not come from source.
if Ghost_Mode > None then
Set_Is_Ghost_Entity (SId);
end if;
Spec :=
Make_Function_Specification (Loc,
Defining_Unit_Name => SId,
@ -8750,6 +8780,13 @@ package body Sem_Ch13 is
Set_Predicate_Function_M (Full_View (Typ), SId);
end if;
-- Mark the predicate function explicitly as Ghost because it
-- does not come from source.
if Ghost_Mode > None then
Set_Is_Ghost_Entity (SId);
end if;
Spec :=
Make_Function_Specification (Loc,
Defining_Unit_Name => SId,
@ -8896,6 +8933,11 @@ package body Sem_Ch13 is
end if;
end;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Build_Predicate_Functions;
-----------------------------------------

115
gcc/ada/sem_ch3.adb
View file

@ -2558,6 +2558,7 @@ package body Sem_Ch3 is
procedure Analyze_Full_Type_Declaration (N : Node_Id) is
Def : constant Node_Id := Type_Definition (N);
Def_Id : constant Entity_Id := Defining_Identifier (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
T : Entity_Id;
Prev : Entity_Id;
@ -2575,6 +2576,9 @@ package body Sem_Ch3 is
-- list later in Sem_Disp.Check_Operation_From_Incomplete_Type (which
-- is called from Process_Incomplete_Dependents).
procedure Restore_Globals;
-- Restore the values of all saved global variables
------------------------------------
-- Check_Ops_From_Incomplete_Type --
------------------------------------
@ -2612,6 +2616,15 @@ package body Sem_Ch3 is
end if;
end Check_Ops_From_Incomplete_Type;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-- Start of processing for Analyze_Full_Type_Declaration
begin
@ -2760,6 +2773,7 @@ package body Sem_Ch3 is
end if;
if Etype (T) = Any_Type then
Restore_Globals;
return;
end if;
@ -2772,7 +2786,7 @@ package body Sem_Ch3 is
-- A type declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Comes_From_Source (T) and then Ghost_Mode > None then
if Ghost_Mode > None then
Set_Is_Ghost_Entity (T);
end if;
@ -2900,6 +2914,8 @@ package body Sem_Ch3 is
Analyze_Aspect_Specifications (N, Def_Id);
end if;
end if;
Restore_Globals;
end Analyze_Full_Type_Declaration;
----------------------------------
@ -2907,12 +2923,18 @@ package body Sem_Ch3 is
----------------------------------
procedure Analyze_Incomplete_Type_Decl (N : Node_Id) is
F : constant Boolean := Is_Pure (Current_Scope);
T : Entity_Id;
F : constant Boolean := Is_Pure (Current_Scope);
GM : constant Ghost_Mode_Type := Ghost_Mode;
T : Entity_Id;
begin
Check_SPARK_05_Restriction ("incomplete type is not allowed", N);
-- The incomplete 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 (Defining_Identifier (N));
-- Process an incomplete declaration. The identifier must not have been
@ -2962,6 +2984,11 @@ package body Sem_Ch3 is
Set_Private_Dependents (T, New_Elmt_List);
Set_Is_Pure (T, F);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Incomplete_Type_Decl;
-----------------------------------
@ -3036,11 +3063,29 @@ package body Sem_Ch3 is
--------------------------------
procedure Analyze_Number_Declaration (N : Node_Id) is
Id : constant Entity_Id := Defining_Identifier (N);
GM : constant Ghost_Mode_Type := Ghost_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
E : constant Node_Id := Expression (N);
T : Entity_Id;
Id : constant Entity_Id := Defining_Identifier (N);
Index : Interp_Index;
It : Interp;
T : Entity_Id;
-- Start of processing for Analyze_Number_Declaration
begin
-- The number declaration may be subject to pragma Ghost with policy
@ -3068,6 +3113,8 @@ package body Sem_Ch3 is
Set_Etype (Id, Universal_Integer);
Set_Ekind (Id, E_Named_Integer);
Set_Is_Frozen (Id, True);
Restore_Globals;
return;
end if;
@ -3169,6 +3216,8 @@ package body Sem_Ch3 is
Set_Ekind (Id, E_Constant);
Set_Never_Set_In_Source (Id, True);
Set_Is_True_Constant (Id, True);
Restore_Globals;
return;
end if;
@ -3182,6 +3231,8 @@ package body Sem_Ch3 is
Rewrite (E, Make_Integer_Literal (Sloc (N), 1));
Set_Etype (E, Any_Type);
end if;
Restore_Globals;
end Analyze_Number_Declaration;
-----------------------------
@ -3355,10 +3406,11 @@ package body Sem_Ch3 is
--------------------------------
procedure Analyze_Object_Declaration (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
T : Entity_Id;
Loc : constant Source_Ptr := Sloc (N);
Act_T : Entity_Id;
T : Entity_Id;
E : Node_Id := Expression (N);
-- E is set to Expression (N) throughout this routine. When
@ -3385,6 +3437,9 @@ package body Sem_Ch3 is
-- Any other relevant delayed aspects on object declarations ???
procedure Restore_Globals;
-- Restore the values of all saved global variables
-----------------
-- Count_Tasks --
-----------------
@ -3463,6 +3518,15 @@ package body Sem_Ch3 is
return False;
end Delayed_Aspect_Present;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-- Start of processing for Analyze_Object_Declaration
begin
@ -3802,6 +3866,7 @@ package body Sem_Ch3 is
and then Analyzed (N)
and then No (Expression (N))
then
Restore_Globals;
return;
end if;
@ -4073,6 +4138,8 @@ package body Sem_Ch3 is
Set_Renamed_Object (Id, E);
Freeze_Before (N, T);
Set_Is_Frozen (Id);
Restore_Globals;
return;
else
@ -4419,7 +4486,8 @@ package body Sem_Ch3 is
-- Deal with setting In_Private_Part flag if in private part
if Ekind (Scope (Id)) = E_Package and then In_Private_Part (Scope (Id))
if Ekind (Scope (Id)) = E_Package
and then In_Private_Part (Scope (Id))
then
Set_In_Private_Part (Id);
end if;
@ -4453,6 +4521,8 @@ package body Sem_Ch3 is
if Ekind (Id) = E_Variable then
Check_No_Hidden_State (Id);
end if;
Restore_Globals;
end Analyze_Object_Declaration;
---------------------------
@ -4473,10 +4543,11 @@ package body Sem_Ch3 is
-------------------------------------------
procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
T : constant Entity_Id := Defining_Identifier (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Indic : constant Node_Id := Subtype_Indication (N);
Parent_Type : Entity_Id;
T : constant Entity_Id := Defining_Identifier (N);
Parent_Base : Entity_Id;
Parent_Type : Entity_Id;
begin
-- The private extension declaration may be subject to pragma Ghost with
@ -4698,6 +4769,11 @@ package body Sem_Ch3 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, T);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Private_Extension_Declaration;
---------------------------------
@ -4708,9 +4784,10 @@ package body Sem_Ch3 is
(N : Node_Id;
Skip : Boolean := False)
is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
T : Entity_Id;
R_Checks : Check_Result;
T : Entity_Id;
begin
-- The subtype declaration may be subject to pragma Ghost with policy
@ -5316,6 +5393,11 @@ package body Sem_Ch3 is
end if;
Analyze_Dimension (N);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Subtype_Declaration;
--------------------------------
@ -10809,7 +10891,6 @@ package body Sem_Ch3 is
----------------
procedure Post_Error is
procedure Missing_Body;
-- Output missing body message
@ -10835,7 +10916,6 @@ package body Sem_Ch3 is
begin
if not Comes_From_Source (E) then
if Ekind_In (E, E_Task_Type, E_Protected_Type) then
-- It may be an anonymous protected type created for a
@ -19963,11 +20043,7 @@ package body Sem_Ch3 is
Private_To_Full_View => True);
end if;
-- Propagate the attributes related to pragma Ghost from the private to
-- the full view.
if Is_Ghost_Entity (Priv_T) then
Set_Is_Ghost_Entity (Full_T);
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(14)).
@ -19981,6 +20057,11 @@ package body Sem_Ch3 is
if Is_Derived_Type (Full_T) then
Check_Ghost_Derivation (Full_T);
end if;
-- Propagate the attributes related to pragma Ghost from the private
-- to the full view.
Mark_Full_View_As_Ghost (Priv_T, Full_T);
end if;
-- Propagate invariants to full type

24
gcc/ada/sem_ch5.adb
View file

@ -90,6 +90,7 @@ package body Sem_Ch5 is
------------------------
procedure Analyze_Assignment (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Lhs : constant Node_Id := Name (N);
Rhs : constant Node_Id := Expression (N);
T1 : Entity_Id;
@ -106,6 +107,9 @@ package body Sem_Ch5 is
-- the assignment, and at the end of processing before setting any new
-- current values in place.
procedure Restore_Globals;
-- Restore the values of all saved global variables
procedure Set_Assignment_Type
(Opnd : Node_Id;
Opnd_Type : in out Entity_Id);
@ -211,6 +215,15 @@ package body Sem_Ch5 is
end if;
end Kill_Lhs;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-------------------------
-- Set_Assignment_Type --
-------------------------
@ -378,6 +391,7 @@ package body Sem_Ch5 is
Error_Msg_N
("no valid types for left-hand side for assignment", Lhs);
Kill_Lhs;
Restore_Globals;
return;
end if;
end if;
@ -453,12 +467,14 @@ package body Sem_Ch5 is
"specified??", Lhs);
end if;
Restore_Globals;
return;
end if;
end if;
end;
Diagnose_Non_Variable_Lhs (Lhs);
Restore_Globals;
return;
-- Error of assigning to limited type. We do however allow this in
@ -478,6 +494,8 @@ package body Sem_Ch5 is
("left hand of assignment must not be limited type", Lhs);
Explain_Limited_Type (T1, Lhs);
end if;
Restore_Globals;
return;
-- Enforce RM 3.9.3 (8): the target of an assignment operation cannot be
@ -516,6 +534,7 @@ package body Sem_Ch5 is
then
Error_Msg_N ("invalid use of incomplete type", Lhs);
Kill_Lhs;
Restore_Globals;
return;
end if;
@ -533,6 +552,7 @@ package body Sem_Ch5 is
if Rhs = Error then
Kill_Lhs;
Restore_Globals;
return;
end if;
@ -541,6 +561,7 @@ package body Sem_Ch5 is
if not Covers (T1, T2) then
Wrong_Type (Rhs, Etype (Lhs));
Kill_Lhs;
Restore_Globals;
return;
end if;
@ -568,6 +589,7 @@ package body Sem_Ch5 is
if T1 = Any_Type or else T2 = Any_Type then
Kill_Lhs;
Restore_Globals;
return;
end if;
@ -660,6 +682,7 @@ package body Sem_Ch5 is
-- to reset Is_True_Constant, and desirable for xref purposes.
Note_Possible_Modification (Lhs, Sure => True);
Restore_Globals;
return;
-- If we know the right hand side is non-null, then we convert to the
@ -866,6 +889,7 @@ package body Sem_Ch5 is
end;
Analyze_Dimension (N);
Restore_Globals;
end Analyze_Assignment;
-----------------------------

146
gcc/ada/sem_ch6.adb
View file

@ -209,9 +209,10 @@ package body Sem_Ch6 is
---------------------------------------------
procedure Analyze_Abstract_Subprogram_Declaration (N : Node_Id) is
Designator : constant Entity_Id :=
Analyze_Subprogram_Specification (Specification (N));
Scop : constant Entity_Id := Current_Scope;
GM : constant Ghost_Mode_Type := Ghost_Mode;
Scop : constant Entity_Id := Current_Scope;
Subp_Id : constant Entity_Id :=
Analyze_Subprogram_Specification (Specification (N));
begin
-- The abstract subprogram declaration may be subject to pragma Ghost
@ -222,45 +223,49 @@ package body Sem_Ch6 is
Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Designator);
Generate_Definition (Subp_Id);
Set_Is_Abstract_Subprogram (Designator);
New_Overloaded_Entity (Designator);
Check_Delayed_Subprogram (Designator);
Set_Is_Abstract_Subprogram (Subp_Id);
New_Overloaded_Entity (Subp_Id);
Check_Delayed_Subprogram (Subp_Id);
Set_Categorization_From_Scope (Designator, Scop);
Set_Categorization_From_Scope (Subp_Id, Scop);
-- An abstract subprogram declared within a Ghost region is rendered
-- Ghost (SPARK RM 6.9(2)).
if Comes_From_Source (Designator) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Designator);
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Subp_Id);
end if;
if Ekind (Scope (Designator)) = E_Protected_Type then
Error_Msg_N
("abstract subprogram not allowed in protected type", N);
if Ekind (Scope (Subp_Id)) = E_Protected_Type then
Error_Msg_N ("abstract subprogram not allowed in protected type", N);
-- Issue a warning if the abstract subprogram is neither a dispatching
-- operation nor an operation that overrides an inherited subprogram or
-- predefined operator, since this most likely indicates a mistake.
elsif Warn_On_Redundant_Constructs
and then not Is_Dispatching_Operation (Designator)
and then not Present (Overridden_Operation (Designator))
and then (not Is_Operator_Symbol_Name (Chars (Designator))
or else Scop /= Scope (Etype (First_Formal (Designator))))
and then not Is_Dispatching_Operation (Subp_Id)
and then not Present (Overridden_Operation (Subp_Id))
and then (not Is_Operator_Symbol_Name (Chars (Subp_Id))
or else Scop /= Scope (Etype (First_Formal (Subp_Id))))
then
Error_Msg_N
("abstract subprogram is not dispatching or overriding?r?", N);
end if;
Generate_Reference_To_Formals (Designator);
Check_Eliminated (Designator);
Generate_Reference_To_Formals (Subp_Id);
Check_Eliminated (Subp_Id);
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Designator);
Analyze_Aspect_Specifications (N, Subp_Id);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Abstract_Subprogram_Declaration;
---------------------------------
@ -1542,16 +1547,15 @@ package body Sem_Ch6 is
----------------------------
procedure Analyze_Procedure_Call (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
P : constant Node_Id := Name (N);
Actuals : constant List_Id := Parameter_Associations (N);
Actual : Node_Id;
New_N : Node_Id;
GM : constant Ghost_Mode_Type := Ghost_Mode;
procedure Analyze_Call_And_Resolve;
-- Do Analyze and Resolve calls for procedure call
-- At end, check illegal order dependence.
procedure Restore_Globals;
-- Restore the values of all saved global variables
------------------------------
-- Analyze_Call_And_Resolve --
------------------------------
@ -1566,6 +1570,23 @@ package body Sem_Ch6 is
end if;
end Analyze_Call_And_Resolve;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
-- Local variables
Actuals : constant List_Id := Parameter_Associations (N);
Loc : constant Source_Ptr := Sloc (N);
P : constant Node_Id := Name (N);
Actual : Node_Id;
New_N : Node_Id;
-- Start of processing for Analyze_Procedure_Call
begin
@ -1636,6 +1657,7 @@ package body Sem_Ch6 is
and then Is_Record_Type (Etype (Entity (P)))
and then Remote_AST_I_Dereference (P)
then
Restore_Globals;
return;
elsif Is_Entity_Name (P)
@ -1771,6 +1793,8 @@ package body Sem_Ch6 is
else
Error_Msg_N ("invalid procedure or entry call", N);
end if;
Restore_Globals;
end Analyze_Procedure_Call;
------------------------------
@ -2251,6 +2275,7 @@ package body Sem_Ch6 is
-- the subprogram, or to perform conformance checks.
procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Body_Spec : Node_Id := Specification (N);
Body_Id : Entity_Id := Defining_Entity (Body_Spec);
@ -2326,6 +2351,9 @@ package body Sem_Ch6 is
-- Determine whether subprogram Subp_Id is a primitive of a concurrent
-- type that implements an interface and has a private view.
procedure Restore_Globals;
-- Restore the values of all saved global variables
procedure Set_Trivial_Subprogram (N : Node_Id);
-- Sets the Is_Trivial_Subprogram flag in both spec and body of the
-- subprogram whose body is being analyzed. N is the statement node
@ -2902,6 +2930,15 @@ package body Sem_Ch6 is
return False;
end Is_Private_Concurrent_Primitive;
---------------------
-- Restore_Globals --
---------------------
procedure Restore_Globals is
begin
Ghost_Mode := GM;
end Restore_Globals;
----------------------------
-- Set_Trivial_Subprogram --
----------------------------
@ -3044,6 +3081,7 @@ package body Sem_Ch6 is
Check_Missing_Return;
end if;
Restore_Globals;
return;
else
@ -3051,6 +3089,7 @@ package body Sem_Ch6 is
-- enter name will post error.
Enter_Name (Body_Id);
Restore_Globals;
return;
end if;
@ -3061,6 +3100,7 @@ package body Sem_Ch6 is
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
Restore_Globals;
return;
else
@ -3139,6 +3179,7 @@ package body Sem_Ch6 is
-- If this is a duplicate body, no point in analyzing it
if Error_Posted (N) then
Restore_Globals;
return;
end if;
@ -3251,6 +3292,7 @@ package body Sem_Ch6 is
if Is_Abstract_Subprogram (Spec_Id) then
Error_Msg_N ("an abstract subprogram cannot have a body", N);
Restore_Globals;
return;
else
@ -3320,6 +3362,7 @@ package body Sem_Ch6 is
if not Conformant
and then not Mode_Conformant (Body_Id, Spec_Id)
then
Restore_Globals;
return;
end if;
end if;
@ -3526,6 +3569,7 @@ package body Sem_Ch6 is
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
Restore_Globals;
return;
end if;
@ -3989,6 +4033,8 @@ package body Sem_Ch6 is
Set_Has_Nested_Subprogram (Ent);
end if;
end;
Restore_Globals;
end Analyze_Subprogram_Body_Helper;
---------------------------------
@ -4093,12 +4139,30 @@ package body Sem_Ch6 is
------------------------------------
procedure Analyze_Subprogram_Declaration (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_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
Scop : constant Entity_Id := Current_Scope;
Designator : Entity_Id;
Is_Completion : Boolean;
-- Indicates whether a null procedure declaration is a completion
-- Start of processing for Analyze_Subprogram_Declaration
begin
-- The subprogram declaration may be subject to pragma Ghost with policy
-- Ignore. Set the mode now to ensure that any nodes generated during
@ -4124,10 +4188,10 @@ package body Sem_Ch6 is
Analyze_Null_Procedure (N, Is_Completion);
-- The null procedure acts as a body, nothing further is needed
if Is_Completion then
-- The null procedure acts as a body, nothing further is needed
Restore_Globals;
return;
end if;
end if;
@ -4308,6 +4372,8 @@ package body Sem_Ch6 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Designator);
end if;
Restore_Globals;
end Analyze_Subprogram_Declaration;
--------------------------------------
@ -9374,6 +9440,12 @@ package body Sem_Ch6 is
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
-- The Ghost policy in effect at the point of declaration of a
-- parent subprogram and an overriding subprogram must match
-- (SPARK RM 6.9(17)).
Check_Ghost_Overriding (S, Overridden_Subp);
end if;
-- If there is a homonym that is not overloadable, then we have an
@ -9526,6 +9598,12 @@ package body Sem_Ch6 is
if Comes_From_Source (E) then
Check_Overriding_Indicator (E, S, Is_Primitive => False);
-- The Ghost policy in effect at the point of declaration
-- of a parent subprogram and an overriding subprogram
-- must match (SPARK RM 6.9(17)).
Check_Ghost_Overriding (E, S);
end if;
return;
@ -9721,6 +9799,12 @@ package body Sem_Ch6 is
Check_Overriding_Indicator (S, E, Is_Primitive => True);
-- The Ghost policy in effect at the point of declaration
-- of a parent subprogram and an overriding subprogram
-- must match (SPARK RM 6.9(17)).
Check_Ghost_Overriding (S, E);
-- If S is a user-defined subprogram or a null procedure
-- expanded to override an inherited null procedure, or a
-- predefined dispatching primitive then indicate that E
@ -9857,6 +9941,12 @@ package body Sem_Ch6 is
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
-- The Ghost policy in effect at the point of declaration of a parent
-- subprogram and an overriding subprogram must match
-- (SPARK RM 6.9(17)).
Check_Ghost_Overriding (S, Overridden_Subp);
-- Overloading is not allowed in SPARK, except for operators
if Nkind (S) /= N_Defining_Operator_Symbol then

50
gcc/ada/sem_ch7.adb
View file

@ -571,6 +571,7 @@ package body Sem_Ch7 is
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
@ -940,6 +941,11 @@ package body Sem_Ch7 is
Qualify_Entity_Names (N);
end if;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Package_Body_Helper;
------------------------------
@ -1015,10 +1021,23 @@ package body Sem_Ch7 is
---------------------------------
procedure Analyze_Package_Declaration (N : Node_Id) is
Id : constant Node_Id := Defining_Entity (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
PF : Boolean;
-- True when in the context of a declared pure library unit
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
Id : constant Node_Id := Defining_Entity (N);
Body_Required : Boolean;
-- True when this package declaration requires a corresponding body
@ -1026,6 +1045,11 @@ package body Sem_Ch7 is
Comp_Unit : Boolean;
-- True when this package declaration is not a nested declaration
PF : Boolean;
-- True when in the context of a declared pure library unit
-- Start of processing for Analyze_Package_Declaration
begin
if Debug_Flag_C then
Write_Str ("==> package spec ");
@ -1056,6 +1080,13 @@ package body Sem_Ch7 is
Set_SPARK_Aux_Pragma_Inherited (Id, True);
end if;
-- A package declared within a Ghost refion is automatically Ghost
-- (SPARK RM 6.9(2)).
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
@ -1071,6 +1102,7 @@ package body Sem_Ch7 is
-- package Pkg is ...
if From_Limited_With (Id) then
Restore_Globals;
return;
end if;
@ -1098,6 +1130,7 @@ package body Sem_Ch7 is
end if;
Comp_Unit := Nkind (Parent (N)) = N_Compilation_Unit;
if Comp_Unit then
-- Set Body_Required indication on the compilation unit node, and
@ -1108,7 +1141,6 @@ package body Sem_Ch7 is
if not Body_Required then
Set_Suppress_Elaboration_Warnings (Id);
end if;
end if;
End_Package_Scope (Id);
@ -1131,6 +1163,8 @@ package body Sem_Ch7 is
Write_Location (Sloc (N));
Write_Eol;
end if;
Restore_Globals;
end Analyze_Package_Declaration;
-----------------------------------
@ -1817,8 +1851,9 @@ package body Sem_Ch7 is
--------------------------------------
procedure Analyze_Private_Type_Declaration (N : Node_Id) is
PF : constant Boolean := Is_Pure (Enclosing_Lib_Unit_Entity);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
PF : constant Boolean := Is_Pure (Enclosing_Lib_Unit_Entity);
begin
-- The private type declaration may be subject to pragma Ghost with
@ -1850,6 +1885,11 @@ package body Sem_Ch7 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Private_Type_Declaration;
----------------------------------

129
gcc/ada/sem_ch8.adb
View file

@ -550,8 +550,9 @@ package body Sem_Ch8 is
-- there is more than one element in the list.
procedure Analyze_Exception_Renaming (N : Node_Id) is
Id : constant Node_Id := Defining_Identifier (N);
Nam : constant Node_Id := Name (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Entity (N);
Nam : constant Node_Id := Name (N);
begin
-- The exception renaming declaration may be subject to pragma Ghost
@ -565,27 +566,26 @@ package body Sem_Ch8 is
Enter_Name (Id);
Analyze (Nam);
Set_Ekind (Id, E_Exception);
Set_Etype (Id, Standard_Exception_Type);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
Set_Ekind (Id, E_Exception);
Set_Etype (Id, Standard_Exception_Type);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
if not Is_Entity_Name (Nam)
or else Ekind (Entity (Nam)) /= E_Exception
if Is_Entity_Name (Nam)
and then Present (Entity (Nam))
and then Ekind (Entity (Nam)) = E_Exception
then
Error_Msg_N ("invalid exception name in renaming", Nam);
else
if Present (Renamed_Object (Entity (Nam))) then
Set_Renamed_Object (Id, Renamed_Object (Entity (Nam)));
else
Set_Renamed_Object (Id, Entity (Nam));
end if;
-- An exception renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
-- The exception renaming declaration may become Ghost if it renames
-- a Ghost entity.
if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
Mark_Renaming_As_Ghost (N, Entity (Nam));
else
Error_Msg_N ("invalid exception name in renaming", Nam);
end if;
-- Implementation-defined aspect specifications can appear in a renaming
@ -595,6 +595,11 @@ package body Sem_Ch8 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Exception_Renaming;
---------------------------
@ -664,9 +669,10 @@ package body Sem_Ch8 is
(N : Node_Id;
K : Entity_Kind)
is
New_P : constant Entity_Id := Defining_Entity (N);
GM : constant Ghost_Mode_Type := Ghost_Mode;
New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
Inst : Boolean := False; -- prevent junk warning
Inst : Boolean := False; -- prevent junk warning
begin
if Name (N) = Error then
@ -710,7 +716,7 @@ package body Sem_Ch8 is
else
if Present (Renamed_Object (Old_P)) then
Set_Renamed_Object (New_P, Renamed_Object (Old_P));
Set_Renamed_Object (New_P, Renamed_Object (Old_P));
else
Set_Renamed_Object (New_P, Old_P);
end if;
@ -721,12 +727,10 @@ package body Sem_Ch8 is
Set_Etype (New_P, Etype (Old_P));
Set_Has_Completion (New_P);
-- An generic renaming is Ghost if the renamed entity is Ghost or the
-- construct appears within a Ghost scope.
-- The generic renaming declaration may become Ghost if it renames a
-- Ghost entity.
if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_P);
end if;
Mark_Renaming_As_Ghost (N, Old_P);
if In_Open_Scopes (Old_P) then
Error_Msg_N ("within its scope, generic denotes its instance", N);
@ -750,6 +754,11 @@ package body Sem_Ch8 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, New_P);
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Generic_Renaming;
-----------------------------
@ -757,10 +766,10 @@ package body Sem_Ch8 is
-----------------------------
procedure Analyze_Object_Renaming (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Id : constant Entity_Id := Defining_Identifier (N);
Dec : Node_Id;
Loc : constant Source_Ptr := Sloc (N);
Nam : constant Node_Id := Name (N);
Dec : Node_Id;
T : Entity_Id;
T2 : Entity_Id;
@ -856,6 +865,10 @@ package body Sem_Ch8 is
return False;
end In_Generic_Scope;
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Analyze_Object_Renaming
begin
@ -1347,14 +1360,11 @@ package body Sem_Ch8 is
Set_Is_True_Constant (Id, True);
end if;
-- An object renaming is Ghost if the renamed entity is Ghost or the
-- construct appears within a Ghost scope.
-- The object renaming declaration may become Ghost if it renames a
-- Ghost entity.
if (Is_Entity_Name (Nam)
and then Is_Ghost_Entity (Entity (Nam)))
or else Ghost_Mode > None
then
Set_Is_Ghost_Entity (Id);
if Is_Entity_Name (Nam) then
Mark_Renaming_As_Ghost (N, Entity (Nam));
end if;
-- The entity of the renaming declaration needs to reflect whether the
@ -1401,6 +1411,11 @@ package body Sem_Ch8 is
-- Deal with dimensions
Analyze_Dimension (N);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Object_Renaming;
------------------------------
@ -1408,10 +1423,28 @@ package body Sem_Ch8 is
------------------------------
procedure Analyze_Package_Renaming (N : Node_Id) is
GM : constant Ghost_Mode_Type := Ghost_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
New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
Spec : Node_Id;
-- Start of processing for Analyze_Package_Renaming
begin
if Name (N) = Error then
return;
@ -1486,12 +1519,10 @@ package body Sem_Ch8 is
Check_Library_Unit_Renaming (N, Old_P);
Generate_Reference (Old_P, Name (N));
-- A package renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
-- The package renaming declaration may become Ghost if it renames a
-- Ghost entity.
if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_P);
end if;
Mark_Renaming_As_Ghost (N, Old_P);
-- If the renaming is in the visible part of a package, then we set
-- Renamed_In_Spec for the renamed package, to prevent giving
@ -1524,6 +1555,7 @@ package body Sem_Ch8 is
-- subtypes again, so they are compatible with types in their class.
if not Is_Generic_Instance (Old_P) then
Restore_Globals;
return;
else
Spec := Specification (Unit_Declaration_Node (Old_P));
@ -1565,6 +1597,8 @@ package body Sem_Ch8 is
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, New_P);
end if;
Restore_Globals;
end Analyze_Package_Renaming;
-------------------------------
@ -2611,6 +2645,7 @@ package body Sem_Ch8 is
-- defaulted formal subprogram when the actual for a related formal
-- type is class-wide.
GM : constant Ghost_Mode_Type := Ghost_Mode;
Inst_Node : Node_Id := Empty;
New_S : Entity_Id;
@ -3094,12 +3129,10 @@ package body Sem_Ch8 is
Set_Is_Pure (New_S, Is_Pure (Entity (Nam)));
Set_Is_Preelaborated (New_S, Is_Preelaborated (Entity (Nam)));
-- A subprogram renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
-- The subprogram renaming declaration may become Ghost if it renames
-- a Ghost entity.
if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_S);
end if;
Mark_Renaming_As_Ghost (N, Entity (Nam));
-- Ada 2005 (AI-423): Check the consistency of null exclusions
-- between a subprogram and its correct renaming.
@ -3417,11 +3450,10 @@ package body Sem_Ch8 is
if Present (F1) and then Present (Default_Value (F1)) then
if Present (Next_Formal (F1)) then
Error_Msg_NE
("\missing specification for &" &
" and other formals with defaults", Spec, F1);
("\missing specification for & and other formals with "
& "defaults", Spec, F1);
else
Error_Msg_NE
("\missing specification for &", Spec, F1);
Error_Msg_NE ("\missing specification for &", Spec, F1);
end if;
end if;
@ -3507,7 +3539,7 @@ package body Sem_Ch8 is
and then Chars (Current_Scope) /= Chars (Old_S)
then
Error_Msg_N
("redundant renaming, entity is directly visible?r?", Name (N));
("redundant renaming, entity is directly visible?r?", Name (N));
end if;
-- Implementation-defined aspect specifications can appear in a renaming
@ -3544,6 +3576,11 @@ package body Sem_Ch8 is
Analyze (N);
end if;
end if;
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Analyze_Subprogram_Renaming;
-------------------------

1067
gcc/ada/sem_prag.adb
View file

File diff suppressed because it is too large Load diff

152
gcc/ada/sem_prag.ads
View file

@ -33,31 +33,122 @@ with Types; use Types;
package Sem_Prag is
-- The following table lists all pragmas that emulate an Ada 2012 aspect
Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean :=
(Pragma_Abstract_State => True,
Pragma_All_Calls_Remote => True,
Pragma_Annotate => True,
Pragma_Async_Readers => True,
Pragma_Async_Writers => True,
Pragma_Asynchronous => True,
Pragma_Atomic => True,
Pragma_Atomic_Components => True,
Pragma_Attach_Handler => True,
Pragma_Contract_Cases => True,
Pragma_Convention => True,
Pragma_CPU => True,
Pragma_Default_Initial_Condition => True,
Pragma_Default_Storage_Pool => True,
Pragma_Depends => True,
Pragma_Discard_Names => True,
Pragma_Dispatching_Domain => True,
Pragma_Effective_Reads => True,
Pragma_Effective_Writes => True,
Pragma_Elaborate_Body => True,
Pragma_Export => True,
Pragma_Extensions_Visible => True,
Pragma_Favor_Top_Level => True,
Pragma_Ghost => True,
Pragma_Global => True,
Pragma_Import => True,
Pragma_Independent => True,
Pragma_Independent_Components => True,
Pragma_Initial_Condition => True,
Pragma_Initializes => True,
Pragma_Inline => True,
Pragma_Inline_Always => True,
Pragma_Interrupt_Handler => True,
Pragma_Interrupt_Priority => True,
Pragma_Invariant => True,
Pragma_Linker_Section => True,
Pragma_Lock_Free => True,
Pragma_No_Elaboration_Code_All => True,
Pragma_No_Return => True,
Pragma_Obsolescent => True,
Pragma_Pack => True,
Pragma_Part_Of => True,
Pragma_Persistent_BSS => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Preelaborable_Initialization => True,
Pragma_Preelaborate => True,
Pragma_Priority => True,
Pragma_Pure => True,
Pragma_Pure_Function => True,
Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
Pragma_Refined_State => True,
Pragma_Relative_Deadline => True,
Pragma_Remote_Access_Type => True,
Pragma_Remote_Call_Interface => True,
Pragma_Remote_Types => True,
Pragma_Shared => True,
Pragma_Shared_Passive => True,
Pragma_Simple_Storage_Pool_Type => True,
Pragma_SPARK_Mode => True,
Pragma_Storage_Size => True,
Pragma_Suppress => True,
Pragma_Suppress_Debug_Info => True,
Pragma_Suppress_Initialization => True,
Pragma_Test_Case => True,
Pragma_Thread_Local_Storage => True,
Pragma_Type_Invariant => True,
Pragma_Unchecked_Union => True,
Pragma_Universal_Aliasing => True,
Pragma_Universal_Data => True,
Pragma_Unmodified => True,
Pragma_Unreferenced => True,
Pragma_Unreferenced_Objects => True,
Pragma_Unsuppress => True,
Pragma_Volatile => True,
Pragma_Volatile_Components => True,
Pragma_Volatile_Full_Access => True,
Pragma_Warnings => True,
others => False);
-- The following table lists all pragmas that act as an assertion
-- expression.
Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
(Pragma_Assert => True,
Pragma_Assert_And_Cut => True,
Pragma_Assume => True,
Pragma_Check => True,
Pragma_Contract_Cases => True,
Pragma_Initial_Condition => True,
Pragma_Invariant => True,
Pragma_Loop_Invariant => True,
Pragma_Loop_Variant => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Refined_Post => True,
Pragma_Test_Case => True,
Pragma_Type_Invariant => True,
Pragma_Type_Invariant_Class => True,
others => False);
(Pragma_Assert => True,
Pragma_Assert_And_Cut => True,
Pragma_Assume => True,
Pragma_Check => True,
Pragma_Contract_Cases => True,
Pragma_Default_Initial_Condition => True,
Pragma_Initial_Condition => True,
Pragma_Invariant => True,
Pragma_Loop_Invariant => True,
Pragma_Loop_Variant => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Refined_Post => True,
Pragma_Test_Case => True,
Pragma_Type_Invariant => True,
Pragma_Type_Invariant_Class => True,
others => False);
-- The following table lists all the implementation-defined pragmas that
-- may apply to a body stub (no language defined pragmas apply). The table
@ -156,6 +247,25 @@ package Sem_Prag is
-- is the related variable or state. Ensure legality of the combination and
-- issue an error for an illegal combination.
function Check_Kind (Nam : Name_Id) return Name_Id;
-- This function is used in connection with pragmas Assert, Check,
-- and assertion aspects and pragmas, to determine if Check pragmas
-- (or corresponding assertion aspects or pragmas) are currently active
-- as determined by the presence of -gnata on the command line (which
-- sets the default), and the appearance of pragmas Check_Policy and
-- Assertion_Policy as configuration pragmas either in a configuration
-- pragma file, or at the start of the current unit, or locally given
-- Check_Policy and Assertion_Policy pragmas that are currently active.
--
-- The value returned is one of the names Check, Ignore, Disable (On
-- returns Check, and Off returns Ignore).
--
-- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
-- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
-- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
-- _Post, _Invariant, or _Type_Invariant, which are special names used
-- in identifiers to represent these attribute references.
procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
-- Determine whether the placement within the state space of an abstract
-- state, variable or package instantiation denoted by Item_Id requires the

92
gcc/ada/sem_util.adb
View file

@ -35,6 +35,7 @@ with Exp_Disp; use Exp_Disp;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet.Sp; use Namet.Sp;
@ -1313,6 +1314,7 @@ package body Sem_Util is
-- Local variables
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (Typ);
Prag : constant Node_Id :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
@ -1339,6 +1341,11 @@ package body Sem_Util is
return;
end if;
-- Ensure that the analysis and expansion produce Ghost nodes if the
-- type itself is Ghost.
Set_Ghost_Mode_From_Entity (Typ);
Param_Id := First_Formal (Proc_Id);
-- The pragma has an argument. Note that the argument is analyzed
@ -1405,6 +1412,11 @@ package body Sem_Util is
Set_Corresponding_Spec (Body_Decl, Proc_Id);
Insert_After_And_Analyze (Declaration_Node (Typ), Body_Decl);
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Build_Default_Init_Cond_Procedure_Body;
-- Local variables
@ -1453,6 +1465,7 @@ package body Sem_Util is
---------------------------------------------------
procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id) is
GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (Typ);
Prag : constant Node_Id :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
@ -1472,7 +1485,12 @@ package body Sem_Util is
return;
end if;
Proc_Id :=
-- Ensure that the analysis and expansion produce Ghost nodes if the
-- type itself is Ghost.
Set_Ghost_Mode_From_Entity (Typ);
Proc_Id :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (Typ), "Default_Init_Cond"));
@ -1482,6 +1500,13 @@ package body Sem_Util is
Set_Is_Default_Init_Cond_Procedure (Proc_Id);
Set_Default_Init_Cond_Procedure (Typ, Proc_Id);
-- Mark the default initial condition procedure explicitly as Ghost
-- because it does not come from source.
if Ghost_Mode > None then
Set_Is_Ghost_Entity (Proc_Id);
end if;
-- Generate:
-- procedure <Typ>Default_Init_Cond (Inn : <Typ>);
@ -1494,6 +1519,11 @@ package body Sem_Util is
Make_Parameter_Specification (Loc,
Defining_Identifier => Make_Temporary (Loc, 'I'),
Parameter_Type => New_Occurrence_Of (Typ, Loc))))));
-- Restore the original Ghost mode once analysis and expansion have
-- taken place.
Ghost_Mode := GM;
end Build_Default_Init_Cond_Procedure_Declaration;
---------------------------
@ -12782,6 +12812,27 @@ package body Sem_Util is
return False;
end Is_Renamed_Entry;
-----------------------------
-- Is_Renaming_Declaration --
-----------------------------
function Is_Renaming_Declaration (N : Node_Id) return Boolean is
begin
case Nkind (N) is
when N_Exception_Renaming_Declaration |
N_Generic_Function_Renaming_Declaration |
N_Generic_Package_Renaming_Declaration |
N_Generic_Procedure_Renaming_Declaration |
N_Object_Renaming_Declaration |
N_Package_Renaming_Declaration |
N_Subprogram_Renaming_Declaration =>
return True;
when others =>
return False;
end case;
end Is_Renaming_Declaration;
----------------------------
-- Is_Reversible_Iterator --
----------------------------
@ -16256,21 +16307,24 @@ package body Sem_Util is
--------------------
function Policy_In_List (List : Node_Id) return Name_Id is
Arg : Node_Id;
Expr : Node_Id;
Arg1 : Node_Id;
Arg2 : Node_Id;
Prag : Node_Id;
begin
Prag := List;
while Present (Prag) loop
Arg := First (Pragma_Argument_Associations (Prag));
Expr := Get_Pragma_Arg (Arg);
Arg1 := First (Pragma_Argument_Associations (Prag));
Arg2 := Next (Arg1);
-- The current Check_Policy pragma matches the requested policy,
-- return the second argument which denotes the policy identifier.
Arg1 := Get_Pragma_Arg (Arg1);
Arg2 := Get_Pragma_Arg (Arg2);
if Chars (Expr) = Policy then
return Chars (Get_Pragma_Arg (Next (Arg)));
-- The current Check_Policy pragma matches the requested policy or
-- appears in the single argument form (Assertion, policy_id).
if Nam_In (Chars (Arg1), Name_Assertion, Policy) then
return Chars (Arg2);
end if;
Prag := Next_Pragma (Prag);
@ -16948,13 +17002,20 @@ package body Sem_Util is
begin
Comp := First_Entity (Typ);
while Present (Comp) loop
if Ekind (Comp) = E_Component
and then Requires_Transient_Scope (Etype (Comp))
then
return True;
else
Next_Entity (Comp);
if Ekind (Comp) = E_Component then
-- ???It's not cleare we need a full recursive call to
-- Requires_Transient_Scope here. Note that the following
-- can't happen.
pragma Assert (Is_Definite_Subtype (Etype (Comp)));
pragma Assert (not Has_Controlled_Component (Etype (Comp)));
if Requires_Transient_Scope (Etype (Comp)) then
return True;
end if;
end if;
Next_Entity (Comp);
end loop;
end;
@ -16985,6 +17046,7 @@ package body Sem_Util is
-- All other cases do not require a transient scope
else
pragma Assert (Is_Protected_Type (Typ) or else Is_Task_Type (Typ));
return False;
end if;
end Requires_Transient_Scope;

3
gcc/ada/sem_util.ads
View file

@ -1440,6 +1440,9 @@ package Sem_Util is
function Is_Renamed_Entry (Proc_Nam : Entity_Id) return Boolean;
-- Return True if Proc_Nam is a procedure renaming of an entry
function Is_Renaming_Declaration (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a renaming declaration
function Is_Reversible_Iterator (Typ : Entity_Id) return Boolean;
-- AI05-0139-2: Check whether Typ is derived from the predefined interface
-- Ada.Iterator_Interfaces.Reversible_Iterator.

16
gcc/ada/sinfo.adb
View file

@ -1884,6 +1884,14 @@ package body Sinfo is
return Flag2 (N);
end Is_Generic_Contract_Pragma;
function Is_Ghost_Pragma
(N : Node_Id) return Boolean is
begin
pragma Assert (False
or else NT (N).Nkind = N_Pragma);
return Flag3 (N);
end Is_Ghost_Pragma;
function Is_Ignored
(N : Node_Id) return Boolean is
begin
@ -5089,6 +5097,14 @@ package body Sinfo is
Set_Flag2 (N, Val);
end Set_Is_Generic_Contract_Pragma;
procedure Set_Is_Ghost_Pragma
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
or else NT (N).Nkind = N_Pragma);
Set_Flag3 (N, Val);
end Set_Is_Ghost_Pragma;
procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True) is
begin

14
gcc/ada/sinfo.ads
View file

@ -1627,6 +1627,11 @@ package Sinfo is
-- Refined_State
-- Test_Case
-- Is_Ghost_Pragma (Flag3-Sem)
-- This flag is present in N_Pragma nodes. It is set when the pragma is
-- either declared within a Ghost construct or it applies to a Ghost
-- construct.
-- Is_Ignored (Flag9-Sem)
-- A flag set in an N_Aspect_Specification or N_Pragma node if there was
-- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
@ -2468,6 +2473,7 @@ package Sinfo is
-- Is_Delayed_Aspect (Flag14-Sem)
-- Is_Disabled (Flag15-Sem)
-- Is_Generic_Contract_Pragma (Flag2-Sem)
-- Is_Ghost_Pragma (Flag3-Sem);
-- Is_Ignored (Flag9-Sem)
-- Is_Inherited (Flag4-Sem)
-- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
@ -9322,6 +9328,9 @@ package Sinfo is
function Is_Generic_Contract_Pragma
(N : Node_Id) return Boolean; -- Flag2
function Is_Ghost_Pragma
(N : Node_Id) return Boolean; -- Flag3
function Is_Ignored
(N : Node_Id) return Boolean; -- Flag9
@ -10345,6 +10354,9 @@ package Sinfo is
procedure Set_Is_Generic_Contract_Pragma
(N : Node_Id; Val : Boolean := True); -- Flag2
procedure Set_Is_Ghost_Pragma
(N : Node_Id; Val : Boolean := True); -- Flag3
procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True); -- Flag9
@ -12736,6 +12748,7 @@ package Sinfo is
pragma Inline (Is_Finalization_Wrapper);
pragma Inline (Is_Folded_In_Parser);
pragma Inline (Is_Generic_Contract_Pragma);
pragma Inline (Is_Ghost_Pragma);
pragma Inline (Is_Ignored);
pragma Inline (Is_In_Discriminant_Check);
pragma Inline (Is_Inherited);
@ -13072,6 +13085,7 @@ package Sinfo is
pragma Inline (Set_Is_Finalization_Wrapper);
pragma Inline (Set_Is_Folded_In_Parser);
pragma Inline (Set_Is_Generic_Contract_Pragma);
pragma Inline (Set_Is_Ghost_Pragma);
pragma Inline (Set_Is_Ignored);
pragma Inline (Set_Is_In_Discriminant_Check);
pragma Inline (Set_Is_Inherited);