diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2015-05-26 10:46:58 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2015-05-26 12:46:58 +0200 |
| commit | 241ebe892af143aaf8cce4bfd80f9b8dce97fe72 (patch) | |
| tree | bed88940e055630033e81202254038ad081b708f /gcc | |
| parent | 138cac6426259ed3ed98371f0aa0989df32c0724 (diff) | |
| download | gcc-241ebe892af143aaf8cce4bfd80f9b8dce97fe72.zip gcc-241ebe892af143aaf8cce4bfd80f9b8dce97fe72.tar.gz gcc-241ebe892af143aaf8cce4bfd80f9b8dce97fe72.tar.bz2 | |
exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and restore the Ghost mode.
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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 178 | ||||
| -rw-r--r-- | gcc/ada/exp_ch11.adb | 55 | ||||
| -rw-r--r-- | gcc/ada/exp_ch3.adb | 46 | ||||
| -rw-r--r-- | gcc/ada/exp_ch5.adb | 41 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.adb | 72 | ||||
| -rw-r--r-- | gcc/ada/exp_ch7.adb | 35 | ||||
| -rw-r--r-- | gcc/ada/exp_ch8.adb | 63 | ||||
| -rw-r--r-- | gcc/ada/exp_disp.adb | 36 | ||||
| -rw-r--r-- | gcc/ada/exp_prag.adb | 80 | ||||
| -rw-r--r-- | gcc/ada/exp_util.adb | 63 | ||||
| -rw-r--r-- | gcc/ada/freeze.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/ghost.adb | 654 | ||||
| -rw-r--r-- | gcc/ada/ghost.ads | 63 | ||||
| -rw-r--r-- | gcc/ada/sem_ch11.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 706 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 115 | ||||
| -rw-r--r-- | gcc/ada/sem_ch5.adb | 24 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 146 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 50 | ||||
| -rw-r--r-- | gcc/ada/sem_ch8.adb | 129 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 1059 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 152 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 92 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 3 | ||||
| -rw-r--r-- | gcc/ada/sinfo.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 14 |
27 files changed, 2922 insertions, 1008 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0cd2ea7..d3ef056 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -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: diff --git a/gcc/ada/exp_ch11.adb b/gcc/ada/exp_ch11.adb index 1d437af..dd0423a 100644 --- a/gcc/ada/exp_ch11.adb +++ b/gcc/ada/exp_ch11.adb @@ -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; --------------------------------------------- diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 0bb41fd..d7f4534 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -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. diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb index a27fc2c..ca6971e 100644 --- a/gcc/ada/exp_ch5.adb +++ b/gcc/ada/exp_ch5.adb @@ -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; diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 3645c76..01081a0 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -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; -------------------------------- diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 661809c..7452146 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -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; ----------------------------- diff --git a/gcc/ada/exp_ch8.adb b/gcc/ada/exp_ch8.adb index 97bfac4..2c47b7f 100644 --- a/gcc/ada/exp_ch8.adb +++ b/gcc/ada/exp_ch8.adb @@ -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; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index a70cf6a..f50899b 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -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); diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index 4bbfbd4..fab3fac 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -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; -------------------------------- diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index d0c5d4e..eec7149 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -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; -------------------------- diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index f411e1e..fc029c9 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -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 diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index b608a45..75ceb4b 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -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_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean; - -- Determine whether statement or pragma N is Ghost or appears within - -- a Ghost statement or pragma. To qualify as such, N must either - -- 1) Occur within a ghost subprogram or package - -- 2) Denote a call to a ghost procedure - -- 3) Denote an assignment statement whose target is a ghost - -- variable. - -- 4) Denote a pragma that mentions a ghost entity - - -------------------------- - -- Is_Ghost_Declaration -- - -------------------------- - - function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is - Par : Node_Id; + 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_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 + + 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 + + ----------------------- + -- Is_OK_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. + + ----------------------- + -- Is_Ghost_Renaming -- + ----------------------- + + function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is + Nam_Id : Entity_Id; + + begin + if Is_Renaming_Declaration (Ren_Decl) then + Nam_Id := Ghost_Entity (Name (Ren_Decl)); + + return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id); + end if; + + return False; + end Is_Ghost_Renaming; + + -- Local variables + Subp_Decl : Node_Id; Subp_Id : Entity_Id; + -- Start of processing for Is_OK_Declaration + begin - -- Climb the parent chain looking for an object declaration + if Is_Declaration (Decl) then - Par := Decl; - while Present (Par) loop - if Is_Declaration (Par) then + -- A renaming declaration is Ghost when it renames a Ghost + -- entity. - -- A declaration is Ghost when it appears within a Ghost - -- package or subprogram. + if Is_Ghost_Renaming (Decl) then + return True; - if Ghost_Mode > None then - return True; + -- The declaration may not have been analyzed yet, determine + -- whether it is subject to pragma Ghost. - -- Otherwise the declaration may not have been analyzed yet, - -- determine whether it is subject to aspect/pragma Ghost. + elsif Is_Subject_To_Ghost (Decl) then + return True; - else - return Is_Subject_To_Ghost (Par); - end if; + -- The declaration appears within an assertion expression - -- Special cases + elsif In_Assertion_Expr > 0 then + return True; + end if; - -- 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. + -- Special cases - elsif Nkind (Par) = N_Parameter_Specification - and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body - 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. - -- References to Ghost entities may be relocated in internally - -- generated bodies. + elsif Nkind (Decl) = N_Parameter_Specification + and then Nkind (Parent (Parent (Decl))) = N_Subprogram_Body + then + return True; - elsif Nkind (Par) = N_Subprogram_Body - and then not Comes_From_Source (Par) - then - Subp_Id := Corresponding_Spec (Par); + -- References to Ghost entities may be relocated in internally + -- generated bodies. - -- 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. + elsif Nkind (Decl) = N_Subprogram_Body + and then not Comes_From_Source (Decl) + then + Subp_Id := Corresponding_Spec (Decl); - if Present (Subp_Id) then - Subp_Decl := - Original_Node (Unit_Declaration_Node (Subp_Id)); + -- 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 Nkind (Subp_Decl) = N_Expression_Function then - return Is_Subject_To_Ghost (Subp_Decl); - end if; + 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; - -- Otherwise this is either an internal body or an internal - -- completion. Both are OK because the real check was done - -- before expansion activities. + -- 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; - - -- Prevent the search from going too far - - if Is_Body_Or_Package_Declaration (Par) then - return False; - end if; - - Par := Parent (Par); - end loop; + end if; return False; - end Is_Ghost_Declaration; + end Is_OK_Declaration; - ---------------------------------- - -- Is_Ghost_Statement_Or_Pragma -- - ---------------------------------- + ------------------ + -- Is_OK_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. + 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. - ------------------------------- - -- Is_Ghost_Entity_Reference -- - ------------------------------- + -------------------- + -- Check_Policies -- + -------------------- - function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is - Ref : Node_Id; + 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 - -- 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; - - return - Is_Entity_Name (Ref) - and then Present (Entity (Ref)) - and then Is_Ghost_Entity (Entity (Ref)); - end Is_Ghost_Entity_Reference; + -- 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; - Stmt : Node_Id; + Arg : Node_Id; + Arg_Id : Entity_Id; + Prag_Id : Pragma_Id; + Prag_Nam : Name_Id; - -- Start of processing for Is_Ghost_Statement_Or_Pragma + -- Start of processing for Is_OK_Pragma begin - if Nkind (N) = N_Pragma then + if Nkind (Prag) = N_Pragma then + Prag_Id := Get_Pragma_Id (Prag); + Prag_Nam := Original_Aspect_Pragma_Name (Prag); - -- A pragma is Ghost when it appears within a Ghost package or - -- subprogram. + -- 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 Ghost_Mode > None then + if Is_Ghost_Pragma (Prag) then return True; - end if; - -- A pragma is Ghost when it mentions a Ghost entity + -- An assertion expression is a Ghost pragma when it contains a + -- reference to a Ghost entity (SPARK RM 6.9(11)). - Arg := First (Pragma_Argument_Associations (N)); - while Present (Arg) loop - if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then - return True; - end if; + elsif Assertion_Expression_Pragma (Prag_Id) then - Next (Arg); - end loop; - end if; + -- Predicates are excluded from this category when they do + -- not apply to a Ghost subtype (SPARK RM 6.9(12)). - Stmt := N; - while Present (Stmt) loop - if Is_Statement (Stmt) then + if Nam_In (Prag_Nam, Name_Dynamic_Predicate, + Name_Predicate, + Name_Static_Predicate) + then + return False; - -- A statement is Ghost when it appears within a Ghost - -- package or subprogram. + -- Otherwise ensure that the assertion policy and the Ghost + -- policy are compatible (SPARK RM 6.9(18)). - if Ghost_Mode > None then + else + Check_Policies (Prag_Nam); return True; + end if; - -- An assignment statement or a procedure call is Ghost when - -- the name denotes a Ghost entity. + -- 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 Nkind_In (Stmt, N_Assignment_Statement, - N_Procedure_Call_Statement) - then - return Is_Ghost_Entity_Reference (Name (Stmt)); - end if; + elsif Nam_In (Prag_Nam, Name_Global, + Name_Depends, + Name_Initializes, + Name_Refined_Global, + Name_Refined_Depends, + Name_Refined_State) + then + return True; - -- Prevent the search from going too far + -- Otherwise a normal pragma is Ghost when it encloses a Ghost + -- name (SPARK RM 6.9(3)). - elsif Is_Body_Or_Package_Declaration (Stmt) then - return False; - end if; + else + Arg := First (Pragma_Argument_Associations (Prag)); + while Present (Arg) loop + Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg)); - Stmt := Parent (Stmt); - end loop; + if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then + return True; + end if; + + Next (Arg); + end loop; + end if; + end if; return False; - end Is_Ghost_Statement_Or_Pragma; + end Is_OK_Pragma; - -- Start of processing for Is_OK_Ghost_Context + --------------------- + -- Is_OK_Statement -- + --------------------- - begin - -- The Ghost entity appears within an assertion expression + function Is_OK_Statement (Stmt : Node_Id) return Boolean is + Nam_Id : Entity_Id; - if In_Assertion_Expr > 0 then - return True; + begin + -- An assignment statement or a procedure call is Ghost when the + -- name denotes a Ghost entity. - -- The Ghost entity is part of a declaration or its completion + if Nkind_In (Stmt, N_Assignment_Statement, + N_Procedure_Call_Statement) + then + Nam_Id := Ghost_Entity (Name (Stmt)); - elsif Is_Ghost_Declaration (Context) then - return True; + 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 - -- The Ghost entity is referenced within a Ghost statement + Par : Node_Id; - elsif Is_Ghost_Statement_Or_Pragma (Context) then + -- Start of processing for Is_OK_Ghost_Context + + begin + -- The context is Ghost when it appears within a Ghost package or + -- subprogram. + + 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 := Name (N); - while Nkind_In (Nam, N_Explicit_Dereference, - N_Indexed_Component, - N_Selected_Component, - N_Slice) - loop - Nam := Prefix (Nam); - end loop; + Nam_Id := Ghost_Entity (Name (N)); - 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 -- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 436e84f..c267e70 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -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, 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, the Ghost_Mode is + -- set based on the mode of the name. -- - -- N is the full view of a private type, Prev_Id denotes the entity - -- of the partial declaration. + -- 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 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 a pragma, the Ghost_Mode is set based on the mode of the + -- pragma. -- - -- 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 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; diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index ca6c963..e1ff0c1 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -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; -------------------------------- diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index d0d25dd..266b746 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -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; ----------------------------------- diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 7abf871..8db5b50 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -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. + + 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 Make_Subprogram_Declaration (Loc, Specification => Spec); + 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 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. - - 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); + -- Create a runtime check to verify the exression of invariant pragma + -- Prag. All generated code is added to list Stmts. - ---------------------------- - -- Replace_Type_Reference -- - ---------------------------- + ------------------- + -- Add_Invariant -- + ------------------- - -- Note: See comments in Add_Predicates.Replace_Type_Reference - -- regarding handling of Sloc and Comes_From_Source. + 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. + + 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. + + ---------------------------- + -- Replace_Type_Reference -- + ---------------------------- + + -- Note: See comments in Add_Predicates.Replace_Type_Reference + -- regarding handling of Sloc and Comes_From_Source. + + procedure Replace_Type_Reference (N : Node_Id) is + Nloc : constant Source_Ptr := Sloc (N); - procedure Replace_Type_Reference (N : Node_Id) is - begin + begin + -- Add semantic information to node to be rewritten, for ASIS + -- navigation needs. - -- Add semantic information to node to be rewritten, for ASIS - -- navigation needs. + if Nkind (N) = N_Identifier then + Set_Entity (N, T); + Set_Etype (N, T); - if Nkind (N) = N_Identifier then - Set_Entity (N, T); - Set_Etype (N, T); + elsif Nkind (N) = N_Selected_Component then + Analyze (Prefix (N)); + Set_Entity (Selector_Name (N), T); + Set_Etype (Selector_Name (N), T); + end if; - 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'Class, replace with T'Class (obj) - -- 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 (Prag) then - 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; + -- 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. - 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))); + if ASIS_Mode + and then Nkind (Parent (N)) = N_Attribute_Reference + and then Attribute_Name (Parent (N)) = Name_Class + then + null; - Set_Entity (Expression (N), Object_Entity); - Set_Etype (Expression (N), Typ); - end if; + 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 + -- Invariant, replace with obj - else - Rewrite (N, Make_Identifier (Sloc (N), Object_Name)); - Set_Entity (N, Object_Entity); - Set_Etype (N, Typ); - end if; + 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; + Set_Comes_From_Source (N, True); + end Replace_Type_Reference; - -- Start of processing for Add_Invariants + -- Local variables - 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); + 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; - Arg1 := Get_Pragma_Arg (Arg1); - Arg2 := Get_Pragma_Arg (Arg2); + -- Start of processing for Add_Invariant - -- For Inherit case, ignore Invariant, process only Class case + begin + -- Extract the arguments of the invariant pragma - if Inherit then - if not Class_Present (Ritem) then - goto Continue; - end if; + Arg1 := First (Pragma_Argument_Associations (Prag)); + Arg2 := Next (Arg1); + Arg3 := Next (Arg2); - -- For Inherit false, process only item for right type + Arg1 := Get_Pragma_Arg (Arg1); + Arg2 := Get_Pragma_Arg (Arg2); - else - if Entity (Arg1) /= Typ then - goto Continue; - end if; - end if; + -- 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 No (Stmts) then - Stmts := Empty_List; + if Inherit then + if not Class_Present (Prag) then + return; end if; - Exp := New_Copy_Tree (Arg2); + -- Otherwise the pragma must apply to the current type - -- Preserve sloc of original pragma Invariant + elsif Entity (Arg1) /= T then + return; + end if; - Loc := Sloc (Ritem); + Expr := New_Copy_Tree (Arg2); - -- 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 all occurrences of the type's name with references to + -- the formal parameter of the invariant procedure. - Replace_Type_References (Exp, T); + Replace_Type_References (Expr, 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 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 From_Aspect_Specification (Ritem) then - declare - Aitem : Node_Id; + if Present (Asp) then + Set_Entity (Identifier (Asp), New_Copy_Tree (Expr)); + end if; - begin - -- Loop to find corresponding aspect, note that this - -- must be present given the pragma is marked delayed. + -- 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. - -- Note: in practice Next_Rep_Item (Ritem) is Empty so - -- this loop does nothing. Furthermore, why isn't this - -- simply Corresponding_Aspect ??? + -- Historic note: we used to set N as the parent, but a package + -- specification as the parent of an expression is bizarre. - 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; + Set_Parent (Expr, Parent (Arg2)); + Preanalyze_Assert_Expression (Expr, Any_Boolean); - 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. + -- 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. - Set_Parent (Exp, N); - Preanalyze_Assert_Expression (Exp, Any_Boolean); + -- ??? Unclear how to handle class-wide invariants that are not + -- function calls. - -- 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. + 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; - -- Unclear how to handle class-wide invariants that are not - -- function calls ??? + -- 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 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 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; - 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; + -- An ignored invariant must not generate a runtime check. Add a + -- null statement to ensure that the invariant procedure does get + -- a completing body. - -- Get name to be used for Check pragma. Using the original - -- name ensures that 'Class case is properly handled. + if No (Stmts) then + Stmts := Empty_List; + end if; - Nam := Original_Aspect_Pragma_Name (Ritem); + if Is_Ignored (Prag) then + Append_To (Stmts, Make_Null_Statement (Ploc)); - -- Build first two arguments for Check pragma + -- Otherwise the invariant is checked. Build a Check pragma to + -- verify the expression at runtime. - Assoc := - New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Chars => Nam)), - Make_Pragma_Argument_Association (Loc, - Expression => Exp)); + else + Assoc := New_List ( + Make_Pragma_Argument_Association (Ploc, + Expression => Make_Identifier (Ploc, Nam)), + Make_Pragma_Argument_Association (Ploc, + Expression => Expr)); - -- 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)); + end if; - -- If Inherited case and option enabled, output info msg. Note - -- that we know this is a case of Invariant'Class. + -- 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 (Ritem); - Error_Msg_N - ("info: & inherits `Invariant''Class` aspect from #?L?", - Typ); - end if; + 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; - <<Continue>> 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 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. + 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_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. + ------------------- + -- Add_Predicate -- + ------------------- - ---------------------------- - -- Replace_Type_Reference -- - ---------------------------- + 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. + + 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 - 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); - 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. - -- 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; - Set_Comes_From_Source (N, True); - end Replace_Type_Reference; + -- Local variables - -- Start of processing for Add_Predicates + Asp : constant Node_Id := Corresponding_Aspect (Prag); + Arg1 : Node_Id; + Arg2 : Node_Id; - begin - Ritem := First_Rep_Item (Typ); + -- Start of processing for Add_Predicate - 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); + begin + -- 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. - Arg1 := Get_Pragma_Arg (Arg1); - Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2)); + Arg1 := First (Pragma_Argument_Associations (Prag)); + Arg2 := Next (Arg1); - -- 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. + Arg1 := Get_Pragma_Arg (Arg1); + Arg2 := New_Copy_Tree (Get_Pragma_Arg (Arg2)); - if Entity (Arg1) = Typ - or else Full_View (Entity (Arg1)) = Typ - then - -- We have a match, this entry is for our subtype + -- 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. - -- We need to replace any occurrences of the name of the - -- type with references to the object. + if Entity (Arg1) = Typ + or else Full_View (Entity (Arg1)) = Typ + then + Replace_Type_References (Arg2, Typ); - 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 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 Present (Asp) then - if From_Aspect_Specification (Ritem) then - declare - Aitem : Node_Id; - Orig_Expr : constant Node_Id := - Expression (Corresponding_Aspect (Ritem)); + -- For ASIS use, perform semantic analysis of the original + -- predicate expression, which is otherwise not utilized. - begin + if ASIS_Mode then + Preanalyze_And_Resolve (Expression (Asp)); + end if; - -- For ASIS use, perform semantic analysis of the - -- original predicate expression, which is otherwise - -- not utilized. + Set_Entity (Identifier (Asp), New_Copy_Tree (Arg2)); + end if; - if ASIS_Mode then - Preanalyze_And_Resolve (Orig_Expr); - end if; + -- Concatenate to the existing predicate expressions by using + -- "and then". - -- Loop to find corresponding aspect, note that this - -- must be present given the pragma is marked delayed. + if Present (Expr) then + Expr := + Make_And_Then (Loc, + Left_Opnd => Relocate_Node (Expr), + Right_Opnd => Relocate_Node (Arg2)); - 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; + -- Otherwise this is the first predicate expression - Aitem := Next_Rep_Item (Aitem); - end loop; - end; - end if; + else + Expr := Relocate_Node (Arg2); + end if; + end if; + end Add_Predicate; - -- Now we can add the expression + -- Local variables - if No (Expr) then - Expr := Relocate_Node (Arg2); + Ritem : Node_Id; - -- There already was a predicate, so add to it + -- Start of processing for Add_Predicates - else - Expr := - Make_And_Then (Loc, - Left_Opnd => Relocate_Node (Expr), - Right_Opnd => Relocate_Node (Arg2)); - end if; - end if; + begin + Ritem := First_Rep_Item (Typ); + while Present (Ritem) loop + if Nkind (Ritem) = N_Pragma + and then Pragma_Name (Ritem) = Name_Predicate + then + 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; ----------------------------------------- diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index a46b651..fa84de4 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -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 diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index c2cefd1..162e6db 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -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; ----------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 5c886db..07579f0 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -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); - if Is_Completion then - - -- The null procedure acts as a body, nothing further is needed + -- The null procedure acts as a body, nothing further is needed + if Is_Completion then + 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 diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index a23ffeb..f39da2c 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -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; ---------------------------------- diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index d353bc9..239fadc 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -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; ------------------------- diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index f952616..fbe5f6c 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -183,25 +183,6 @@ package body Sem_Prag is -- Query whether a particular item appears in a mixed list of nodes and -- entities. It is assumed that all nodes in the list have entities. - 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_Postcondition_Use_In_Inlined_Subprogram (Prag : Node_Id; Spec_Id : Entity_Id); @@ -409,6 +390,8 @@ package body Sem_Prag is -- Local variables + GM : constant Ghost_Mode_Type := Ghost_Mode; + Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); @@ -419,6 +402,12 @@ package body Sem_Prag is -- Start of processing for Analyze_Contract_Cases_In_Decl_Part begin + -- Set the Ghost mode in effect from the pragma. Due to the delayed + -- analysis of the pragma, the Ghost mode at point of declaration and + -- point of analysis may not necessarely be the same. Use the mode in + -- effect at the point of declaration. + + Set_Ghost_Mode (N); Set_Analyzed (N); -- Single and multiple contract cases must appear in aggregate form. If @@ -464,6 +453,11 @@ package body Sem_Prag is else Error_Msg_N ("wrong syntax for constract cases", N); end if; + + -- Restore the original Ghost mode once analysis and expansion have + -- taken place. + + Ghost_Mode := GM; end Analyze_Contract_Cases_In_Decl_Part; ---------------------------------- @@ -1721,11 +1715,18 @@ package body Sem_Prag is (N : Node_Id; Expr_Val : out Boolean) is + GM : constant Ghost_Mode_Type := Ghost_Mode; Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1)); Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1)); begin + -- Set the Ghost mode in effect from the pragma. Due to the delayed + -- analysis of the pragma, the Ghost mode at point of declaration and + -- point of analysis may not necessarely be the same. Use the mode in + -- effect at the point of declaration. + + Set_Ghost_Mode (N); Error_Msg_Name_1 := Pragma_Name (N); -- An external property pragma must apply to an effectively volatile @@ -1756,6 +1757,11 @@ package body Sem_Prag is SPARK_Msg_N ("expression of % must be static", Expr); end if; end if; + + -- Restore the original Ghost mode once analysis and expansion have + -- taken place. + + Ghost_Mode := GM; end Analyze_External_Property_In_Decl_Part; --------------------------------- @@ -2258,11 +2264,18 @@ package body Sem_Prag is -------------------------------------------- procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is + GM : constant Ghost_Mode_Type := Ghost_Mode; Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N); Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); begin + -- Set the Ghost mode in effect from the pragma. Due to the delayed + -- analysis of the pragma, the Ghost mode at point of declaration and + -- point of analysis may not necessarely be the same. Use the mode in + -- effect at the point of declaration. + + Set_Ghost_Mode (N); Set_Analyzed (N); -- The expression is preanalyzed because it has not been moved to its @@ -2270,6 +2283,11 @@ package body Sem_Prag is -- is not desired at this point. Preanalyze_Assert_Expression (Expr, Standard_Boolean); + + -- Restore the original Ghost mode once analysis and expansion have + -- taken place. + + Ghost_Mode := GM; end Analyze_Initial_Condition_In_Decl_Part; -------------------------------------- @@ -3314,6 +3332,10 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec_Of (Subp_Decl); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Spec_Id); Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); -- Fully analyze the pragma when it appears inside a subprogram body @@ -3505,6 +3527,7 @@ package body Sem_Prag is procedure Analyze_Pre_Post_Condition is Prag_Iden : constant Node_Id := Pragma_Identifier (N); Subp_Decl : Node_Id; + Subp_Id : Entity_Id; Duplicates_OK : Boolean := False; -- Flag set when a pre/postcondition allows multiple pragmas of the @@ -3642,6 +3665,13 @@ package body Sem_Prag is return; end if; + Subp_Id := Defining_Entity (Subp_Decl); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Subp_Id); + -- Fully analyze the pragma when it appears inside a subprogram -- body because it cannot benefit from forward references. @@ -3728,6 +3758,11 @@ package body Sem_Prag is return; end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Spec_Id); + -- If we get here, then the pragma is legal if Nam_In (Pname, Name_Refined_Depends, @@ -5836,9 +5871,9 @@ package body Sem_Prag is ------------------------------------------------ procedure Process_Atomic_Independent_Shared_Volatile is - E_Id : Node_Id; - E : Entity_Id; D : Node_Id; + E : Entity_Id; + E_Id : Node_Id; K : Node_Kind; Utyp : Entity_Id; @@ -5882,6 +5917,11 @@ package body Sem_Prag is D := Declaration_Node (E); K := Nkind (D); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + -- Check duplicate before we chain ourselves Check_Duplicate_Pragma (E); @@ -7506,6 +7546,11 @@ package body Sem_Prag is else Process_Convention (C, Def_Id); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Def_Id); Kill_Size_Check_Code (Def_Id); Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False); end if; @@ -7878,11 +7923,19 @@ package body Sem_Prag is -------------------- procedure Process_Inline (Status : Inline_Status) is - Assoc : Node_Id; - Decl : Node_Id; - Subp_Id : Node_Id; - Subp : Entity_Id; - Applies : Boolean; + Applies : Boolean; + Assoc : Node_Id; + Decl : Node_Id; + Subp : Entity_Id; + Subp_Id : Node_Id; + + Ghost_Error_Posted : Boolean := False; + -- Flag set when an error concerning the illegal mix of Ghost and + -- non-Ghost subprograms is emitted. + + Ghost_Id : Entity_Id := Empty; + -- The entity of the first Ghost subprogram encountered while + -- processing the arguments of the pragma. procedure Make_Inline (Subp : Entity_Id); -- Subp is the defining unit name of the subprogram declaration. Set @@ -8151,6 +8204,37 @@ package body Sem_Prag is Set_Is_Inlined (Subp, True); end if; end case; + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Subp); + + -- Capture the entity of the first Ghost subprogram being + -- processed for error detection purposes. + + if Is_Ghost_Entity (Subp) then + if No (Ghost_Id) then + Ghost_Id := Subp; + end if; + + -- Otherwise the subprogram is non-Ghost. It is illegal to mix + -- references to Ghost and non-Ghost entities (SPARK RM 6.9). + + elsif Present (Ghost_Id) and then not Ghost_Error_Posted then + Ghost_Error_Posted := True; + + Error_Msg_Name_1 := Pname; + Error_Msg_N + ("pragma % cannot mention ghost and non-ghost subprograms", + N); + + Error_Msg_Sloc := Sloc (Ghost_Id); + Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id); + + Error_Msg_Sloc := Sloc (Subp); + Error_Msg_NE ("\& # declared as non-ghost", N, Subp); + end if; end Set_Inline_Flags; -- Start of processing for Process_Inline @@ -8422,6 +8506,10 @@ package body Sem_Prag is Proc_Scope : constant Entity_Id := Scope (Handler_Proc); begin + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Handler_Proc); Set_Is_Interrupt_Handler (Handler_Proc); -- If the pragma is not associated with a handler procedure within a @@ -8757,8 +8845,8 @@ package body Sem_Prag is procedure Process_Suppress_Unsuppress (Suppress_Case : Boolean) is C : Check_Id; - E_Id : Node_Id; E : Entity_Id; + E_Id : Node_Id; In_Package_Spec : constant Boolean := Is_Package_Or_Generic_Package (Current_Scope) @@ -8813,8 +8901,8 @@ package body Sem_Prag is -- on user code: we want to generate checks for analysis purposes, as -- set respectively by -gnatC and -gnatd.F - if (CodePeer_Mode or GNATprove_Mode) - and then Comes_From_Source (N) + if Comes_From_Source (N) + and then (CodePeer_Mode or GNATprove_Mode) then return; end if; @@ -8917,6 +9005,11 @@ package body Sem_Prag is return; end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + -- Enforce RM 11.5(7) which requires that for a pragma that -- appears within a package spec, the named entity must be -- within the package spec. We allow the package name itself @@ -10033,7 +10126,7 @@ package body Sem_Prag is -- An abstract state declared within a Ghost region becomes -- Ghost (SPARK RM 6.9(2)). - if Ghost_Mode > None then + if Ghost_Mode > None or else Is_Ghost_Entity (Pack_Id) then Set_Is_Ghost_Entity (State_Id); end if; @@ -10299,15 +10392,11 @@ package body Sem_Prag is Pack_Id := Defining_Entity (Pack_Decl); - Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); - - -- Mark the associated package as Ghost if it is subject to aspect - -- or pragma Ghost as this affects the declaration of an abstract - -- state. + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. - if Is_Subject_To_Ghost (Unit_Declaration_Node (Pack_Id)) then - Set_Is_Ghost_Entity (Pack_Id); - end if; + Mark_Pragma_As_Ghost (N, Pack_Id); + Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); States := Expression (Get_Argument (N, Pack_Id)); @@ -10554,11 +10643,14 @@ package body Sem_Prag is Lib_Entity := Find_Lib_Unit_Name; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Lib_Entity); + -- This pragma should only apply to a RCI unit (RM E.2.3(23)) - if Present (Lib_Entity) - and then not Debug_Flag_U - then + if Present (Lib_Entity) and then not Debug_Flag_U then if not Is_Remote_Call_Interface (Lib_Entity) then Error_Pragma ("pragma% only apply to rci unit"); @@ -10567,7 +10659,6 @@ package body Sem_Prag is else Set_Has_All_Calls_Remote (Lib_Entity); end if; - end if; end All_Calls_Remote; @@ -10604,80 +10695,87 @@ package body Sem_Prag is -- not analyzed. when Pragma_Annotate => Annotate : declare - Arg : Node_Id; - Exp : Node_Id; + Arg : Node_Id; + Expr : Node_Id; + Nam_Arg : Node_Id; begin GNAT_Pragma; Check_At_Least_N_Arguments (1); - -- See if last argument is Entity => local_Name, and if so process - -- and then remove it for remaining processing. + Nam_Arg := Last (Pragma_Argument_Associations (N)); - declare - Last_Arg : constant Node_Id := - Last (Pragma_Argument_Associations (N)); + -- Determine whether the last argument is "Entity => local_NAME" + -- and if it is, perform the required semantic checks. Remove the + -- argument from further processing. - begin - if Nkind (Last_Arg) = N_Pragma_Argument_Association - and then Chars (Last_Arg) = Name_Entity - then - Check_Arg_Is_Local_Name (Last_Arg); - Arg_Count := Arg_Count - 1; + if Nkind (Nam_Arg) = N_Pragma_Argument_Association + and then Chars (Nam_Arg) = Name_Entity + then + Check_Arg_Is_Local_Name (Nam_Arg); + Arg_Count := Arg_Count - 1; - -- Not allowed in compiler units (bootstrap issues) + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored Ghost + -- code. - Check_Compiler_Unit ("Entity for pragma Annotate", N); + if Is_Entity_Name (Get_Pragma_Arg (Nam_Arg)) + and then Present (Entity (Get_Pragma_Arg (Nam_Arg))) + then + Mark_Pragma_As_Ghost (N, Entity (Get_Pragma_Arg (Nam_Arg))); end if; - end; - -- Continue processing with last argument removed for now + -- Not allowed in compiler units (bootstrap issues) + + Check_Compiler_Unit ("Entity for pragma Annotate", N); + end if; + + -- Continue the processing with last argument removed for now Check_Arg_Is_Identifier (Arg1); Check_No_Identifiers; Store_Note (N); - -- Second parameter is optional, it is never analyzed + -- The second parameter is optional, it is never analyzed if No (Arg2) then null; - -- Here if we have a second parameter + -- Otherwise there is a second parameter else - -- Second parameter must be identifier + -- The second parameter must be an identifier Check_Arg_Is_Identifier (Arg2); - -- Process remaining parameters if any + -- Process the remaining parameters (if any) Arg := Next (Arg2); while Present (Arg) loop - Exp := Get_Pragma_Arg (Arg); - Analyze (Exp); + Expr := Get_Pragma_Arg (Arg); + Analyze (Expr); - if Is_Entity_Name (Exp) then + if Is_Entity_Name (Expr) then null; -- For string literals, we assume Standard_String as the -- type, unless the string contains wide or wide_wide -- characters. - elsif Nkind (Exp) = N_String_Literal then - if Has_Wide_Wide_Character (Exp) then - Resolve (Exp, Standard_Wide_Wide_String); - elsif Has_Wide_Character (Exp) then - Resolve (Exp, Standard_Wide_String); + elsif Nkind (Expr) = N_String_Literal then + if Has_Wide_Wide_Character (Expr) then + Resolve (Expr, Standard_Wide_Wide_String); + elsif Has_Wide_Character (Expr) then + Resolve (Expr, Standard_Wide_String); else - Resolve (Exp, Standard_String); + Resolve (Expr, Standard_String); end if; - elsif Is_Overloaded (Exp) then - Error_Pragma_Arg - ("ambiguous argument for pragma%", Exp); + elsif Is_Overloaded (Expr) then + Error_Pragma_Arg ("ambiguous argument for pragma%", Expr); else - Resolve (Exp); + Resolve (Expr); end if; Next (Arg); @@ -10751,12 +10849,18 @@ package body Sem_Prag is -- Local variables - Expr : Node_Id; - Newa : List_Id; + GM : constant Ghost_Mode_Type := Ghost_Mode; + Expr : Node_Id; + New_Args : List_Id; -- Start of processing for Assert begin + -- Ensure that analysis and expansion produce Ghost nodes if the + -- pragma itself is Ghost. + + Set_Ghost_Mode (N); + -- Assert is an Ada 2005 RM-defined pragma if Prag_Id = Pragma_Assert then @@ -10779,7 +10883,7 @@ package body Sem_Prag is -- assertion pragma contains attribute Loop_Entry, ensure that -- the related pragma is within a loop. - if Prag_Id = Pragma_Loop_Invariant + if Prag_Id = Pragma_Loop_Invariant or else Prag_Id = Pragma_Loop_Variant or else Contains_Loop_Entry (Expr) then @@ -10788,7 +10892,7 @@ package body Sem_Prag is -- Perform preanalysis to deal with embedded Loop_Entry -- attributes. - Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean); + Preanalyze_Assert_Expression (Expr, Any_Boolean); end if; -- Implement Assert[_And_Cut]/Assume/Loop_Invariant by generating @@ -10805,7 +10909,7 @@ package body Sem_Prag is -- Assume, or Assert_And_Cut pragma can be retrieved from the -- pragma kind of Original_Node(N). - Newa := New_List ( + New_Args := New_List ( Make_Pragma_Argument_Association (Loc, Expression => Make_Identifier (Loc, Pname)), Make_Pragma_Argument_Association (Sloc (Expr), @@ -10818,7 +10922,7 @@ package body Sem_Prag is -- ASIS use, before rewriting. Preanalyze_And_Resolve (Expression (Arg2), Standard_String); - Append_To (Newa, New_Copy_Tree (Arg2)); + Append_To (New_Args, New_Copy_Tree (Arg2)); end if; -- Rewrite as Check pragma @@ -10826,8 +10930,14 @@ package body Sem_Prag is Rewrite (N, Make_Pragma (Loc, Chars => Name_Check, - Pragma_Argument_Associations => Newa)); + Pragma_Argument_Associations => New_Args)); + Analyze (N); + + -- Restore the original Ghost mode once analysis and expansion + -- have taken place. + + Ghost_Mode := GM; end Assert; ---------------------- @@ -11114,6 +11224,12 @@ package body Sem_Prag is then Obj_Id := Entity (Obj); + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored Ghost + -- code. + + Mark_Pragma_As_Ghost (N, Obj_Id); + -- Detect a duplicate pragma. Note that it is not efficient to -- examine preceding statements as Boolean aspects may appear -- anywhere between the related object declaration and its @@ -11150,12 +11266,12 @@ package body Sem_Prag is -- pragma Asynchronous (LOCAL_NAME); when Pragma_Asynchronous => Asynchronous : declare - Nm : Entity_Id; C_Ent : Entity_Id; + Decl : Node_Id; + Formal : Entity_Id; L : List_Id; + Nm : Entity_Id; S : Node_Id; - N : Node_Id; - Formal : Entity_Id; procedure Process_Async_Pragma; -- Common processing for procedure and access-to-procedure case @@ -11207,6 +11323,11 @@ package body Sem_Prag is Analyze (Get_Pragma_Arg (Arg1)); Nm := Entity (Get_Pragma_Arg (Arg1)); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Nm); + if not Is_Remote_Call_Interface (C_Ent) and then not Is_Remote_Types (C_Ent) then @@ -11235,24 +11356,24 @@ package body Sem_Prag is ("pragma% cannot be applied to function", Arg1); elsif Is_Remote_Access_To_Subprogram_Type (Nm) then - if Is_Record_Type (Nm) then + if Is_Record_Type (Nm) then -- A record type that is the Equivalent_Type for a remote -- access-to-subprogram type. - N := Declaration_Node (Corresponding_Remote_Type (Nm)); + Decl := Declaration_Node (Corresponding_Remote_Type (Nm)); - else - -- A non-expanded RAS type (distribution is not enabled) + else + -- A non-expanded RAS type (distribution is not enabled) - N := Declaration_Node (Nm); - end if; + Decl := Declaration_Node (Nm); + end if; - if Nkind (N) = N_Full_Type_Declaration - and then Nkind (Type_Definition (N)) = + if Nkind (Decl) = N_Full_Type_Declaration + and then Nkind (Type_Definition (Decl)) = N_Access_Procedure_Definition then - L := Parameter_Specifications (Type_Definition (N)); + L := Parameter_Specifications (Type_Definition (Decl)); Process_Async_Pragma; if Is_Asynchronous (Nm) @@ -11303,11 +11424,10 @@ package body Sem_Prag is when Pragma_Atomic_Components | Pragma_Volatile_Components => - Atomic_Components : declare - E_Id : Node_Id; - E : Entity_Id; D : Node_Id; + E : Entity_Id; + E_Id : Node_Id; K : Node_Kind; begin @@ -11323,6 +11443,10 @@ package body Sem_Prag is E := Entity (E_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); Check_Duplicate_Pragma (E); if Rep_Item_Too_Early (E, N) @@ -11468,12 +11592,18 @@ package body Sem_Prag is -- allowed, since they have special meaning for Check_Policy. when Pragma_Check => Check : declare - Expr : Node_Id; - Eloc : Source_Ptr; + GM : constant Ghost_Mode_Type := Ghost_Mode; Cname : Name_Id; + Eloc : Source_Ptr; + Expr : Node_Id; Str : Node_Id; begin + -- Ensure that analysis and expansion produce Ghost nodes if the + -- pragma itself is Ghost. + + Set_Ghost_Mode (N); + GNAT_Pragma; Check_At_Least_N_Arguments (2); Check_At_Most_N_Arguments (3); @@ -11494,8 +11624,8 @@ package body Sem_Prag is case Cname is when Name_Assertions => Error_Pragma_Arg - ("""Assertions"" is not allowed as a check kind " - & "for pragma%", Arg1); + ("""Assertions"" is not allowed as a check kind for " + & "pragma%", Arg1); when Name_Statement_Assertions => Error_Pragma_Arg @@ -11556,21 +11686,18 @@ package body Sem_Prag is -- Deal with SCO generation case Cname is - when Name_Predicate | - Name_Invariant => - -- Nothing to do: since checks occur in client units, - -- the SCO for the aspect in the declaration unit is - -- conservatively always enabled. + -- Nothing to do for invariants and predicates as the checks + -- occur in the client units. The SCO for the aspect in the + -- declaration unit is conservatively always enabled. + when Name_Invariant | Name_Predicate => null; - when others => + -- Otherwise mark aspect/pragma SCO as enabled + when others => if Is_Checked (N) and then not Split_PPC (N) then - - -- Mark aspect/pragma SCO as enabled - Set_SCO_Pragma_Enabled (Loc); end if; end case; @@ -11629,7 +11756,7 @@ package body Sem_Prag is Left_Opnd => Make_Identifier (Eloc, Name_False), Right_Opnd => Expr), Then_Statements => New_List ( - Make_Null_Statement (Eloc)))); + Make_Null_Statement (Eloc)))); -- Now go ahead and analyze the if statement @@ -11671,6 +11798,11 @@ package body Sem_Prag is Analyze_And_Resolve (Expr, Any_Boolean); In_Assertion_Expr := In_Assertion_Expr - 1; end if; + + -- Restore the original Ghost mode once analysis and expansion + -- have taken place. + + Ghost_Mode := GM; end Check; -------------------------- @@ -12222,6 +12354,10 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec_Of (Subp_Decl); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Spec_Id); Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); -- Fully analyze the pragma when it appears inside a subprogram @@ -12278,6 +12414,11 @@ package body Sem_Prag is Check_Ada_83_Warning; Check_Arg_Count (2); Process_Convention (C, E); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); end Convention; --------------------------- @@ -12745,6 +12886,10 @@ package body Sem_Prag is Stmt := Prev (Stmt); end loop; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); Set_Has_Default_Init_Cond (Typ); Set_Has_Inherited_Default_Init_Cond (Typ, False); @@ -12804,7 +12949,10 @@ package body Sem_Prag is -- pragma Default_Storage_Pool (storage_pool_NAME | null); - when Pragma_Default_Storage_Pool => + when Pragma_Default_Storage_Pool => Default_Storage_Pool : declare + Pool : Node_Id; + + begin Ada_2012_Pragma; Check_Arg_Count (1); @@ -12815,44 +12963,57 @@ package body Sem_Prag is Check_Is_In_Decl_Part_Or_Package_Spec; end if; - -- Case of Default_Storage_Pool (null); + if Present (Arg1) then + Pool := Get_Pragma_Arg (Arg1); + + -- Case of Default_Storage_Pool (null); - if Nkind (Expression (Arg1)) = N_Null then - Analyze (Expression (Arg1)); + if Nkind (Pool) = N_Null then + Analyze (Pool); - -- This is an odd case, this is not really an expression, so - -- we don't have a type for it. So just set the type to Empty. + -- This is an odd case, this is not really an expression, + -- so we don't have a type for it. So just set the type to + -- Empty. - Set_Etype (Expression (Arg1), Empty); + Set_Etype (Pool, Empty); - -- Case of Default_Storage_Pool (storage_pool_NAME); + -- Case of Default_Storage_Pool (storage_pool_NAME); - else - -- If it's a configuration pragma, then the only allowed - -- argument is "null". + else + -- If it's a configuration pragma, then the only allowed + -- argument is "null". - if Is_Configuration_Pragma then - Error_Pragma_Arg ("NULL expected", Arg1); - end if; + if Is_Configuration_Pragma then + Error_Pragma_Arg ("NULL expected", Arg1); + end if; - -- The expected type for a non-"null" argument is - -- Root_Storage_Pool'Class, and the pool must be a variable. + -- The expected type for a non-"null" argument is + -- Root_Storage_Pool'Class, and the pool must be a variable. - Analyze_And_Resolve - (Get_Pragma_Arg (Arg1), - Typ => Class_Wide_Type (RTE (RE_Root_Storage_Pool))); + Analyze_And_Resolve + (Pool, Class_Wide_Type (RTE (RE_Root_Storage_Pool))); - if not Is_Variable (Expression (Arg1)) then - Error_Pragma_Arg - ("default storage pool must be a variable", Arg1); + if Is_Variable (Pool) then + + -- A pragma that applies to a Ghost entity becomes Ghost + -- for the purposes of legality checks and removal of + -- ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Entity (Pool)); + + else + Error_Pragma_Arg + ("default storage pool must be a variable", Arg1); + end if; end if; - end if; - -- Finally, record the pool name (or null). Freeze.Freeze_Entity - -- for an access type will use this information to set the - -- appropriate attributes of the access type. + -- Record the pool name (or null). Freeze.Freeze_Entity for an + -- access type will use this information to set the appropriate + -- attributes of the access type. - Default_Pool := Expression (Arg1); + Default_Pool := Pool; + end if; + end Default_Storage_Pool; ------------- -- Depends -- @@ -12941,7 +13102,7 @@ package body Sem_Prag is when Pragma_Discard_Names => Discard_Names : declare E : Entity_Id; - E_Id : Entity_Id; + E_Id : Node_Id; begin Check_Ada_83_Warning; @@ -12980,6 +13141,12 @@ package body Sem_Prag is E := Entity (E_Id); end if; + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored + -- Ghost code. + + Mark_Pragma_As_Ghost (N, E); + if (Is_First_Subtype (E) and then (Is_Enumeration_Type (E) or else Is_Tagged_Type (E))) @@ -12992,7 +13159,6 @@ package body Sem_Prag is Error_Pragma_Arg ("inappropriate entity for pragma%", Arg1); end if; - end if; end if; end Discard_Names; @@ -13024,6 +13190,12 @@ package body Sem_Prag is Arg := Get_Pragma_Arg (Arg1); Ent := Defining_Identifier (Parent (P)); + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored Ghost + -- code. + + Mark_Pragma_As_Ghost (N, Ent); + -- The expression must be analyzed in the special manner -- described in "Handling of Default and Per-Object -- Expressions" in sem.ads. @@ -13245,6 +13417,11 @@ package body Sem_Prag is Cunit_Node := Cunit (Current_Sem_Unit); Cunit_Ent := Cunit_Entity (Current_Sem_Unit); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Cunit_Ent); + if Nkind_In (Unit (Cunit_Node), N_Package_Body, N_Subprogram_Body) then @@ -13432,6 +13609,12 @@ package body Sem_Prag is else Process_Convention (C, Def_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored Ghost + -- code. + + Mark_Pragma_As_Ghost (N, Def_Id); + if Ekind (Def_Id) /= E_Constant then Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False); @@ -13848,6 +14031,12 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec_Of (Subp_Decl); + -- Mark the pragma as Ghost if the related subprogram is also + -- Ghost. This also ensures that any expansion performed further + -- below will produce Ghost nodes. + + Mark_Pragma_As_Ghost (N, Spec_Id); + -- Examine the formals of the related subprogram Formal := First_Formal (Spec_Id); @@ -13881,6 +14070,7 @@ package body Sem_Prag is Error_Msg_NE ("\subprogram & lacks parameter of specific tagged or " & "generic private type", N, Spec_Id); + return; end if; @@ -13914,10 +14104,9 @@ package body Sem_Prag is -- [, [Link_Name =>] static_string_EXPRESSION ]); when Pragma_External => External : declare - Def_Id : Entity_Id; - - C : Convention_Id; - pragma Warnings (Off, C); + C : Convention_Id; + E : Entity_Id; + pragma Warnings (Off, C); begin GNAT_Pragma; @@ -13928,11 +14117,17 @@ package body Sem_Prag is Name_Link_Name)); Check_At_Least_N_Arguments (2); Check_At_Most_N_Arguments (4); - Process_Convention (C, Def_Id); + Process_Convention (C, E); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False); - Process_Interface_Name (Def_Id, Arg3, Arg4); - Set_Exported (Def_Id, Arg2); + Process_Interface_Name (E, Arg3, Arg4); + Set_Exported (E, Arg2); end External; -------------------------- @@ -14003,20 +14198,25 @@ package body Sem_Prag is -- pragma Favor_Top_Level (type_NAME); when Pragma_Favor_Top_Level => Favor_Top_Level : declare - Named_Entity : Entity_Id; + Typ : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); Check_Arg_Is_Local_Name (Arg1); - Named_Entity := Entity (Get_Pragma_Arg (Arg1)); + Typ := Entity (Get_Pragma_Arg (Arg1)); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); -- If it's an access-to-subprogram type (in particular, not a -- subtype), set the flag on that type. - if Is_Access_Subprogram_Type (Named_Entity) then - Set_Can_Use_Internal_Rep (Named_Entity, False); + if Is_Access_Subprogram_Type (Typ) then + Set_Can_Use_Internal_Rep (Typ, False); -- Otherwise it's an error (name denotes the wrong sort of entity) @@ -14110,6 +14310,7 @@ package body Sem_Prag is end if; -- Protected and task types cannot be subject to pragma Ghost + -- (SPARK RM 6.9(19)). elsif Nkind (Stmt) = N_Protected_Type_Declaration then Error_Pragma ("pragma % cannot apply to a protected type"); @@ -14248,6 +14449,19 @@ package body Sem_Prag is return; end if; end if; + + -- A synchronized object cannot be subject to pragma Ghost + -- (SPARK RM 6.9(19)). + + elsif Ekind (Id) = E_Variable then + if Is_Protected_Type (Etype (Id)) then + Error_Pragma ("pragma % cannot apply to a protected object"); + return; + + elsif Is_Task_Type (Etype (Id)) then + Error_Pragma ("pragma % cannot apply to a task object"); + return; + end if; end if; -- Analyze the Boolean expression (if any) @@ -14815,11 +15029,11 @@ package body Sem_Prag is -- pragma Independent_Components (array_or_record_LOCAL_NAME); when Pragma_Independent_Components => Independent_Components : declare + C : Node_Id; + D : Node_Id; E_Id : Node_Id; E : Entity_Id; - D : Node_Id; K : Node_Kind; - C : Node_Id; begin Check_Ada_83_Warning; @@ -14835,6 +15049,11 @@ package body Sem_Prag is E := Entity (E_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + -- Check duplicate before we chain ourselves Check_Duplicate_Pragma (E); @@ -14944,6 +15163,11 @@ package body Sem_Prag is Pack_Id := Defining_Entity (Pack_Decl); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Pack_Id); + -- Verify the declaration order of pragma Initial_Condition with -- respect to pragmas Abstract_State and Initializes when SPARK -- checks are enabled. @@ -15055,6 +15279,10 @@ package body Sem_Prag is Pack_Id := Defining_Entity (Pack_Decl); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Pack_Id); Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); -- Verify the declaration order of pragmas Abstract_State and @@ -15512,9 +15740,10 @@ package body Sem_Prag is -- [,[Message =>] String_Expression]); when Pragma_Invariant => Invariant : declare - Type_Id : Node_Id; - Typ : Entity_Id; + GM : constant Ghost_Mode_Type := Ghost_Mode; Discard : Boolean; + Typ : Entity_Id; + Type_Id : Node_Id; begin GNAT_Pragma; @@ -15569,6 +15798,11 @@ package body Sem_Prag is ("pragma% only allowed for private type", Arg1); end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); + -- Not allowed for abstract type in the non-class case (it is -- allowed to use Invariant'Class for abstract types). @@ -15577,6 +15811,11 @@ package body Sem_Prag is ("pragma% not allowed for abstract type", Arg1); end if; + -- Link the pragma on to the rep item chain, for processing when + -- the type is frozen. + + Discard := Rep_Item_Too_Late (Typ, N, FOnly => True); + -- Note that the type has at least one invariant, and also that -- it has inheritable invariants if we have Invariant'Class -- or Type_Invariant'Class. Build the corresponding invariant @@ -15596,11 +15835,10 @@ package body Sem_Prag is Set_Has_Inheritable_Invariants (Typ); end if; - -- The remaining processing is simply to link the pragma on to - -- the rep item chain, for processing when the type is frozen. - -- This is accomplished by a call to Rep_Item_Too_Late. + -- Restore the original Ghost mode once analysis and expansion + -- have taken place. - Discard := Rep_Item_Too_Late (Typ, N, FOnly => True); + Ghost_Mode := GM; end Invariant; ---------------------- @@ -16197,14 +16435,22 @@ package body Sem_Prag is -------------------- -- pragma Linker_Section ( - -- [Entity =>] LOCAL_NAME - -- [Section =>] static_string_EXPRESSION); + -- [Entity =>] LOCAL_NAME + -- [Section =>] static_string_EXPRESSION); when Pragma_Linker_Section => Linker_Section : declare Arg : Node_Id; Ent : Entity_Id; LPE : Node_Id; + Ghost_Error_Posted : Boolean := False; + -- Flag set when an error concerning the illegal mix of Ghost and + -- non-Ghost subprograms is emitted. + + Ghost_Id : Entity_Id := Empty; + -- The entity of the first Ghost subprogram encountered while + -- processing the arguments of the pragma. + begin GNAT_Pragma; Check_Arg_Order ((Name_Entity, Name_Section)); @@ -16236,6 +16482,12 @@ package body Sem_Prag is Set_Linker_Section_Pragma (Ent, N); + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored + -- Ghost code. + + Mark_Pragma_As_Ghost (N, Ent); + -- Subprograms when Subprogram_Kind => @@ -16253,6 +16505,43 @@ package body Sem_Prag is loop if No (Linker_Section_Pragma (Ent)) then Set_Linker_Section_Pragma (Ent, N); + + -- A pragma that applies to a Ghost entity becomes + -- Ghost for the purposes of legality checks and + -- removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Ent); + + -- Capture the entity of the first Ghost subprogram + -- being processed for error detection purposes. + + if Is_Ghost_Entity (Ent) then + if No (Ghost_Id) then + Ghost_Id := Ent; + end if; + + -- Otherwise the subprogram is non-Ghost. It is + -- illegal to mix references to Ghost and non-Ghost + -- entities (SPARK RM 6.9). + + elsif Present (Ghost_Id) + and then not Ghost_Error_Posted + then + Ghost_Error_Posted := True; + + Error_Msg_Name_1 := Pname; + Error_Msg_N + ("pragma % cannot mention ghost and " + & "non-ghost subprograms", N); + + Error_Msg_Sloc := Sloc (Ghost_Id); + Error_Msg_NE + ("\& # declared as ghost", N, Ghost_Id); + + Error_Msg_Sloc := Sloc (Ent); + Error_Msg_NE + ("\& # declared as non-ghost", N, Ent); + end if; end if; Ent := Homonym (Ent); @@ -16624,8 +16913,7 @@ package body Sem_Prag is -- pragma No_Elaboration_Code_All; - when Pragma_No_Elaboration_Code_All => NECA : declare - begin + when Pragma_No_Elaboration_Code_All => GNAT_Pragma; Check_Valid_Library_Unit_Pragma; @@ -16672,7 +16960,6 @@ package body Sem_Prag is if In_Extended_Main_Source_Unit (N) then Opt.No_Elab_Code_All_Pragma := N; end if; - end NECA; --------------- -- No_Inline -- @@ -16691,10 +16978,18 @@ package body Sem_Prag is -- pragma No_Return (procedure_LOCAL_NAME {, procedure_Local_Name}); when Pragma_No_Return => No_Return : declare - Id : Node_Id; + Arg : Node_Id; E : Entity_Id; Found : Boolean; - Arg : Node_Id; + Id : Node_Id; + + Ghost_Error_Posted : Boolean := False; + -- Flag set when an error concerning the illegal mix of Ghost and + -- non-Ghost subprograms is emitted. + + Ghost_Id : Entity_Id := Empty; + -- The entity of the first Ghost procedure encountered while + -- processing the arguments of the pragma. begin Ada_2005_Pragma; @@ -16719,6 +17014,7 @@ package body Sem_Prag is -- Loop to find matching procedures E := Entity (Id); + Found := False; while Present (E) and then Scope (E) = Current_Scope @@ -16726,6 +17022,41 @@ package body Sem_Prag is if Ekind_In (E, E_Procedure, E_Generic_Procedure) then Set_No_Return (E); + -- A pragma that applies to a Ghost entity becomes Ghost + -- for the purposes of legality checks and removal of + -- ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + + -- Capture the entity of the first Ghost procedure being + -- processed for error detection purposes. + + if Is_Ghost_Entity (E) then + if No (Ghost_Id) then + Ghost_Id := E; + end if; + + -- Otherwise the subprogram is non-Ghost. It is illegal + -- to mix references to Ghost and non-Ghost entities + -- (SPARK RM 6.9). + + elsif Present (Ghost_Id) + and then not Ghost_Error_Posted + then + Ghost_Error_Posted := True; + + Error_Msg_Name_1 := Pname; + Error_Msg_N + ("pragma % cannot mention ghost and non-ghost " + & "procedures", N); + + Error_Msg_Sloc := Sloc (Ghost_Id); + Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id); + + Error_Msg_Sloc := Sloc (E); + Error_Msg_NE ("\& # declared as non-ghost", N, E); + end if; + -- Set flag on any alias as well if Is_Overloadable (E) and then Present (Alias (E)) then @@ -16794,8 +17125,8 @@ package body Sem_Prag is -- pragma No_Tagged_Streams ([Entity => ]tagged_type_local_NAME); when Pragma_No_Tagged_Streams => No_Tagged_Strms : declare - E_Id : Node_Id; E : Entity_Id; + E_Id : Node_Id; begin GNAT_Pragma; @@ -16906,8 +17237,8 @@ package body Sem_Prag is -- [,[Version =>] Ada_05]] ); when Pragma_Obsolescent => Obsolescent : declare - Ename : Node_Id; Decl : Node_Id; + Ename : Node_Id; procedure Set_Obsolescent (E : Entity_Id); -- Given an entity Ent, mark it as obsolescent if appropriate @@ -16925,6 +17256,12 @@ package body Sem_Prag is Active := True; Ent := E; + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored Ghost + -- code. + + Mark_Pragma_As_Ghost (N, E); + -- Entity name was given if Present (Ename) then @@ -17295,10 +17632,10 @@ package body Sem_Prag is when Pragma_Pack => Pack : declare Assoc : constant Node_Id := Arg1; - Type_Id : Node_Id; - Typ : Entity_Id; Ctyp : Entity_Id; Ignore : Boolean := False; + Typ : Entity_Id; + Type_Id : Node_Id; begin Check_No_Identifiers; @@ -17324,6 +17661,11 @@ package body Sem_Prag is Typ := Underlying_Type (Typ); end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); + if not Is_Array_Type (Typ) and then not Is_Record_Type (Typ) then Error_Pragma ("pragma% must specify array or record type"); end if; @@ -17581,6 +17923,11 @@ package body Sem_Prag is Item_Id := Defining_Entity (Stmt); State := Get_Pragma_Arg (Arg1); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Item_Id); + -- Detect any discrepancies between the placement of the object -- or package instantiation with respect to state space and the -- encapsulating state. @@ -17703,6 +18050,11 @@ package body Sem_Prag is Check_First_Subtype (Arg1); Ent := Entity (Get_Pragma_Arg (Arg1)); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Ent); + -- The pragma may come from an aspect on a private declaration, -- even if the freeze point at which this is analyzed in the -- private part after the full view. @@ -17791,6 +18143,12 @@ package body Sem_Prag is Ent := Entity (Get_Pragma_Arg (Arg1)); Decl := Parent (Ent); + -- A pragma that applies to a Ghost entity becomes Ghost for + -- the purposes of legality checks and removal of ignored Ghost + -- code. + + Mark_Pragma_As_Ghost (N, Ent); + -- Check for duplication before inserting in list of -- representation items. @@ -17939,9 +18297,9 @@ package body Sem_Prag is -- [Check =>] boolean_EXPRESSION); when Pragma_Predicate => Predicate : declare - Type_Id : Node_Id; - Typ : Entity_Id; Discard : Boolean; + Typ : Entity_Id; + Type_Id : Node_Id; begin GNAT_Pragma; @@ -17959,6 +18317,11 @@ package body Sem_Prag is return; end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); + -- The remaining processing is simply to link the pragma on to -- the rep item chain, for processing when the type is frozen. -- This is accomplished by a call to Rep_Item_Too_Late. We also @@ -17990,6 +18353,11 @@ package body Sem_Prag is end if; Ent := Find_Lib_Unit_Name; + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Ent); Check_Duplicate_Pragma (Ent); -- This filters out pragmas inside generic parents that show up @@ -18616,6 +18984,11 @@ package body Sem_Prag is end if; Ent := Find_Lib_Unit_Name; + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Ent); Set_Is_Pure (Ent); Set_Has_Pragma_Pure (Ent); Set_Suppress_Elaboration_Warnings (Ent); @@ -18628,9 +19001,9 @@ package body Sem_Prag is -- pragma Pure_Function ([Entity =>] function_LOCAL_NAME); when Pragma_Pure_Function => Pure_Function : declare - E_Id : Node_Id; - E : Entity_Id; Def_Id : Entity_Id; + E : Entity_Id; + E_Id : Node_Id; Effective : Boolean := False; begin @@ -18648,6 +19021,11 @@ package body Sem_Prag is E := Entity (E_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + if Present (E) then loop Def_Id := Get_Base_Subprogram (E); @@ -18917,6 +19295,11 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec (Pack_Decl); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Spec_Id); + -- State refinement is allowed only when the corresponding package -- declaration has non-null pragma Abstract_State. Refinement not -- enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)). @@ -18982,7 +19365,7 @@ package body Sem_Prag is -- Item chain of Ent since it is rewritten by the expander as a -- procedure call statement that will break the chain. - Set_Has_Relative_Deadline_Pragma (P, True); + Set_Has_Relative_Deadline_Pragma (P); end Relative_Deadline; ------------------------ @@ -19002,6 +19385,11 @@ package body Sem_Prag is E := Entity (Get_Pragma_Arg (Arg1)); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + if Nkind (Parent (E)) = N_Formal_Type_Declaration and then Ekind (E) = E_General_Access_Type and then Is_Class_Wide_Type (Directly_Designated_Type (E)) @@ -19042,6 +19430,11 @@ package body Sem_Prag is K := Nkind (Unit (Cunit_Node)); Cunit_Ent := Cunit_Entity (Current_Sem_Unit); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Cunit_Ent); + if K = N_Package_Declaration or else K = N_Generic_Package_Declaration or else K = N_Subprogram_Declaration @@ -19079,6 +19472,11 @@ package body Sem_Prag is Cunit_Node := Cunit (Current_Sem_Unit); Cunit_Ent := Cunit_Entity (Current_Sem_Unit); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Cunit_Ent); + if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration, N_Generic_Package_Declaration) then @@ -19231,6 +19629,11 @@ package body Sem_Prag is Cunit_Node := Cunit (Current_Sem_Unit); Cunit_Ent := Cunit_Entity (Current_Sem_Unit); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Cunit_Ent); + if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration, N_Generic_Package_Declaration) then @@ -19262,8 +19665,8 @@ package body Sem_Prag is when Pragma_Simple_Storage_Pool_Type => Simple_Storage_Pool_Type : declare - Type_Id : Node_Id; Typ : Entity_Id; + Type_Id : Node_Id; begin GNAT_Pragma; @@ -19278,6 +19681,11 @@ package body Sem_Prag is return; end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); + -- We require the pragma to apply to a type declared in a package -- declaration, but not (immediately) within a package body. @@ -20195,12 +20603,23 @@ package body Sem_Prag is -- pragma Suppress_Debug_Info ([Entity =>] LOCAL_NAME); - when Pragma_Suppress_Debug_Info => + when Pragma_Suppress_Debug_Info => Suppress_Debug_Info : declare + Nam_Id : Entity_Id; + + begin GNAT_Pragma; Check_Arg_Count (1); Check_Optional_Identifier (Arg1, Name_Entity); Check_Arg_Is_Local_Name (Arg1); - Set_Debug_Info_Off (Entity (Get_Pragma_Arg (Arg1))); + + Nam_Id := Entity (Get_Pragma_Arg (Arg1)); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Nam_Id); + Set_Debug_Info_Off (Nam_Id); + end Suppress_Debug_Info; ---------------------------------- -- Suppress_Exception_Locations -- @@ -20221,8 +20640,8 @@ package body Sem_Prag is -- pragma Suppress_Initialization ([Entity =>] type_Name); when Pragma_Suppress_Initialization => Suppress_Init : declare - E_Id : Node_Id; E : Entity_Id; + E_Id : Node_Id; begin GNAT_Pragma; @@ -20238,6 +20657,11 @@ package body Sem_Prag is E := Entity (E_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + if not Is_Type (E) and then Ekind (E) /= E_Variable then Error_Pragma_Arg ("pragma% requires variable, type or subtype", Arg1); @@ -20631,6 +21055,11 @@ package body Sem_Prag is return; end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Subp_Id); + -- Preanalyze the original aspect argument "Name" for ASIS or for -- a generic subprogram to properly capture global references. @@ -20678,8 +21107,8 @@ package body Sem_Prag is -- pragma Thread_Local_Storage ([Entity =>] LOCAL_NAME); when Pragma_Thread_Local_Storage => Thread_Local_Storage : declare - Id : Node_Id; E : Entity_Id; + Id : Node_Id; begin GNAT_Pragma; @@ -20698,8 +21127,14 @@ package body Sem_Prag is E := Entity (Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E); + if Rep_Item_Too_Early (E, N) - or else Rep_Item_Too_Late (E, N) + or else + Rep_Item_Too_Late (E, N) then raise Pragma_Exit; end if; @@ -20824,12 +21259,12 @@ package body Sem_Prag is when Pragma_Unchecked_Union => Unchecked_Union : declare Assoc : constant Node_Id := Arg1; Type_Id : constant Node_Id := Get_Pragma_Arg (Assoc); - Typ : Entity_Id; - Tdef : Node_Id; Clist : Node_Id; - Vpart : Node_Id; Comp : Node_Id; + Tdef : Node_Id; + Typ : Entity_Id; Variant : Node_Id; + Vpart : Node_Id; begin Ada_2005_Pragma; @@ -20841,6 +21276,11 @@ package body Sem_Prag is Typ := Entity (Type_Id); + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Typ); + if Typ = Any_Type or else Rep_Item_Too_Early (Typ, N) then @@ -20869,7 +21309,7 @@ package body Sem_Prag is elsif not Has_Discriminants (Typ) then Error_Msg_N - ("unchecked union must have one discriminant", Typ); + ("unchecked union must have one discriminant", Typ); return; -- Note: in previous versions of GNAT we used to check for limited @@ -20974,6 +21414,10 @@ package body Sem_Prag is Error_Pragma_Arg ("pragma% requires type", Arg1); end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, E_Id); Set_Universal_Aliasing (Implementation_Base_Type (E_Id)); Record_Rep_Item (E_Id, N); end Universal_Alias; @@ -21010,9 +21454,17 @@ package body Sem_Prag is -- pragma Unmodified (LOCAL_NAME {, LOCAL_NAME}); when Pragma_Unmodified => Unmodified : declare - Arg_Node : Node_Id; + Arg : Node_Id; Arg_Expr : Node_Id; - Arg_Ent : Entity_Id; + Arg_Id : Entity_Id; + + Ghost_Error_Posted : Boolean := False; + -- Flag set when an error concerning the illegal mix of Ghost and + -- non-Ghost variables is emitted. + + Ghost_Id : Entity_Id := Empty; + -- The entity of the first Ghost variable encountered while + -- processing the arguments of the pragma. begin GNAT_Pragma; @@ -21020,9 +21472,9 @@ package body Sem_Prag is -- Loop through arguments - Arg_Node := Arg1; - while Present (Arg_Node) loop - Check_No_Identifier (Arg_Node); + Arg := Arg1; + while Present (Arg) loop + Check_No_Identifier (Arg); -- Note: the analyze call done by Check_Arg_Is_Local_Name will -- in fact generate reference, so that the entity will have a @@ -21032,22 +21484,59 @@ package body Sem_Prag is -- Has_Pragma_Unreferenced flag is set, so that no warning is -- generated for this reference. - Check_Arg_Is_Local_Name (Arg_Node); - Arg_Expr := Get_Pragma_Arg (Arg_Node); + Check_Arg_Is_Local_Name (Arg); + Arg_Expr := Get_Pragma_Arg (Arg); if Is_Entity_Name (Arg_Expr) then - Arg_Ent := Entity (Arg_Expr); + Arg_Id := Entity (Arg_Expr); + + if Is_Assignable (Arg_Id) then + Set_Has_Pragma_Unmodified (Arg_Id); + + -- A pragma that applies to a Ghost entity becomes Ghost + -- for the purposes of legality checks and removal of + -- ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Arg_Id); + + -- Capture the entity of the first Ghost variable being + -- processed for error detection purposes. + + if Is_Ghost_Entity (Arg_Id) then + if No (Ghost_Id) then + Ghost_Id := Arg_Id; + end if; + + -- Otherwise the variable is non-Ghost. It is illegal + -- to mix references to Ghost and non-Ghost entities + -- (SPARK RM 6.9). + + elsif Present (Ghost_Id) + and then not Ghost_Error_Posted + then + Ghost_Error_Posted := True; + + Error_Msg_Name_1 := Pname; + Error_Msg_N + ("pragma % cannot mention ghost and non-ghost " + & "variables", N); + + Error_Msg_Sloc := Sloc (Ghost_Id); + Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id); + + Error_Msg_Sloc := Sloc (Arg_Id); + Error_Msg_NE ("\& # declared as non-ghost", N, Arg_Id); + end if; + + -- Otherwise the pragma referenced an illegal entity - if not Is_Assignable (Arg_Ent) then - Error_Pragma_Arg - ("pragma% can only be applied to a variable", - Arg_Expr); else - Set_Has_Pragma_Unmodified (Arg_Ent); + Error_Pragma_Arg + ("pragma% can only be applied to a variable", Arg_Expr); end if; end if; - Next (Arg_Node); + Next (Arg); end loop; end Unmodified; @@ -21062,11 +21551,19 @@ package body Sem_Prag is -- pragma Unreferenced (library_unit_NAME {, library_unit_NAME} when Pragma_Unreferenced => Unreferenced : declare - Arg_Node : Node_Id; + Arg : Node_Id; Arg_Expr : Node_Id; - Arg_Ent : Entity_Id; + Arg_Id : Entity_Id; Citem : Node_Id; + Ghost_Error_Posted : Boolean := False; + -- Flag set when an error concerning the illegal mix of Ghost and + -- non-Ghost names is emitted. + + Ghost_Id : Entity_Id := Empty; + -- The entity of the first Ghost name encountered while processing + -- the arguments of the pragma. + begin GNAT_Pragma; Check_At_Least_N_Arguments (1); @@ -21080,20 +21577,20 @@ package body Sem_Prag is -- Par.Prag) that the arguments are either identifiers or -- selected components. - Arg_Node := Arg1; - while Present (Arg_Node) loop + Arg := Arg1; + while Present (Arg) loop Citem := First (List_Containing (N)); while Citem /= N loop + Arg_Expr := Get_Pragma_Arg (Arg); + if Nkind (Citem) = N_With_Clause - and then - Same_Name (Name (Citem), Get_Pragma_Arg (Arg_Node)) + and then Same_Name (Name (Citem), Arg_Expr) then Set_Has_Pragma_Unreferenced (Cunit_Entity (Get_Source_Unit (Library_Unit (Citem)))); - Set_Elab_Unit_Name - (Get_Pragma_Arg (Arg_Node), Name (Citem)); + Set_Elab_Unit_Name (Arg_Expr, Name (Citem)); exit; end if; @@ -21102,18 +21599,18 @@ package body Sem_Prag is if Citem = N then Error_Pragma_Arg - ("argument of pragma% is not withed unit", Arg_Node); + ("argument of pragma% is not withed unit", Arg); end if; - Next (Arg_Node); + Next (Arg); end loop; -- Case of not in list of context items else - Arg_Node := Arg1; - while Present (Arg_Node) loop - Check_No_Identifier (Arg_Node); + Arg := Arg1; + while Present (Arg) loop + Check_No_Identifier (Arg); -- Note: the analyze call done by Check_Arg_Is_Local_Name -- will in fact generate reference, so that the entity will @@ -21123,11 +21620,11 @@ package body Sem_Prag is -- before the Has_Pragma_Unreferenced flag is set, so that -- no warning is generated for this reference. - Check_Arg_Is_Local_Name (Arg_Node); - Arg_Expr := Get_Pragma_Arg (Arg_Node); + Check_Arg_Is_Local_Name (Arg); + Arg_Expr := Get_Pragma_Arg (Arg); if Is_Entity_Name (Arg_Expr) then - Arg_Ent := Entity (Arg_Expr); + Arg_Id := Entity (Arg_Expr); -- If the entity is overloaded, the pragma applies to the -- most recent overloading, as documented. In this case, @@ -21135,13 +21632,48 @@ package body Sem_Prag is -- must be done here explicitly. if Is_Overloaded (Arg_Expr) then - Generate_Reference (Arg_Ent, N); + Generate_Reference (Arg_Id, N); end if; - Set_Has_Pragma_Unreferenced (Arg_Ent); + Set_Has_Pragma_Unreferenced (Arg_Id); + + -- A pragma that applies to a Ghost entity becomes Ghost + -- for the purposes of legality checks and removal of + -- ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Arg_Id); + + -- Capture the entity of the first Ghost name being + -- processed for error detection purposes. + + if Is_Ghost_Entity (Arg_Id) then + if No (Ghost_Id) then + Ghost_Id := Arg_Id; + end if; + + -- Otherwise the name is non-Ghost. It is illegal to mix + -- references to Ghost and non-Ghost entities + -- (SPARK RM 6.9). + + elsif Present (Ghost_Id) + and then not Ghost_Error_Posted + then + Ghost_Error_Posted := True; + + Error_Msg_Name_1 := Pname; + Error_Msg_N + ("pragma % cannot mention ghost and non-ghost names", + N); + + Error_Msg_Sloc := Sloc (Ghost_Id); + Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id); + + Error_Msg_Sloc := Sloc (Arg_Id); + Error_Msg_NE ("\& # declared as non-ghost", N, Arg_Id); + end if; end if; - Next (Arg_Node); + Next (Arg); end loop; end if; end Unreferenced; @@ -21153,28 +21685,78 @@ package body Sem_Prag is -- pragma Unreferenced_Objects (LOCAL_NAME {, LOCAL_NAME}); when Pragma_Unreferenced_Objects => Unreferenced_Objects : declare - Arg_Node : Node_Id; + Arg : Node_Id; Arg_Expr : Node_Id; + Arg_Id : Entity_Id; + + Ghost_Error_Posted : Boolean := False; + -- Flag set when an error concerning the illegal mix of Ghost and + -- non-Ghost types is emitted. + + Ghost_Id : Entity_Id := Empty; + -- The entity of the first Ghost type encountered while processing + -- the arguments of the pragma. begin GNAT_Pragma; Check_At_Least_N_Arguments (1); - Arg_Node := Arg1; - while Present (Arg_Node) loop - Check_No_Identifier (Arg_Node); - Check_Arg_Is_Local_Name (Arg_Node); - Arg_Expr := Get_Pragma_Arg (Arg_Node); + Arg := Arg1; + while Present (Arg) loop + Check_No_Identifier (Arg); + Check_Arg_Is_Local_Name (Arg); + Arg_Expr := Get_Pragma_Arg (Arg); + + if Is_Entity_Name (Arg_Expr) then + Arg_Id := Entity (Arg_Expr); - if not Is_Entity_Name (Arg_Expr) - or else not Is_Type (Entity (Arg_Expr)) - then + if Is_Type (Arg_Id) then + Set_Has_Pragma_Unreferenced_Objects (Arg_Id); + + -- A pragma that applies to a Ghost entity becomes Ghost + -- for the purposes of legality checks and removal of + -- ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Arg_Id); + + -- Capture the entity of the first Ghost type being + -- processed for error detection purposes. + + if Is_Ghost_Entity (Arg_Id) then + if No (Ghost_Id) then + Ghost_Id := Arg_Id; + end if; + + -- Otherwise the type is non-Ghost. It is illegal to mix + -- references to Ghost and non-Ghost entities + -- (SPARK RM 6.9). + + elsif Present (Ghost_Id) + and then not Ghost_Error_Posted + then + Ghost_Error_Posted := True; + + Error_Msg_Name_1 := Pname; + Error_Msg_N + ("pragma % cannot mention ghost and non-ghost types", + N); + + Error_Msg_Sloc := Sloc (Ghost_Id); + Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id); + + Error_Msg_Sloc := Sloc (Arg_Id); + Error_Msg_NE ("\& # declared as non-ghost", N, Arg_Id); + end if; + else + Error_Pragma_Arg + ("argument for pragma% must be type or subtype", Arg); + end if; + else Error_Pragma_Arg - ("argument for pragma% must be type or subtype", Arg_Node); + ("argument for pragma% must be type or subtype", Arg); end if; - Set_Has_Pragma_Unreferenced_Objects (Entity (Arg_Expr)); - Next (Arg_Node); + Next (Arg); end loop; end Unreferenced_Objects; @@ -21320,7 +21902,7 @@ package body Sem_Prag is GNAT_Pragma; Process_Atomic_Independent_Shared_Volatile; - ------------------------- + ------------------------- -- Volatile_Components -- ------------------------- @@ -21909,6 +22491,7 @@ package body Sem_Prag is -- Local variables + GM : constant Ghost_Mode_Type := Ghost_Mode; Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); @@ -21918,6 +22501,13 @@ package body Sem_Prag is -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part begin + -- Set the Ghost mode in effect from the pragma. Due to the delayed + -- analysis of the pragma, the Ghost mode at point of declaration and + -- point of analysis may not necessarely be the same. Use the mode in + -- effect at the point of declaration. + + Set_Ghost_Mode (N); + -- Ensure that the subprogram and its formals are visible when analyzing -- the expression of the pragma. @@ -21951,6 +22541,11 @@ package body Sem_Prag is -- subprogram subject to pragma Inline_Always. Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); + + -- Restore the original Ghost mode once analysis and expansion have + -- taken place. + + Ghost_Mode := GM; end Analyze_Pre_Post_Condition_In_Decl_Part; ------------------------------------------ diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index cb3f82e..52f6935 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 4a74acf..c7d220c 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -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); + + Arg1 := Get_Pragma_Arg (Arg1); + Arg2 := Get_Pragma_Arg (Arg2); - -- The current Check_Policy pragma matches the requested policy, - -- return the second argument which denotes the policy identifier. + -- The current Check_Policy pragma matches the requested policy or + -- appears in the single argument form (Assertion, policy_id). - if Chars (Expr) = Policy then - return Chars (Get_Pragma_Arg (Next (Arg))); + 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; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 0cc27b1..d8a04e0 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -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. diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 63a6ad5..824acd5 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -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 diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 4af7b54..eefca47 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -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); |