From d65a80fd559aca749b54eb6affd71d2d84f410f8 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Fri, 13 Jan 2017 09:34:48 +0000 Subject: [PATCH] atree.adb (Allocate_Initialize_Node): A newly created node is no longer marked as Ghost at this level. 2017-01-13 Hristian Kirtchev * atree.adb (Allocate_Initialize_Node): A newly created node is no longer marked as Ghost at this level. (Mark_New_Ghost_Node): New routine. (New_Copy): Mark the copy as Ghost. (New_Entity): Mark the entity as Ghost. (New_Node): Mark the node as Ghost. * einfo.adb (Is_Checked_Ghost_Entity): This attribute can now apply to unanalyzed entities. (Is_Ignored_Ghost_Entity): This attribute can now apply to unanalyzed entities. (Set_Is_Checked_Ghost_Entity): This attribute now applies to all entities as well as unanalyzed entities. (Set_Is_Ignored_Ghost_Entity): This attribute now applies to all entities as well as unanalyzed entities. * expander.adb Add with and use clauses for Ghost. (Expand): Install and revert the Ghost region associated with the node being expanded. * exp_ch3.adb (Expand_Freeze_Array_Type): Remove all Ghost-related code. (Expand_Freeze_Class_Wide_Type): Remoe all Ghost-related code. (Expand_Freeze_Enumeration_Type): Remove all Ghost-related code. (Expand_Freeze_Record_Type): Remove all Ghost-related code. (Freeze_Type): Install and revert the Ghost region associated with the type being frozen. * exp_ch5.adb Remove with and use clauses for Ghost. (Expand_N_Assignment_Statement): Remove all Ghost-related code. * exp_ch6.adb Remove with and use clauses for Ghost. (Expand_N_Procedure_Call_Statement): Remove all Ghost-relatd code. (Expand_N_Subprogram_Body): Remove all Ghost-related code. * exp_ch7.adb (Build_Invariant_Procedure_Body): Install and revert the Ghost region of the working type. (Build_Invariant_Procedure_Declaration): Install and revert the Ghost region of the working type. (Expand_N_Package_Body): Remove all Ghost-related code. * exp_ch8.adb Remove with and use clauses for Ghost. (Expand_N_Exception_Renaming_Declaration): Remove all Ghost-related code. (Expand_N_Object_Renaming_Declaration): Remove all Ghost-related code. (Expand_N_Package_Renaming_Declaration): Remove all Ghost-related code. (Expand_N_Subprogram_Renaming_Declaration): Remove all Ghost-related code. * exp_ch13.adb Remove with and use clauses for Ghost. (Expand_N_Freeze_Entity): Remove all Ghost-related code. * exp_disp.adb (Make_DT): Install and revert the Ghost region of the tagged type. Move the generation of various entities within the Ghost region of the type. * exp_prag.adb Remove with and use clauses for Ghost. (Expand_Pragma_Check): Remove all Ghost-related code. (Expand_Pragma_Contract_Cases): Remove all Ghost-related code. (Expand_Pragma_Initial_Condition): Remove all Ghost-related code. (Expand_Pragma_Loop_Variant): Remove all Ghost-related code. * exp_util.adb (Build_DIC_Procedure_Body): Install and revert the Ghost region of the working types. (Build_DIC_Procedure_Declaration): Install and revert the Ghost region of the working type. (Make_Invariant_Call): Install and revert the Ghost region of the associated type. (Make_Predicate_Call): Reimplemented. Install and revert the Ghost region of the associated type. * freeze.adb (Freeze_Entity): Install and revert the Ghost region of the entity being frozen. (New_Freeze_Node): Removed. * ghost.adb Remove with and use clauses for Opt. (Check_Ghost_Completion): Update the parameter profile and all references to formal parameters. (Ghost_Entity): Update the comment on usage. (Install_Ghost_Mode): New routines. (Is_Ghost_Assignment): New routine. (Is_Ghost_Declaration): New routine. (Is_Ghost_Pragma): New routine. (Is_Ghost_Procedure_Call): New routine. (Is_Ghost_Renaming): Removed. (Is_OK_Declaration): Reimplemented. (Is_OK_Pragma): Reimplemented. (Is_OK_Statement): Reimplemented. (Is_Subject_To_Ghost): Update the comment on usage. (Mark_And_Set_Ghost_Assignment): New routine. (Mark_And_Set_Ghost_Body): New routine. (Mark_And_Set_Ghost_Completion): New routine. (Mark_And_Set_Ghost_Declaration): New routine. (Mark_And_Set_Ghost_Instantiation): New routine. (Mark_And_Set_Ghost_Procedure_Call): New routine. (Mark_Full_View_As_Ghost): Removed. (Mark_Ghost_Declaration_Or_Body): New routine. (Mark_Ghost_Pragma): New routine. (Mark_Ghost_Renaming): New routine. (Mark_Pragma_As_Ghost): Removed. (Mark_Renaming_As_Ghost): Removed. (Propagate_Ignored_Ghost_Code): Update the comment on usage. (Prune_Node): Freeze nodes no longer need special pruning, they are processed by the general ignored Ghost code mechanism. (Restore_Ghost_Mode): New routine. (Set_Ghost_Mode): Reimplemented. (Set_Ghost_Mode_From_Entity): Removed. * ghost.ads Add with and use clauses for Ghost. (Check_Ghost_Completion): Update the parameter profile along with the comment on usage. (Install_Ghost_Mode): New routine. (Is_Ghost_Assignment): New routine. (Is_Ghost_Declaration): New routine. (Is_Ghost_Pragma): New routine. (Is_Ghost_Procedure_Call): New routine. (Mark_And_Set_Ghost_Assignment): New routine. (Mark_And_Set_Ghost_Body): New routine. (Mark_And_Set_Ghost_Completion): New routine. (Mark_And_Set_Ghost_Declaration): New routine. (Mark_And_Set_Ghost_Instantiation): New routine. (Mark_And_Set_Ghost_Procedure_Call): New routine. (Mark_Full_View_As_Ghost): Removed. (Mark_Ghost_Pragma): New routine. (Mark_Ghost_Renaming): New routine. (Mark_Pragma_As_Ghost): Removed. (Mark_Renaming_As_Ghost): Removed. (Restore_Ghost_Mode): New routine. (Set_Ghost_Mode): Redefined. (Set_Ghost_Mode_From_Entity): Removed. * sem.adb (Analyze): Install and revert the Ghost region of the node being analyzed. (Do_Analyze): Change the way a clean Ghost region is installed and reverted. * sem_ch3.adb (Analyze_Full_Type_Declaration): Remove all Ghost-related code. (Analyze_Incomplete_Type_Decl): Remove all Ghost-related code. (Analyze_Number_Declaration): Remove all Ghost-related code. (Analyze_Object_Declaration): Install and revert the Ghost region of a deferred object declaration's completion. (Array_Type_Declaration): Remove all Ghost-related code. (Build_Derived_Type): Update the comment on the propagation of Ghost attributes from a parent to a derived type. (Derive_Subprogram): Remove all Ghost-related code. (Make_Class_Wide_Type): Remove all Ghost-related code. (Make_Implicit_Base): Remove all Ghost-related code. (Process_Full_View): Install and revert the Ghost region of the partial view. There is no longer need to check the Ghost completion here. * sem_ch5.adb (Analyze_Assignment): Install and revert the Ghost region of the left hand side. * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Remove all Ghost-related code. (Analyze_Expression_Function): Remove all Ghost-related code. (Analyze_Generic_Subprogram_Body): Remove all Ghost-related code. (Analyze_Procedure_Call): Install and revert the Ghost region of the procedure being called. (Analyze_Subprogram_Body_Helper): Install and revert the Ghost region of the spec or body. (Analyze_Subprogram_Declaration): Remove all Ghost-related code. (Build_Subprogram_Declaration): Remove all Ghost-related code. (Find_Corresponding_Spec): Remove all Ghost-related code. (Process_Formals): Remove all Ghost-related code. * sem_ch7.adb (Analyze_Package_Body_Helper): Install and revert the Ghost region of the spec. (Analyze_Package_Declaration): Remove all Ghost-related code. * sem_ch8.adb (Analyze_Exception_Renaming): Mark a renaming as Ghost when it aliases a Ghost entity. (Analyze_Generic_Renaming): Mark a renaming as Ghost when it aliases a Ghost entity. (Analyze_Object_Renaming): Mark a renaming as Ghost when it aliases a Ghost entity. (Analyze_Package_Renaming): Mark a renaming as Ghost when it aliases a Ghost entity. (Analyze_Subprogram_Renaming): Mark a renaming as Ghost when it aliases a Ghost entity. * sem_ch11.adb Remove with and use clauses for Ghost. (Analyze_Exception_Declaration): Remove all Ghost-related code. * sem_ch12.adb (Analyze_Generic_Package_Declaration): Remove all Ghost-related code. (Analyze_Generic_Subprogram_Declaration): Remove all Ghost-related code. (Analyze_Package_Instantiation): Install and revert the Ghost region of the package instantiation. (Analyze_Subprogram_Instantiation): Install and revert the Ghost region of the subprogram instantiation. (Instantiate_Package_Body): Code clean up. Install and revert the Ghost region of the package body. (Instantiate_Subprogram_Body): Code clean up. Install and revert the Ghost region of the subprogram body. * sem_ch13.adb (Build_Predicate_Functions): Install and revert the Ghost region of the related type. (Build_Predicate_Function_Declaration): Code clean up. Install and rever the Ghost region of the related type. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Install and revert the Ghost region of the pragma. (Analyze_Initial_Condition_In_Decl_Part): Install and revert the Ghost region of the pragma. (Analyze_Pragma): Install and revert the Ghost region of various pragmas. Mark a pragma as Ghost when it is related to a Ghost entity or encloses a Ghost entity. (Analyze_Pre_Post_Condition): Install and revert the Ghost region of the pragma. (Analyze_Pre_Post_Condition_In_Decl_Part): Install and revert the Ghost region of the pragma. * sem_res.adb (Resolve): Remove all Ghost-related code. * sem_util.adb (Is_Declaration): Reimplemented. (Is_Declaration_Other_Than_Renaming): New routine. * sem_util.ads (Is_Declaration_Other_Than_Renaming): New routine. * sinfo.adb (Is_Checked_Ghost_Pragma): New routine. (Is_Ghost_Pragma): Removed. (Is_Ignored_Ghost_Pragma): New routine. (Set_Is_Checked_Ghost_Pragma): New routine. (Set_Is_Ghost_Pragma): Removed. (Set_Is_Ignored_Ghost_Pragma): New routine. * sinfo.ads: Update the documentation on Ghost mode and Ghost regions. New attributes Is_Checked_Ghost_Pragma and Is_Ignored_Ghost_Pragma along with usages in nodes. Remove attribute Is_Ghost_Pragma along with usages in nodes. (Is_Checked_Ghost_Pragma): New routine along with pragma Inline. (Is_Ghost_Pragma): Removed along with pragma Inline. (Is_Ignored_Ghost_Pragma): New routine along with pragma Inline. (Set_Is_Checked_Ghost_Pragma): New routine along with pragma Inline. (Set_Is_Ghost_Pragma): Removed along with pragma Inline. (Set_Is_Ignored_Ghost_Pragma): New routine along with pragma Inline. From-SVN: r244395 --- gcc/ada/ChangeLog | 213 +++++++++++ gcc/ada/atree.adb | 54 ++- gcc/ada/einfo.adb | 40 +-- gcc/ada/exp_ch13.adb | 17 +- gcc/ada/exp_ch3.adb | 41 +-- gcc/ada/exp_ch5.adb | 24 +- gcc/ada/exp_ch6.adb | 24 +- gcc/ada/exp_ch7.adb | 61 ++-- gcc/ada/exp_ch8.adb | 48 +-- gcc/ada/exp_disp.adb | 111 +++--- gcc/ada/exp_prag.adb | 55 +-- gcc/ada/exp_util.adb | 83 ++--- gcc/ada/expander.adb | 17 +- gcc/ada/freeze.adb | 113 ++---- gcc/ada/ghost.adb | 835 ++++++++++++++++++++++++++++++------------- gcc/ada/ghost.ads | 196 +++++++--- gcc/ada/sem.adb | 14 +- gcc/ada/sem_ch11.adb | 8 - gcc/ada/sem_ch12.adb | 158 ++++---- gcc/ada/sem_ch13.adb | 67 ++-- gcc/ada/sem_ch3.adb | 142 ++------ gcc/ada/sem_ch5.adb | 54 ++- gcc/ada/sem_ch6.adb | 149 ++------ gcc/ada/sem_ch7.adb | 37 +- gcc/ada/sem_ch8.adb | 142 +++++--- gcc/ada/sem_prag.adb | 264 +++++++------- gcc/ada/sem_res.adb | 28 +- gcc/ada/sem_util.adb | 21 +- gcc/ada/sem_util.ads | 3 + gcc/ada/sinfo.adb | 44 ++- gcc/ada/sinfo.ads | 121 +++++-- 31 files changed, 1752 insertions(+), 1432 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9af0589b60c..9c04b307d1e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,216 @@ +2017-01-13 Hristian Kirtchev + + * atree.adb (Allocate_Initialize_Node): A newly created node is + no longer marked as Ghost at this level. + (Mark_New_Ghost_Node): New routine. + (New_Copy): Mark the copy as Ghost. + (New_Entity): Mark the entity as Ghost. + (New_Node): Mark the node as Ghost. + * einfo.adb (Is_Checked_Ghost_Entity): This attribute can now + apply to unanalyzed entities. + (Is_Ignored_Ghost_Entity): This attribute can now apply to unanalyzed + entities. + (Set_Is_Checked_Ghost_Entity): This attribute now + applies to all entities as well as unanalyzed entities. + (Set_Is_Ignored_Ghost_Entity): This attribute now applies to + all entities as well as unanalyzed entities. + * expander.adb Add with and use clauses for Ghost. + (Expand): Install and revert the Ghost region associated with the node + being expanded. + * exp_ch3.adb (Expand_Freeze_Array_Type): Remove all Ghost-related code. + (Expand_Freeze_Class_Wide_Type): Remoe all Ghost-related code. + (Expand_Freeze_Enumeration_Type): Remove all Ghost-related code. + (Expand_Freeze_Record_Type): Remove all Ghost-related code. + (Freeze_Type): Install and revert the Ghost region associated + with the type being frozen. + * exp_ch5.adb Remove with and use clauses for Ghost. + (Expand_N_Assignment_Statement): Remove all Ghost-related code. + * exp_ch6.adb Remove with and use clauses for Ghost. + (Expand_N_Procedure_Call_Statement): Remove all Ghost-relatd code. + (Expand_N_Subprogram_Body): Remove all Ghost-related code. + * exp_ch7.adb (Build_Invariant_Procedure_Body): Install and revert the + Ghost region of the working type. + (Build_Invariant_Procedure_Declaration): Install and revert + the Ghost region of the working type. + (Expand_N_Package_Body): Remove all Ghost-related code. + * exp_ch8.adb Remove with and use clauses for Ghost. + (Expand_N_Exception_Renaming_Declaration): Remove all Ghost-related + code. + (Expand_N_Object_Renaming_Declaration): Remove all Ghost-related code. + (Expand_N_Package_Renaming_Declaration): Remove all Ghost-related code. + (Expand_N_Subprogram_Renaming_Declaration): Remove all Ghost-related + code. + * exp_ch13.adb Remove with and use clauses for Ghost. + (Expand_N_Freeze_Entity): Remove all Ghost-related code. + * exp_disp.adb (Make_DT): Install and revert the Ghost region of + the tagged type. Move the generation of various entities within + the Ghost region of the type. + * exp_prag.adb Remove with and use clauses for Ghost. + (Expand_Pragma_Check): Remove all Ghost-related code. + (Expand_Pragma_Contract_Cases): Remove all Ghost-related code. + (Expand_Pragma_Initial_Condition): Remove all Ghost-related code. + (Expand_Pragma_Loop_Variant): Remove all Ghost-related code. + * exp_util.adb (Build_DIC_Procedure_Body): Install + and revert the Ghost region of the working types. + (Build_DIC_Procedure_Declaration): Install and revert the + Ghost region of the working type. + (Make_Invariant_Call): Install and revert the Ghost region of the + associated type. + (Make_Predicate_Call): Reimplemented. Install and revert the + Ghost region of the associated type. + * freeze.adb (Freeze_Entity): Install and revert the Ghost region + of the entity being frozen. + (New_Freeze_Node): Removed. + * ghost.adb Remove with and use clauses for Opt. + (Check_Ghost_Completion): Update the parameter profile + and all references to formal parameters. + (Ghost_Entity): Update the comment on usage. + (Install_Ghost_Mode): New routines. + (Is_Ghost_Assignment): New routine. + (Is_Ghost_Declaration): New routine. + (Is_Ghost_Pragma): New routine. + (Is_Ghost_Procedure_Call): New routine. + (Is_Ghost_Renaming): Removed. + (Is_OK_Declaration): Reimplemented. + (Is_OK_Pragma): Reimplemented. + (Is_OK_Statement): Reimplemented. + (Is_Subject_To_Ghost): Update the comment on usage. + (Mark_And_Set_Ghost_Assignment): New routine. + (Mark_And_Set_Ghost_Body): New routine. + (Mark_And_Set_Ghost_Completion): New routine. + (Mark_And_Set_Ghost_Declaration): New routine. + (Mark_And_Set_Ghost_Instantiation): New routine. + (Mark_And_Set_Ghost_Procedure_Call): New routine. + (Mark_Full_View_As_Ghost): Removed. + (Mark_Ghost_Declaration_Or_Body): New routine. + (Mark_Ghost_Pragma): New routine. + (Mark_Ghost_Renaming): New routine. + (Mark_Pragma_As_Ghost): Removed. + (Mark_Renaming_As_Ghost): Removed. + (Propagate_Ignored_Ghost_Code): Update the comment on usage. + (Prune_Node): Freeze nodes no longer need special pruning, they + are processed by the general ignored Ghost code mechanism. + (Restore_Ghost_Mode): New routine. + (Set_Ghost_Mode): Reimplemented. + (Set_Ghost_Mode_From_Entity): Removed. + * ghost.ads Add with and use clauses for Ghost. + (Check_Ghost_Completion): Update the parameter profile + along with the comment on usage. + (Install_Ghost_Mode): New routine. + (Is_Ghost_Assignment): New routine. + (Is_Ghost_Declaration): New routine. + (Is_Ghost_Pragma): New routine. + (Is_Ghost_Procedure_Call): New routine. + (Mark_And_Set_Ghost_Assignment): New routine. + (Mark_And_Set_Ghost_Body): New routine. + (Mark_And_Set_Ghost_Completion): New routine. + (Mark_And_Set_Ghost_Declaration): New routine. + (Mark_And_Set_Ghost_Instantiation): New routine. + (Mark_And_Set_Ghost_Procedure_Call): New routine. + (Mark_Full_View_As_Ghost): Removed. + (Mark_Ghost_Pragma): New routine. + (Mark_Ghost_Renaming): New routine. + (Mark_Pragma_As_Ghost): Removed. + (Mark_Renaming_As_Ghost): Removed. + (Restore_Ghost_Mode): New routine. + (Set_Ghost_Mode): Redefined. + (Set_Ghost_Mode_From_Entity): Removed. + * sem.adb (Analyze): Install and revert the Ghost region of the + node being analyzed. + (Do_Analyze): Change the way a clean Ghost + region is installed and reverted. + * sem_ch3.adb (Analyze_Full_Type_Declaration): Remove + all Ghost-related code. + (Analyze_Incomplete_Type_Decl): Remove all Ghost-related code. + (Analyze_Number_Declaration): Remove all Ghost-related code. + (Analyze_Object_Declaration): Install and revert the Ghost region of + a deferred object declaration's completion. + (Array_Type_Declaration): Remove all Ghost-related code. + (Build_Derived_Type): Update the comment on + the propagation of Ghost attributes from a parent to a derived type. + (Derive_Subprogram): Remove all Ghost-related code. + (Make_Class_Wide_Type): Remove all Ghost-related code. + (Make_Implicit_Base): Remove all Ghost-related code. + (Process_Full_View): Install and revert the Ghost region of + the partial view. There is no longer need to check the Ghost + completion here. + * sem_ch5.adb (Analyze_Assignment): Install and revert the Ghost + region of the left hand side. + * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Remove + all Ghost-related code. + (Analyze_Expression_Function): Remove all Ghost-related code. + (Analyze_Generic_Subprogram_Body): Remove all Ghost-related code. + (Analyze_Procedure_Call): Install and revert the Ghost region of + the procedure being called. + (Analyze_Subprogram_Body_Helper): Install and revert the Ghost + region of the spec or body. + (Analyze_Subprogram_Declaration): Remove all Ghost-related code. + (Build_Subprogram_Declaration): Remove all Ghost-related code. + (Find_Corresponding_Spec): Remove all Ghost-related code. + (Process_Formals): Remove all Ghost-related code. + * sem_ch7.adb (Analyze_Package_Body_Helper): Install and revert + the Ghost region of the spec. + (Analyze_Package_Declaration): Remove all Ghost-related code. + * sem_ch8.adb (Analyze_Exception_Renaming): Mark a renaming as + Ghost when it aliases a Ghost entity. + (Analyze_Generic_Renaming): Mark a renaming as Ghost when it aliases + a Ghost entity. + (Analyze_Object_Renaming): Mark a renaming as Ghost when + it aliases a Ghost entity. + (Analyze_Package_Renaming): Mark a renaming as Ghost when it aliases + a Ghost entity. + (Analyze_Subprogram_Renaming): Mark a renaming as Ghost when it + aliases a Ghost entity. + * sem_ch11.adb Remove with and use clauses for Ghost. + (Analyze_Exception_Declaration): Remove all Ghost-related code. + * sem_ch12.adb (Analyze_Generic_Package_Declaration): Remove all + Ghost-related code. + (Analyze_Generic_Subprogram_Declaration): Remove all Ghost-related + code. + (Analyze_Package_Instantiation): Install and revert the Ghost region + of the package instantiation. + (Analyze_Subprogram_Instantiation): Install + and revert the Ghost region of the subprogram instantiation. + (Instantiate_Package_Body): Code clean up. Install and revert the + Ghost region of the package body. + (Instantiate_Subprogram_Body): Code clean up. Install and revert the + Ghost region of the subprogram body. + * sem_ch13.adb (Build_Predicate_Functions): Install + and revert the Ghost region of the related type. + (Build_Predicate_Function_Declaration): Code clean up. Install + and rever the Ghost region of the related type. + * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): + Install and revert the Ghost region of the pragma. + (Analyze_Initial_Condition_In_Decl_Part): Install and revert the + Ghost region of the pragma. + (Analyze_Pragma): Install and revert the Ghost region of various + pragmas. Mark a pragma as Ghost when it is related to a Ghost entity + or encloses a Ghost entity. + (Analyze_Pre_Post_Condition): Install and revert the Ghost + region of the pragma. + (Analyze_Pre_Post_Condition_In_Decl_Part): Install and revert the + Ghost region of the pragma. + * sem_res.adb (Resolve): Remove all Ghost-related code. + * sem_util.adb (Is_Declaration): Reimplemented. + (Is_Declaration_Other_Than_Renaming): New routine. + * sem_util.ads (Is_Declaration_Other_Than_Renaming): New routine. + * sinfo.adb (Is_Checked_Ghost_Pragma): New routine. + (Is_Ghost_Pragma): Removed. + (Is_Ignored_Ghost_Pragma): New routine. + (Set_Is_Checked_Ghost_Pragma): New routine. + (Set_Is_Ghost_Pragma): Removed. + (Set_Is_Ignored_Ghost_Pragma): New routine. + * sinfo.ads: Update the documentation on Ghost mode and + Ghost regions. New attributes Is_Checked_Ghost_Pragma + and Is_Ignored_Ghost_Pragma along with usages in nodes. + Remove attribute Is_Ghost_Pragma along with usages in nodes. + (Is_Checked_Ghost_Pragma): New routine along with pragma Inline. + (Is_Ghost_Pragma): Removed along with pragma Inline. + (Is_Ignored_Ghost_Pragma): New routine along with pragma Inline. + (Set_Is_Checked_Ghost_Pragma): New routine along with pragma Inline. + (Set_Is_Ghost_Pragma): Removed along with pragma Inline. + (Set_Is_Ignored_Ghost_Pragma): New routine along with pragma Inline. + 2017-01-12 Tristan Gingold * s-mmap.ads, s-mmap.adb, s-mmosin-unix.ads, s-mmosin-unix.adb, diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 44188cfbba9..1444fcb6dfe 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -549,16 +549,20 @@ package body Atree is -- Local Subprograms -- ----------------------- - procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id); - -- Fixup parent pointers for the syntactic children of Fix_Node after - -- a copy, setting them to Fix_Node when they pointed to Ref_Node. - function Allocate_Initialize_Node (Src : Node_Id; With_Extension : Boolean) return Node_Id; -- Allocate a new node or node extension. If Src is not empty, the -- information for the newly-allocated node is copied from it. + procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id); + -- Fixup parent pointers for the syntactic children of Fix_Node after a + -- copy, setting them to Fix_Node when they pointed to Ref_Node. + + procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id); + -- Mark arbitrary node or entity N as Ghost when it is created within a + -- Ghost region. + ------------------------------ -- Allocate_Initialize_Node -- ------------------------------ @@ -594,13 +598,6 @@ package body Atree is Node_Count := Node_Count + 1; end if; - -- Mark the node as ignored Ghost if it is created in an ignored Ghost - -- region. - - if Ghost_Mode = Ignore then - Set_Is_Ignored_Ghost_Node (New_Id); - end if; - -- Clear Check_Actuals to False Set_Check_Actuals (New_Id, False); @@ -1432,7 +1429,6 @@ package body Atree is ----------------- procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id) is - procedure Fix_Parent (Field : Union_Id); -- Fixup one parent pointer. Field is checked to see if it points to -- a node, list, or element list that has a parent that points to @@ -1590,6 +1586,28 @@ package body Atree is Orig_Nodes.Release; end Lock; + ------------------------- + -- Mark_New_Ghost_Node -- + ------------------------- + + procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id) is + begin + -- The Ghost node is created within a Ghost region + + if Ghost_Mode = Check then + if Nkind (N) in N_Entity then + Set_Is_Checked_Ghost_Entity (N); + end if; + + elsif Ghost_Mode = Ignore then + if Nkind (N) in N_Entity then + Set_Is_Ignored_Ghost_Entity (N); + end if; + + Set_Is_Ignored_Ghost_Node (N); + end if; + end Mark_New_Ghost_Node; + ---------------------------- -- Mark_Rewrite_Insertion -- ---------------------------- @@ -1630,6 +1648,10 @@ package body Atree is -- aspects if this is required for the particular situation. Set_Has_Aspects (New_Id, False); + + -- Mark the copy as Ghost depending on the current Ghost region + + Mark_New_Ghost_Node (New_Id); end if; return New_Id; @@ -1662,6 +1684,10 @@ package body Atree is Nodes.Table (Ent).Sloc := New_Sloc; pragma Debug (New_Node_Debugging_Output (Ent)); + -- Mark the new entity as Ghost depending on the current Ghost region + + Mark_New_Ghost_Node (Ent); + return Ent; end New_Entity; @@ -1690,6 +1716,10 @@ package body Atree is Current_Error_Node := Nod; end if; + -- Mark the new node as Ghost depending on the current Ghost region + + Mark_New_Ghost_Node (Nod); + return Nod; end New_Node; diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 213bfa8ecb1..c2146756843 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -2093,7 +2093,10 @@ package body Einfo is function Is_Checked_Ghost_Entity (Id : E) return B is begin - pragma Assert (Nkind (Id) in N_Entity); + -- Allow this attribute to appear on non-analyzed entities + + pragma Assert (Nkind (Id) in N_Entity + or else Ekind (Id) = E_Void); return Flag277 (Id); end Is_Checked_Ghost_Entity; @@ -2280,7 +2283,10 @@ package body Einfo is function Is_Ignored_Ghost_Entity (Id : E) return B is begin - pragma Assert (Nkind (Id) in N_Entity); + -- Allow this attribute to appear on non-analyzed entities + + pragma Assert (Nkind (Id) in N_Entity + or else Ekind (Id) = E_Void); return Flag278 (Id); end Is_Ignored_Ghost_Entity; @@ -5161,20 +5167,9 @@ package body Einfo is procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is begin - pragma Assert (Is_Formal (Id) - or else Is_Object (Id) - or else Is_Package_Or_Generic_Package (Id) - or else Is_Subprogram_Or_Generic_Subprogram (Id) - or else Is_Type (Id) - or else Ekind (Id) = E_Abstract_State - or else Ekind (Id) = E_Component - or else Ekind (Id) = E_Discriminant - or else Ekind (Id) = E_Exception - or else Ekind (Id) = E_Package_Body - or else Ekind (Id) = E_Subprogram_Body - - -- Allow this attribute to appear on non-analyzed entities + -- Allow this attribute to appear on non-analyzed entities + pragma Assert (Nkind (Id) in N_Entity or else Ekind (Id) = E_Void); Set_Flag277 (Id, V); end Set_Is_Checked_Ghost_Entity; @@ -5377,20 +5372,9 @@ package body Einfo is procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is begin - pragma Assert (Is_Formal (Id) - or else Is_Object (Id) - or else Is_Package_Or_Generic_Package (Id) - or else Is_Subprogram_Or_Generic_Subprogram (Id) - or else Is_Type (Id) - or else Ekind (Id) = E_Abstract_State - or else Ekind (Id) = E_Component - or else Ekind (Id) = E_Discriminant - or else Ekind (Id) = E_Exception - or else Ekind (Id) = E_Package_Body - or else Ekind (Id) = E_Subprogram_Body - - -- Allow this attribute to appear on non-analyzed entities + -- Allow this attribute to appear on non-analyzed entities + pragma Assert (Nkind (Id) in N_Entity or else Ekind (Id) = E_Void); Set_Flag278 (Id, V); end Set_Is_Ignored_Ghost_Entity; diff --git a/gcc/ada/exp_ch13.adb b/gcc/ada/exp_ch13.adb index dd004a0991f..1c170e210b4 100644 --- a/gcc/ada/exp_ch13.adb +++ b/gcc/ada/exp_ch13.adb @@ -32,7 +32,6 @@ with Exp_Imgv; use Exp_Imgv; with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Freeze; use Freeze; -with Ghost; use Ghost; with Namet; use Namet; with Nlists; use Nlists; with Nmake; use Nmake; @@ -345,10 +344,8 @@ package body Exp_Ch13 is Insert_Action (N, Make_Object_Declaration (Loc, Defining_Identifier => Temp_Id, - Object_Definition => - New_Occurrence_Of (Expr_Typ, Loc), - Expression => - Relocate_Node (Expr))); + Object_Definition => New_Occurrence_Of (Expr_Typ, Loc), + Expression => Relocate_Node (Expr))); New_Expr := New_Occurrence_Of (Temp_Id, Loc); Set_Etype (New_Expr, Expr_Typ); @@ -371,8 +368,6 @@ package body Exp_Ch13 is procedure Expand_N_Freeze_Entity (N : Node_Id) is E : constant Entity_Id := Entity (N); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Decl : Node_Id; Delete : Boolean := False; E_Scope : Entity_Id; @@ -380,10 +375,6 @@ package body Exp_Ch13 is In_Outer_Scope : Boolean; begin - -- Ensure that all freezing activities are properly flagged as Ghost - - Set_Ghost_Mode_From_Entity (E); - -- If there are delayed aspect specifications, we insert them just -- before the freeze node. They are already analyzed so we don't need -- to reanalyze them (they were analyzed before the type was frozen), @@ -451,14 +442,12 @@ package body Exp_Ch13 is -- statement, insert them back into the tree now. Explode_Initialization_Compound_Statement (E); - Ghost_Mode := Save_Ghost_Mode; return; -- Only other items requiring any front end action are types and -- subprograms. elsif not Is_Type (E) and then not Is_Subprogram (E) then - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -470,7 +459,6 @@ package body Exp_Ch13 is if No (E_Scope) then Check_Error_Detected; - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -688,7 +676,6 @@ package body Exp_Ch13 is -- whether we are inside a (possibly nested) call to this procedure. Inside_Freezing_Actions := Inside_Freezing_Actions - 1; - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Freeze_Entity; ------------------------------------------- diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index c1039c5b53f..93ae83fd233 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -4361,13 +4361,7 @@ package body Exp_Ch3 is Base : constant Entity_Id := Base_Type (Typ); Comp_Typ : constant Entity_Id := Component_Type (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin - -- Ensure that all freezing activities are properly flagged as Ghost - - Set_Ghost_Mode_From_Entity (Typ); - if not Is_Bit_Packed_Array (Typ) then -- If the component contains tasks, so does the array type. This may @@ -4435,8 +4429,6 @@ package body Exp_Ch3 is then Build_Array_Init_Proc (Base, N); end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_Freeze_Array_Type; ----------------------------------- @@ -4477,8 +4469,6 @@ package body Exp_Ch3 is Typ : constant Entity_Id := Entity (N); Root : constant Entity_Id := Root_Type (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - -- Start of processing for Expand_Freeze_Class_Wide_Type begin @@ -4511,15 +4501,10 @@ package body Exp_Ch3 is return; end if; - -- Ensure that all freezing activities are properly flagged as Ghost - - Set_Ghost_Mode_From_Entity (Typ); - -- Create the body of TSS primitive Finalize_Address. This automatically -- sets the TSS entry for the class-wide type. Make_Finalize_Address_Body (Typ); - Ghost_Mode := Save_Ghost_Mode; end Expand_Freeze_Class_Wide_Type; ------------------------------------ @@ -4530,8 +4515,6 @@ package body Exp_Ch3 is Typ : constant Entity_Id := Entity (N); Loc : constant Source_Ptr := Sloc (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Arr : Entity_Id; Ent : Entity_Id; Fent : Entity_Id; @@ -4546,10 +4529,6 @@ package body Exp_Ch3 is pragma Warnings (Off, Func); begin - -- Ensure that all freezing activities are properly flagged as Ghost - - Set_Ghost_Mode_From_Entity (Typ); - -- Various optimizations possible if given representation is contiguous Is_Contiguous := True; @@ -4832,11 +4811,8 @@ package body Exp_Ch3 is Set_Debug_Info_Off (Fent); end if; - Ghost_Mode := Save_Ghost_Mode; - exception when RE_Not_Available => - Ghost_Mode := Save_Ghost_Mode; return; end Expand_Freeze_Enumeration_Type; @@ -4848,8 +4824,6 @@ package body Exp_Ch3 is Typ : constant Node_Id := Entity (N); Typ_Decl : constant Node_Id := Parent (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Comp : Entity_Id; Comp_Typ : Entity_Id; Predef_List : List_Id; @@ -4867,10 +4841,6 @@ package body Exp_Ch3 is -- Start of processing for Expand_Freeze_Record_Type begin - -- Ensure that all freezing activities are properly flagged as Ghost - - Set_Ghost_Mode_From_Entity (Typ); - -- Build discriminant checking functions if not a derived type (for -- derived types that are not tagged types, always use the discriminant -- checking functions of the parent type). However, for untagged types @@ -5291,8 +5261,6 @@ package body Exp_Ch3 is end loop; end; end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_Freeze_Record_Type; ------------------------------------ @@ -7135,10 +7103,9 @@ package body Exp_Ch3 is -- Local variables Def_Id : constant Entity_Id := Entity (N); + Mode : Ghost_Mode_Type; Result : Boolean := False; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - -- Start of processing for Freeze_Type begin @@ -7146,7 +7113,7 @@ package body Exp_Ch3 is -- now to ensure that any nodes generated during freezing are properly -- marked as Ghost. - Set_Ghost_Mode (N, Def_Id); + Set_Ghost_Mode (Def_Id, Mode); -- Process any remote access-to-class-wide types designating the type -- being frozen. @@ -7474,12 +7441,12 @@ package body Exp_Ch3 is Build_Invariant_Procedure_Body (Def_Id); end if; - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Mode); return Result; exception when RE_Not_Available => - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Mode); return False; end Freeze_Type; diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb index e6f076eee1d..ffe4b5cfbdc 100644 --- a/gcc/ada/exp_ch5.adb +++ b/gcc/ada/exp_ch5.adb @@ -38,7 +38,6 @@ 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; @@ -1613,15 +1612,7 @@ package body Exp_Ch5 is Typ : constant Entity_Id := Underlying_Type (Etype (Lhs)); Exp : Node_Id; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin - -- The assignment statement is Ghost when the left hand side is Ghost. - -- Set the mode now to ensure that any nodes generated during expansion - -- are properly marked as 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 @@ -1631,7 +1622,6 @@ package body Exp_Ch5 is if Componentwise_Assignment (N) then Expand_Assign_Record (N); - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -1723,7 +1713,6 @@ package body Exp_Ch5 is Rewrite (N, Call); Analyze (N); - Ghost_Mode := Save_Ghost_Mode; return; end if; end; @@ -1812,8 +1801,8 @@ package body Exp_Ch5 is loop Set_Analyzed (Exp, False); - if Nkind_In - (Exp, N_Selected_Component, N_Indexed_Component) + if Nkind_In (Exp, N_Indexed_Component, + N_Selected_Component) then Exp := Prefix (Exp); else @@ -1874,7 +1863,6 @@ package body Exp_Ch5 is Rewrite (N, Make_Null_Statement (Loc)); Analyze (N); - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -2099,7 +2087,6 @@ package body Exp_Ch5 is if not Crep then Expand_Bit_Packed_Element_Set (N); - Ghost_Mode := Save_Ghost_Mode; return; -- Change of representation case @@ -2198,7 +2185,6 @@ package body Exp_Ch5 is -- expansion, since they would be missed in -gnatc mode ??? Error_Msg_N ("assignment not available on limited type", N); - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -2401,7 +2387,6 @@ package body Exp_Ch5 is -- it with all checks suppressed. Analyze (N, Suppress => All_Checks); - Ghost_Mode := Save_Ghost_Mode; return; end Tagged_Case; @@ -2419,7 +2404,6 @@ package body Exp_Ch5 is end loop; Expand_Assign_Array (N, Actual_Rhs); - Ghost_Mode := Save_Ghost_Mode; return; end; @@ -2427,7 +2411,6 @@ package body Exp_Ch5 is elsif Is_Record_Type (Typ) then Expand_Assign_Record (N); - Ghost_Mode := Save_Ghost_Mode; return; -- Scalar types. This is where we perform the processing related to the @@ -2540,11 +2523,8 @@ package body Exp_Ch5 is end if; end if; - Ghost_Mode := Save_Ghost_Mode; - exception when RE_Not_Available => - Ghost_Mode := Save_Ghost_Mode; return; end Expand_N_Assignment_Statement; diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 7b7e1351b9f..77b8ad2679d 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -44,7 +44,6 @@ with Exp_Pakd; use Exp_Pakd; with Exp_Tss; use Exp_Tss; 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; @@ -5188,17 +5187,8 @@ package body Exp_Ch6 is --------------------------------------- procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin - -- The procedure call is Ghost when the name is Ghost. Set the mode now - -- to ensure that any nodes generated during expansion are properly set - -- as Ghost. - - Set_Ghost_Mode (N); - Expand_Call (N); - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Procedure_Call_Statement; -------------------------------------- @@ -5358,8 +5348,6 @@ package body Exp_Ch6 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Except_H : Node_Id; L : List_Id; Spec_Id : Entity_Id; @@ -5390,13 +5378,6 @@ package body Exp_Ch6 is end if; end if; - -- The subprogram body is Ghost when it is stand alone and subject to - -- pragma Ghost or the corresponding spec is Ghost. To accomodate both - -- cases, set the mode now to ensure that any nodes generated during - -- expansion are marked as Ghost. - - Set_Ghost_Mode (N, Spec_Id); - -- 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. @@ -5518,7 +5499,6 @@ package body Exp_Ch6 is Make_Handled_Sequence_Of_Statements (Loc, Statements => New_List (Make_Null_Statement (Loc)))); - Ghost_Mode := Save_Ghost_Mode; return; end if; end if; @@ -5543,7 +5523,7 @@ package body Exp_Ch6 is begin if not Acts_As_Spec (N) and then Nkind (Parent (Parent (Spec_Id))) /= - N_Subprogram_Body_Stub + N_Subprogram_Body_Stub then null; @@ -5631,8 +5611,6 @@ package body Exp_Ch6 is -- Set to encode entity names in package body before gigi is called Qualify_Entity_Names (N); - - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Subprogram_Body; ----------------------------------- diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 9c5cb468c2c..6b994aabd97 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -4353,9 +4353,8 @@ package body Exp_Ch7 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Dummy : Entity_Id; + Mode : Ghost_Mode_Type; Priv_Item : Node_Id; Proc_Body : Node_Id; Proc_Body_Id : Entity_Id; @@ -4406,6 +4405,11 @@ package body Exp_Ch7 is Work_Typ := Corresponding_Concurrent_Type (Work_Typ); end if; + -- The working type may be subject to pragma Ghost. Set the mode now to + -- ensure that the invariant procedure is properly marked as Ghost. + + Set_Ghost_Mode (Work_Typ, Mode); + -- The type must either have invariants of its own, inherit class-wide -- invariants from parent types or interfaces, or be an array or record -- type whose components have invariants. @@ -4416,7 +4420,7 @@ package body Exp_Ch7 is -- inherited by implementing types. if Is_Interface (Work_Typ) then - return; + goto Leave; end if; -- Obtain both views of the type @@ -4445,7 +4449,7 @@ package body Exp_Ch7 is -- Nothing to do because the processing of the underlying full -- view already checked the invariants of the partial view. - return; + goto Leave; end if; -- Create a declaration for the "partial" invariant procedure if it @@ -4482,14 +4486,9 @@ package body Exp_Ch7 is -- Nothing to do if the invariant procedure already has a body if Present (Corresponding_Body (Proc_Decl)) then - return; + goto Leave; end if; - -- The working type may be subject to pragma Ghost. Set the mode now to - -- ensure that the invariant procedure is properly marked as Ghost. - - Set_Ghost_Mode_From_Entity (Work_Typ); - -- Emulate the environment of the invariant procedure by installing -- its scope and formal parameters. Note that this is not needed, but -- having the scope of the invariant procedure installed helps with @@ -4667,7 +4666,8 @@ package body Exp_Ch7 is Append_Freeze_Action (Work_Typ, Proc_Body); end if; - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); end Build_Invariant_Procedure_Body; ------------------------------------------- @@ -4680,8 +4680,7 @@ package body Exp_Ch7 is is Loc : constant Source_Ptr := Sloc (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - + Mode : Ghost_Mode_Type; Proc_Decl : Node_Id; Proc_Id : Entity_Id; Proc_Nam : Name_Id; @@ -4725,6 +4724,11 @@ package body Exp_Ch7 is Work_Typ := Corresponding_Concurrent_Type (Work_Typ); end if; + -- The working type may be subject to pragma Ghost. Set the mode now to + -- ensure that the invariant procedure is properly marked as Ghost. + + Set_Ghost_Mode (Work_Typ, Mode); + -- The type must either have invariants of its own, inherit class-wide -- invariants from parent or interface types, or be an array or record -- type whose components have invariants. @@ -4735,26 +4739,21 @@ package body Exp_Ch7 is -- inherited by implementing types. if Is_Interface (Work_Typ) then - return; + goto Leave; -- Nothing to do if the type already has a "partial" invariant procedure elsif Partial_Invariant then if Present (Partial_Invariant_Procedure (Work_Typ)) then - return; + goto Leave; end if; -- Nothing to do if the type already has a "full" invariant procedure elsif Present (Invariant_Procedure (Work_Typ)) then - return; + goto Leave; end if; - -- The working type may be subject to pragma Ghost. Set the mode now to - -- ensure that the invariant procedure is properly marked as Ghost. - - Set_Ghost_Mode_From_Entity (Work_Typ); - -- The caller requests the declaration of the "partial" invariant -- procedure. @@ -4791,13 +4790,6 @@ package body Exp_Ch7 is Set_Needs_Debug_Info (Proc_Id); end if; - -- Mark the invariant procedure explicitly as Ghost because it does not - -- come from source. - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Proc_Id); - end if; - -- Obtain all views of the input type Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ); @@ -4868,7 +4860,8 @@ package body Exp_Ch7 is Insert_After_And_Analyze (Typ_Decl, Proc_Decl); end if; - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); end Build_Invariant_Procedure_Declaration; --------------------- @@ -5835,15 +5828,7 @@ package body Exp_Ch7 is Spec_Id : constant Entity_Id := Corresponding_Spec (N); Fin_Id : Entity_Id; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin - -- The package body is Ghost when the corresponding spec is Ghost. Set - -- the mode now to ensure that any nodes generated during expansion are - -- properly marked as Ghost. - - Set_Ghost_Mode (N, Spec_Id); - -- This is done only for non-generic packages if Ekind (Spec_Id) = E_Package then @@ -5899,8 +5884,6 @@ package body Exp_Ch7 is end; end if; end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Package_Body; ---------------------------------- diff --git a/gcc/ada/exp_ch8.adb b/gcc/ada/exp_ch8.adb index 9e06db27417..9a4e5e53d1b 100644 --- a/gcc/ada/exp_ch8.adb +++ b/gcc/ada/exp_ch8.adb @@ -30,7 +30,6 @@ 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; @@ -50,25 +49,14 @@ package body Exp_Ch8 is --------------------------------------------- procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Decl : Node_Id; begin - -- The exception renaming declaration is Ghost when it is subject to - -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set - -- the mode now to ensure that any nodes generated during expansion are - -- properly marked as Ghost. - - Set_Ghost_Mode (N); - Decl := Debug_Renaming_Declaration (N); if Present (Decl) then Insert_Action (N, Decl); end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Exception_Renaming_Declaration; ------------------------------------------ @@ -161,20 +149,9 @@ package body Exp_Ch8 is end if; end Evaluation_Required; - -- Local variables - - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - -- Start of processing for Expand_N_Object_Renaming_Declaration begin - -- The object renaming declaration is Ghost when it is subject to pragma - -- Ghost or renames a Ghost entity. To accomodate both cases, set the - -- mode now to ensure that any nodes generated during expansion are - -- properly marked as Ghost. - - Set_Ghost_Mode (N); - -- Perform name evaluation if required if Evaluation_Required (Nam) then @@ -217,8 +194,6 @@ package body Exp_Ch8 is if Present (Decl) then Insert_Action (N, Decl); end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Object_Renaming_Declaration; ------------------------------------------- @@ -226,18 +201,9 @@ package body Exp_Ch8 is ------------------------------------------- procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Decl : Node_Id; begin - -- The package renaming declaration is Ghost when it is subject to - -- pragma Ghost or renames a Ghost entity. To accomodate both cases, - -- set the mode now to ensure that any nodes generated during expansion - -- are properly marked as Ghost. - - Set_Ghost_Mode (N); - Decl := Debug_Renaming_Declaration (N); if Present (Decl) then @@ -276,8 +242,6 @@ package body Exp_Ch8 is Insert_Action (N, Decl); end if; end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Package_Renaming_Declaration; ---------------------------------------------- @@ -327,19 +291,11 @@ package body Exp_Ch8 is -- Local variables - Nam : constant Node_Id := Name (N); - Save_Ghost_Mode : 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 is Ghost when it is subject to - -- pragma Ghost or renames a Ghost entity. To accomodate both cases, 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. @@ -403,8 +359,6 @@ package body Exp_Ch8 is end if; end; end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_N_Subprogram_Renaming_Declaration; end Exp_Ch8; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 03c45585836..034e199e2e7 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -4367,71 +4367,62 @@ package body Exp_Disp is -- Local variables - Elab_Code : constant List_Id := New_List; - Result : constant List_Id := New_List; - Tname : constant Name_Id := Chars (Typ); + Elab_Code : constant List_Id := New_List; + Result : constant List_Id := New_List; + Tname : constant Name_Id := Chars (Typ); + + -- The following name entries are used by Make_DT to generate a number + -- of entities related to a tagged type. These entities may be generated + -- in a scope other than that of the tagged type declaration, and if + -- the entities for two tagged types with the same name happen to be + -- generated in the same scope, we have to take care to use different + -- names. This is achieved by means of a unique serial number appended + -- to each generated entity name. + + Name_DT : constant Name_Id := + New_External_Name (Tname, 'T', Suffix_Index => -1); + Name_Exname : constant Name_Id := + New_External_Name (Tname, 'E', Suffix_Index => -1); + Name_HT_Link : constant Name_Id := + New_External_Name (Tname, 'H', Suffix_Index => -1); + Name_Predef_Prims : constant Name_Id := + New_External_Name (Tname, 'R', Suffix_Index => -1); + Name_SSD : constant Name_Id := + New_External_Name (Tname, 'S', Suffix_Index => -1); + Name_TSD : constant Name_Id := + New_External_Name (Tname, 'B', Suffix_Index => -1); + AI : Elmt_Id; AI_Tag_Elmt : Elmt_Id; AI_Tag_Comp : Elmt_Id; + DT : Entity_Id; DT_Aggr_List : List_Id; DT_Constr_List : List_Id; DT_Ptr : Entity_Id; + Exname : Entity_Id; + HT_Link : Entity_Id; ITable : Node_Id; I_Depth : Nat := 0; Iface_Table_Node : Node_Id; + Mode : Ghost_Mode_Type; Name_ITable : Name_Id; Nb_Predef_Prims : Nat := 0; Nb_Prim : Nat := 0; New_Node : Node_Id; Num_Ifaces : Nat := 0; Parent_Typ : Entity_Id; + Predef_Prims : Entity_Id; Prim : Entity_Id; Prim_Elmt : Elmt_Id; Prim_Ops_Aggr_List : List_Id; + SSD : Entity_Id; Suffix_Index : Int; Typ_Comps : Elist_Id; Typ_Ifaces : Elist_Id; + TSD : Entity_Id; TSD_Aggr_List : List_Id; TSD_Tags_List : List_Id; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - - -- The following name entries are used by Make_DT to generate a number - -- of entities related to a tagged type. These entities may be generated - -- in a scope other than that of the tagged type declaration, and if - -- the entities for two tagged types with the same name happen to be - -- generated in the same scope, we have to take care to use different - -- names. This is achieved by means of a unique serial number appended - -- to each generated entity name. - - Name_DT : constant Name_Id := - New_External_Name (Tname, 'T', Suffix_Index => -1); - Name_Exname : constant Name_Id := - New_External_Name (Tname, 'E', Suffix_Index => -1); - Name_HT_Link : constant Name_Id := - New_External_Name (Tname, 'H', Suffix_Index => -1); - Name_Predef_Prims : constant Name_Id := - New_External_Name (Tname, 'R', Suffix_Index => -1); - Name_SSD : constant Name_Id := - New_External_Name (Tname, 'S', Suffix_Index => -1); - Name_TSD : constant Name_Id := - New_External_Name (Tname, 'B', Suffix_Index => -1); - - -- Entities built with above names - - DT : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_DT); - Exname : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_Exname); - HT_Link : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_HT_Link); - Predef_Prims : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_Predef_Prims); - SSD : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_SSD); - TSD : constant Entity_Id := - Make_Defining_Identifier (Loc, Name_TSD); - -- Start of processing for Make_DT begin @@ -4441,7 +4432,7 @@ package body Exp_Disp is -- the mode now to ensure that any nodes generated during dispatch table -- creation are properly marked as Ghost. - Set_Ghost_Mode (Declaration_Node (Typ), Typ); + Set_Ghost_Mode (Typ, Mode); -- Handle cases in which there is no need to build the dispatch table @@ -4449,19 +4440,17 @@ package body Exp_Disp is or else No (Access_Disp_Table (Typ)) or else Is_CPP_Class (Typ) then - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; elsif No_Run_Time_Mode then Error_Msg_CRT ("tagged types", Typ); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; elsif not RTE_Available (RE_Tag) then Append_To (Result, Make_Object_Declaration (Loc, - Defining_Identifier => Node (First_Elmt - (Access_Disp_Table (Typ))), + Defining_Identifier => + Node (First_Elmt (Access_Disp_Table (Typ))), Object_Definition => New_Occurrence_Of (RTE (RE_Tag), Loc), Constant_Present => True, Expression => @@ -4470,8 +4459,7 @@ package body Exp_Disp is Analyze_List (Result, Suppress => All_Checks); Error_Msg_CRT ("tagged types", Typ); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; end if; -- Ensure that the value of Max_Predef_Prims defined in a-tags is @@ -4481,18 +4469,23 @@ package body Exp_Disp is if RTE_Available (RE_Interface_Data) then if Max_Predef_Prims /= 15 then Error_Msg_N ("run-time library configuration error", Typ); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; end if; else if Max_Predef_Prims /= 9 then Error_Msg_N ("run-time library configuration error", Typ); Error_Msg_CRT ("tagged types", Typ); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; end if; end if; + DT := Make_Defining_Identifier (Loc, Name_DT); + Exname := Make_Defining_Identifier (Loc, Name_Exname); + HT_Link := Make_Defining_Identifier (Loc, Name_HT_Link); + Predef_Prims := Make_Defining_Identifier (Loc, Name_Predef_Prims); + SSD := Make_Defining_Identifier (Loc, Name_SSD); + TSD := Make_Defining_Identifier (Loc, Name_TSD); + -- Initialize Parent_Typ handling private types Parent_Typ := Etype (Typ); @@ -4695,7 +4688,7 @@ package body Exp_Disp is Set_SCIL_Entity (New_Node, Typ); Set_SCIL_Node (Last (Result), New_Node); - goto Early_Exit_For_SCIL; + goto Leave_SCIL; -- Gnat2scil has its own implementation of dispatch tables, -- different than what is being implemented here. Generating @@ -4772,7 +4765,7 @@ package body Exp_Disp is Set_SCIL_Entity (New_Node, Typ); Set_SCIL_Node (Last (Result), New_Node); - goto Early_Exit_For_SCIL; + goto Leave_SCIL; -- Gnat2scil has its own implementation of dispatch tables, -- different than what is being implemented here. Generating @@ -6238,13 +6231,15 @@ package body Exp_Disp is end; end if; - <> + <> -- Register the tagged type in the call graph nodes table Register_CG_Node (Typ); - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); + return Result; end Make_DT; diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index ac24d4f5edf..858c632275e 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -32,7 +32,6 @@ 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; @@ -317,8 +316,6 @@ package body Exp_Prag is -- Assert_Failure, so that coverage analysis tools can relate the -- call to the failed check. - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin -- Nothing to do if pragma is ignored @@ -326,15 +323,8 @@ package body Exp_Prag is return; end if; - -- Pragmas Assert, Assert_And_Cut, Assume, Check and Loop_Invariant are - -- Ghost when they apply to a Ghost entity. Set the mode now to ensure - -- that any nodes generated during expansion are properly flagged as - -- Ghost. - - Set_Ghost_Mode (N); - - -- Since this check is active, we rewrite the pragma into a - -- corresponding if statement, and then analyze the statement. + -- Since this check is active, rewrite the pragma into a corresponding + -- if statement, and then analyze the statement. -- The normal case expansion transforms: @@ -492,12 +482,9 @@ package body Exp_Prag is elsif Nam = Name_Assert then Error_Msg_N ("?A?assertion will fail at run time", N); else - Error_Msg_N ("?A?check will fail at run time", N); end if; end if; - - Ghost_Mode := Save_Ghost_Mode; end Expand_Pragma_Check; --------------------------------- @@ -997,8 +984,6 @@ package body Exp_Prag is Aggr : constant Node_Id := Expression (First (Pragma_Argument_Associations (CCs))); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Case_Guard : Node_Id; CG_Checks : Node_Id; CG_Stmts : List_Id; @@ -1032,12 +1017,6 @@ package body Exp_Prag is return; end if; - -- The contract cases is Ghost when it applies to a Ghost entity. Set - -- the mode now to ensure that any nodes generated during expansion are - -- properly flagged as Ghost. - - Set_Ghost_Mode (CCs); - -- The expansion of contract cases is quite distributed as it produces -- various statements to evaluate the case guards and consequences. To -- preserve the original context, set the Is_Assertion_Expr flag. This @@ -1272,7 +1251,6 @@ package body Exp_Prag is Append_To (Stmts, Conseq_Checks); In_Assertion_Expr := In_Assertion_Expr - 1; - Ghost_Mode := Save_Ghost_Mode; end Expand_Pragma_Contract_Cases; --------------------------------------- @@ -1372,15 +1350,14 @@ package body Exp_Prag is ------------------------------------- procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is - Loc : constant Source_Ptr := Sloc (Spec_Or_Body); + Loc : constant Source_Ptr := Sloc (Spec_Or_Body); + Check : Node_Id; Expr : Node_Id; Init_Cond : Node_Id; List : List_Id; Pack_Id : Entity_Id; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin if Nkind (Spec_Or_Body) = N_Package_Body then Pack_Id := Corresponding_Spec (Spec_Or_Body); @@ -1419,12 +1396,6 @@ package body Exp_Prag is Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition); - -- The initial condition is Ghost when it applies to a Ghost entity. Set - -- the mode now to ensure that any nodes generated during expansion are - -- properly flagged as Ghost. - - Set_Ghost_Mode (Init_Cond); - -- The caller should check whether the package is subject to pragma -- Initial_Condition. @@ -1437,7 +1408,6 @@ package body Exp_Prag is -- runtime check as it will repeat the illegality. if Error_Posted (Init_Cond) or else Error_Posted (Expr) then - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -1455,8 +1425,6 @@ package body Exp_Prag is Append_To (List, Check); Analyze (Check); - - Ghost_Mode := Save_Ghost_Mode; end Expand_Pragma_Initial_Condition; ------------------------------------ @@ -1632,8 +1600,8 @@ package body Exp_Prag is -- Local variables - Expr : constant Node_Id := Expression (Variant); - Expr_Typ : constant Entity_Id := Etype (Expr); + Expr : constant Node_Id := Expression (Variant); + Expr_Typ : constant Entity_Id := Etype (Expr); Loc : constant Source_Ptr := Sloc (Expr); Loop_Loc : constant Source_Ptr := Sloc (Loop_Stmt); Curr_Id : Entity_Id; @@ -1804,10 +1772,6 @@ package body Exp_Prag is end if; end Process_Variant; - -- Local variables - - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - -- Start of processing for Expand_Pragma_Loop_Variant begin @@ -1820,12 +1784,6 @@ package body Exp_Prag is return; end if; - -- The loop variant is Ghost when it applies to a Ghost entity. Set - -- the mode now to ensure that any nodes generated during expansion - -- are properly flagged as Ghost. - - Set_Ghost_Mode (N); - -- The expansion of Loop_Variant is quite distributed as it produces -- various statements to capture and compare the arguments. To preserve -- the original context, set the Is_Assertion_Expr flag. This aids the @@ -1896,7 +1854,6 @@ package body Exp_Prag is -- for documentation purposes. It will be ignored by the backend. In_Assertion_Expr := In_Assertion_Expr - 1; - Ghost_Mode := Save_Ghost_Mode; end Expand_Pragma_Loop_Variant; -------------------------------- diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index d400041862b..82970136f0f 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1712,12 +1712,11 @@ package body Exp_Util is Loc : constant Source_Ptr := Sloc (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - DIC_Prag : Node_Id; DIC_Typ : Entity_Id; Dummy_1 : Entity_Id; Dummy_2 : Entity_Id; + Mode : Ghost_Mode_Type; Proc_Body : Node_Id; Proc_Body_Id : Entity_Id; Proc_Decl : Node_Id; @@ -1749,6 +1748,11 @@ package body Exp_Util is Work_Typ := Corresponding_Concurrent_Type (Work_Typ); end if; + -- The working type may be subject to pragma Ghost. Set the mode now to + -- ensure that the DIC procedure is properly marked as Ghost. + + Set_Ghost_Mode (Work_Typ, Mode); + -- The working type must be either define a DIC pragma of its own or -- inherit one from a parent type. @@ -1767,7 +1771,7 @@ package body Exp_Util is -- argument is "null". if not Is_Verifiable_DIC_Pragma (DIC_Prag) then - return; + goto Leave; end if; -- The working type may lack a DIC procedure declaration. This may be @@ -1799,14 +1803,9 @@ package body Exp_Util is -- Nothing to do if the DIC procedure already has a body if Present (Corresponding_Body (Proc_Decl)) then - return; + goto Leave; end if; - -- The working type may be subject to pragma Ghost. Set the mode now to - -- ensure that the DIC procedure is properly marked as Ghost. - - Set_Ghost_Mode_From_Entity (Work_Typ); - -- Emulate the environment of the DIC procedure by installing its scope -- and formal parameters. @@ -1917,7 +1916,8 @@ package body Exp_Util is Append_Freeze_Action (Work_Typ, Proc_Body); end if; - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); end Build_DIC_Procedure_Body; ------------------------------------- @@ -1927,10 +1927,9 @@ package body Exp_Util is procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is Loc : constant Source_Ptr := Sloc (Typ); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - DIC_Prag : Node_Id; DIC_Typ : Entity_Id; + Mode : Ghost_Mode_Type; Proc_Decl : Node_Id; Proc_Id : Entity_Id; Typ_Decl : Node_Id; @@ -1973,6 +1972,11 @@ package body Exp_Util is Work_Typ := Corresponding_Concurrent_Type (Work_Typ); end if; + -- The working type may be subject to pragma Ghost. Set the mode now to + -- ensure that the DIC procedure is properly marked as Ghost. + + Set_Ghost_Mode (Work_Typ, Mode); + -- The type must be either subject to a DIC pragma or inherit one from a -- parent type. @@ -1991,19 +1995,14 @@ package body Exp_Util is -- argument is "null". if not Is_Verifiable_DIC_Pragma (DIC_Prag) then - return; + goto Leave; -- Nothing to do if the type already has a DIC procedure elsif Present (DIC_Procedure (Work_Typ)) then - return; + goto Leave; end if; - -- The working type may be subject to pragma Ghost. Set the mode now to - -- ensure that the DIC procedure is properly marked as Ghost. - - Set_Ghost_Mode_From_Entity (Work_Typ); - Proc_Id := Make_Defining_Identifier (Loc, Chars => @@ -2025,13 +2024,6 @@ package body Exp_Util is Set_Needs_Debug_Info (Proc_Id); end if; - -- Mark the DIC procedure explicitly as Ghost because it does not come - -- from source. - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Proc_Id); - end if; - -- Obtain all views of the input type Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ); @@ -2106,7 +2098,8 @@ package body Exp_Util is Insert_After_And_Analyze (Typ_Decl, Proc_Decl); end if; - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); end Build_DIC_Procedure_Declaration; -------------------------- @@ -7816,8 +7809,9 @@ package body Exp_Util is ------------------------- function Make_Invariant_Call (Expr : Node_Id) return Node_Id is - Loc : constant Source_Ptr := Sloc (Expr); - Typ : constant Entity_Id := Base_Type (Etype (Expr)); + Loc : constant Source_Ptr := Sloc (Expr); + Typ : constant Entity_Id := Base_Type (Etype (Expr)); + Proc_Id : Entity_Id; begin @@ -7910,11 +7904,11 @@ package body Exp_Util is Expr : Node_Id; Mem : Boolean := False) return Node_Id is - Loc : constant Source_Ptr := Sloc (Expr); - Call : Node_Id; - PFM : Entity_Id; + Loc : constant Source_Ptr := Sloc (Expr); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Call : Node_Id; + Func_Id : Entity_Id; + Mode : Ghost_Mode_Type; begin pragma Assert (Present (Predicate_Function (Typ))); @@ -7922,33 +7916,24 @@ package body Exp_Util is -- The related type may be subject to pragma Ghost. Set the mode now to -- ensure that the call is properly marked as Ghost. - Set_Ghost_Mode_From_Entity (Typ); + Set_Ghost_Mode (Typ, Mode); -- Call special membership version if requested and available - if Mem then - 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))); - - Ghost_Mode := Save_Ghost_Mode; - return Call; - end if; + if Mem and then Present (Predicate_Function_M (Typ)) then + Func_Id := Predicate_Function_M (Typ); + else + Func_Id := Predicate_Function (Typ); end if; -- Case of calling normal predicate function Call := Make_Function_Call (Loc, - Name => - New_Occurrence_Of (Predicate_Function (Typ), Loc), + Name => New_Occurrence_Of (Func_Id, Loc), Parameter_Associations => New_List (Relocate_Node (Expr))); - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Mode); return Call; end Make_Predicate_Call; diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb index 84d64226772..64192b7989d 100644 --- a/gcc/ada/expander.adb +++ b/gcc/ada/expander.adb @@ -41,6 +41,7 @@ with Exp_Ch11; use Exp_Ch11; with Exp_Ch12; use Exp_Ch12; with Exp_Ch13; use Exp_Ch13; with Exp_Prag; use Exp_Prag; +with Ghost; use Ghost; with Opt; use Opt; with Rtsfind; use Rtsfind; with Sem; use Sem; @@ -77,6 +78,8 @@ package body Expander is ------------ procedure Expand (N : Node_Id) is + Mode : Ghost_Mode_Type; + begin -- If we were analyzing a default expression (or other spec expression) -- the Full_Analysis flag must be off. If we are in expansion mode then @@ -88,6 +91,11 @@ package body Expander is and then (Full_Analysis or else not Expander_Active) and then not (Inside_A_Generic and then Expander_Active)); + -- Establish the Ghost mode of the context to ensure that any generated + -- nodes during expansion are marked as Ghost. + + Set_Ghost_Mode (N, Mode); + -- The GNATprove_Mode flag indicates that a light expansion for formal -- verification should be used. This expansion is never done inside -- generics, because otherwise, this breaks the name resolution @@ -105,7 +113,7 @@ package body Expander is -- needed, and in general cannot be done correctly, in this mode, so -- we are all done. - return; + goto Leave; -- There are three reasons for the Expander_Active flag to be false @@ -140,7 +148,7 @@ package body Expander is Pop_Scope; end if; - return; + goto Leave; else begin @@ -482,7 +490,7 @@ package body Expander is exception when RE_Not_Available => - return; + goto Leave; end; -- Set result as analyzed and then do a possible transient wrap. The @@ -510,6 +518,9 @@ package body Expander is Debug_A_Exit ("expanding ", N, " (done)"); end if; + + <> + Restore_Ghost_Mode (Mode); end Expand; --------------------------- diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 0cc588102e2..c601ac02ae7 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2071,9 +2071,6 @@ package body Freeze is -- Determine whether an arbitrary entity is subject to Boolean aspect -- Import and its value is specified as True. - function New_Freeze_Node return Node_Id; - -- Create a new freeze node for entity E - procedure Wrap_Imported_Subprogram (E : Entity_Id); -- If E is an entity for an imported subprogram with pre/post-conditions -- then this procedure will create a wrapper to ensure that proper run- @@ -2283,14 +2280,12 @@ package body Freeze is if Convention (Rec_Type) = Convention_C then Error_Msg_N - ("?x?discriminated record has no direct " & - "equivalent in C", - A2); + ("?x?discriminated record has no direct equivalent in " + & "C", A2); else Error_Msg_N - ("?x?discriminated record has no direct " & - "equivalent in C++", - A2); + ("?x?discriminated record has no direct equivalent in " + & "C++", A2); end if; Error_Msg_NE @@ -4703,39 +4698,6 @@ package body Freeze is return False; end Has_Boolean_Aspect_Import; - --------------------- - -- New_Freeze_Node -- - --------------------- - - function New_Freeze_Node return Node_Id is - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Result : Node_Id; - - begin - -- Handle the case where an ignored Ghost subprogram freezes the type - -- of one of its formals. The type can either be non-Ghost or checked - -- Ghost. Since the freeze node for the type is generated in the - -- context of the subprogram, the node will be incorrectly flagged as - -- ignored Ghost and erroneously removed from the tree. - - -- type Typ is ...; - -- procedure Ignored_Ghost_Proc (Formal : Typ) with Ghost; - - -- Reset the Ghost mode to "none". This preserves the freeze node. - - if Ghost_Mode = Ignore - and then not Is_Ignored_Ghost_Entity (E) - and then not Is_Ignored_Ghost_Node (E) - then - Ghost_Mode := None; - end if; - - Result := New_Node (N_Freeze_Entity, Loc); - - Ghost_Mode := Save_Ghost_Mode; - return Result; - end New_Freeze_Node; - ------------------------------ -- Wrap_Imported_Subprogram -- ------------------------------ @@ -4927,7 +4889,7 @@ package body Freeze is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Mode : Ghost_Mode_Type; -- Start of processing for Freeze_Entity @@ -4936,7 +4898,7 @@ package body Freeze is -- now to ensure that any nodes generated during freezing are properly -- flagged as Ghost. - Set_Ghost_Mode_From_Entity (E); + Set_Ghost_Mode (E, Mode); -- 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 @@ -4953,14 +4915,12 @@ package body Freeze is -- Do not freeze if already frozen since we only need one freeze node if Is_Frozen (E) then - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; elsif Ekind (E) = E_Generic_Package then Result := Freeze_Generic_Entities (E); - - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; -- It is improper to freeze an external entity within a generic because -- its freeze node will appear in a non-valid context. The entity will @@ -4974,8 +4934,8 @@ package body Freeze is Analyze_Aspects_At_Freeze_Point (E); end if; - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; -- AI05-0213: A formal incomplete type does not freeze the actual. In -- the instance, the same applies to the subtype renaming the actual. @@ -4985,20 +4945,20 @@ package body Freeze is and then No (Full_View (Base_Type (E))) and then Ada_Version >= Ada_2012 then - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; -- Formal subprograms are never frozen elsif Is_Formal_Subprogram (E) then - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; -- Generic types are never frozen as they lack delayed semantic checks elsif Is_Generic_Type (E) then - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; -- Do not freeze a global entity within an inner scope created during -- expansion. A call to subprogram E within some internal procedure @@ -5031,8 +4991,8 @@ package body Freeze is then exit; else - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; end if; end if; @@ -5067,8 +5027,8 @@ package body Freeze is end loop; if No (S) then - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; end if; end; end if; @@ -5153,8 +5113,7 @@ package body Freeze is if not Is_Internal (E) and then Do_Freeze_Profile then if not Freeze_Profile (E) then - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; end if; end if; @@ -5336,8 +5295,8 @@ package body Freeze is and then not Has_Delayed_Freeze (E)) then Check_Compile_Time_Size (E); - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; end if; -- Check for error of Type_Invariant'Class applied to an untagged @@ -5607,8 +5566,7 @@ package body Freeze is if not Is_Frozen (Root_Type (E)) then Set_Is_Frozen (E, False); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; end if; -- The equivalent type associated with a class-wide subtype needs @@ -5749,8 +5707,7 @@ package body Freeze is and then not Present (Full_View (E)) then Set_Is_Frozen (E, False); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; -- Case of full view present @@ -5841,8 +5798,7 @@ package body Freeze is Set_RM_Size (E, RM_Size (Full_View (E))); end if; - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; -- Case of underlying full view present @@ -5871,8 +5827,7 @@ package body Freeze is Check_Debug_Info_Needed (E); - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; -- Case of no full view present. If entity is derived or subtype, -- it is safe to freeze, correctness depends on the frozen status @@ -5885,8 +5840,8 @@ package body Freeze is else Set_Is_Frozen (E, False); - Ghost_Mode := Save_Ghost_Mode; - return No_List; + Result := No_List; + goto Leave; end if; -- For access subprogram, freeze types of all formals, the return @@ -5933,8 +5888,7 @@ package body Freeze is -- generic processing), so we never need freeze nodes for them. if Is_Generic_Type (E) then - Ghost_Mode := Save_Ghost_Mode; - return Result; + goto Leave; end if; -- Some special processing for non-generic types to complete @@ -6465,7 +6419,7 @@ package body Freeze is Set_Sloc (F_Node, Loc); else - F_Node := New_Freeze_Node; + F_Node := New_Node (N_Freeze_Entity, Loc); Set_Freeze_Node (E, F_Node); Set_Access_Types_To_Process (F_Node, No_Elist); Set_TSS_Elist (F_Node, No_Elist); @@ -6547,7 +6501,8 @@ package body Freeze is end if; end if; - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); return Result; end Freeze_Entity; diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 26ea406f433..b55cff633db 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -33,7 +33,6 @@ with Lib; use Lib; with Namet; use Namet; with Nlists; use Nlists; with Nmake; use Nmake; -with Opt; use Opt; with Sem; use Sem; with Sem_Aux; use Sem_Aux; with Sem_Disp; use Sem_Disp; @@ -65,20 +64,30 @@ package body Ghost is ----------------------- 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. + -- Find the entity of a reference to a Ghost entity. Return Empty if there + -- is no such entity. + + procedure Install_Ghost_Mode (Mode : Name_Id); + -- Install a specific Ghost mode denoted by Mode by setting global variable + -- Ghost_Mode. function Is_Subject_To_Ghost (N : Node_Id) return Boolean; - -- Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether - -- declaration or body N is subject to aspect or pragma Ghost. Use this - -- routine in cases where [source] pragma Ghost has not been analyzed yet, - -- but the context needs to establish the "ghostness" of N. + -- Determine whether declaration or body N is subject to aspect or pragma + -- Ghost. This routine must be used in cases where pragma Ghost has not + -- been analyzed yet, but the context needs to establish the "ghostness" + -- of N. + + procedure Mark_Ghost_Declaration_Or_Body + (N : Node_Id; + Mode : Name_Id); + -- Mark the defining entity of declaration or body N as Ghost depending on + -- mode Mode. Mark all formals parameters when N denotes a subprogram or a + -- body. procedure Propagate_Ignored_Ghost_Code (N : Node_Id); - -- 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. + -- Signal all enclosing scopes that they now contain at least one ignored + -- Ghost node denoted by N. Add the compilation unit containing N to table + -- Ignored_Ghost_Units for post processing. ---------------------------- -- Add_Ignored_Ghost_Unit -- @@ -112,34 +121,37 @@ package body Ghost is ---------------------------- procedure Check_Ghost_Completion - (Partial_View : Entity_Id; - Full_View : Entity_Id) + (Prev_Id : Entity_Id; + Compl_Id : Entity_Id) is Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); begin + -- Nothing to do if one of the views is missing + + if No (Prev_Id) or else No (Compl_Id) then + null; + -- The Ghost policy in effect at the point of declaration and at the -- point of completion must match (SPARK RM 6.9(14)). - if Is_Checked_Ghost_Entity (Partial_View) + elsif Is_Checked_Ghost_Entity (Prev_Id) and then Policy = Name_Ignore then - Error_Msg_Sloc := Sloc (Full_View); + Error_Msg_Sloc := Sloc (Compl_Id); - 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", Prev_Id); + Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id); + Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id); - elsif Is_Ignored_Ghost_Entity (Partial_View) + elsif Is_Ignored_Ghost_Entity (Prev_Id) and then Policy = Name_Check then - Error_Msg_Sloc := Sloc (Full_View); + Error_Msg_Sloc := Sloc (Compl_Id); - 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", Prev_Id); + Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id); + Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id); end if; end Check_Ghost_Completion; @@ -165,23 +177,31 @@ package body Ghost is 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 + -- + -- * Define a Ghost entity + -- + -- * Be subject to pragma Ghost 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 + -- + -- * Be an assertion expression pragma + -- + -- * Denote pragma Global, Depends, Initializes, Refined_Global, + -- Refined_Depends or Refined_State. + -- + -- * Specify an aspect of a Ghost entity + -- + -- * 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 + -- + -- * Denote a procedure call to a Ghost procedure + -- + -- * Denote an assignment statement whose target is Ghost ----------------------- -- Is_OK_Declaration -- @@ -192,10 +212,6 @@ package body Ghost is -- Determine whether node N appears in the profile of a subprogram -- body. - function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean; - -- Determine whether node Ren_Decl denotes a renaming declaration - -- with a Ghost name. - -------------------------------- -- In_Subprogram_Body_Profile -- -------------------------------- @@ -216,23 +232,6 @@ package body Ghost is and then Nkind (Parent (Spec)) = N_Subprogram_Body; end In_Subprogram_Body_Profile; - ----------------------- - -- 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; @@ -241,20 +240,8 @@ package body Ghost is -- Start of processing for Is_OK_Declaration begin - if Is_Declaration (Decl) then - - -- A renaming declaration is Ghost when it renames a Ghost - -- entity. - - if Is_Ghost_Renaming (Decl) then - return True; - - -- The declaration may not have been analyzed yet, determine - -- whether it is subject to pragma Ghost. - - elsif Is_Subject_To_Ghost (Decl) then - return True; - end if; + if Is_Ghost_Declaration (Decl) then + return True; -- Special cases @@ -303,7 +290,7 @@ package body Ghost 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); + return Is_Ghost_Declaration (Subp_Decl); end if; end if; @@ -358,8 +345,6 @@ package body Ghost is -- Local variables - Arg : Node_Id; - Arg_Id : Entity_Id; Prag_Id : Pragma_Id; Prag_Nam : Name_Id; @@ -399,21 +384,6 @@ package body Ghost is Name_Refined_State) then return True; - - -- Otherwise a normal pragma is Ghost when it encloses a Ghost - -- name (SPARK RM 6.9(3)). - - else - Arg := First (Pragma_Argument_Associations (Prag)); - while Present (Arg) loop - Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg)); - - if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then - return True; - end if; - - Next (Arg); - end loop; end if; end if; @@ -425,18 +395,17 @@ package body Ghost is --------------------- function Is_OK_Statement (Stmt : Node_Id) return Boolean is - Nam_Id : Entity_Id; - begin - -- An assignment statement or a procedure call is Ghost when the - -- name denotes a Ghost entity. + -- An assignment statement is Ghost when the target is a Ghost + -- entity. - if Nkind_In (Stmt, N_Assignment_Statement, - N_Procedure_Call_Statement) - then - Nam_Id := Ghost_Entity (Name (Stmt)); + if Nkind (Stmt) = N_Assignment_Statement then + return Is_Ghost_Assignment (Stmt); - return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id); + -- A procedure call is Ghost when it calls a Ghost procedure + + elsif Nkind (Stmt) = N_Procedure_Call_Statement then + return Is_Ghost_Procedure_Call (Stmt); -- Special cases @@ -829,7 +798,7 @@ package body Ghost is Ref : Node_Id; begin - -- When the reference extracts a subcomponent, recover the related + -- When the reference denotes a subcomponent, recover the related -- object (SPARK RM 6.9(1)). Ref := N; @@ -881,6 +850,96 @@ package body Ghost is Ignored_Ghost_Units.Init; end Initialize; + ------------------------ + -- Install_Ghost_Mode -- + ------------------------ + + procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is + begin + Ghost_Mode := Mode; + end Install_Ghost_Mode; + + procedure Install_Ghost_Mode (Mode : Name_Id) is + begin + if Mode = Name_Check then + Ghost_Mode := Check; + + elsif Mode = Name_Ignore then + Ghost_Mode := Ignore; + + elsif Mode = Name_None then + Ghost_Mode := None; + end if; + end Install_Ghost_Mode; + + ------------------------- + -- Is_Ghost_Assignment -- + ------------------------- + + function Is_Ghost_Assignment (N : Node_Id) return Boolean is + Id : Entity_Id; + + begin + -- An assignment statement is Ghost when its target denotes a Ghost + -- entity. + + if Nkind (N) = N_Assignment_Statement then + Id := Ghost_Entity (Name (N)); + + return Present (Id) and then Is_Ghost_Entity (Id); + end if; + + return False; + end Is_Ghost_Assignment; + + -------------------------- + -- Is_Ghost_Declaration -- + -------------------------- + + function Is_Ghost_Declaration (N : Node_Id) return Boolean is + Id : Entity_Id; + + begin + -- A declaration is Ghost when it elaborates a Ghost entity or is + -- subject to pragma Ghost. + + if Is_Declaration (N) then + Id := Defining_Entity (N); + + return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N); + end if; + + return False; + end Is_Ghost_Declaration; + + --------------------- + -- Is_Ghost_Pragma -- + --------------------- + + function Is_Ghost_Pragma (N : Node_Id) return Boolean is + begin + return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N); + end Is_Ghost_Pragma; + + ----------------------------- + -- Is_Ghost_Procedure_Call -- + ----------------------------- + + function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is + Id : Entity_Id; + + begin + -- A procedure call is Ghost when it invokes a Ghost procedure + + if Nkind (N) = N_Procedure_Call_Statement then + Id := Ghost_Entity (Name (N)); + + return Present (Id) and then Is_Ghost_Entity (Id); + end if; + + return False; + end Is_Ghost_Procedure_Call; + ------------------------- -- Is_Subject_To_Ghost -- ------------------------- @@ -1021,66 +1080,399 @@ package body Ghost is Ignored_Ghost_Units.Release; end Lock; + ----------------------------------- + -- Mark_And_Set_Ghost_Assignment -- + ----------------------------------- + + procedure Mark_And_Set_Ghost_Assignment + (N : Node_Id; + Mode : out Ghost_Mode_Type) + is + Id : Entity_Id; + + begin + -- Save the previous Ghost mode in effect + + Mode := Ghost_Mode; + + -- An assignment statement becomes Ghost when its target denotes a Ghost + -- object. Install the Ghost mode of the target. + + Id := Ghost_Entity (Name (N)); + + if Present (Id) then + if Is_Checked_Ghost_Entity (Id) then + Install_Ghost_Mode (Check); + + elsif Is_Ignored_Ghost_Entity (Id) then + Install_Ghost_Mode (Ignore); + + Set_Is_Ignored_Ghost_Node (N); + Propagate_Ignored_Ghost_Code (N); + end if; + end if; + end Mark_And_Set_Ghost_Assignment; + ----------------------------- - -- Mark_Full_View_As_Ghost -- + -- Mark_And_Set_Ghost_Body -- ----------------------------- - procedure Mark_Full_View_As_Ghost - (Priv_Typ : Entity_Id; - Full_Typ : Entity_Id) + procedure Mark_And_Set_Ghost_Body + (N : Node_Id; + Spec_Id : Entity_Id; + Mode : out Ghost_Mode_Type) is - Full_Decl : constant Node_Id := Declaration_Node (Full_Typ); + Body_Id : constant Entity_Id := Defining_Entity (N); + Policy : Name_Id := No_Name; begin - if Is_Checked_Ghost_Entity (Priv_Typ) then - Set_Is_Checked_Ghost_Entity (Full_Typ); + -- Save the previous Ghost mode in effect + + Mode := Ghost_Mode; + + -- A body becomes Ghost when it is subject to aspect or pragma Ghost - 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); + if Is_Subject_To_Ghost (N) then + Policy := Policy_In_Effect (Name_Ghost); + + -- A body declared within a Ghost region is automatically Ghost + -- (SPARK RM 6.9(2)). + + elsif Ghost_Mode = Check then + Policy := Name_Check; + + elsif Ghost_Mode = Ignore then + Policy := Name_Ignore; + + -- Inherit the "ghostness" of the previous declaration when the body + -- acts as a completion. + + elsif Present (Spec_Id) then + if Is_Checked_Ghost_Entity (Spec_Id) then + Policy := Name_Check; + + elsif Is_Ignored_Ghost_Entity (Spec_Id) then + Policy := Name_Ignore; + end if; end if; - end Mark_Full_View_As_Ghost; - -------------------------- - -- Mark_Pragma_As_Ghost -- - -------------------------- + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(14)). + + Check_Ghost_Completion + (Prev_Id => Spec_Id, + Compl_Id => Body_Id); + + -- Mark the body as its formals as Ghost + + Mark_Ghost_Declaration_Or_Body (N, Policy); + + -- Install the appropriate Ghost mode + + Install_Ghost_Mode (Policy); + end Mark_And_Set_Ghost_Body; + + ----------------------------------- + -- Mark_And_Set_Ghost_Completion -- + ----------------------------------- - procedure Mark_Pragma_As_Ghost - (Prag : Node_Id; - Context_Id : Entity_Id) + procedure Mark_And_Set_Ghost_Completion + (N : Node_Id; + Prev_Id : Entity_Id; + Mode : out Ghost_Mode_Type) is + Compl_Id : constant Entity_Id := Defining_Entity (N); + Policy : Name_Id := No_Name; + begin - if Is_Checked_Ghost_Entity (Context_Id) then - Set_Is_Ghost_Pragma (Prag); + -- Save the previous Ghost mode in effect + + Mode := Ghost_Mode; + + -- A completion elaborated in a Ghost region is automatically Ghost + -- (SPARK RM 6.9(2)). + + if Ghost_Mode = Check then + Policy := Name_Check; + + elsif Ghost_Mode = Ignore then + Policy := Name_Ignore; + + -- The completion becomes Ghost when its initial declaration is also + -- Ghost. + + elsif Is_Checked_Ghost_Entity (Prev_Id) then + Policy := Name_Check; - elsif Is_Ignored_Ghost_Entity (Context_Id) then - Set_Is_Ghost_Pragma (Prag); - Set_Is_Ignored_Ghost_Node (Prag); - Propagate_Ignored_Ghost_Code (Prag); + elsif Is_Ignored_Ghost_Entity (Prev_Id) then + Policy := Name_Ignore; end if; - end Mark_Pragma_As_Ghost; - ---------------------------- - -- Mark_Renaming_As_Ghost -- - ---------------------------- + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(14)). + + Check_Ghost_Completion + (Prev_Id => Prev_Id, + Compl_Id => Compl_Id); + + -- Mark the completion as Ghost + + Mark_Ghost_Declaration_Or_Body (N, Policy); + + -- Install the appropriate Ghost mode + + Install_Ghost_Mode (Policy); + end Mark_And_Set_Ghost_Completion; - procedure Mark_Renaming_As_Ghost - (Ren_Decl : Node_Id; - Nam_Id : Entity_Id) + ------------------------------------ + -- Mark_And_Set_Ghost_Declaration -- + ------------------------------------ + + procedure Mark_And_Set_Ghost_Declaration + (N : Node_Id; + Mode : out Ghost_Mode_Type) is - Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl); + Par_Id : Entity_Id; + Policy : Name_Id := No_Name; begin - if Is_Checked_Ghost_Entity (Nam_Id) then - Set_Is_Checked_Ghost_Entity (Ren_Id); + -- Save the previous Ghost mode in effect + + Mode := Ghost_Mode; + + -- A declaration becomes Ghost when it is subject to aspect or pragma + -- Ghost. + + if Is_Subject_To_Ghost (N) then + Policy := Policy_In_Effect (Name_Ghost); + + -- A declaration elaborated in a Ghost region is automatically Ghost + -- (SPARK RM 6.9(2)). + + elsif Ghost_Mode = Check then + Policy := Name_Check; + + elsif Ghost_Mode = Ignore then + Policy := Name_Ignore; + + -- A child package or subprogram declaration becomes Ghost when its + -- parent is Ghost (SPARK RM 6.9(2)). - 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); + elsif Nkind_In (N, N_Generic_Function_Renaming_Declaration, + N_Generic_Package_Declaration, + N_Generic_Package_Renaming_Declaration, + N_Generic_Procedure_Renaming_Declaration, + N_Generic_Subprogram_Declaration, + N_Package_Declaration, + N_Package_Renaming_Declaration, + N_Subprogram_Declaration, + N_Subprogram_Renaming_Declaration) + and then Present (Parent_Spec (N)) + then + Par_Id := Defining_Entity (Unit (Parent_Spec (N))); + + if Is_Checked_Ghost_Entity (Par_Id) then + Policy := Name_Check; + + elsif Is_Ignored_Ghost_Entity (Par_Id) then + Policy := Name_Ignore; + end if; + end if; + + -- Mark the declaration and its formals as Ghost + + Mark_Ghost_Declaration_Or_Body (N, Policy); + + -- Install the appropriate Ghost mode + + Install_Ghost_Mode (Policy); + end Mark_And_Set_Ghost_Declaration; + + -------------------------------------- + -- Mark_And_Set_Ghost_Instantiation -- + -------------------------------------- + + procedure Mark_And_Set_Ghost_Instantiation + (N : Node_Id; + Gen_Id : Entity_Id; + Mode : out Ghost_Mode_Type) + is + Policy : Name_Id := No_Name; + + begin + -- Save the previous Ghost mode in effect + + Mode := Ghost_Mode; + + -- An instantiation becomes Ghost when it is subject to pragma Ghost + + if Is_Subject_To_Ghost (N) then + Policy := Policy_In_Effect (Name_Ghost); + + -- An instantiation declaration within a Ghost region is automatically + -- Ghost (SPARK RM 6.9(2)). + + elsif Ghost_Mode = Check then + Policy := Name_Check; + + elsif Ghost_Mode = Ignore then + Policy := Name_Ignore; + + -- Inherit the "ghostness" of the generic unit + + elsif Is_Checked_Ghost_Entity (Gen_Id) then + Policy := Name_Check; + + elsif Is_Ignored_Ghost_Entity (Gen_Id) then + Policy := Name_Ignore; + end if; + + -- Mark the instantiation as Ghost + + Mark_Ghost_Declaration_Or_Body (N, Policy); + + -- Install the appropriate Ghost mode + + Install_Ghost_Mode (Policy); + end Mark_And_Set_Ghost_Instantiation; + + --------------------------------------- + -- Mark_And_Set_Ghost_Procedure_Call -- + --------------------------------------- + + procedure Mark_And_Set_Ghost_Procedure_Call + (N : Node_Id; + Mode : out Ghost_Mode_Type) + is + Id : Entity_Id; + + begin + -- Save the previous Ghost mode in effect + + Mode := Ghost_Mode; + + -- A procedure call becomes Ghost when the procedure being invoked is + -- Ghost. Install the Ghost mode of the procedure. + + Id := Ghost_Entity (Name (N)); + + if Present (Id) then + if Is_Checked_Ghost_Entity (Id) then + Install_Ghost_Mode (Check); + + elsif Is_Ignored_Ghost_Entity (Id) then + Install_Ghost_Mode (Ignore); + + Set_Is_Ignored_Ghost_Node (N); + Propagate_Ignored_Ghost_Code (N); + end if; + end if; + end Mark_And_Set_Ghost_Procedure_Call; + + ------------------------------------ + -- Mark_Ghost_Declaration_Or_Body -- + ------------------------------------ + + procedure Mark_Ghost_Declaration_Or_Body + (N : Node_Id; + Mode : Name_Id) + is + Id : constant Entity_Id := Defining_Entity (N); + + Mark_Formals : Boolean := False; + Param : Node_Id; + Param_Id : Entity_Id; + + begin + -- Mark the related node and its entity + + if Mode = Name_Check then + Mark_Formals := True; + Set_Is_Checked_Ghost_Entity (Id); + + elsif Mode = Name_Ignore then + Mark_Formals := True; + Set_Is_Ignored_Ghost_Entity (Id); + Set_Is_Ignored_Ghost_Node (N); + Propagate_Ignored_Ghost_Code (N); + end if; + + -- Mark all formal parameters when the related node denotes a subprogram + -- or a body. The traversal is performed via the specification because + -- the related subprogram or body may be unanalyzed. + + -- ??? could extra formal parameters cause a Ghost leak? + + if Mark_Formals + and then Nkind_In (N, N_Abstract_Subprogram_Declaration, + N_Formal_Abstract_Subprogram_Declaration, + N_Formal_Concrete_Subprogram_Declaration, + N_Generic_Subprogram_Declaration, + N_Subprogram_Body, + N_Subprogram_Body_Stub, + N_Subprogram_Declaration, + N_Subprogram_Renaming_Declaration) + then + Param := First (Parameter_Specifications (Specification (N))); + while Present (Param) loop + Param_Id := Defining_Entity (Param); + + if Mode = Name_Check then + Set_Is_Checked_Ghost_Entity (Param_Id); + + elsif Mode = Name_Ignore then + Set_Is_Ignored_Ghost_Entity (Param_Id); + end if; + + Next (Param); + end loop; + end if; + end Mark_Ghost_Declaration_Or_Body; + + ----------------------- + -- Mark_Ghost_Pragma -- + ----------------------- + + procedure Mark_Ghost_Pragma + (N : Node_Id; + Id : Entity_Id) + is + begin + -- A pragma becomes Ghost when it encloses a Ghost entity or relates to + -- a Ghost entity. + + if Is_Checked_Ghost_Entity (Id) then + Set_Is_Checked_Ghost_Pragma (N); + + elsif Is_Ignored_Ghost_Entity (Id) then + Set_Is_Ignored_Ghost_Pragma (N); + Set_Is_Ignored_Ghost_Node (N); + Propagate_Ignored_Ghost_Code (N); + end if; + end Mark_Ghost_Pragma; + + ------------------------- + -- Mark_Ghost_Renaming -- + ------------------------- + + procedure Mark_Ghost_Renaming + (N : Node_Id; + Id : Entity_Id) + is + Policy : Name_Id := No_Name; + + begin + -- A renaming becomes Ghost when it renames a Ghost entity + + if Is_Checked_Ghost_Entity (Id) then + Policy := Name_Check; + + elsif Is_Ignored_Ghost_Entity (Id) then + Policy := Name_Ignore; end if; - end Mark_Renaming_As_Ghost; + + Mark_Ghost_Declaration_Or_Body (N, Policy); + end Mark_Ghost_Renaming; ---------------------------------- -- Propagate_Ignored_Ghost_Code -- @@ -1091,7 +1483,7 @@ package body Ghost is Scop : Entity_Id; begin - -- Traverse the parent chain looking for blocks, packages and + -- Traverse the parent chain looking for blocks, packages, and -- subprograms or their respective bodies. Nod := Parent (N); @@ -1187,17 +1579,6 @@ package body Ghost is Prune (N); return Skip; - -- A freeze node for an ignored ghost entity must be pruned as - -- well, to prevent meaningless references in the back end. - - -- ??? the freeze node itself should be ignored ghost - - elsif Nkind (N) = N_Freeze_Entity - and then Is_Ignored_Ghost_Entity (Entity (N)) - then - Prune (N); - return Skip; - -- Scoping constructs such as blocks, packages, subprograms and -- bodies offer some flexibility with respect to pruning. @@ -1249,134 +1630,102 @@ package body Ghost is end loop; end Remove_Ignored_Ghost_Code; + ------------------------ + -- Restore_Ghost_Mode -- + ------------------------ + + procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type) is + begin + Ghost_Mode := Mode; + end Restore_Ghost_Mode; + -------------------- -- Set_Ghost_Mode -- -------------------- - 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 Ent_Id. - - procedure Set_From_Policy; - -- Set the value of global variable Ghost_Mode depending on the current - -- Ghost policy in effect. - - --------------------- - -- Set_From_Entity -- - --------------------- - - procedure Set_From_Entity (Ent_Id : Entity_Id) is - begin - 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_From_Entity; + procedure Set_Ghost_Mode + (N : Node_Or_Entity_Id; + Mode : out Ghost_Mode_Type) + is + procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); + -- Install the Ghost mode of entity Id - --------------------- - -- Set_From_Policy -- - --------------------- - - procedure Set_From_Policy is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + -------------------------------- + -- Set_Ghost_Mode_From_Entity -- + -------------------------------- + procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is begin - if Policy = Name_Check then - Ghost_Mode := Check; - - elsif Policy = Name_Ignore then - Ghost_Mode := Ignore; - - Set_Is_Ignored_Ghost_Node (N); - Propagate_Ignored_Ghost_Code (N); + if Is_Checked_Ghost_Entity (Id) then + Install_Ghost_Mode (Check); + elsif Is_Ignored_Ghost_Entity (Id) then + Install_Ghost_Mode (Ignore); + else + Install_Ghost_Mode (None); end if; - end Set_From_Policy; + end Set_Ghost_Mode_From_Entity; -- Local variables - Nam_Id : Entity_Id; + Id : Entity_Id; -- Start of processing for Set_Ghost_Mode begin - -- The input node denotes one of the many declaration kinds that may be - -- subject to pragma Ghost. - - if Is_Declaration (N) then - if Is_Subject_To_Ghost (N) then - Set_From_Policy; + -- Save the previous Ghost mode in effect - -- The declaration denotes the completion of a deferred constant, - -- pragma Ghost appears on the partial declaration. + Mode := Ghost_Mode; - elsif Nkind (N) = N_Object_Declaration - and then Constant_Present (N) - and then Present (Id) - then - Set_From_Entity (Id); + -- The Ghost mode of an assignment statement depends on the Ghost mode + -- of the target. - -- The declaration denotes the full view of a private type, pragma - -- Ghost appears on the partial declaration. + if Nkind (N) = N_Assignment_Statement then + Id := Ghost_Entity (Name (N)); - elsif Nkind (N) = N_Full_Type_Declaration - and then Is_Private_Type (Defining_Entity (N)) - and then Present (Id) - then - Set_From_Entity (Id); + if Present (Id) then + Set_Ghost_Mode_From_Entity (Id); end if; - -- The input denotes an assignment or a procedure call. In this case - -- the Ghost mode is dictated by the name of the construct. + -- The Ghost mode of a body or a declaration depends on the Ghost mode + -- of its defining entity. - elsif Nkind_In (N, N_Assignment_Statement, - N_Procedure_Call_Statement) - then - Nam_Id := Ghost_Entity (Name (N)); + elsif Is_Body (N) or else Is_Declaration (N) then + Set_Ghost_Mode_From_Entity (Defining_Entity (N)); - if Present (Nam_Id) then - Set_From_Entity (Nam_Id); - end if; + -- The Ghost mode of an entity depends on the entity itself - -- The input denotes a package or subprogram body + elsif Nkind (N) in N_Entity then + Set_Ghost_Mode_From_Entity (N); - elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then - if (Present (Id) and then Is_Ghost_Entity (Id)) - or else Is_Subject_To_Ghost (N) - then - Set_From_Policy; - end if; + -- The Ghost mode of a [generic] freeze node depends on the Ghost mode + -- of the entity being frozen. + + elsif Nkind_In (N, N_Freeze_Entity, N_Freeze_Generic_Entity) then + Set_Ghost_Mode_From_Entity (Entity (N)); - -- The input denotes a pragma + -- The Ghost mode of a pragma depends on the associated entity. The + -- property is encoded in the pragma itself. - elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then - if Is_Ignored_Ghost_Node (N) then - Ghost_Mode := Ignore; + elsif Nkind (N) = N_Pragma then + if Is_Checked_Ghost_Pragma (N) then + Install_Ghost_Mode (Check); + elsif Is_Ignored_Ghost_Pragma (N) then + Install_Ghost_Mode (Ignore); else - Ghost_Mode := Check; + Install_Ghost_Mode (None); end if; - -- The input denotes a freeze node + -- The Ghost mode of a procedure call depends on the Ghost mode of the + -- procedure being invoked. - elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then - Set_From_Entity (Id); - end if; - end Set_Ghost_Mode; + elsif Nkind (N) = N_Procedure_Call_Statement then + Id := Ghost_Entity (Name (N)); - -------------------------------- - -- Set_Ghost_Mode_From_Entity -- - -------------------------------- - - procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is - begin - if Is_Checked_Ghost_Entity (Id) then - Ghost_Mode := Check; - elsif Is_Ignored_Ghost_Entity (Id) then - Ghost_Mode := Ignore; + if Present (Id) then + Set_Ghost_Mode_From_Entity (Id); + end if; end if; - end Set_Ghost_Mode_From_Entity; + end Set_Ghost_Mode; ------------------------- -- Set_Is_Ghost_Entity -- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 7a0aec3906c..d5f11dfd6fd 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-2016, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -26,6 +26,7 @@ -- This package contains routines that deal with the static and runtime -- semantics of Ghost entities. +with Opt; use Opt; with Types; use Types; package Ghost is @@ -35,13 +36,15 @@ package Ghost is -- post processing. procedure Check_Ghost_Completion - (Partial_View : Entity_Id; - Full_View : Entity_Id); - -- Verify that the Ghost policy of a full view or a completion is the same - -- as the Ghost policy of the partial view. Emit an error if this is not - -- the case. - - procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id); + (Prev_Id : Entity_Id; + Compl_Id : Entity_Id); + -- Verify that the Ghost policy of initial entity Prev_Id is compatible + -- with the Ghost policy of completing entity Compl_Id. Emit an error if + -- this is not the case. + + procedure Check_Ghost_Context + (Ghost_Id : Entity_Id; + Ghost_Ref : Node_Id); -- Determine whether node Ghost_Ref appears within a Ghost-friendly context -- where Ghost entity Ghost_Id can safely reside. @@ -71,70 +74,149 @@ package Ghost is procedure Initialize; -- Initialize internal tables - procedure Lock; - -- Lock internal tables before calling backend + procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); + -- Set the value of global variable Ghost_Mode depending on the Ghost + -- policy denoted by Mode. - 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. + function Is_Ghost_Assignment (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes an assignment statement whose + -- target is a Ghost entity. - 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. + function Is_Ghost_Declaration (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a declaration which defines + -- 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. + function Is_Ghost_Pragma (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a pragma which encloses a + -- Ghost entity or is associated with a Ghost entity. - procedure Remove_Ignored_Ghost_Code; - -- Remove all code marked as ignored Ghost from the trees of all qualifying - -- units (SPARK RM 6.9(4)). - -- - -- WARNING: this is a separate front end pass, care should be taken to keep - -- it optimized. + function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a procedure call invoking a + -- Ghost procedure. - procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty); - -- Set the value of global variable Ghost_Mode depending on the following - -- scenarios: + procedure Lock; + -- Lock internal tables before calling backend + + procedure Mark_And_Set_Ghost_Assignment + (N : Node_Id; + Mode : out Ghost_Mode_Type); + -- Mark assignment statement N as Ghost when: + -- + -- * The left hand side denotes a Ghost entity + -- + -- Install the Ghost mode of the assignment statement. Mode is the Ghost + -- mode in effect prior to processing the assignment. This routine starts + -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Body + (N : Node_Id; + Spec_Id : Entity_Id; + Mode : out Ghost_Mode_Type); + -- Mark package or subprogram body N as Ghost when: + -- + -- * The body is subject to pragma Ghost + -- + -- * The body completes a previous declaration whose spec denoted by + -- Spec_Id is a Ghost entity. + -- + -- * The body appears within a Ghost region -- - -- If N is a declaration, determine whether N is subject to pragma Ghost. - -- If this is the case, the Ghost_Mode is set based on the current Ghost - -- policy in effect. Special cases: + -- Install the Ghost mode of the body. Mode is the Ghost mode prior to + -- processing the body. This routine starts a Ghost region and must be + -- used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Completion + (N : Node_Id; + Prev_Id : Entity_Id; + Mode : out Ghost_Mode_Type); + -- Mark completion N of a deferred constant or private type [extension] + -- Ghost when: -- - -- N is the completion of a deferred constant, the Ghost_Mode is set - -- based on the mode of partial declaration entity denoted by Id. + -- * The entity of the previous declaration denoted by Prev_Id is Ghost -- - -- 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. + -- * The completion appears within a Ghost region -- - -- If N is an assignment statement or a procedure call, the Ghost_Mode is - -- set based on the mode of the name. + -- Install the Ghost mode of the completion. Mode is the Ghost mode prior + -- to processing the completion. This routine starts a Ghost region and + -- must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Declaration + (N : Node_Id; + Mode : out Ghost_Mode_Type); + -- Mark declaration N as Ghost when: -- - -- 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. + -- * The declaration is subject to pragma Ghost -- - -- If N is a pragma, the Ghost_Mode is set based on the mode of the - -- pragma. + -- * The declaration denotes a child package or subprogram and the parent + -- is a Ghost unit. -- - -- If N is a freeze node, the Global_Mode is set based on the mode of - -- entity Id. + -- * The declaration appears within a Ghost region -- - -- 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. + -- Install the Ghost mode of the declaration. Mode is the Ghost mode prior + -- to processing the declaration. This routine starts a Ghost region and + -- must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Instantiation + (N : Node_Id; + Gen_Id : Entity_Id; + Mode : out Ghost_Mode_Type); + -- Mark instantiation N as Ghost when: + -- + -- * The instantiation is subject to pragma Ghost + -- + -- * The generic template denoted by Gen_Id is Ghost + -- + -- * The instantiation appears within a Ghost region + -- + -- Install the Ghost mode of the instantiation. Mode is the Ghost mode + -- prior to processing the instantiation. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Procedure_Call + (N : Node_Id; + Mode : out Ghost_Mode_Type); + -- Mark procedure call N as Ghost when: + -- + -- * The procedure being invoked is a Ghost entity + -- + -- Install the Ghost mode of the procedure call. Mode is the Ghost mode + -- prior to processing the procedure call. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_Ghost_Pragma + (N : Node_Id; + Id : Entity_Id); + -- Mark pragma N as Ghost when: + -- + -- * The pragma encloses Ghost entity Id + -- + -- * The pragma is associated with Ghost entity Id - procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); - -- Set the valye of global variable Ghost_Mode depending on the mode of - -- entity Id. + procedure Mark_Ghost_Renaming + (N : Node_Id; + Id : Entity_Id); + -- Mark renaming declaration N as Ghost when: -- - -- 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. + -- * Renamed entity Id denotes a Ghost entity + + procedure Remove_Ignored_Ghost_Code; + -- Remove all code marked as ignored Ghost from the trees of all qualifying + -- units (SPARK RM 6.9(4)). + -- + -- WARNING: this is a separate front end pass, care should be taken to keep + -- it optimized. + + procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type); + -- Terminate a Ghost region by restoring the Ghost mode prior to the + -- region denoted by Mode. This routine must be used in conjunction + -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode. + + procedure Set_Ghost_Mode + (N : Node_Or_Entity_Id; + Mode : out Ghost_Mode_Type); + -- Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior + -- to processing the node. This routine starts a Ghost region and must be + -- used in conjunction with Restore_Ghost_Mode. procedure Set_Is_Ghost_Entity (Id : Entity_Id); -- Set the relevant Ghost attributes of entity Id depending on the current diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index a9700f64b43..75d6e3904b4 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -98,7 +98,8 @@ package body Sem is ------------- procedure Analyze (N : Node_Id) is - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Mode : Ghost_Mode_Type; + Mode_Set : Boolean := False; begin Debug_A_Entry ("analyzing ", N); @@ -115,7 +116,8 @@ package body Sem is -- marked as Ghost. if Is_Declaration (N) then - Set_Ghost_Mode (N); + Mark_And_Set_Ghost_Declaration (N, Mode); + Mode_Set := True; end if; -- Otherwise processing depends on the node kind @@ -747,7 +749,9 @@ package body Sem is Expand_SPARK_Potential_Renaming (N); end if; - Ghost_Mode := Save_Ghost_Mode; + if Mode_Set then + Restore_Ghost_Mode (Mode); + end if; end Analyze; -- Version with check(s) suppressed @@ -1351,7 +1355,7 @@ package body Sem is -- Set up a clean environment before analyzing - Ghost_Mode := None; + Install_Ghost_Mode (None); Outer_Generic_Scope := Empty; Scope_Suppress := Suppress_Options; Scope_Stack.Table @@ -1373,7 +1377,7 @@ package body Sem is Pop_Scope; Restore_Scope_Stack (List); - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Save_Ghost_Mode); Style_Max_Line_Length := Save_Max_Line; end Do_Analyze; diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 381972d1fb4..3e71b543c97 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -27,7 +27,6 @@ with Atree; use Atree; with Checks; use Checks; with Einfo; use Einfo; with Errout; use Errout; -with Ghost; use Ghost; with Lib; use Lib; with Lib.Xref; use Lib.Xref; with Namet; use Namet; @@ -67,13 +66,6 @@ package body Sem_Ch11 is Set_Is_Statically_Allocated (Id); Set_Is_Pure (Id, PF); - -- An exception declared within a Ghost region is automatically Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; - if Has_Aspects (N) then Analyze_Aspect_Specifications (N, Id); end if; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 603c5433d78..89b5586a5ff 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3331,13 +3331,6 @@ package body Sem_Ch12 is Set_Ekind (Id, E_Generic_Package); Set_Etype (Id, Standard_Void_Type); - -- A generic package declared within a Ghost region is rendered Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; - -- Analyze aspects now, so that generated pragmas appear in the -- declarations before building and analyzing the generic copy. @@ -3548,13 +3541,6 @@ package body Sem_Ch12 is Set_Etype (Id, Standard_Void_Type); end if; - -- A generic subprogram declared within a Ghost region is rendered Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; - -- For a library unit, we have reconstructed the entity for the unit, -- and must reset it in the library tables. We also make sure that -- Body_Required is set properly in the original compilation unit node. @@ -3676,6 +3662,8 @@ package body Sem_Ch12 is -- Local declarations + Mode : Ghost_Mode_Type; + Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation -- to match the visibility of the formal type @@ -3746,6 +3734,13 @@ package body Sem_Ch12 is Check_Generic_Child_Unit (Gen_Id, Parent_Installed); Gen_Unit := Entity (Gen_Id); + -- A package instantiation is Ghost when it is subject to pragma Ghost + -- or the generic template is Ghost. Set the mode now to ensure that + -- any nodes generated during analysis and expansion are marked as + -- Ghost. + + Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode); + -- Verify that it is the name of a generic package -- A visibility glitch: if the instance is a child unit and the generic @@ -4437,6 +4432,8 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Act_Decl_Id); end if; + Restore_Ghost_Mode (Mode); + exception when Instantiation_Error => if Parent_Installed then @@ -4451,6 +4448,8 @@ package body Sem_Ch12 is SPARK_Mode := Save_SM; SPARK_Mode_Pragma := Save_SMP; Style_Check := Save_Style_Check; + + Restore_Ghost_Mode (Mode); end Analyze_Package_Instantiation; -------------------------- @@ -5084,6 +5083,8 @@ package body Sem_Ch12 is -- Local variables + Mode : Ghost_Mode_Type; + Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit @@ -5126,6 +5127,13 @@ package body Sem_Ch12 is Check_Generic_Child_Unit (Gen_Id, Parent_Installed); Gen_Unit := Entity (Gen_Id); + -- A subprogram instantiation is Ghost when it is subject to pragma + -- Ghost or the generic template is Ghost. Set the mode now to ensure + -- that any nodes generated during analysis and expansion are marked as + -- Ghost. + + Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode); + Generate_Reference (Gen_Unit, Gen_Id); if Nkind (Gen_Id) = N_Identifier @@ -5137,7 +5145,7 @@ package body Sem_Ch12 is if Etype (Gen_Unit) = Any_Type then Restore_Env; - return; + goto Leave; end if; -- Verify that it is a generic subprogram of the right kind, and that @@ -5322,8 +5330,8 @@ package body Sem_Ch12 is Error_Msg_NE ("access parameter& is controlling,", N, Formal); Error_Msg_NE - ("\corresponding parameter of & must be " - & "explicitly null-excluding", N, Gen_Id); + ("\corresponding parameter of & must be explicitly " + & "null-excluding", N, Gen_Id); end if; Next_Formal (Formal); @@ -5386,6 +5394,8 @@ package body Sem_Ch12 is Analyze_Aspect_Specifications (N, Act_Decl_Id); end if; + Restore_Ghost_Mode (Mode); + exception when Instantiation_Error => if Parent_Installed then @@ -5399,6 +5409,8 @@ package body Sem_Ch12 is Ignore_Pragma_SPARK_Mode := Save_IPSM; SPARK_Mode := Save_SM; SPARK_Mode_Pragma := Save_SMP; + + Restore_Ghost_Mode (Mode); end Analyze_Subprogram_Instantiation; ------------------------- @@ -10780,32 +10792,17 @@ package body Sem_Ch12 is Body_Optional : Boolean := False) is Act_Decl : constant Node_Id := Body_Info.Act_Decl; + Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl); + Act_Spec : constant Node_Id := Specification (Act_Decl); Inst_Node : constant Node_Id := Body_Info.Inst_Node; - Loc : constant Source_Ptr := Sloc (Inst_Node); - Gen_Id : constant Node_Id := Name (Inst_Node); Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node); Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); - Act_Spec : constant Node_Id := Specification (Act_Decl); - Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec); + Loc : constant Source_Ptr := Sloc (Inst_Node); Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; Save_Style_Check : constant Boolean := Style_Check; - Act_Body : Node_Id; - Act_Body_Id : Entity_Id; - Act_Body_Name : Node_Id; - Gen_Body : Node_Id; - Gen_Body_Id : Node_Id; - Par_Ent : Entity_Id := Empty; - Par_Vis : Boolean := False; - - Parent_Installed : Boolean := False; - - Vis_Prims_List : Elist_Id := No_Elist; - -- List of primitives made temporarily visible in the instantiation - -- to match the visibility of the formal type - procedure Check_Initialized_Types; -- In a generic package body, an entity of a generic private type may -- appear uninitialized. This is suspicious, unless the actual is a @@ -10874,6 +10871,23 @@ package body Sem_Ch12 is end loop; end Check_Initialized_Types; + -- Local variables + + Act_Body : Node_Id; + Act_Body_Id : Entity_Id; + Act_Body_Name : Node_Id; + Gen_Body : Node_Id; + Gen_Body_Id : Node_Id; + Mode : Ghost_Mode_Type; + Par_Ent : Entity_Id := Empty; + Par_Vis : Boolean := False; + + Parent_Installed : Boolean := False; + + Vis_Prims_List : Elist_Id := No_Elist; + -- List of primitives made temporarily visible in the instantiation + -- to match the visibility of the formal type. + -- Start of processing for Instantiate_Package_Body begin @@ -10886,6 +10900,12 @@ package body Sem_Ch12 is return; end if; + -- The package being instantiated may be subject to pragma Ghost. Set + -- the mode now to ensure that any nodes generated during instantiation + -- are properly marked as Ghost. + + Set_Ghost_Mode (Act_Decl_Id, Mode); + Expander_Mode_Save_And_Set (Body_Info.Expander_Status); -- Re-establish the state of information on which checks are suppressed. @@ -10911,7 +10931,7 @@ package body Sem_Ch12 is if not Unit_Requires_Body (Defining_Entity (Gen_Decl)) and then Body_Optional then - return; + goto Leave; else Load_Parent_Of_Generic (Inst_Node, Specification (Gen_Decl), Body_Optional); @@ -11175,6 +11195,9 @@ package body Sem_Ch12 is end if; Expander_Mode_Restore; + + <> + Restore_Ghost_Mode (Mode); end Instantiate_Package_Body; --------------------------------- @@ -11186,13 +11209,12 @@ package body Sem_Ch12 is Body_Optional : Boolean := False) is Act_Decl : constant Node_Id := Body_Info.Act_Decl; + Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl); Inst_Node : constant Node_Id := Body_Info.Inst_Node; - Loc : constant Source_Ptr := Sloc (Inst_Node); Gen_Id : constant Node_Id := Name (Inst_Node); Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node); Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); - Act_Decl_Id : constant Entity_Id := - Defining_Unit_Name (Specification (Act_Decl)); + Loc : constant Source_Ptr := Sloc (Inst_Node); Pack_Id : constant Entity_Id := Defining_Unit_Name (Parent (Act_Decl)); @@ -11204,6 +11226,7 @@ package body Sem_Ch12 is Act_Body_Id : Entity_Id; Gen_Body : Node_Id; Gen_Body_Id : Node_Id; + Mode : Ghost_Mode_Type; Pack_Body : Node_Id; Par_Ent : Entity_Id := Empty; Par_Vis : Boolean := False; @@ -11222,6 +11245,12 @@ package body Sem_Ch12 is return; end if; + -- The subprogram being instantiated may be subject to pragma Ghost. Set + -- the mode now to ensure that any nodes generated during instantiation + -- are properly marked as Ghost. + + Set_Ghost_Mode (Act_Decl_Id, Mode); + Expander_Mode_Save_And_Set (Body_Info.Expander_Status); -- Re-establish the state of information on which checks are suppressed. @@ -11248,7 +11277,7 @@ package body Sem_Ch12 is Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit)); Set_Convention (Act_Decl_Id, Convention (Gen_Unit)); Set_Has_Completion (Act_Decl_Id); - return; + goto Leave; -- For other cases, compile the body @@ -11273,12 +11302,11 @@ package body Sem_Ch12 is if Expander_Active and then Operating_Mode = Generate_Code then - Error_Msg_N - ("missing proper body for instantiation", Gen_Body); + Error_Msg_N ("missing proper body for instantiation", Gen_Body); end if; Set_Has_Completion (Act_Decl_Id); - return; + goto Leave; end if; Save_Env (Gen_Unit, Act_Decl_Id); @@ -11410,27 +11438,25 @@ package body Sem_Ch12 is and then Nkind (Parent (Inst_Node)) /= N_Compilation_Unit then if Body_Optional then - return; + goto Leave; elsif Ekind (Act_Decl_Id) = E_Procedure then Act_Body := Make_Subprogram_Body (Loc, - Specification => - Make_Procedure_Specification (Loc, - Defining_Unit_Name => - Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)), - Parameter_Specifications => - New_Copy_List - (Parameter_Specifications (Parent (Act_Decl_Id)))), - - Declarations => Empty_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => - New_List ( - Make_Raise_Program_Error (Loc, - Reason => - PE_Access_Before_Elaboration)))); + Specification => + Make_Procedure_Specification (Loc, + Defining_Unit_Name => + Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)), + Parameter_Specifications => + New_Copy_List + (Parameter_Specifications (Parent (Act_Decl_Id)))), + + Declarations => Empty_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List ( + Make_Raise_Program_Error (Loc, + Reason => PE_Access_Before_Elaboration)))); else Ret_Expr := @@ -11444,9 +11470,9 @@ package body Sem_Ch12 is Make_Subprogram_Body (Loc, Specification => Make_Function_Specification (Loc, - Defining_Unit_Name => + Defining_Unit_Name => Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)), - Parameter_Specifications => + Parameter_Specifications => New_Copy_List (Parameter_Specifications (Parent (Act_Decl_Id))), Result_Definition => @@ -11455,9 +11481,8 @@ package body Sem_Ch12 is Declarations => Empty_List, Handled_Statement_Sequence => Make_Handled_Sequence_Of_Statements (Loc, - Statements => - New_List - (Make_Simple_Return_Statement (Loc, Ret_Expr)))); + Statements => New_List ( + Make_Simple_Return_Statement (Loc, Ret_Expr)))); end if; Pack_Body := @@ -11471,6 +11496,9 @@ package body Sem_Ch12 is end if; Expander_Mode_Restore; + + <> + Restore_Ghost_Mode (Mode); end Instantiate_Subprogram_Body; ---------------------- diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index a88f8486d80..bb57ad07b71 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -8524,7 +8524,7 @@ package body Sem_Ch13 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Mode : Ghost_Mode_Type; -- Start of processing for Build_Predicate_Functions @@ -8541,7 +8541,7 @@ package body Sem_Ch13 is -- The related type may be subject to pragma Ghost. Set the mode now to -- ensure that the predicate functions are properly marked as Ghost. - Set_Ghost_Mode_From_Entity (Typ); + Set_Ghost_Mode (Typ, Mode); -- Prepare to construct predicate expression @@ -8647,20 +8647,12 @@ package body Sem_Ch13 is FBody : Node_Id; begin - -- The predicate function is shared between views of a type if Is_Private_Type (Typ) and then Present (Full_View (Typ)) then 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; - -- Build function body Spec := @@ -8743,13 +8735,6 @@ 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, @@ -8902,7 +8887,7 @@ package body Sem_Ch13 is end; end if; - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Mode); end Build_Predicate_Functions; ------------------------------------------ @@ -8914,45 +8899,45 @@ package body Sem_Ch13 is is Loc : constant Source_Ptr := Sloc (Typ); - Object_Entity : constant Entity_Id := - Make_Defining_Identifier (Loc, - Chars => New_Internal_Name ('I')); - - -- The formal parameter of the function + Func_Decl : Node_Id; + Func_Id : Entity_Id; + Mode : Ghost_Mode_Type; + Spec : Node_Id; - SId : constant Entity_Id := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (Typ), "Predicate")); + begin + -- The related type may be subject to pragma Ghost. Set the mode now to + -- ensure that the predicate functions are properly marked as Ghost. - -- The entity for the function spec + Set_Ghost_Mode (Typ, Mode); - FDecl : Node_Id; - Spec : Node_Id; + Func_Id := + Make_Defining_Identifier (Loc, + Chars => New_External_Name (Chars (Typ), "Predicate")); - begin Spec := Make_Function_Specification (Loc, - Defining_Unit_Name => SId, + Defining_Unit_Name => Func_Id, Parameter_Specifications => New_List ( Make_Parameter_Specification (Loc, - Defining_Identifier => Object_Entity, + Defining_Identifier => Make_Temporary (Loc, 'I'), Parameter_Type => New_Occurrence_Of (Typ, Loc))), Result_Definition => New_Occurrence_Of (Standard_Boolean, Loc)); - FDecl := Make_Subprogram_Declaration (Loc, Specification => Spec); + Func_Decl := Make_Subprogram_Declaration (Loc, Specification => Spec); - Set_Ekind (SId, E_Function); - Set_Etype (SId, Standard_Boolean); - Set_Is_Internal (SId); - Set_Is_Predicate_Function (SId); - Set_Predicate_Function (Typ, SId); + Set_Ekind (Func_Id, E_Function); + Set_Etype (Func_Id, Standard_Boolean); + Set_Is_Internal (Func_Id); + Set_Is_Predicate_Function (Func_Id); + Set_Predicate_Function (Typ, Func_Id); - Insert_After (Parent (Typ), FDecl); + Insert_After (Parent (Typ), Func_Decl); + Analyze (Func_Decl); - Analyze (FDecl); + Restore_Ghost_Mode (Mode); - return FDecl; + return Func_Decl; end Build_Predicate_Function_Declaration; ----------------------------------------- diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index ec47142644e..99d8b58982e 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2824,13 +2824,6 @@ package body Sem_Ch3 is if not Analyzed (T) then Set_Analyzed (T); - -- A type declared within a Ghost region is automatically Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (T); - end if; - case Nkind (Def) is when N_Access_To_Subprogram_Definition => Access_Subprogram_Declaration (T, Def); @@ -3072,13 +3065,6 @@ package body Sem_Ch3 is Set_Is_First_Subtype (T, True); Set_Etype (T, T); - -- An incomplete type declared within a Ghost region is automatically - -- Ghost (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (T); - end if; - -- Ada 2005 (AI-326): Minimum decoration to give support to tagged -- incomplete types. @@ -3186,13 +3172,6 @@ package body Sem_Ch3 is Generate_Definition (Id); Enter_Name (Id); - -- A number declared within a Ghost region is automatically Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; - -- This is an optimization of a common case of an integer literal if Nkind (E) = N_Integer_Literal then @@ -3435,8 +3414,9 @@ package body Sem_Ch3 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Related_Id : Entity_Id; + Mode : Ghost_Mode_Type; + Mode_Set : Boolean := False; + Related_Id : Entity_Id; -- Start of processing for Analyze_Object_Declaration @@ -3501,14 +3481,14 @@ package body Sem_Ch3 is end if; end if; - -- The object declaration is Ghost when it is subject to pragma Ghost or - -- completes a deferred Ghost constant. Set the mode now to ensure that - -- any nodes generated during analysis and expansion are properly marked - -- as Ghost. + if Present (Prev_Entity) then + + -- The object declaration is Ghost when it completes a deferred Ghost + -- constant. - Set_Ghost_Mode (N, Prev_Entity); + Mark_And_Set_Ghost_Completion (N, Prev_Entity, Mode); + Mode_Set := True; - if Present (Prev_Entity) then Constant_Redeclaration (Id, N, T); Generate_Reference (Prev_Entity, Id, 'c'); @@ -3802,8 +3782,7 @@ package body Sem_Ch3 is and then Analyzed (N) and then No (Expression (N)) then - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; -- If E is null and has been replaced by an N_Raise_Constraint_Error @@ -4061,23 +4040,6 @@ package body Sem_Ch3 is Set_Ekind (Id, E_Variable); end if; - -- An object declared within a Ghost region is automatically - -- Ghost (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - - -- The Ghost policy in effect at the point of declaration - -- and at the point of completion must match - -- (SPARK RM 6.9(14)). - - if Present (Prev_Entity) - and then Is_Ghost_Entity (Prev_Entity) - then - Check_Ghost_Completion (Prev_Entity, Id); - end if; - end if; - Rewrite (N, Make_Object_Renaming_Declaration (Loc, Defining_Identifier => Id, @@ -4087,9 +4049,7 @@ package body Sem_Ch3 is Set_Renamed_Object (Id, E); Freeze_Before (N, T); Set_Is_Frozen (Id); - - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; else -- Ensure that the generated subtype has a unique external name @@ -4263,22 +4223,6 @@ package body Sem_Ch3 is Init_Esize (Id); Set_Optimize_Alignment_Flags (Id); - -- An object declared within a Ghost region is automatically Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None - or else (Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity)) - then - Set_Is_Ghost_Entity (Id); - - -- The Ghost policy in effect at the point of declaration and at the - -- point of completion must match (SPARK RM 6.9(14)). - - if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then - Check_Ghost_Completion (Prev_Entity, Id); - end if; - end if; - -- Deal with aliased case if Aliased_Present (N) then @@ -4481,7 +4425,9 @@ package body Sem_Ch3 is Check_No_Hidden_State (Id); end if; - Ghost_Mode := Save_Ghost_Mode; + if Mode_Set then + Restore_Ghost_Mode (Mode); + end if; end Analyze_Object_Declaration; --------------------------- @@ -5501,13 +5447,13 @@ package body Sem_Ch3 is procedure Array_Type_Declaration (T : in out Entity_Id; Def : Node_Id) is Component_Def : constant Node_Id := Component_Definition (Def); Component_Typ : constant Node_Id := Subtype_Indication (Component_Def); + P : constant Node_Id := Parent (Def); Element_Type : Entity_Id; Implicit_Base : Entity_Id; Index : Node_Id; - Related_Id : Entity_Id := Empty; Nb_Index : Nat; - P : constant Node_Id := Parent (Def); Priv : Entity_Id; + Related_Id : Entity_Id := Empty; begin if Nkind (Def) = N_Constrained_Array_Definition then @@ -5563,8 +5509,8 @@ package body Sem_Ch3 is then declare Loc : constant Source_Ptr := Sloc (Def); - New_E : Entity_Id; Decl : Entity_Id; + New_E : Entity_Id; begin New_E := Make_Temporary (Loc, 'T'); @@ -5705,12 +5651,6 @@ package body Sem_Ch3 is Propagate_Concurrent_Flags (Implicit_Base, Element_Type); - -- Inherit the "ghostness" from the constrained array type - - if Ghost_Mode > None or else Is_Ghost_Entity (T) then - Set_Is_Ghost_Entity (Implicit_Base); - end if; - -- Unconstrained array case else @@ -6188,12 +6128,6 @@ package body Sem_Ch3 is Copy_Array_Base_Type_Attributes (Implicit_Base, Parent_Base); Set_Has_Delayed_Freeze (Implicit_Base, True); - - -- Inherit the "ghostness" from the parent base type - - if Ghost_Mode > None or else Is_Ghost_Entity (Parent_Base) then - Set_Is_Ghost_Entity (Implicit_Base); - end if; end Make_Implicit_Base; -- Start of processing for Build_Derived_Array_Type @@ -9132,7 +9066,7 @@ package body Sem_Ch3 is -- (anonymous) base type. if Has_Predicates (Parent_Type) - or else Has_Predicates (First_Subtype (Parent_Type)) + or else Has_Predicates (First_Subtype (Parent_Type)) then Set_Has_Predicates (Derived_Type); end if; @@ -9148,8 +9082,9 @@ package body Sem_Ch3 is Set_May_Inherit_Delayed_Rep_Aspects (Derived_Type); end if; - -- Propagate the attributes related to pragma Ghost from the parent type - -- to the derived type or type extension (SPARK RM 6.9(9)). + -- A derived type becomes Ghost when its parent type is also Ghost + -- (SPARK RM 6.9(9)). Note that the Ghost-related attributes are not + -- directly inherited because the Ghost policy in effect may differ. if Is_Ghost_Entity (Parent_Type) then Set_Is_Ghost_Entity (Derived_Type); @@ -14936,12 +14871,6 @@ package body Sem_Ch3 is Set_Alias (New_Subp, Actual_Subp); end if; - -- Inherit the "ghostness" from the parent subprogram - - if Is_Ghost_Entity (Alias (New_Subp)) then - Set_Is_Ghost_Entity (New_Subp); - end if; - -- Derived subprograms of a tagged type must inherit the convention -- of the parent subprogram (a requirement of AI-117). Derived -- subprograms of untagged types simply get convention Ada by default. @@ -18346,12 +18275,6 @@ package body Sem_Ch3 is -- The class-wide type of a class-wide type is itself (RM 3.9(14)) Set_Class_Wide_Type (CW_Type, CW_Type); - - -- Inherit the "ghostness" from the root tagged type - - if Ghost_Mode > None or else Is_Ghost_Entity (T) then - Set_Is_Ghost_Entity (CW_Type); - end if; end Make_Class_Wide_Type; ---------------- @@ -19584,11 +19507,14 @@ package body Sem_Ch3 is Full_Indic : Node_Id; Full_Parent : Entity_Id; + Mode : Ghost_Mode_Type; Priv_Parent : Entity_Id; -- Start of processing for Process_Full_View begin + Mark_And_Set_Ghost_Completion (N, Priv_T, Mode); + -- First some sanity checks that must be done after semantic -- decoration of the full view and thus cannot be placed with other -- similar checks in Find_Type_Name @@ -19701,7 +19627,7 @@ package body Sem_Ch3 is -- error situation [7.3(8)]. if Priv_Parent = Any_Type or else Full_Parent = Any_Type then - return; + goto Leave; -- Ada 2005 (AI-251): Interfaces in the full type can be given in -- any order. Therefore we don't have to check that its parent must @@ -20053,7 +19979,7 @@ package body Sem_Ch3 is Next_Elmt (Prim_Elmt); end loop; - return; + goto Leave; end; -- For non-concurrent types, transfer explicit primitives, but @@ -20190,19 +20116,6 @@ package body Sem_Ch3 is Set_Has_Specified_Stream_Output (Full_T); end if; - if Is_Ghost_Entity (Priv_T) then - - -- The Ghost policy in effect at the point of declaration and at the - -- point of completion must match (SPARK RM 6.9(14)). - - Check_Ghost_Completion (Priv_T, Full_T); - - -- 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 Default_Initial_Condition-related attributes from the -- partial view to the full view and its base type. @@ -20251,6 +20164,9 @@ package body Sem_Ch3 is Set_Predicate_Function (Full_T, Predicate_Function (Priv_T)); end if; end if; + + <> + Restore_Ghost_Mode (Mode); end Process_Full_View; ----------------------------------- diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index fefdbc31b2a..620b562bc2c 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -270,7 +270,7 @@ package body Sem_Ch5 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Mode : Ghost_Mode_Type; -- Start of processing for Analyze_Assignment @@ -287,7 +287,7 @@ package body Sem_Ch5 is -- Ghost entity. Set the mode now to ensure that any nodes generated -- during analysis and expansion are properly marked as Ghost. - Set_Ghost_Mode (N); + Mark_And_Set_Ghost_Assignment (N, Mode); Analyze (Rhs); -- Ensure that we never do an assignment on a variable marked as @@ -356,8 +356,8 @@ package body Sem_Ch5 is if PIt = No_Interp then Error_Msg_N - ("ambiguous left-hand side" - & " in assignment", Lhs); + ("ambiguous left-hand side in " + & "assignment", Lhs); exit; else Resolve (Prefix (Lhs), PIt.Typ); @@ -392,8 +392,7 @@ package body Sem_Ch5 is Error_Msg_N ("no valid types for left-hand side for assignment", Lhs); Kill_Lhs; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; end if; @@ -464,21 +463,20 @@ package body Sem_Ch5 is -- effect (AARM D.5.2 (5/2)). if Locking_Policy /= 'C' then - Error_Msg_N ("assignment to the attribute PRIORITY has " & - "no effect??", Lhs); - Error_Msg_N ("\since no Locking_Policy has been " & - "specified??", Lhs); + Error_Msg_N + ("assignment to the attribute PRIORITY has no effect??", + Lhs); + Error_Msg_N + ("\since no Locking_Policy has been specified??", Lhs); end if; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; end if; end; Diagnose_Non_Variable_Lhs (Lhs); - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; -- Error of assigning to limited type. We do however allow this in -- certain cases where the front end generates the assignments. @@ -497,17 +495,14 @@ package body Sem_Ch5 is Explain_Limited_Type (T1, Lhs); end if; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; -- A class-wide type may be a limited view. This illegal case is not -- caught by previous checks. - elsif Ekind (T1) = E_Class_Wide_Type - and then From_Limited_With (T1) - then + elsif Ekind (T1) = E_Class_Wide_Type and then From_Limited_With (T1) then Error_Msg_NE ("invalid use of limited view of&", Lhs, T1); - return; + goto Leave; -- Enforce RM 3.9.3 (8): the target of an assignment operation cannot be -- abstract. This is only checked when the assignment Comes_From_Source, @@ -545,8 +540,7 @@ package body Sem_Ch5 is then Error_Msg_N ("invalid use of incomplete type", Lhs); Kill_Lhs; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; -- Now we can complete the resolution of the right hand side @@ -563,8 +557,7 @@ package body Sem_Ch5 is if Rhs = Error then Kill_Lhs; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; T2 := Etype (Rhs); @@ -572,8 +565,7 @@ package body Sem_Ch5 is if not Covers (T1, T2) then Wrong_Type (Rhs, Etype (Lhs)); Kill_Lhs; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; -- Ada 2005 (AI-326): In case of explicit dereference of incomplete @@ -600,8 +592,7 @@ package body Sem_Ch5 is if T1 = Any_Type or else T2 = Any_Type then Kill_Lhs; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; -- If the rhs is class-wide or dynamically tagged, then require the lhs @@ -693,8 +684,7 @@ package body Sem_Ch5 is -- to reset Is_True_Constant, and desirable for xref purposes. Note_Possible_Modification (Lhs, Sure => True); - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; -- If we know the right hand side is non-null, then we convert to the -- target type, since we don't need a run time check in that case. @@ -914,7 +904,9 @@ package body Sem_Ch5 is end; Analyze_Dimension (N); - Ghost_Mode := Save_Ghost_Mode; + + <> + Restore_Ghost_Mode (Mode); end Analyze_Assignment; ----------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index b3e597f3d09..9d8792ac157 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -233,13 +233,6 @@ package body Sem_Ch6 is Set_Categorization_From_Scope (Subp_Id, Scop); - -- An abstract subprogram declared within a Ghost region is rendered - -- Ghost (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Subp_Id); - end if; - if Ekind (Scope (Subp_Id)) = E_Protected_Type then Error_Msg_N ("abstract subprogram not allowed in protected type", N); @@ -502,15 +495,6 @@ package body Sem_Ch6 is Set_Is_Inlined (Defining_Entity (N)); - -- If the expression function is Ghost, mark its body entity as - -- Ghost too. This avoids spurious errors on unanalyzed body entities - -- of expression functions, which are not yet marked as ghost, yet - -- identified as the Corresponding_Body of the ghost declaration. - - if Is_Ghost_Entity (Def_Id) then - Set_Is_Ghost_Entity (Defining_Entity (New_Body)); - end if; - -- Establish the linkages between the spec and the body. These are -- used when the expression function acts as the prefix of attribute -- 'Access in order to freeze the original expression which has been @@ -1264,19 +1248,6 @@ package body Sem_Ch6 is Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id)); Set_Scope (Body_Id, Scope (Gen_Id)); - -- Inherit the "ghostness" of the generic spec. Note that this - -- property is not directly inherited as the body may be subject - -- to a different Ghost assertion policy. - - if Ghost_Mode > None or else Is_Ghost_Entity (Gen_Id) then - Set_Is_Ghost_Entity (Body_Id); - - -- The Ghost policy in effect at the point of declaration and at - -- the point of completion must match (SPARK RM 6.9(14)). - - Check_Ghost_Completion (Gen_Id, Body_Id); - end if; - Check_Fully_Conformant (Body_Id, Gen_Id, Body_Id); if Nkind (N) = N_Subprogram_Body_Stub then @@ -1559,10 +1530,9 @@ package body Sem_Ch6 is Loc : constant Source_Ptr := Sloc (N); P : constant Node_Id := Name (N); Actual : Node_Id; + Mode : Ghost_Mode_Type; New_N : Node_Id; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - -- Start of processing for Analyze_Procedure_Call begin @@ -1604,7 +1574,7 @@ package body Sem_Ch6 is -- Set the mode now to ensure that any nodes generated during analysis -- and expansion are properly marked as Ghost. - Set_Ghost_Mode (N); + Mark_And_Set_Ghost_Procedure_Call (N, Mode); -- Otherwise analyze the parameters @@ -1628,7 +1598,7 @@ package body Sem_Ch6 is if Present (Actuals) then Error_Msg_N ("no parameters allowed for this call", First (Actuals)); - return; + goto Leave; end if; Set_Etype (N, Standard_Void_Type); @@ -1638,8 +1608,7 @@ package body Sem_Ch6 is and then Is_Record_Type (Etype (Entity (P))) and then Remote_AST_I_Dereference (P) then - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; elsif Is_Entity_Name (P) and then Ekind (Entity (P)) /= E_Entry_Family @@ -1775,7 +1744,8 @@ package body Sem_Ch6 is Error_Msg_N ("invalid procedure or entry call", N); end if; - Ghost_Mode := Save_Ghost_Mode; + <> + Restore_Ghost_Mode (Mode); end Analyze_Procedure_Call; ------------------------------ @@ -1783,9 +1753,8 @@ package body Sem_Ch6 is ------------------------------ procedure Analyze_Return_Statement (N : Node_Id) is - - pragma Assert (Nkind_In (N, N_Simple_Return_Statement, - N_Extended_Return_Statement)); + pragma Assert (Nkind_In (N, N_Extended_Return_Statement, + N_Simple_Return_Statement)); Returns_Object : constant Boolean := Nkind (N) = N_Extended_Return_Statement @@ -2489,12 +2458,7 @@ package body Sem_Ch6 is Body_Id := Analyze_Subprogram_Specification (Body_Spec); -- Ensure that the generated corresponding spec and original body - -- share the same Ghost and SPARK_Mode attributes. - - Set_Is_Checked_Ghost_Entity - (Body_Id, Is_Checked_Ghost_Entity (Spec_Id)); - Set_Is_Ignored_Ghost_Entity - (Body_Id, Is_Ignored_Ghost_Entity (Spec_Id)); + -- share the same SPARK_Mode attributes. Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id)); Set_SPARK_Pragma_Inherited @@ -3131,7 +3095,8 @@ package body Sem_Ch6 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Mode : Ghost_Mode_Type; + Mode_Set : Boolean := False; -- Start of processing for Analyze_Subprogram_Body_Helper @@ -3183,7 +3148,9 @@ package body Sem_Ch6 is -- the mode now to ensure that any nodes generated during analysis -- and expansion are properly marked as Ghost. - Set_Ghost_Mode (N, Spec_Id); + Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); + Mode_Set := True; + Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id)); Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id)); @@ -3194,15 +3161,13 @@ package body Sem_Ch6 is Check_Missing_Return; end if; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; - else - -- Previous entity conflicts with subprogram name. Attempting to - -- enter name will post error. + -- Otherwise a previous entity conflicts with the subprogram name. + -- Attempting to enter name will post error. + else Enter_Name (Body_Id); - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -3213,7 +3178,6 @@ package body Sem_Ch6 is -- analysis. elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then - Ghost_Mode := Save_Ghost_Mode; return; else @@ -3230,7 +3194,8 @@ package body Sem_Ch6 is -- Ghost. Set the mode now to ensure that any nodes generated -- during analysis and expansion are properly marked as Ghost. - Set_Ghost_Mode (N, Spec_Id); + Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); + Mode_Set := True; else Spec_Id := Find_Corresponding_Spec (N); @@ -3240,7 +3205,8 @@ package body Sem_Ch6 is -- Ghost. Set the mode now to ensure that any nodes generated -- during analysis and expansion are properly marked as Ghost. - Set_Ghost_Mode (N, Spec_Id); + Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); + Mode_Set := True; -- In GNATprove mode, if the body has no previous spec, create -- one so that the inlining machinery can operate properly. @@ -3304,8 +3270,7 @@ package body Sem_Ch6 is -- If this is a duplicate body, no point in analyzing it if Error_Posted (N) then - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; -- A subprogram body should cause freezing of its own declaration, @@ -3342,7 +3307,8 @@ package body Sem_Ch6 is -- the mode now to ensure that any nodes generated during analysis -- and expansion are properly marked as Ghost. - Set_Ghost_Mode (N, Spec_Id); + Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); + Mode_Set := True; end if; end if; @@ -3394,7 +3360,7 @@ package body Sem_Ch6 is -- function. Set_Is_Immediately_Visible (Corresponding_Spec (N), False); - return; + goto Leave; end if; -- If a separate spec is present, then deal with freezing issues @@ -3445,26 +3411,12 @@ package body Sem_Ch6 is if Is_Abstract_Subprogram (Spec_Id) then Error_Msg_N ("an abstract subprogram cannot have a body", N); - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; else Set_Convention (Body_Id, Convention (Spec_Id)); Set_Has_Completion (Spec_Id); - -- Inherit the "ghostness" of the subprogram spec. Note that this - -- property is not directly inherited as the body may be subject - -- to a different Ghost assertion policy. - - if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then - Set_Is_Ghost_Entity (Body_Id); - - -- The Ghost policy in effect at the point of declaration and - -- at the point of completion must match (SPARK RM 6.9(14)). - - Check_Ghost_Completion (Spec_Id, Body_Id); - end if; - if Is_Protected_Type (Scope (Spec_Id)) then Prot_Typ := Scope (Spec_Id); end if; @@ -3518,8 +3470,7 @@ package body Sem_Ch6 is if not Conformant and then not Mode_Conformant (Body_Id, Spec_Id) then - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; end if; @@ -3630,13 +3581,6 @@ package body Sem_Ch6 is New_Overloaded_Entity (Body_Id); - -- A subprogram body declared within a Ghost region is automatically - -- Ghost (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Body_Id); - end if; - if Nkind (N) /= N_Subprogram_Body_Stub then Set_Acts_As_Spec (N); Generate_Definition (Body_Id); @@ -3759,8 +3703,7 @@ package body Sem_Ch6 is Analyze_Aspect_Specifications_On_Body_Or_Stub (N); end if; - Ghost_Mode := Save_Ghost_Mode; - return; + goto Leave; end if; -- Handle inlining @@ -4182,7 +4125,8 @@ package body Sem_Ch6 is -- Check for variables that are never modified declare - E1, E2 : Entity_Id; + E1 : Entity_Id; + E2 : Entity_Id; begin -- If there is a separate spec, then transfer Never_Set_In_Source @@ -4247,7 +4191,10 @@ package body Sem_Ch6 is Set_Directly_Designated_Type (Etype (Spec_Id), Desig_View); end if; - Ghost_Mode := Save_Ghost_Mode; + <> + if Mode_Set then + Restore_Ghost_Mode (Mode); + end if; end Analyze_Subprogram_Body_Helper; ------------------------------------ @@ -4309,13 +4256,6 @@ package body Sem_Ch6 is Set_SPARK_Pragma_Inherited (Designator); end if; - -- A subprogram declared within a Ghost region is automatically Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Designator); - end if; - if Debug_Flag_C then Write_Str ("==> subprogram spec "); Write_Name (Chars (Designator)); @@ -8197,10 +8137,6 @@ package body Sem_Ch6 is Set_Convention (Designator, Convention (E)); - if Is_Ghost_Entity (E) then - Set_Is_Ghost_Entity (Designator); - end if; - -- Skip past subprogram bodies and subprogram renamings that -- may appear to have a matching spec, but that aren't fully -- conformant with it. That can occur in cases where an @@ -9762,8 +9698,8 @@ package body Sem_Ch6 is Set_Is_Primitive (S); Check_Private_Overriding (B_Typ); - -- The Ghost policy in effect at the point of declaration of - -- a tagged type and a primitive operation must match + -- The Ghost policy in effect at the point of declaration + -- or a tagged type and a primitive operation must match -- (SPARK RM 6.9(16)). Check_Ghost_Primitive (S, B_Typ); @@ -9795,8 +9731,8 @@ package body Sem_Ch6 is Set_Has_Primitive_Operations (B_Typ); Check_Private_Overriding (B_Typ); - -- The Ghost policy in effect at the point of declaration of - -- a tagged type and a primitive operation must match + -- The Ghost policy in effect at the point of declaration + -- of a tagged type and a primitive operation must match -- (SPARK RM 6.9(16)). Check_Ghost_Primitive (S, B_Typ); @@ -11058,13 +10994,6 @@ package body Sem_Ch6 is Set_Etype (Formal, Formal_Type); - -- A formal parameter declared within a Ghost region is automatically - -- Ghost (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Formal); - end if; - -- Deal with default expression if present Default := Expression (Param_Spec); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 9d0eaec17e3..f5c02c8fa52 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -537,10 +537,10 @@ package body Sem_Ch7 is -- Local variables - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; Body_Id : Entity_Id; HSS : Node_Id; Last_Spec_Entity : Entity_Id; + Mode : Ghost_Mode_Type; New_N : Node_Id; Pack_Decl : Node_Id; Spec_Id : Entity_Id; @@ -643,7 +643,7 @@ package body Sem_Ch7 is -- the mode now to ensure that any nodes generated during analysis and -- expansion are properly flagged as ignored Ghost. - Set_Ghost_Mode (N, Spec_Id); + Mark_And_Set_Ghost_Body (N, Spec_Id, Mode); Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id)); Style.Check_Identifier (Body_Id, Spec_Id); @@ -738,19 +738,6 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma_Inherited (Body_Id); end if; - -- Inherit the "ghostness" of the package spec. Note that this property - -- is not directly inherited as the body may be subject to a different - -- Ghost assertion policy. - - if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then - Set_Is_Ghost_Entity (Body_Id); - - -- The Ghost policy in effect at the point of declaration and at the - -- point of completion must match (SPARK RM 6.9(14)). - - Check_Ghost_Completion (Spec_Id, Body_Id); - end if; - Set_Categorization_From_Pragmas (N); Install_Visible_Declarations (Spec_Id); @@ -942,7 +929,7 @@ package body Sem_Ch7 is end if; end if; - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Mode); end Analyze_Package_Body_Helper; --------------------------------- @@ -951,7 +938,6 @@ package body Sem_Ch7 is procedure Analyze_Package_Declaration (N : Node_Id) is Id : constant Node_Id := Defining_Entity (N); - Par : constant Node_Id := Parent_Spec (N); Is_Comp_Unit : constant Boolean := Nkind (Parent (N)) = N_Compilation_Unit; @@ -983,16 +969,6 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma_Inherited (Id); end if; - -- A package declared within a Ghost refion is automatically Ghost. A - -- child package is Ghost when its parent is Ghost (SPARK RM 6.9(2)). - - if Ghost_Mode > None - or else (Present (Par) - and then Is_Ghost_Entity (Defining_Entity (Unit (Par)))) - 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. @@ -1793,13 +1769,6 @@ package body Sem_Ch7 is New_Private_Type (N, Id, N); Set_Depends_On_Private (Id); - -- A type declared within a Ghost region is automatically Ghost - -- (SPARK RM 6.9(2)). - - if Ghost_Mode > None then - Set_Is_Ghost_Entity (Id); - end if; - if Has_Aspects (N) then Analyze_Aspect_Specifications (N, Id); end if; diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 1a81cbfc449..86eed89bd7b 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -575,7 +575,7 @@ package body Sem_Ch8 is -- The exception renaming declaration may become Ghost if it renames -- a Ghost entity. - Mark_Renaming_As_Ghost (N, Entity (Nam)); + Mark_Ghost_Renaming (N, Entity (Nam)); else Error_Msg_N ("invalid exception name in renaming", Nam); end if; @@ -658,10 +658,8 @@ package body Sem_Ch8 is K : Entity_Kind) is New_P : constant Entity_Id := Defining_Entity (N); - Old_P : Entity_Id; - Inst : Boolean := False; - -- Prevent junk warning + Old_P : Entity_Id; begin if Name (N) = Error then @@ -705,17 +703,17 @@ package body Sem_Ch8 is Set_Renamed_Object (New_P, Old_P); end if; + -- The generic renaming declaration may become Ghost if it renames a + -- Ghost entity. + + Mark_Ghost_Renaming (N, Old_P); + Set_Is_Pure (New_P, Is_Pure (Old_P)); Set_Is_Preelaborated (New_P, Is_Preelaborated (Old_P)); Set_Etype (New_P, Etype (Old_P)); Set_Has_Completion (New_P); - -- The generic renaming declaration may become Ghost if it renames a - -- Ghost entity. - - 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); end if; @@ -840,7 +838,15 @@ package body Sem_Ch8 is -- already-analyzed expression. if Nkind (Nam) = N_Selected_Component and then Analyzed (Nam) then - T := Etype (Nam); + + -- The object renaming declaration may become Ghost if it renames a + -- Ghost entity. + + if Is_Entity_Name (Nam) then + Mark_Ghost_Renaming (N, Entity (Nam)); + end if; + + T := Etype (Nam); Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam); if Present (Dec) then @@ -860,6 +866,13 @@ package body Sem_Ch8 is T := Entity (Subtype_Mark (N)); Analyze (Nam); + -- The object renaming declaration may become Ghost if it renames a + -- Ghost entity. + + if Is_Entity_Name (Nam) then + Mark_Ghost_Renaming (N, Entity (Nam)); + end if; + -- Reject renamings of conversions unless the type is tagged, or -- the conversion is implicit (which can occur for cases of anonymous -- access types in Ada 2012). @@ -928,12 +941,20 @@ package body Sem_Ch8 is -- Ada 2005 (AI-230/AI-254): Access renaming else pragma Assert (Present (Access_Definition (N))); - T := Access_Definition - (Related_Nod => N, - N => Access_Definition (N)); + T := + Access_Definition + (Related_Nod => N, + N => Access_Definition (N)); Analyze (Nam); + -- The object renaming declaration may become Ghost if it renames a + -- Ghost entity. + + if Is_Entity_Name (Nam) then + Mark_Ghost_Renaming (N, Entity (Nam)); + end if; + -- Ada 2005 AI05-105: if the declaration has an anonymous access -- type, the renamed object must also have an anonymous type, and -- this is a name resolution rule. This was implicit in the last part @@ -1071,7 +1092,6 @@ package body Sem_Ch8 is ("\suggest using an initialized constant " & "object instead?R?", Nam); end if; - end case; end if; @@ -1296,13 +1316,6 @@ package body Sem_Ch8 is Set_Is_True_Constant (Id, True); end if; - -- The object renaming declaration may become Ghost if it renames a - -- Ghost entity. - - 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 -- renamed object is volatile. Is_Volatile is set if the renamed object -- is volatile in the RM legality sense. @@ -1393,7 +1406,7 @@ package body Sem_Ch8 is else Error_Msg_Sloc := Sloc (Old_P); Error_Msg_NE - ("expect package name in renaming, found& declared#", + ("expect package name in renaming, found& declared#", Name (N), Old_P); end if; @@ -1418,19 +1431,18 @@ package body Sem_Ch8 is Set_Renamed_Object (New_P, Old_P); end if; - Set_Has_Completion (New_P); + -- The package renaming declaration may become Ghost if it renames a + -- Ghost entity. - Set_First_Entity (New_P, First_Entity (Old_P)); - Set_Last_Entity (New_P, Last_Entity (Old_P)); + Mark_Ghost_Renaming (N, Old_P); + + Set_Has_Completion (New_P); + Set_First_Entity (New_P, First_Entity (Old_P)); + Set_Last_Entity (New_P, Last_Entity (Old_P)); Set_First_Private_Entity (New_P, First_Private_Entity (Old_P)); Check_Library_Unit_Renaming (N, Old_P); Generate_Reference (Old_P, Name (N)); - -- The package renaming declaration may become Ghost if it renames a - -- Ghost entity. - - 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 -- warnings about no entities referenced. Such a warning would be @@ -2574,8 +2586,8 @@ package body Sem_Ch8 is and then Expander_Active then declare - Stream_Prim : Entity_Id; Prefix_Type : constant Entity_Id := Entity (Prefix (Nam)); + Stream_Prim : Entity_Id; begin -- The class-wide forms of the stream attributes are not @@ -2610,13 +2622,13 @@ package body Sem_Ch8 is Find_Optional_Prim_Op (Prefix_Type, TSS_Stream_Write); when others => Error_Msg_N - ("attribute must be a primitive" - & " dispatching operation", Nam); + ("attribute must be a primitive dispatching operation", + Nam); return; end case; - -- If no operation was found, and the type is limited, - -- the user should have defined one. + -- If no operation was found, and the type is limited, the user + -- should have defined one. if No (Stream_Prim) then if Is_Limited_Type (Prefix_Type) then @@ -2655,8 +2667,8 @@ package body Sem_Ch8 is end if; end if; - -- Check whether this declaration corresponds to the instantiation - -- of a formal subprogram. + -- Check whether this declaration corresponds to the instantiation of a + -- formal subprogram. -- If this is an instantiation, the corresponding actual is frozen and -- error messages can be made more precise. If this is a default @@ -2677,8 +2689,8 @@ package body Sem_Ch8 is -- is an external axiomatization on the package. if CW_Actual - and then Box_Present (Inst_Node) - and then not + and then Box_Present (Inst_Node) + and then not (GNATprove_Mode and then Present (Containing_Package_With_Ext_Axioms (Formal_Spec))) @@ -2691,11 +2703,17 @@ package body Sem_Ch8 is and then not Is_Overloaded (Nam) then Old_S := Entity (Nam); + + -- The subprogram renaming declaration may become Ghost if it + -- renames a Ghost entity. + + Mark_Ghost_Renaming (N, Old_S); + New_S := Analyze_Subprogram_Specification (Spec); -- Operator case - if Ekind (Entity (Nam)) = E_Operator then + if Ekind (Old_S) = E_Operator then -- Box present @@ -2729,9 +2747,9 @@ package body Sem_Ch8 is and then Hidden /= Old_S then Error_Msg_Sloc := Sloc (Hidden); - Error_Msg_N ("default subprogram is resolved " & - "in the generic declaration " & - "(RM 12.6(17))??", N); + Error_Msg_N + ("default subprogram is resolved in the generic " + & "declaration (RM 12.6(17))??", N); Error_Msg_NE ("\and will not use & #??", N, Hidden); end if; end; @@ -2740,6 +2758,14 @@ package body Sem_Ch8 is else Analyze (Nam); + + -- The subprogram renaming declaration may become Ghost if it + -- renames a Ghost entity. + + if Is_Entity_Name (Nam) then + Mark_Ghost_Renaming (N, Entity (Nam)); + end if; + New_S := Analyze_Subprogram_Specification (Spec); end if; @@ -2749,6 +2775,13 @@ package body Sem_Ch8 is Analyze (Nam); + -- The subprogram renaming declaration may become Ghost if it renames + -- a Ghost entity. + + if Is_Entity_Name (Nam) then + Mark_Ghost_Renaming (N, Entity (Nam)); + end if; + -- The renaming defines a new overloaded entity, which is analyzed -- like a subprogram declaration. @@ -2845,8 +2878,9 @@ package body Sem_Ch8 is Error_Msg_NE ("subprogram& overrides inherited operation", N, Rename_Spec); - elsif - Style_Check and then not Must_Override (Specification (N)) + + elsif Style_Check + and then not Must_Override (Specification (N)) then Style.Missing_Overriding (N, Rename_Spec); end if; @@ -3025,11 +3059,6 @@ package body Sem_Ch8 is Set_Is_Pure (New_S, Is_Pure (Entity (Nam))); Set_Is_Preelaborated (New_S, Is_Preelaborated (Entity (Nam))); - -- The subprogram renaming declaration may become Ghost if it renames - -- a Ghost entity. - - Mark_Renaming_As_Ghost (N, Entity (Nam)); - -- Ada 2005 (AI-423): Check the consistency of null exclusions -- between a subprogram and its correct renaming. @@ -3068,8 +3097,8 @@ package body Sem_Ch8 is not Is_Abstract_Type (Find_Dispatching_Type (Old_S))) then Error_Msg_N - ("renamed entity cannot be " - & "subprogram that requires overriding (RM 8.5.4 (5.1))", N); + ("renamed entity cannot be subprogram that requires overriding " + & "(RM 8.5.4 (5.1))", N); end if; end if; @@ -3124,7 +3153,7 @@ package body Sem_Ch8 is then Error_Msg_N ("subprogram in renaming_as_body cannot be intrinsic", - Name (N)); + Name (N)); end if; Set_Has_Completion (Rename_Spec); @@ -3364,8 +3393,7 @@ package body Sem_Ch8 is then Error_Msg_Node_2 := T1; Error_Msg_NE - ("default & on & is not directly visible", - Nam, Nam); + ("default & on & is not directly visible", Nam, Nam); end if; end; end if; @@ -3396,8 +3424,8 @@ package body Sem_Ch8 is then Error_Msg_N ("access parameter is controlling,", New_F); Error_Msg_NE - ("\corresponding parameter of& " - & "must be explicitly null excluding", New_F, Old_S); + ("\corresponding parameter of& must be explicitly null " + & "excluding", New_F, Old_S); end if; Next_Formal (Old_F); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 37c206e4bcc..513b19b8874 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -459,9 +459,8 @@ package body Sem_Prag is CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - CCase : Node_Id; + Mode : Ghost_Mode_Type; Restore_Scope : Boolean := False; -- Start of processing for Analyze_Contract_Cases_In_Decl_Part @@ -478,7 +477,7 @@ package body Sem_Prag is -- point of analysis may not necessarily be the same. Use the mode in -- effect at the point of declaration. - Set_Ghost_Mode (N); + Set_Ghost_Mode (N, Mode); -- Single and multiple contract cases must appear in aggregate form. If -- this is not the case, then either the parser of the analysis of the @@ -524,8 +523,8 @@ package body Sem_Prag is Error_Msg_N ("wrong syntax for constract cases", N); end if; - Ghost_Mode := Save_Ghost_Mode; Set_Is_Analyzed_Pragma (N); + Restore_Ghost_Mode (Mode); end Analyze_Contract_Cases_In_Decl_Part; ---------------------------------- @@ -2656,7 +2655,7 @@ package body Sem_Prag is Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Mode : Ghost_Mode_Type; begin -- Do not analyze the pragma multiple times @@ -2670,16 +2669,16 @@ package body Sem_Prag is -- point of analysis may not necessarily be the same. Use the mode in -- effect at the point of declaration. - Set_Ghost_Mode (N); + Set_Ghost_Mode (N, Mode); -- The expression is preanalyzed because it has not been moved to its -- final place yet. A direct analysis may generate side effects and this -- is not desired at this point. Preanalyze_Assert_Expression (Expr, Standard_Boolean); - Ghost_Mode := Save_Ghost_Mode; - Set_Is_Analyzed_Pragma (N); + + Restore_Ghost_Mode (Mode); end Analyze_Initial_Condition_In_Decl_Part; -------------------------------------- @@ -4133,7 +4132,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Spec_Id); Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); end Analyze_Depends_Global; @@ -4316,16 +4315,16 @@ package body Sem_Prag is 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_Ghost_Pragma (N, Subp_Id); + -- Chain the pragma on the contract for further processing by -- Analyze_Pre_Post_Condition_In_Decl_Part. Add_Contract_Item (N, 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 an entry or -- subprogram body because it cannot benefit from forward references. @@ -4446,7 +4445,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Spec_Id); if Nam_In (Pname, Name_Refined_Depends, Name_Refined_Global) then Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); @@ -4510,7 +4509,7 @@ package body Sem_Prag is -- the purposes of legality checks and removal of ignored -- Ghost code. - Mark_Pragma_As_Ghost (N, Arg_Id); + Mark_Ghost_Pragma (N, Arg_Id); -- Capture the entity of the first Ghost variable being -- processed for error detection purposes. @@ -4684,7 +4683,7 @@ package body Sem_Prag is -- for the purposes of legality checks and removal of -- ignored Ghost code. - Mark_Pragma_As_Ghost (N, Arg_Id); + Mark_Ghost_Pragma (N, Arg_Id); -- Capture the entity of the first Ghost name being -- processed for error detection purposes. @@ -6793,13 +6792,12 @@ package body Sem_Prag is return; end if; - E := Entity (E_Arg); - Decl := Declaration_Node (E); + E := Entity (E_Arg); -- 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); + Mark_Ghost_Pragma (N, E); -- Check duplicate before we chain ourselves @@ -6856,6 +6854,8 @@ package body Sem_Prag is -- Now check appropriateness of the entity + Decl := Declaration_Node (E); + if Is_Type (E) then if Rep_Item_Too_Early (E, N) or else @@ -8358,7 +8358,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Def_Id); Kill_Size_Check_Code (Def_Id); Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False); end if; @@ -9006,7 +9006,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Subp); -- Capture the entity of the first Ghost subprogram being -- processed for error detection purposes. @@ -9266,7 +9266,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Handler); Set_Is_Interrupt_Handler (Handler); pragma Assert (Ekind (Prot_Typ) = E_Protected_Type); @@ -9759,7 +9759,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); -- Enforce RM 11.5(7) which requires that for a pragma that -- appears within a package spec, the named entity must be @@ -11216,6 +11216,12 @@ 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_Ghost_Pragma (N, Pack_Id); + Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); + -- Chain the pragma on the contract for completeness Add_Contract_Item (N, Pack_Id); @@ -11231,13 +11237,6 @@ package body Sem_Prag is -- Analyze all these pragmas in the order outlined above Analyze_If_Present (Pragma_SPARK_Mode); - - -- 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)); - States := Expression (Get_Argument (N, Pack_Id)); -- Multiple non-null abstract states appear as an aggregate @@ -11484,7 +11483,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Lib_Entity); -- This pragma should only apply to a RCI unit (RM E.2.3(23)) @@ -11560,7 +11559,7 @@ package body Sem_Prag is 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))); + Mark_Ghost_Pragma (N, Entity (Get_Pragma_Arg (Nam_Arg))); end if; -- Not allowed in compiler units (bootstrap issues) @@ -12111,16 +12110,16 @@ package body Sem_Prag is if Ekind (Obj_Id) = E_Variable then - -- Chain the pragma on the contract for further processing by - -- Analyze_External_Property_In_Decl_Part. - - Add_Contract_Item (N, Obj_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, Obj_Id); + Mark_Ghost_Pragma (N, Obj_Id); + + -- Chain the pragma on the contract for further processing by + -- Analyze_External_Property_In_Decl_Part. + + Add_Contract_Item (N, Obj_Id); -- Analyze the Boolean expression (if any) @@ -12202,7 +12201,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Nm); if not Is_Remote_Call_Interface (C_Ent) and then not Is_Remote_Types (C_Ent) @@ -12322,7 +12321,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); Check_Duplicate_Pragma (E); if Rep_Item_Too_Early (E, N) @@ -12471,16 +12470,15 @@ package body Sem_Prag is Cname : Name_Id; Eloc : Source_Ptr; Expr : Node_Id; + Mode : Ghost_Mode_Type; Str : Node_Id; - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - begin -- Pragma Check is Ghost when it applies to a Ghost entity. Set -- the mode now to ensure that any nodes generated during analysis -- and expansion are marked as Ghost. - Set_Ghost_Mode (N); + Set_Ghost_Mode (N, Mode); GNAT_Pragma; Check_At_Least_N_Arguments (2); @@ -12677,7 +12675,7 @@ package body Sem_Prag is In_Assertion_Expr := In_Assertion_Expr - 1; end if; - Ghost_Mode := Save_Ghost_Mode; + Restore_Ghost_Mode (Mode); end Check; -------------------------- @@ -13175,14 +13173,14 @@ package body Sem_Prag is return; end if; - -- Chain the pragma on the contract for completeness - - Add_Contract_Item (N, Obj_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, Obj_Id); + Mark_Ghost_Pragma (N, Obj_Id); + + -- Chain the pragma on the contract for completeness + + Add_Contract_Item (N, Obj_Id); -- Analyze the Boolean expression (if any) @@ -13287,17 +13285,17 @@ package body Sem_Prag is Spec_Id := Unique_Defining_Entity (Subp_Decl); - -- Chain the pragma on the contract for further processing by - -- Analyze_Contract_Cases_In_Decl_Part. - - Add_Contract_Item (N, 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, Spec_Id); + Mark_Ghost_Pragma (N, Spec_Id); Ensure_Aggregate_Form (Get_Argument (N, Spec_Id)); + -- Chain the pragma on the contract for further processing by + -- Analyze_Contract_Cases_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + -- Fully analyze the pragma when it appears inside an entry -- or subprogram body because it cannot benefit from forward -- references. @@ -13361,7 +13359,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); end Convention; --------------------------- @@ -13832,7 +13830,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); -- The pragma signals that the type defines its own DIC assertion -- expression. @@ -13961,7 +13959,7 @@ package body Sem_Prag is -- for the purposes of legality checks and removal of -- ignored Ghost code. - Mark_Pragma_As_Ghost (N, Entity (Pool)); + Mark_Ghost_Pragma (N, Entity (Pool)); else Error_Pragma_Arg @@ -14145,7 +14143,7 @@ package body Sem_Prag is -- the purposes of legality checks and removal of ignored -- Ghost code. - Mark_Pragma_As_Ghost (N, E); + Mark_Ghost_Pragma (N, E); if (Is_First_Subtype (E) and then @@ -14194,7 +14192,7 @@ package body Sem_Prag is -- the purposes of legality checks and removal of ignored Ghost -- code. - Mark_Pragma_As_Ghost (N, Ent); + Mark_Ghost_Pragma (N, Ent); -- The expression must be analyzed in the special manner -- described in "Handling of Default and Per-Object @@ -14420,7 +14418,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Cunit_Ent); if Nkind_In (Unit (Cunit_Node), N_Package_Body, N_Subprogram_Body) @@ -14612,7 +14610,7 @@ package body Sem_Prag is -- the purposes of legality checks and removal of ignored Ghost -- code. - Mark_Pragma_As_Ghost (N, Def_Id); + Mark_Ghost_Pragma (N, Def_Id); if Ekind (Def_Id) /= E_Constant then Note_Possible_Modification @@ -15032,6 +15030,13 @@ package body Sem_Prag is return; end if; + -- 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. + + Spec_Id := Unique_Defining_Entity (Subp_Decl); + Mark_Ghost_Pragma (N, Spec_Id); + -- Chain the pragma on the contract for completeness Add_Contract_Item (N, Defining_Entity (Subp_Decl)); @@ -15042,13 +15047,6 @@ package body Sem_Prag is Analyze_If_Present (Pragma_SPARK_Mode); - -- 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. - - Spec_Id := Unique_Defining_Entity (Subp_Decl); - Mark_Pragma_As_Ghost (N, Spec_Id); - -- Examine the formals of the related subprogram Formal := First_Formal (Spec_Id); @@ -15123,7 +15121,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False); @@ -15211,7 +15209,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); -- If it's an access-to-subprogram type (in particular, not a -- subtype), set the flag on that type. @@ -16112,7 +16110,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); -- Check duplicate before we chain ourselves @@ -16218,6 +16216,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_Ghost_Pragma (N, Pack_Id); + -- Chain the pragma on the contract for further processing by -- Analyze_Initial_Condition_In_Decl_Part. @@ -16236,11 +16239,6 @@ package body Sem_Prag is Analyze_If_Present (Pragma_SPARK_Mode); Analyze_If_Present (Pragma_Abstract_State); Analyze_If_Present (Pragma_Initializes); - - -- 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); end Initial_Condition; ------------------------ @@ -16332,6 +16330,12 @@ 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_Ghost_Pragma (N, Pack_Id); + Ensure_Aggregate_Form (Get_Argument (N, Pack_Id)); + -- Chain the pragma on the contract for further processing by -- Analyze_Initializes_In_Decl_Part. @@ -16349,13 +16353,6 @@ package body Sem_Prag is Analyze_If_Present (Pragma_SPARK_Mode); Analyze_If_Present (Pragma_Abstract_State); - - -- 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)); - Analyze_If_Present (Pragma_Initial_Condition); end Initializes; @@ -16903,7 +16900,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); -- The pragma defines a type-specific invariant, the type is said -- to have invariants of its "own". @@ -17253,7 +17250,7 @@ package body Sem_Prag is -- the purposes of legality checks and removal of ignored -- Ghost code. - Mark_Pragma_As_Ghost (N, Ent); + Mark_Ghost_Pragma (N, Ent); -- Subprograms @@ -17277,7 +17274,7 @@ package body Sem_Prag is -- Ghost for the purposes of legality checks and -- removal of ignored Ghost code. - Mark_Pragma_As_Ghost (N, Ent); + Mark_Ghost_Pragma (N, Ent); -- Capture the entity of the first Ghost subprogram -- being processed for error detection purposes. @@ -17685,7 +17682,7 @@ package body Sem_Prag is -- Ghost. This also ensures that any expansion performed further -- below will produce Ghost nodes. - Mark_Pragma_As_Ghost (N, Entry_Id); + Mark_Ghost_Pragma (N, Entry_Id); -- Analyze the Integer expression @@ -17866,7 +17863,7 @@ package body Sem_Prag is -- for the purposes of legality checks and removal of -- ignored Ghost code. - Mark_Pragma_As_Ghost (N, E); + Mark_Ghost_Pragma (N, E); -- Capture the entity of the first Ghost procedure being -- processed for error detection purposes. @@ -18110,7 +18107,7 @@ package body Sem_Prag is -- the purposes of legality checks and removal of ignored Ghost -- code. - Mark_Pragma_As_Ghost (N, E); + Mark_Ghost_Pragma (N, E); -- Entity name was given @@ -18514,7 +18511,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (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"); @@ -18737,12 +18734,11 @@ package body Sem_Prag is end if; Item_Id := Defining_Entity (Stmt); - Encap := 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); + Mark_Ghost_Pragma (N, Item_Id); -- Chain the pragma on the contract for further processing by -- Analyze_Part_Of_In_Decl_Part or for completeness. @@ -18762,6 +18758,8 @@ package body Sem_Prag is -- instantiation. else + Encap := Get_Pragma_Arg (Arg1); + -- Detect any discrepancies between the placement of the -- constant or package instantiation with respect to state -- space and the encapsulating state. @@ -18888,7 +18886,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (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 @@ -18976,13 +18974,12 @@ package body Sem_Prag is end if; 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); + Mark_Ghost_Pragma (N, Ent); -- Check for duplication before inserting in list of -- representation items. @@ -18993,6 +18990,8 @@ package body Sem_Prag is return; end if; + Decl := Parent (Ent); + if Present (Expression (Decl)) then Error_Pragma_Arg ("object for pragma% cannot have initialization", Arg1); @@ -19197,7 +19196,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); -- The remaining processing is simply to link the pragma on to -- the rep item chain, for processing when the type is frozen. @@ -19249,7 +19248,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); -- The remaining processing is simply to link the pragma on to -- the rep item chain, for processing when the type is frozen. @@ -19284,7 +19283,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Ent); Check_Duplicate_Pragma (Ent); -- This filters out pragmas inside generic parents that show up @@ -19919,7 +19918,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Ent); if not Debug_Flag_U then Set_Is_Pure (Ent); @@ -19958,7 +19957,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); if Present (E) then loop @@ -20303,6 +20302,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_Ghost_Pragma (N, Spec_Id); + -- Chain the pragma on the contract for further processing by -- Analyze_Refined_State_In_Decl_Part. @@ -20313,11 +20317,6 @@ package body Sem_Prag is Analyze_If_Present (Pragma_SPARK_Mode); - -- 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)). @@ -20401,7 +20400,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); if Nkind (Parent (E)) = N_Formal_Type_Declaration and then Ekind (E) = E_General_Access_Type @@ -20446,7 +20445,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Cunit_Ent); if K = N_Package_Declaration or else K = N_Generic_Package_Declaration @@ -20488,7 +20487,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Cunit_Ent); if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration, N_Generic_Package_Declaration) @@ -20688,7 +20687,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Cunit_Ent); if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration, N_Generic_Package_Declaration) @@ -20740,7 +20739,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); -- We require the pragma to apply to a type declared in a package -- declaration, but not (immediately) within a package body. @@ -21922,7 +21921,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Nam_Id); Set_Debug_Info_Off (Nam_Id); end Suppress_Debug_Info; @@ -21965,7 +21964,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); if not Is_Type (E) and then Ekind (E) /= E_Variable then Error_Pragma_Arg @@ -22366,16 +22365,16 @@ package body Sem_Prag is 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_Ghost_Pragma (N, Subp_Id); + -- Chain the pragma on the contract for further processing by -- Analyze_Test_Case_In_Decl_Part. Add_Contract_Item (N, Subp_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, Subp_Id); - -- Preanalyze the original aspect argument "Name" for ASIS or for -- a generic subprogram to properly capture global references. @@ -22449,7 +22448,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E); if Rep_Item_Too_Early (E, N) or else @@ -22598,7 +22597,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, Typ); if Typ = Any_Type or else Rep_Item_Too_Early (Typ, N) @@ -22759,7 +22758,7 @@ package body Sem_Prag is -- 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); + Mark_Ghost_Pragma (N, E_Id); Set_Universal_Aliasing (Implementation_Base_Type (E_Id)); Record_Rep_Item (E_Id, N); end Universal_Alias; @@ -22835,7 +22834,7 @@ package body Sem_Prag is -- for the purposes of legality checks and removal of -- ignored Ghost code. - Mark_Pragma_As_Ghost (N, Arg_Id); + Mark_Ghost_Pragma (N, Arg_Id); -- Capture the entity of the first Ghost type being -- processed for error detection purposes. @@ -23069,6 +23068,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_Ghost_Pragma (N, Spec_Id); + -- Chain the pragma on the contract for completeness Add_Contract_Item (N, Spec_Id); @@ -23079,11 +23083,6 @@ package body Sem_Prag is Analyze_If_Present (Pragma_SPARK_Mode); - -- 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); - -- A volatile function cannot override a non-volatile function -- (SPARK RM 7.1.2(15)). Overriding checks are usually performed -- in New_Overloaded_Entity, however at that point the pragma has @@ -23634,9 +23633,8 @@ package body Sem_Prag is Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - Errors : Nat; + Mode : Ghost_Mode_Type; Restore_Scope : Boolean := False; -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part @@ -23653,7 +23651,7 @@ package body Sem_Prag is -- point of analysis may not necessarily be the same. Use the mode in -- effect at the point of declaration. - Set_Ghost_Mode (N); + Set_Ghost_Mode (N, Mode); -- Ensure that the subprogram and its formals are visible when analyzing -- the expression of the pragma. @@ -23722,9 +23720,9 @@ package body Sem_Prag is -- subprogram subject to pragma Inline_Always. Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - Ghost_Mode := Save_Ghost_Mode; - Set_Is_Analyzed_Pragma (N); + + Restore_Ghost_Mode (Mode); end Analyze_Pre_Post_Condition_In_Decl_Part; ------------------------------------------ diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 1c5fe4cb056..fc377a952fd 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -1996,10 +1996,6 @@ package body Sem_Res is return; end Resolution_Failed; - -- Local variables - - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; - -- Start of processing for Resolve begin @@ -2007,14 +2003,6 @@ package body Sem_Res is return; end if; - -- A declaration may be subject to pragma Ghost. Set the mode now to - -- ensure that any nodes generated during analysis and expansion are - -- marked as Ghost. - - if Is_Declaration (N) then - Set_Ghost_Mode (N); - end if; - -- Access attribute on remote subprogram cannot be used for a non-remote -- access-to-subprogram type. @@ -2130,7 +2118,6 @@ package body Sem_Res is if Analyzed (N) then Debug_A_Exit ("resolving ", N, " (done, already analyzed)"); Analyze_Dimension (N); - Ghost_Mode := Save_Ghost_Mode; return; -- Any case of Any_Type as the Etype value means that we had a @@ -2138,7 +2125,6 @@ package body Sem_Res is elsif Etype (N) = Any_Type then Debug_A_Exit ("resolving ", N, " (done, Etype = Any_Type)"); - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -2578,7 +2564,6 @@ package body Sem_Res is then Resolve (N, Full_View (Typ)); Set_Etype (N, Typ); - Ghost_Mode := Save_Ghost_Mode; return; -- Check for an aggregate. Sometimes we can get bogus aggregates @@ -2687,7 +2672,6 @@ package body Sem_Res is if Address_Integer_Convert_OK (Typ, Etype (N)) then Rewrite (N, Unchecked_Convert_To (Typ, Relocate_Node (N))); Analyze_And_Resolve (N, Typ); - Ghost_Mode := Save_Ghost_Mode; return; -- Under relaxed RM semantics silently replace occurrences of null @@ -2725,8 +2709,8 @@ package body Sem_Res is Error_Msg_Node_2 := Typ; Error_Msg_NE - ("no visible interpretation of& " - & "matches expected type&", N, Subp_Name); + ("no visible interpretation of& matches expected type&", + N, Subp_Name); end; if All_Errors_Mode then @@ -2758,14 +2742,12 @@ package body Sem_Res is end if; Resolution_Failed; - Ghost_Mode := Save_Ghost_Mode; return; -- Test if we have more than one interpretation for the context elsif Ambiguous then Resolution_Failed; - Ghost_Mode := Save_Ghost_Mode; return; -- Only one intepretation @@ -2838,7 +2820,6 @@ package body Sem_Res is and then Present (Entity (N)) and then Ekind (Entity (N)) /= E_Operator then - if not Is_Predefined_Op (Entity (N)) then Rewrite_Operator_As_Call (N, Entity (N)); @@ -2853,14 +2834,12 @@ package body Sem_Res is -- Rewrite_Renamed_Operator. if Analyzed (N) then - Ghost_Mode := Save_Ghost_Mode; return; end if; end if; end if; case N_Subexpr'(Nkind (N)) is - when N_Aggregate => Resolve_Aggregate (N, Ctx_Type); when N_Allocator => Resolve_Allocator (N, Ctx_Type); @@ -3003,7 +2982,6 @@ package body Sem_Res is if Nkind (N) not in N_Subexpr then Debug_A_Exit ("resolving ", N, " (done)"); Expand (N); - Ghost_Mode := Save_Ghost_Mode; return; end if; @@ -3038,8 +3016,6 @@ package body Sem_Res is Expand (N); end if; - - Ghost_Mode := Save_Ghost_Mode; end Resolve; ------------- diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 58a157bdd5a..f9efdab2c0d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12074,33 +12074,38 @@ package body Sem_Util is -------------------- function Is_Declaration (N : Node_Id) return Boolean is + begin + return + Is_Declaration_Other_Than_Renaming (N) + or else Is_Renaming_Declaration (N); + end Is_Declaration; + + ---------------------------------------- + -- Is_Declaration_Other_Than_Renaming -- + ---------------------------------------- + + function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is begin case Nkind (N) is when N_Abstract_Subprogram_Declaration | N_Exception_Declaration | - N_Exception_Renaming_Declaration | + N_Expression_Function | N_Full_Type_Declaration | - N_Generic_Function_Renaming_Declaration | N_Generic_Package_Declaration | - N_Generic_Package_Renaming_Declaration | - N_Generic_Procedure_Renaming_Declaration | N_Generic_Subprogram_Declaration | N_Number_Declaration | N_Object_Declaration | - N_Object_Renaming_Declaration | N_Package_Declaration | - N_Package_Renaming_Declaration | N_Private_Extension_Declaration | N_Private_Type_Declaration | N_Subprogram_Declaration | - N_Subprogram_Renaming_Declaration | N_Subtype_Declaration => return True; when others => return False; end case; - end Is_Declaration; + end Is_Declaration_Other_Than_Renaming; -------------------------------- -- Is_Declared_Within_Variant -- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index a1e79b1c330..2088e7f691e 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1361,6 +1361,9 @@ package Sem_Util is function Is_Declaration (N : Node_Id) return Boolean; -- Determine whether arbitrary node N denotes a declaration + function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a non-renaming declaration + function Is_Declared_Within_Variant (Comp : Entity_Id) return Boolean; -- Returns True iff component Comp is declared within a variant part diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index 2d6e1af64d7..2ded5b82759 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -1809,6 +1809,14 @@ package body Sinfo is return Flag11 (N); end Is_Checked; + function Is_Checked_Ghost_Pragma + (N : Node_Id) return Boolean is + begin + pragma Assert (False + or else NT (N).Nkind = N_Pragma); + return Flag3 (N); + end Is_Checked_Ghost_Pragma; + function Is_Component_Left_Opnd (N : Node_Id) return Boolean is begin @@ -1917,22 +1925,22 @@ package body Sinfo is return Flag2 (N); end Is_Generic_Contract_Pragma; - function Is_Ghost_Pragma + function Is_Ignored (N : Node_Id) return Boolean is begin pragma Assert (False + or else NT (N).Nkind = N_Aspect_Specification or else NT (N).Nkind = N_Pragma); - return Flag3 (N); - end Is_Ghost_Pragma; + return Flag9 (N); + end Is_Ignored; - function Is_Ignored + function Is_Ignored_Ghost_Pragma (N : Node_Id) return Boolean is begin pragma Assert (False - or else NT (N).Nkind = N_Aspect_Specification or else NT (N).Nkind = N_Pragma); - return Flag9 (N); - end Is_Ignored; + return Flag8 (N); + end Is_Ignored_Ghost_Pragma; function Is_In_Discriminant_Check (N : Node_Id) return Boolean is @@ -5088,6 +5096,14 @@ package body Sinfo is Set_Flag11 (N, Val); end Set_Is_Checked; + procedure Set_Is_Checked_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_Checked_Ghost_Pragma; + procedure Set_Is_Component_Left_Opnd (N : Node_Id; Val : Boolean := True) is begin @@ -5196,22 +5212,22 @@ package body Sinfo is Set_Flag2 (N, Val); end Set_Is_Generic_Contract_Pragma; - procedure Set_Is_Ghost_Pragma + procedure Set_Is_Ignored (N : Node_Id; Val : Boolean := True) is begin pragma Assert (False + or else NT (N).Nkind = N_Aspect_Specification or else NT (N).Nkind = N_Pragma); - Set_Flag3 (N, Val); - end Set_Is_Ghost_Pragma; + Set_Flag9 (N, Val); + end Set_Is_Ignored; - procedure Set_Is_Ignored + procedure Set_Is_Ignored_Ghost_Pragma (N : Node_Id; Val : Boolean := True) is begin pragma Assert (False - or else NT (N).Nkind = N_Aspect_Specification or else NT (N).Nkind = N_Pragma); - Set_Flag9 (N, Val); - end Set_Is_Ignored; + Set_Flag8 (N, Val); + end Set_Is_Ignored_Ghost_Pragma; procedure Set_Is_In_Discriminant_Check (N : Node_Id; Val : Boolean := True) is diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 6c5472a1d9c..dd1aec58036 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -528,26 +528,81 @@ package Sinfo is -- Ghost Mode -- ---------------- - -- When a declaration is subject to pragma Ghost, it establishes a Ghost - -- region depending on the Ghost assertion policy in effect at the point - -- of declaration. This region is temporal and starts right before the - -- analysis of the Ghost declaration and ends after its expansion. The - -- values of global variable Opt.Ghost_Mode are as follows: + -- The SPARK RM 6.9 defines two classes of constructs - Ghost entities and + -- Ghost statements. The intent of the feature is to treat Ghost constructs + -- as non-existent when Ghost assertion policy Ignore is in effect. + + -- The corresponding nodes which map to Ghost constructs are: + + -- Ghost entities + -- Declaration nodes + -- N_Package_Body + -- N_Subprogram_Body + + -- Ghost statements + -- N_Assignment_Statement + -- N_Procedure_Call_Statement + -- N_Pragma + + -- In addition, the compiler treats instantiations as Ghost entities + + -- To achieve the removal of ignored Ghost constructs, the compiler relies + -- on global variable Ghost_Mode and a mechanism called "Ghost regions". + -- The values of the global variable are as follows: -- 1. Check - All static semantics as defined in SPARK RM 6.9 are in - -- effect. + -- effect. The Ghost region has mode Check. -- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI - -- files, object files as well as the final executable. + -- files, object files, and the final executable. The Ghost region + -- has mode Ignore. + + -- 3. None - No Ghost region is in effect + + -- A Ghost region is a compiler operating mode, similar to Check_Syntax, + -- however a region is much more finely grained and depends on the policy + -- in effect. The region starts prior to the analysis of a Ghost construct + -- and ends immediately after its expansion. The region is established as + -- follows: + + -- 1. Declarations - Prior to analysis, if the declaration is subject to + -- pragma Ghost. + + -- 2. Renaming declarations - Same as 1) or when the renamed entity is + -- Ghost. - -- To achieve the runtime semantics of "Ignore", the compiler marks each - -- node created during an ignored Ghost region and signals all enclosing - -- scopes that such a node resides within. The compilation unit where the - -- node resides is also added to an auxiliary table for post processing. + -- 3. Completing declarations - Same as 1) or when the declaration is + -- partially analyzed and the declaration completes a Ghost entity. + + -- 4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is + -- partially analyzed and completes a Ghost entity. + + -- 5. N_Assignment_Statement - After the left hand side is analyzed and + -- references a Ghost entity. + + -- 6. N_Procedure_Call_Statement - After the name is analyzed and denotes + -- a Ghost procedure. + + -- 7. N_Pragma - During analysis, when the related entity is Ghost or the + -- pragma encloses a Ghost entity. + + -- 8. Instantiations - Save as 1) or when the instantiation is partially + -- analyzed and the generic template is Ghost. + + -- Routines Mark_And_Set_Ghost_xxx install a new Ghost region and routine + -- Restore_Ghost_Mode ends a Ghost region. A region may be reinstalled + -- similar to scopes for decoupled expansion such as the generation of + -- dispatch tables or the creation of a predicate function. + + -- If the mode of a Ghost region is Ignore, any newly created nodes as well + -- as source entities are marked as ignored Ghost. In additon, the marking + -- process signals all enclosing scopes that an ignored Ghost node resides + -- within. The compilation unit where the node resides is also added to an + -- auxiliary table for post processing. -- After the analysis and expansion of all compilation units takes place -- as well as the instantiation of all inlined [generic] bodies, the GNAT - -- driver initiates a separate pass which removes all ignored Ghost code + -- driver initiates a separate pass which removes all ignored Ghost nodes -- from all units stored in the auxiliary table. -------------------- @@ -1581,6 +1636,11 @@ package Sinfo is -- be further modified (in some cases these flags are copied when a -- pragma is rewritten). + -- Is_Checked_Ghost_Pragma (Flag3-Sem) + -- This flag is present in N_Pragma nodes. It is set when the pragma is + -- related to a checked Ghost entity or encloses a checked Ghost entity. + -- This flag has no relation to Is_Checked. + -- Is_Component_Left_Opnd (Flag13-Sem) -- Is_Component_Right_Opnd (Flag14-Sem) -- Present in concatenation nodes, to indicate that the corresponding @@ -1651,11 +1711,6 @@ 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) @@ -1670,6 +1725,11 @@ package Sinfo is -- aspect/pragma is fully analyzed and checked for other syntactic -- and semantic errors, but it does not have any semantic effect. + -- Is_Ignored_Ghost_Pragma (Flag8-Sem) + -- This flag is present in N_Pragma nodes. It is set when the pragma is + -- related to an ignored Ghost entity or encloses ignored Ghost entity. + -- This flag has no relation to Is_Ignored. + -- Is_In_Discriminant_Check (Flag11-Sem) -- This flag is present in a selected component, and is used to indicate -- that the reference occurs within a discriminant check. The @@ -2519,11 +2579,12 @@ package Sinfo is -- Import_Interface_Present (Flag16-Sem) -- Is_Analyzed_Pragma (Flag5-Sem) -- Is_Checked (Flag11-Sem) + -- Is_Checked_Ghost_Pragma (Flag3-Sem) -- 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_Ignored_Ghost_Pragma (Flag8-Sem) -- Is_Inherited_Pragma (Flag4-Sem) -- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set -- Uneval_Old_Accept (Flag7-Sem) @@ -9364,6 +9425,9 @@ package Sinfo is function Is_Checked (N : Node_Id) return Boolean; -- Flag11 + function Is_Checked_Ghost_Pragma + (N : Node_Id) return Boolean; -- Flag3 + function Is_Component_Left_Opnd (N : Node_Id) return Boolean; -- Flag13 @@ -9403,12 +9467,12 @@ 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 + function Is_Ignored_Ghost_Pragma + (N : Node_Id) return Boolean; -- Flag8 + function Is_In_Discriminant_Check (N : Node_Id) return Boolean; -- Flag11 @@ -10414,6 +10478,9 @@ package Sinfo is procedure Set_Is_Checked (N : Node_Id; Val : Boolean := True); -- Flag11 + procedure Set_Is_Checked_Ghost_Pragma + (N : Node_Id; Val : Boolean := True); -- Flag3 + procedure Set_Is_Component_Left_Opnd (N : Node_Id; Val : Boolean := True); -- Flag13 @@ -10453,12 +10520,12 @@ 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 + procedure Set_Is_Ignored_Ghost_Pragma + (N : Node_Id; Val : Boolean := True); -- Flag8 + procedure Set_Is_In_Discriminant_Check (N : Node_Id; Val : Boolean := True); -- Flag11 @@ -12865,6 +12932,7 @@ package Sinfo is pragma Inline (Is_Asynchronous_Call_Block); pragma Inline (Is_Boolean_Aspect); pragma Inline (Is_Checked); + pragma Inline (Is_Checked_Ghost_Pragma); pragma Inline (Is_Component_Left_Opnd); pragma Inline (Is_Component_Right_Opnd); pragma Inline (Is_Controlling_Actual); @@ -12878,8 +12946,8 @@ 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_Ignored_Ghost_Pragma); pragma Inline (Is_In_Discriminant_Check); pragma Inline (Is_Inherited_Pragma); pragma Inline (Is_Machine_Number); @@ -13210,6 +13278,7 @@ package Sinfo is pragma Inline (Set_Is_Asynchronous_Call_Block); pragma Inline (Set_Is_Boolean_Aspect); pragma Inline (Set_Is_Checked); + pragma Inline (Set_Is_Checked_Ghost_Pragma); pragma Inline (Set_Is_Component_Left_Opnd); pragma Inline (Set_Is_Component_Right_Opnd); pragma Inline (Set_Is_Controlling_Actual); @@ -13223,8 +13292,8 @@ 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_Ignored_Ghost_Pragma); pragma Inline (Set_Is_In_Discriminant_Check); pragma Inline (Set_Is_Inherited_Pragma); pragma Inline (Set_Is_Machine_Number); -- 2.30.2