From 8636f52f7b50176948646cc151bfd514b8b71c03 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Wed, 7 Jan 2015 08:41:47 +0000 Subject: [PATCH] 2015-01-07 Hristian Kirtchev * alloc.ads Alphabetize several declarations. Add constants Ignored_Ghost_Units_Initial and Ignored_Ghost_Units_Increment. * atree.adb Add with and use clauses for Opt. (Allocate_Initialize_Node): Mark a node as ignored Ghost if it is created in an ignored Ghost region. (Ekind_In): New variant. (Is_Ignored_Ghost_Node): New routine. (Set_Is_Ignored_Ghost_Node): New routine. * atree.adb Aplhabetize several subprograms declarations. Flag Spare0 is now known as Is_Ignored_Ghost_Node. (Ekind_In): New variant. (Is_Ignored_Ghost_Node): New routine. (Set_Is_Ignored_Ghost_Node): New routine. * einfo.adb: Flag 279 is now known as Contains_Ignored_Ghost_Code. (Contains_Ignored_Ghost_Code): New routine. (Set_Contains_Ignored_Ghost_Code): New routine. (Set_Is_Checked_Ghost_Entity, Set_Is_Ignored_Ghost_Entity): It is now possible to set this property on an unanalyzed entity. (Write_Entity_Flags): Output the status of flag Contains_Ignored_Ghost_Code. * einfo.ads New attribute Contains_Ignored_Ghost_Code along with usage in nodes. (Contains_Ignored_Ghost_Code): New routine along with pragma Inline. (Set_Contains_Ignored_Ghost_Code): New routine along with pragma Inline. * exp_ch3.adb Add with and use clauses for Ghost. (Freeze_Type): Capture/restore the value of Ghost_Mode on entry/exit. Set the Ghost_Mode in effect. (Restore_Globals): New routine. * exp_ch7.adb (Process_Declarations): Do not process a context that invoves an ignored Ghost entity. * exp_dbug.adb (Qualify_All_Entity_Names): Skip an ignored Ghost construct that has been rewritten as a null statement. * exp_disp.adb Add with and use clauses for Ghost. (Make_DT): Capture/restore the value of Ghost_Mode on entry/exit. Set the Ghost_Mode in effect. (Restore_Globals): New routine. * exp_util.adb (Requires_Cleanup_Actions): An ignored Ghost entity does not require any clean up. Add two missing cases that deal with block statements. * freeze.adb Add with and use clauses for Ghost. (Freeze_Entity): Capture/restore the value of Ghost_Mode on entry/exit. Set the Ghost_Mode in effect. (Restore_Globals): New routine. * frontend.adb Add with and use clauses for Ghost. Remove any ignored Ghost code from all units that qualify. * ghost.adb New unit. * ghost.ads New unit. * gnat1drv.adb Add with clause for Ghost. Initialize and lock the table in package Ghost. * lib.ads: Alphabetize several subprogram declarations. * lib-xref.adb (Output_References): Do not generate reference information for ignored Ghost entities. * opt.ads Add new type Ghost_Mode_Type and new global variable Ghost_Mode. * rtsfind.adb (Load_RTU): Provide a clean environment when loading a runtime unit. * sem.adb (Analyze): Capture/restore the value of Ghost_Mode on entry/exit as the node may set a different mode. (Do_Analyze): Capture/restore the value of Ghost_Mode on entry/exit as the unit may be withed from a unit with a different Ghost mode. * sem_ch3.adb Add with and use clauses for Ghost. (Analyze_Full_Type_Declaration, Analyze_Incomplete_Type_Decl, Analyze_Number_Declaration, Analyze_Private_Extension_Declaration, Analyze_Subtype_Declaration): Set the Ghost_Mode in effect. Mark the entity as Ghost when there is a Ghost_Mode in effect. (Array_Type_Declaration): The implicit base type inherits the "ghostness" from the array type. (Derive_Subprogram): The alias inherits the "ghostness" from the parent subprogram. (Make_Implicit_Base): The implicit base type inherits the "ghostness" from the parent type. * sem_ch5.adb Add with and use clauses for Ghost. (Analyze_Assignment): Set the Ghost_Mode in effect. * sem_ch6.adb Add with and use clauses for Ghost. (Analyze_Abstract_Subprogram_Declaration, Analyze_Procedure_Call, Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Declaration): Set the Ghost_Mode in effect. Mark the entity as Ghost when there is a Ghost_Mode in effect. * sem_ch7.adb Add with and use clauses for Ghost. (Analyze_Package_Body_Helper, Analyze_Package_Declaration, Analyze_Private_Type_Declaration): Set the Ghost_Mode in effect. Mark the entity as Ghost when there is a Ghost_Mode in effect. * sem_ch8.adb Add with and use clauses for Ghost. (Analyze_Exception_Renaming, Analyze_Generic_Renaming, Analyze_Object_Renaming, Analyze_Package_Renaming, Analyze_Subprogram_Renaming): Set the Ghost_Mode in effect. Mark the entity as Ghost when there is a Ghost_Mode in effect. (Find_Type): Check the Ghost context of a type. * sem_ch11.adb Add with and use clauses for Ghost. (Analyze_Exception_Declaration): Set the Ghost_Mode in effect. Mark the entity as Ghost when there is a Ghost_Mode in effect. * sem_ch12.adb Add with and use clauses for Ghost. (Analyze_Generic_Package_Declaration, Analyze_Generic_Subprogram_Declaration): Set the Ghost_Mode in effect. Mark the entity as Ghost when there is a Ghost_Mode in effect. * sem_prag.adb Add with and use clauses for Ghost. (Analyze_Pragma): Ghost-related checks are triggered when there is a Ghost mode in effect. (Create_Abstract_State): Mark the entity as Ghost when there is a Ghost_Mode in effect. * sem_res.adb Add with and use clauses for Ghost. (Check_Ghost_Context): Removed. * sem_util.adb (Check_Ghost_Completion): Removed. (Check_Ghost_Derivation): Removed. (Incomplete_Or_Partial_View): Add a guard in case the entity has not been analyzed yet and does carry a scope. (Is_Declaration): New routine. (Is_Ghost_Entity): Removed. (Is_Ghost_Statement_Or_Pragma): Removed. (Is_Subject_To_Ghost): Removed. (Set_Is_Ghost_Entity): Removed. (Within_Ghost_Scope): Removed. * sem_util.adb (Check_Ghost_Completion): Removed. (Check_Ghost_Derivation): Removed. (Is_Declaration): New routine. (Is_Ghost_Entity): Removed. (Is_Ghost_Statement_Or_Pragma): Removed. (Is_Subject_To_Ghost): Removed. (Set_Is_Ghost_Entity): Removed. (Within_Ghost_Scope): Removed. * sinfo.ads Add a section on Ghost mode. * treepr.adb (Print_Header_Flag): New routine. (Print_Node_Header): Factor out code. Output flag Is_Ignored_Ghost_Node. * gcc-interface/Make-lang.in: Add dependency for unit Ghost. From-SVN: r219280 --- gcc/ada/ChangeLog | 135 ++++ gcc/ada/alloc.ads | 13 +- gcc/ada/atree.adb | 72 ++- gcc/ada/atree.ads | 104 ++-- gcc/ada/einfo.adb | 45 +- gcc/ada/einfo.ads | 21 +- gcc/ada/exp_ch3.adb | 30 + gcc/ada/exp_ch7.adb | 63 +- gcc/ada/exp_dbug.adb | 16 +- gcc/ada/exp_disp.adb | 30 + gcc/ada/exp_util.adb | 84 ++- gcc/ada/freeze.adb | 57 +- gcc/ada/frontend.adb | 10 +- gcc/ada/gcc-interface/Make-lang.in | 1 + gcc/ada/ghost.adb | 949 +++++++++++++++++++++++++++++ gcc/ada/ghost.ads | 115 ++++ gcc/ada/gnat1drv.adb | 6 +- gcc/ada/lib-xref.adb | 20 +- gcc/ada/lib.ads | 240 ++++---- gcc/ada/opt.ads | 8 + gcc/ada/rtsfind.adb | 14 + gcc/ada/sem.adb | 217 ++++--- gcc/ada/sem_ch11.adb | 12 +- gcc/ada/sem_ch12.adb | 20 +- gcc/ada/sem_ch3.adb | 141 +++-- gcc/ada/sem_ch5.adb | 8 + gcc/ada/sem_ch6.adb | 63 +- gcc/ada/sem_ch7.adb | 26 +- gcc/ada/sem_ch8.adb | 46 +- gcc/ada/sem_prag.adb | 16 +- gcc/ada/sem_res.adb | 192 +----- gcc/ada/sem_util.adb | 386 ++---------- gcc/ada/sem_util.ads | 42 +- gcc/ada/sinfo.ads | 26 + gcc/ada/treepr.adb | 52 +- 35 files changed, 2281 insertions(+), 999 deletions(-) create mode 100644 gcc/ada/ghost.adb create mode 100644 gcc/ada/ghost.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6e363c35f19..39b20091d49 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,138 @@ +2015-01-07 Hristian Kirtchev + + * alloc.ads Alphabetize several declarations. Add constants + Ignored_Ghost_Units_Initial and Ignored_Ghost_Units_Increment. + * atree.adb Add with and use clauses for Opt. + (Allocate_Initialize_Node): Mark a node as ignored Ghost + if it is created in an ignored Ghost region. + (Ekind_In): New variant. + (Is_Ignored_Ghost_Node): New routine. + (Set_Is_Ignored_Ghost_Node): New routine. + * atree.adb Aplhabetize several subprograms declarations. Flag + Spare0 is now known as Is_Ignored_Ghost_Node. + (Ekind_In): New variant. + (Is_Ignored_Ghost_Node): New routine. + (Set_Is_Ignored_Ghost_Node): New routine. + * einfo.adb: Flag 279 is now known as Contains_Ignored_Ghost_Code. + (Contains_Ignored_Ghost_Code): New routine. + (Set_Contains_Ignored_Ghost_Code): New routine. + (Set_Is_Checked_Ghost_Entity, Set_Is_Ignored_Ghost_Entity): + It is now possible to set this property on an unanalyzed entity. + (Write_Entity_Flags): Output the status of flag + Contains_Ignored_Ghost_Code. + * einfo.ads New attribute Contains_Ignored_Ghost_Code along with + usage in nodes. + (Contains_Ignored_Ghost_Code): New routine + along with pragma Inline. + (Set_Contains_Ignored_Ghost_Code): New routine along with pragma Inline. + * exp_ch3.adb Add with and use clauses for Ghost. + (Freeze_Type): Capture/restore the value of Ghost_Mode on entry/exit. + Set the Ghost_Mode in effect. + (Restore_Globals): New routine. + * exp_ch7.adb (Process_Declarations): Do not process a context + that invoves an ignored Ghost entity. + * exp_dbug.adb (Qualify_All_Entity_Names): Skip an ignored Ghost + construct that has been rewritten as a null statement. + * exp_disp.adb Add with and use clauses for Ghost. + (Make_DT): Capture/restore the value of Ghost_Mode on entry/exit. Set + the Ghost_Mode in effect. + (Restore_Globals): New routine. + * exp_util.adb (Requires_Cleanup_Actions): An ignored Ghost entity + does not require any clean up. Add two missing cases that deal + with block statements. + * freeze.adb Add with and use clauses for Ghost. + (Freeze_Entity): Capture/restore the value of Ghost_Mode on entry/exit. + Set the Ghost_Mode in effect. + (Restore_Globals): New routine. + * frontend.adb Add with and use clauses for Ghost. Remove any + ignored Ghost code from all units that qualify. + * ghost.adb New unit. + * ghost.ads New unit. + * gnat1drv.adb Add with clause for Ghost. Initialize and lock + the table in package Ghost. + * lib.ads: Alphabetize several subprogram declarations. + * lib-xref.adb (Output_References): Do not generate reference + information for ignored Ghost entities. + * opt.ads Add new type Ghost_Mode_Type and new global variable + Ghost_Mode. + * rtsfind.adb (Load_RTU): Provide a clean environment when + loading a runtime unit. + * sem.adb (Analyze): Capture/restore the value of Ghost_Mode on + entry/exit as the node may set a different mode. + (Do_Analyze): + Capture/restore the value of Ghost_Mode on entry/exit as the + unit may be withed from a unit with a different Ghost mode. + * sem_ch3.adb Add with and use clauses for Ghost. + (Analyze_Full_Type_Declaration, Analyze_Incomplete_Type_Decl, + Analyze_Number_Declaration, Analyze_Private_Extension_Declaration, + Analyze_Subtype_Declaration): Set the Ghost_Mode in effect. Mark + the entity as Ghost when there is a Ghost_Mode in effect. + (Array_Type_Declaration): The implicit base type inherits the + "ghostness" from the array type. + (Derive_Subprogram): The + alias inherits the "ghostness" from the parent subprogram. + (Make_Implicit_Base): The implicit base type inherits the + "ghostness" from the parent type. + * sem_ch5.adb Add with and use clauses for Ghost. + (Analyze_Assignment): Set the Ghost_Mode in effect. + * sem_ch6.adb Add with and use clauses for Ghost. + (Analyze_Abstract_Subprogram_Declaration, Analyze_Procedure_Call, + Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Declaration): + Set the Ghost_Mode in effect. Mark the entity as Ghost when + there is a Ghost_Mode in effect. + * sem_ch7.adb Add with and use clauses for Ghost. + (Analyze_Package_Body_Helper, Analyze_Package_Declaration, + Analyze_Private_Type_Declaration): Set the Ghost_Mode in + effect. Mark the entity as Ghost when there is a Ghost_Mode + in effect. + * sem_ch8.adb Add with and use clauses for Ghost. + (Analyze_Exception_Renaming, Analyze_Generic_Renaming, + Analyze_Object_Renaming, Analyze_Package_Renaming, + Analyze_Subprogram_Renaming): Set the Ghost_Mode in effect. Mark + the entity as Ghost when there is a Ghost_Mode in effect. + (Find_Type): Check the Ghost context of a type. + * sem_ch11.adb Add with and use clauses for Ghost. + (Analyze_Exception_Declaration): Set the Ghost_Mode in + effect. Mark the entity as Ghost when there is a Ghost_Mode + in effect. + * sem_ch12.adb Add with and use clauses for Ghost. + (Analyze_Generic_Package_Declaration, + Analyze_Generic_Subprogram_Declaration): Set the Ghost_Mode in effect. + Mark the entity as Ghost when there is a Ghost_Mode in effect. + * sem_prag.adb Add with and use clauses for Ghost. + (Analyze_Pragma): Ghost-related checks are triggered when there + is a Ghost mode in effect. + (Create_Abstract_State): Mark the + entity as Ghost when there is a Ghost_Mode in effect. + * sem_res.adb Add with and use clauses for Ghost. + (Check_Ghost_Context): Removed. + * sem_util.adb (Check_Ghost_Completion): Removed. + (Check_Ghost_Derivation): Removed. + (Incomplete_Or_Partial_View): + Add a guard in case the entity has not been analyzed yet + and does carry a scope. + (Is_Declaration): New routine. + (Is_Ghost_Entity): Removed. + (Is_Ghost_Statement_Or_Pragma): + Removed. + (Is_Subject_To_Ghost): Removed. + (Set_Is_Ghost_Entity): + Removed. + (Within_Ghost_Scope): Removed. + * sem_util.adb (Check_Ghost_Completion): Removed. + (Check_Ghost_Derivation): Removed. + (Is_Declaration): New routine. + (Is_Ghost_Entity): Removed. + (Is_Ghost_Statement_Or_Pragma): Removed. + (Is_Subject_To_Ghost): Removed. + (Set_Is_Ghost_Entity): Removed. + (Within_Ghost_Scope): Removed. + * sinfo.ads Add a section on Ghost mode. + * treepr.adb (Print_Header_Flag): New routine. + (Print_Node_Header): Factor out code. Output flag + Is_Ignored_Ghost_Node. + * gcc-interface/Make-lang.in: Add dependency for unit Ghost. + 2015-01-06 Eric Botcazou * freeze.adb (Freeze_Array_Type) : Remove always diff --git a/gcc/ada/alloc.ads b/gcc/ada/alloc.ads index 18a2be62157..e175f8b433d 100644 --- a/gcc/ada/alloc.ads +++ b/gcc/ada/alloc.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -64,14 +64,17 @@ package Alloc is File_Name_Chars_Initial : constant := 10_000; -- Osint File_Name_Chars_Increment : constant := 100; - Inlined_Bodies_Initial : constant := 50; -- Inline - Inlined_Bodies_Increment : constant := 200; + In_Out_Warnings_Initial : constant := 100; -- Sem_Warn + In_Out_Warnings_Increment : constant := 100; + + Ignored_Ghost_Units_Initial : constant := 20; -- Sem_Util + Ignored_Ghost_Units_Increment : constant := 50; Inlined_Initial : constant := 100; -- Inline Inlined_Increment : constant := 100; - In_Out_Warnings_Initial : constant := 100; -- Sem_Warn - In_Out_Warnings_Increment : constant := 100; + Inlined_Bodies_Initial : constant := 50; -- Inline + Inlined_Bodies_Increment : constant := 200; Interp_Map_Initial : constant := 200; -- Sem_Type Interp_Map_Increment : constant := 100; diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index eb196e4fa1c..3264ac37867 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -39,6 +39,7 @@ pragma Style_Checks (All_Checks); with Aspects; use Aspects; with Debug; use Debug; with Nlists; use Nlists; +with Opt; use Opt; with Output; use Output; with Sinput; use Sinput; with Tree_IO; use Tree_IO; @@ -569,10 +570,10 @@ package body Atree is then New_Id := Src; - else - -- We are allocating a new node, or extending a node - -- other than Nodes.Last. + -- We are allocating a new node, or extending a node other than + -- Nodes.Last. + else if Present (Src) then Nodes.Append (Nodes.Table (Src)); Flags.Append (Flags.Table (Src)); @@ -586,6 +587,13 @@ package body Atree is Node_Count := Node_Count + 1; end if; + -- Mark the node as ignored Ghost if it is created in an ignored Ghost + -- region. + + if Ghost_Mode = Ignore then + Set_Is_Ignored_Ghost_Node (New_Id); + end if; + -- Specifically copy Paren_Count to deal with creating new table entry -- if the parentheses count is at the maximum possible value already. @@ -1079,6 +1087,30 @@ package body Atree is T = V8; end Ekind_In; + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8 or else + T = V9; + end Ekind_In; + function Ekind_In (E : Entity_Id; V1 : Entity_Kind; @@ -1163,6 +1195,22 @@ package body Atree is return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8); end Ekind_In; + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind) return Boolean + is + begin + return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9); + end Ekind_In; + ------------------------ -- Set_Reporting_Proc -- ------------------------ @@ -1382,6 +1430,15 @@ package body Atree is Set_Error_Posted (Error, True); end Initialize; + --------------------------- + -- Is_Ignored_Ghost_Node -- + --------------------------- + + function Is_Ignored_Ghost_Node (N : Node_Id) return Boolean is + begin + return Flags.Table (N).Is_Ignored_Ghost_Node; + end Is_Ignored_Ghost_Node; + -------------------------- -- Is_Rewrite_Insertion -- -------------------------- @@ -2031,6 +2088,15 @@ package body Atree is Nodes.Table (N).Has_Aspects := Val; end Set_Has_Aspects; + ------------------------------- + -- Set_Is_Ignored_Ghost_Node -- + ------------------------------- + + procedure Set_Is_Ignored_Ghost_Node (N : Node_Id; Val : Boolean := True) is + begin + Flags.Table (N).Is_Ignored_Ghost_Node := Val; + end Set_Is_Ignored_Ghost_Node; + ----------------------- -- Set_Original_Node -- ----------------------- diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 3bc71f5974d..7d2e64f4f88 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -605,42 +605,46 @@ package Atree is -- The following functions return the contents of the indicated field of -- the node referenced by the argument, which is a Node_Id. - function Nkind (N : Node_Id) return Node_Kind; - pragma Inline (Nkind); - function Analyzed (N : Node_Id) return Boolean; pragma Inline (Analyzed); - function Has_Aspects (N : Node_Id) return Boolean; - pragma Inline (Has_Aspects); - function Comes_From_Source (N : Node_Id) return Boolean; pragma Inline (Comes_From_Source); function Error_Posted (N : Node_Id) return Boolean; pragma Inline (Error_Posted); - function Sloc (N : Node_Id) return Source_Ptr; - pragma Inline (Sloc); + function Has_Aspects (N : Node_Id) return Boolean; + pragma Inline (Has_Aspects); - function Paren_Count (N : Node_Id) return Nat; - pragma Inline (Paren_Count); + function Is_Ignored_Ghost_Node + (N : Node_Id) return Boolean; + pragma Inline (Is_Ignored_Ghost_Node); - function Parent (N : Node_Id) return Node_Id; - pragma Inline (Parent); - -- Returns the parent of a node if the node is not a list member, or else - -- the parent of the list containing the node if the node is a list member. + function Nkind (N : Node_Id) return Node_Kind; + pragma Inline (Nkind); function No (N : Node_Id) return Boolean; pragma Inline (No); -- Tests given Id for equality with the Empty node. This allows notations -- like "if No (Variant_Part)" as opposed to "if Variant_Part = Empty". + function Parent (N : Node_Id) return Node_Id; + pragma Inline (Parent); + -- Returns the parent of a node if the node is not a list member, or else + -- the parent of the list containing the node if the node is a list member. + + function Paren_Count (N : Node_Id) return Nat; + pragma Inline (Paren_Count); + function Present (N : Node_Id) return Boolean; pragma Inline (Present); -- Tests given Id for inequality with the Empty node. This allows notations -- like "if Present (Statement)" as opposed to "if Statement /= Empty". + function Sloc (N : Node_Id) return Source_Ptr; + pragma Inline (Sloc); + --------------------- -- Node_Kind Tests -- --------------------- @@ -784,6 +788,18 @@ package Atree is V7 : Entity_Kind; V8 : Entity_Kind) return Boolean; + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind) return Boolean; + function Ekind_In (T : Entity_Kind; V1 : Entity_Kind; @@ -840,6 +856,18 @@ package Atree is V7 : Entity_Kind; V8 : Entity_Kind) return Boolean; + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind; + V9 : Entity_Kind) return Boolean; + pragma Inline (Ekind_In); -- Inline all above functions @@ -865,39 +893,42 @@ package Atree is -- to be set in the specified field. Note that Set_Nkind is in the next -- section, since its use is restricted. - procedure Set_Sloc (N : Node_Id; Val : Source_Ptr); - pragma Inline (Set_Sloc); - - procedure Set_Paren_Count (N : Node_Id; Val : Nat); - pragma Inline (Set_Paren_Count); - - procedure Set_Parent (N : Node_Id; Val : Node_Id); - pragma Inline (Set_Parent); - - procedure Set_Analyzed (N : Node_Id; Val : Boolean := True); + procedure Set_Analyzed (N : Node_Id; Val : Boolean := True); pragma Inline (Set_Analyzed); - procedure Set_Error_Posted (N : Node_Id; Val : Boolean := True); - pragma Inline (Set_Error_Posted); - procedure Set_Comes_From_Source (N : Node_Id; Val : Boolean); pragma Inline (Set_Comes_From_Source); - -- Note that this routine is very rarely used, since usually the - -- default mechanism provided sets the right value, but in some - -- unusual cases, the value needs to be reset (e.g. when a source - -- node is copied, and the copy must not have Comes_From_Source set). + -- Note that this routine is very rarely used, since usually the default + -- mechanism provided sets the right value, but in some unusual cases, the + -- value needs to be reset (e.g. when a source node is copied, and the copy + -- must not have Comes_From_Source set). + + procedure Set_Error_Posted (N : Node_Id; Val : Boolean := True); + pragma Inline (Set_Error_Posted); procedure Set_Has_Aspects (N : Node_Id; Val : Boolean := True); pragma Inline (Set_Has_Aspects); + procedure Set_Is_Ignored_Ghost_Node (N : Node_Id; Val : Boolean := True); + pragma Inline (Set_Is_Ignored_Ghost_Node); + procedure Set_Original_Node (N : Node_Id; Val : Node_Id); pragma Inline (Set_Original_Node); -- Note that this routine is used only in very peculiar cases. In normal -- cases, the Original_Node link is set by calls to Rewrite. We currently - -- use it in ASIS mode to manually set the link from pragma expressions - -- to their aspect original source expressions, so that the original source + -- use it in ASIS mode to manually set the link from pragma expressions to + -- their aspect original source expressions, so that the original source -- expressions accessed by ASIS are also semantically analyzed. + procedure Set_Parent (N : Node_Id; Val : Node_Id); + pragma Inline (Set_Parent); + + procedure Set_Paren_Count (N : Node_Id; Val : Nat); + pragma Inline (Set_Paren_Count); + + procedure Set_Sloc (N : Node_Id; Val : Source_Ptr); + pragma Inline (Set_Sloc); + ------------------------------ -- Entity Update Procedures -- ------------------------------ @@ -4007,7 +4038,12 @@ package Atree is Flag1 : Boolean; Flag2 : Boolean; Flag3 : Boolean; - Spare0 : Boolean; + + Is_Ignored_Ghost_Node : Boolean; + -- Flag denothing whether the node is subject to pragma Ghost with + -- policy Ignore. The name of the flag should be Flag4, however this + -- requires changing the names of all remaining 300+ flags. + Spare1 : Boolean; Spare2 : Boolean; Spare3 : Boolean; diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 7407d48f0ea..de4e1ef540a 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -574,8 +574,8 @@ package body Einfo is -- No_Dynamic_Predicate_On_Actual Flag276 -- Is_Checked_Ghost_Entity Flag277 -- Is_Ignored_Ghost_Entity Flag278 + -- Contains_Ignored_Ghost_Code Flag279 - -- (unused) Flag279 -- (unused) Flag280 -- (unused) Flag281 @@ -1117,6 +1117,21 @@ package body Einfo is return Node18 (Id); end Entry_Index_Constant; + function Contains_Ignored_Ghost_Code (Id : E) return B is + begin + pragma Assert + (Ekind_In (Id, E_Block, + E_Function, + E_Generic_Function, + E_Generic_Package, + E_Generic_Procedure, + E_Package, + E_Package_Body, + E_Procedure, + E_Subprogram_Body)); + return Flag279 (Id); + end Contains_Ignored_Ghost_Code; + function Contract (Id : E) return N is begin pragma Assert @@ -3609,6 +3624,21 @@ package body Einfo is Set_Node20 (Id, V); end Set_Component_Type; + procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True) is + begin + pragma Assert + (Ekind_In (Id, E_Block, + E_Function, + E_Generic_Function, + E_Generic_Package, + E_Generic_Procedure, + E_Package, + E_Package_Body, + E_Procedure, + E_Subprogram_Body)); + Set_Flag279 (Id, V); + end Set_Contains_Ignored_Ghost_Code; + procedure Set_Contract (Id : E; V : N) is begin pragma Assert @@ -4747,7 +4777,11 @@ package body Einfo is or else Ekind (Id) = E_Discriminant or else Ekind (Id) = E_Exception or else Ekind (Id) = E_Package_Body - or else Ekind (Id) = E_Subprogram_Body); + or else Ekind (Id) = E_Subprogram_Body + + -- Allow this attribute to appear on non-analyzed entities + + or else Ekind (Id) = E_Void); Set_Flag277 (Id, V); end Set_Is_Checked_Ghost_Entity; @@ -4942,7 +4976,11 @@ package body Einfo is or else Ekind (Id) = E_Discriminant or else Ekind (Id) = E_Exception or else Ekind (Id) = E_Package_Body - or else Ekind (Id) = E_Subprogram_Body); + or else Ekind (Id) = E_Subprogram_Body + + -- Allow this attribute to appear on non-analyzed entities + + or else Ekind (Id) = E_Void); Set_Flag278 (Id, V); end Set_Is_Ignored_Ghost_Entity; @@ -8371,6 +8409,7 @@ package body Einfo is W ("C_Pass_By_Copy", Flag125 (Id)); W ("Can_Never_Be_Null", Flag38 (Id)); W ("Checks_May_Be_Suppressed", Flag31 (Id)); + W ("Contains_Ignored_Ghost_Code", Flag279 (Id)); W ("Debug_Info_Off", Flag166 (Id)); W ("Default_Expressions_Processed", Flag108 (Id)); W ("Delay_Cleanups", Flag114 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 91d7c56ddf6..938559a0fcd 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -661,6 +661,11 @@ package Einfo is -- Component_Type (Node20) [implementation base type only] -- Defined in array types and string types. References component type. +-- Contains_Ignored_Ghost_Code (Flag279) +-- Defined in blocks, packages and their bodies, subprograms and their +-- bodies. Set if the entity contains any ignored Ghost code in the form +-- of declaration, procedure call, assignment statement or pragma. + -- Corresponding_Concurrent_Type (Node18) -- Defined in record types that are constructed by the expander to -- represent task and protected types (Is_Concurrent_Record_Type flag @@ -5458,6 +5463,7 @@ package Einfo is -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) -- Entry_Cancel_Parameter (Node23) + -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Cleanups (Flag114) -- Discard_Names (Flag88) -- Has_Master_Entity (Flag21) @@ -5531,8 +5537,8 @@ package Einfo is -- Has_Biased_Representation (Flag139) -- Has_Completion (Flag26) (constants only) -- Has_Independent_Components (Flag34) - -- Has_Thunks (Flag228) (constants only) -- Has_Size_Clause (Flag29) + -- Has_Thunks (Flag228) (constants only) -- Has_Up_Level_Access (Flag215) -- Has_Volatile_Components (Flag87) -- Is_Atomic (Flag85) @@ -5709,11 +5715,12 @@ package Einfo is -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Body_Needed_For_SAL (Flag40) - -- Elaboration_Entity_Required (Flag174) + -- Contains_Ignored_Ghost_Code (Flag279) -- Default_Expressions_Processed (Flag108) -- Delay_Cleanups (Flag114) -- Delay_Subprogram_Descriptors (Flag50) -- Discard_Names (Flag88) + -- Elaboration_Entity_Required (Flag174) -- Has_Anonymous_Master (Flag253) -- Has_Completion (Flag26) -- Has_Controlling_Result (Flag98) @@ -5921,6 +5928,7 @@ package Einfo is -- Contract (Node34) -- Delay_Subprogram_Descriptors (Flag50) -- Body_Needed_For_SAL (Flag40) + -- Contains_Ignored_Ghost_Code (Flag279) -- Discard_Names (Flag88) -- Elaboration_Entity_Required (Flag174) -- Elaborate_Body_Desirable (Flag210) (non-generic case only) @@ -5955,6 +5963,7 @@ package Einfo is -- SPARK_Aux_Pragma (Node33) -- SPARK_Pragma (Node32) -- Contract (Node34) + -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Subprogram_Descriptors (Flag50) -- Has_Anonymous_Master (Flag253) -- SPARK_Aux_Pragma_Inherited (Flag266) @@ -6005,6 +6014,7 @@ package Einfo is -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Body_Needed_For_SAL (Flag40) + -- Contains_Ignored_Ghost_Code (Flag279) -- Delay_Cleanups (Flag114) -- Discard_Names (Flag88) -- Elaboration_Entity_Required (Flag174) @@ -6174,8 +6184,9 @@ package Einfo is -- Scope_Depth_Value (Uint22) -- Extra_Formals (Node28) -- SPARK_Pragma (Node32) - -- SPARK_Pragma_Inherited (Flag265) -- Contract (Node34) + -- Contains_Ignored_Ghost_Code (Flag279) + -- SPARK_Pragma_Inherited (Flag265) -- Scope_Depth (synth) -- E_Subprogram_Type @@ -6527,6 +6538,7 @@ package Einfo is function Component_Clause (Id : E) return N; function Component_Size (Id : E) return U; function Component_Type (Id : E) return E; + function Contains_Ignored_Ghost_Code (Id : E) return B; function Contract (Id : E) return N; function Corresponding_Concurrent_Type (Id : E) return E; function Corresponding_Discriminant (Id : E) return E; @@ -7168,6 +7180,7 @@ package Einfo is procedure Set_Component_Clause (Id : E; V : N); procedure Set_Component_Size (Id : E; V : U); procedure Set_Component_Type (Id : E; V : E); + procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True); procedure Set_Contract (Id : E; V : N); procedure Set_Corresponding_Concurrent_Type (Id : E; V : E); procedure Set_Corresponding_Discriminant (Id : E; V : E); @@ -7924,6 +7937,7 @@ package Einfo is pragma Inline (Component_Clause); pragma Inline (Component_Size); pragma Inline (Component_Type); + pragma Inline (Contains_Ignored_Ghost_Code); pragma Inline (Contract); pragma Inline (Corresponding_Concurrent_Type); pragma Inline (Corresponding_Discriminant); @@ -8413,6 +8427,7 @@ package Einfo is pragma Inline (Set_Component_Clause); pragma Inline (Set_Component_Size); pragma Inline (Set_Component_Type); + pragma Inline (Set_Contains_Ignored_Ghost_Code); pragma Inline (Set_Contract); pragma Inline (Set_Corresponding_Concurrent_Type); pragma Inline (Set_Corresponding_Discriminant); diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index f2f42d4d9fd..d45dbddc41b 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -43,6 +43,7 @@ with Exp_Strm; use Exp_Strm; with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Freeze; use Freeze; +with Ghost; use Ghost; with Namet; use Namet; with Nlists; use Nlists; with Nmake; use Nmake; @@ -7427,11 +7428,37 @@ package body Exp_Ch3 is -- node using Append_Freeze_Actions. function Freeze_Type (N : Node_Id) return Boolean is + GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the current Ghost mode in effect in case the type being frozen + -- sets a different mode. + + procedure Restore_Globals; + -- Restore the values of all saved global variables + + --------------------- + -- Restore_Globals -- + --------------------- + + procedure Restore_Globals is + begin + Ghost_Mode := GM; + end Restore_Globals; + + -- Local variables + Def_Id : constant Entity_Id := Entity (N); RACW_Seen : Boolean := False; Result : Boolean := False; + -- Start of processing for Freeze_Type + begin + -- The type being frozen may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- freezing are properly flagged as ignored Ghost. + + Set_Ghost_Mode_For_Freeze (Def_Id, N); + -- Process associated access types needing special processing if Present (Access_Types_To_Process (N)) then @@ -7750,10 +7777,13 @@ package body Exp_Ch3 is end if; Freeze_Stream_Operations (N, Def_Id); + + Restore_Globals; return Result; exception when RE_Not_Available => + Restore_Globals; return False; end Freeze_Type; diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index de60b4abed2..f611fada6d4 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -1741,13 +1741,19 @@ package body Exp_Ch7 is if Nkind (Decl) = N_Full_Type_Declaration then Typ := Defining_Identifier (Decl); - if Is_Tagged_Type (Typ) + -- Ignored Ghost types do not need any cleanup actions because + -- they will not appear in the final tree. + + if Is_Ignored_Ghost_Entity (Typ) then + null; + + elsif Is_Tagged_Type (Typ) and then Is_Library_Level_Entity (Typ) and then Convention (Typ) = Convention_Ada and then Present (Access_Disp_Table (Typ)) and then RTE_Available (RE_Register_Tag) - and then not No_Run_Time_Mode and then not Is_Abstract_Type (Typ) + and then not No_Run_Time_Mode then Processing_Actions; end if; @@ -1773,6 +1779,12 @@ package body Exp_Ch7 is elsif Is_Processed_Transient (Obj_Id) then null; + -- Ignored Ghost objects do not need any cleanup actions + -- because they will not appear in the final tree. + + elsif Is_Ignored_Ghost_Entity (Obj_Id) then + null; + -- The object is of the form: -- Obj : Typ [:= Expr]; @@ -1880,6 +1892,12 @@ package body Exp_Ch7 is if For_Package and then Finalize_Storage_Only (Obj_Typ) then null; + -- Ignored Ghost object renamings do not need any cleanup + -- actions because they will not appear in the final tree. + + elsif Is_Ignored_Ghost_Entity (Obj_Id) then + null; + -- Return object of a build-in-place function. This case is -- recognized and marked by the expansion of an extended return -- statement (see Expand_N_Extended_Return_Statement). @@ -1921,11 +1939,17 @@ package body Exp_Ch7 is then Typ := Entity (Decl); - if (Is_Access_Type (Typ) - and then not Is_Access_Subprogram_Type (Typ) - and then Needs_Finalization - (Available_View (Designated_Type (Typ)))) - or else (Is_Type (Typ) and then Needs_Finalization (Typ)) + -- Freeze nodes for ignored Ghost types do not need cleanup + -- actions because they will never appear in the final tree. + + if Is_Ignored_Ghost_Entity (Typ) then + null; + + elsif (Is_Access_Type (Typ) + and then not Is_Access_Subprogram_Type (Typ) + and then Needs_Finalization + (Available_View (Designated_Type (Typ)))) + or else (Is_Type (Typ) and then Needs_Finalization (Typ)) then Old_Counter_Val := Counter_Val; @@ -1950,14 +1974,16 @@ package body Exp_Ch7 is -- Nested package declarations, avoid generics elsif Nkind (Decl) = N_Package_Declaration then - Spec := Specification (Decl); - Pack_Id := Defining_Unit_Name (Spec); + Pack_Id := Defining_Entity (Decl); + Spec := Specification (Decl); - if Nkind (Pack_Id) = N_Defining_Program_Unit_Name then - Pack_Id := Defining_Identifier (Pack_Id); - end if; + -- Do not inspect an ignored Ghost package because all code + -- found within will not appear in the final tree. + + if Is_Ignored_Ghost_Entity (Pack_Id) then + null; - if Ekind (Pack_Id) /= E_Generic_Package then + elsif Ekind (Pack_Id) /= E_Generic_Package then Old_Counter_Val := Counter_Val; Process_Declarations (Private_Declarations (Spec), Preprocess); @@ -1980,9 +2006,16 @@ package body Exp_Ch7 is -- Nested package bodies, avoid generics elsif Nkind (Decl) = N_Package_Body then - Spec := Corresponding_Spec (Decl); - if Ekind (Spec) /= E_Generic_Package then + -- Do not inspect an ignored Ghost package body because all + -- code found within will not appear in the final tree. + + if Is_Ignored_Ghost_Entity (Defining_Entity (Decl)) then + null; + + elsif Ekind (Corresponding_Spec (Decl)) /= + E_Generic_Package + then Old_Counter_Val := Counter_Val; Process_Declarations (Declarations (Decl), Preprocess); diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb index 80bf4ed235a..3ed470a4d91 100644 --- a/gcc/ada/exp_dbug.adb +++ b/gcc/ada/exp_dbug.adb @@ -1101,10 +1101,21 @@ package body Exp_Dbug is procedure Qualify_All_Entity_Names is E : Entity_Id; Ent : Entity_Id; + Nod : Node_Id; begin for J in Name_Qualify_Units.First .. Name_Qualify_Units.Last loop - E := Defining_Entity (Name_Qualify_Units.Table (J)); + Nod := Name_Qualify_Units.Table (J); + + -- When a scoping construct is ignored Ghost, it is rewritten as + -- a null statement. Skip such constructs as they no longer carry + -- names. + + if Nkind (Nod) = N_Null_Statement then + goto Continue; + end if; + + E := Defining_Entity (Nod); Reset_Buffers; Qualify_Entity_Name (E); @@ -1128,6 +1139,9 @@ package body Exp_Dbug is exit when Ent = E; end loop; end if; + + <> + null; end loop; end Qualify_All_Entity_Names; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 905311b6eb9..3f999647413 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -36,6 +36,7 @@ with Exp_Dbug; use Exp_Dbug; with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Freeze; use Freeze; +with Ghost; use Ghost; with Itypes; use Itypes; with Layout; use Layout; with Nlists; use Nlists; @@ -3663,6 +3664,10 @@ package body Exp_Disp is -- end; function Make_DT (Typ : Entity_Id; N : Node_Id := Empty) return List_Id is + GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the current Ghost mode in effect in case the tagged type sets a + -- different mode. + Loc : constant Source_Ptr := Sloc (Typ); Max_Predef_Prims : constant Int := @@ -3725,6 +3730,9 @@ package body Exp_Disp is -- this secondary dispatch table by Make_Tags when its unique external -- name was generated. + procedure Restore_Globals; + -- Restore the values of all saved global variables + ------------------------------ -- Check_Premature_Freezing -- ------------------------------ @@ -4409,6 +4417,15 @@ package body Exp_Disp is Append_Elmt (Iface_DT, DT_Decl); end Make_Secondary_DT; + --------------------- + -- Restore_Globals -- + --------------------- + + procedure Restore_Globals is + begin + Ghost_Mode := GM; + end Restore_Globals; + -- Local variables Elab_Code : constant List_Id := New_List; @@ -4479,6 +4496,13 @@ package body Exp_Disp is begin pragma Assert (Is_Frozen (Typ)); + -- The tagged type for which the dispatch table is being build may be + -- subject to pragma Ghost with policy Ignore. Set the mode now to + -- ensure that any nodes generated during freezing are properly flagged + -- as ignored Ghost. + + Set_Ghost_Mode_For_Freeze (Typ, Typ); + -- Handle cases in which there is no need to build the dispatch table if Has_Dispatch_Table (Typ) @@ -4487,10 +4511,12 @@ package body Exp_Disp is or else Convention (Typ) = Convention_CIL or else Convention (Typ) = Convention_Java then + Restore_Globals; return Result; elsif No_Run_Time_Mode then Error_Msg_CRT ("tagged types", Typ); + Restore_Globals; return Result; elsif not RTE_Available (RE_Tag) then @@ -4506,6 +4532,7 @@ package body Exp_Disp is Analyze_List (Result, Suppress => All_Checks); Error_Msg_CRT ("tagged types", Typ); + Restore_Globals; return Result; end if; @@ -4516,12 +4543,14 @@ package body Exp_Disp is if RTE_Available (RE_Interface_Data) then if Max_Predef_Prims /= 15 then Error_Msg_N ("run-time library configuration error", Typ); + Restore_Globals; return Result; end if; else if Max_Predef_Prims /= 9 then Error_Msg_N ("run-time library configuration error", Typ); Error_Msg_CRT ("tagged types", Typ); + Restore_Globals; return Result; end if; end if; @@ -6242,6 +6271,7 @@ package body Exp_Disp is Register_CG_Node (Typ); + Restore_Globals; return Result; end Make_DT; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 47acc6f668c..7bc6bc3f135 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -7830,13 +7830,19 @@ package body Exp_Util is if Nkind (Decl) = N_Full_Type_Declaration then Typ := Defining_Identifier (Decl); - if Is_Tagged_Type (Typ) + -- Ignored Ghost types do not need any cleanup actions because + -- they will not appear in the final tree. + + if Is_Ignored_Ghost_Entity (Typ) then + null; + + elsif Is_Tagged_Type (Typ) and then Is_Library_Level_Entity (Typ) and then Convention (Typ) = Convention_Ada and then Present (Access_Disp_Table (Typ)) and then RTE_Available (RE_Unregister_Tag) - and then not No_Run_Time_Mode and then not Is_Abstract_Type (Typ) + and then not No_Run_Time_Mode then return True; end if; @@ -7862,6 +7868,12 @@ package body Exp_Util is elsif Is_Processed_Transient (Obj_Id) then null; + -- Ignored Ghost objects do not need any cleanup actions because + -- they will not appear in the final tree. + + elsif Is_Ignored_Ghost_Entity (Obj_Id) then + null; + -- The object is of the form: -- Obj : Typ [:= Expr]; -- @@ -7940,6 +7952,12 @@ package body Exp_Util is if Lib_Level and then Finalize_Storage_Only (Obj_Typ) then null; + -- Ignored Ghost object renamings do not need any cleanup actions + -- because they will not appear in the final tree. + + elsif Is_Ignored_Ghost_Entity (Obj_Id) then + null; + -- Return object of a build-in-place function. This case is -- recognized and marked by the expansion of an extended return -- statement (see Expand_N_Extended_Return_Statement). @@ -7981,11 +7999,17 @@ package body Exp_Util is then Typ := Entity (Decl); - if ((Is_Access_Type (Typ) - and then not Is_Access_Subprogram_Type (Typ) - and then Needs_Finalization - (Available_View (Designated_Type (Typ)))) - or else (Is_Type (Typ) and then Needs_Finalization (Typ))) + -- Freeze nodes for ignored Ghost types do not need cleanup + -- actions because they will never appear in the final tree. + + if Is_Ignored_Ghost_Entity (Typ) then + null; + + elsif ((Is_Access_Type (Typ) + and then not Is_Access_Subprogram_Type (Typ) + and then Needs_Finalization + (Available_View (Designated_Type (Typ)))) + or else (Is_Type (Typ) and then Needs_Finalization (Typ))) and then Requires_Cleanup_Actions (Actions (Decl), Lib_Level, Nested_Constructs) then @@ -7997,15 +8021,17 @@ package body Exp_Util is elsif Nested_Constructs and then Nkind (Decl) = N_Package_Declaration then - Pack_Id := Defining_Unit_Name (Specification (Decl)); + Pack_Id := Defining_Entity (Decl); - if Nkind (Pack_Id) = N_Defining_Program_Unit_Name then - Pack_Id := Defining_Identifier (Pack_Id); - end if; + -- Do not inspect an ignored Ghost package because all code found + -- within will not appear in the final tree. - if Ekind (Pack_Id) /= E_Generic_Package - and then - Requires_Cleanup_Actions (Specification (Decl), Lib_Level) + if Is_Ignored_Ghost_Entity (Pack_Id) then + null; + + elsif Ekind (Pack_Id) /= E_Generic_Package + and then Requires_Cleanup_Actions + (Specification (Decl), Lib_Level) then return True; end if; @@ -8013,13 +8039,39 @@ package body Exp_Util is -- Nested package bodies elsif Nested_Constructs and then Nkind (Decl) = N_Package_Body then - Pack_Id := Corresponding_Spec (Decl); - if Ekind (Pack_Id) /= E_Generic_Package + -- Do not inspect an ignored Ghost package body because all code + -- found within will not appear in the final tree. + + if Is_Ignored_Ghost_Entity (Defining_Entity (Decl)) then + null; + + elsif Ekind (Corresponding_Spec (Decl)) /= E_Generic_Package and then Requires_Cleanup_Actions (Decl, Lib_Level) then return True; end if; + + elsif Nkind (Decl) = N_Block_Statement + and then + + -- Handle a rare case caused by a controlled transient variable + -- created as part of a record init proc. The variable is wrapped + -- in a block, but the block is not associated with a transient + -- scope. + + (Inside_Init_Proc + + -- Handle the case where the original context has been wrapped in + -- a block to avoid interference between exception handlers and + -- At_End handlers. Treat the block as transparent and process its + -- contents. + + or else Is_Finalization_Wrapper (Decl)) + then + if Requires_Cleanup_Actions (Decl, Lib_Level) then + return True; + end if; end if; Next (Decl); diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index c07bb563c52..52d1118afa2 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -36,6 +36,7 @@ with Exp_Disp; use Exp_Disp; with Exp_Pakd; use Exp_Pakd; with Exp_Util; use Exp_Util; with Exp_Tss; use Exp_Tss; +with Ghost; use Ghost; with Layout; use Layout; with Lib; use Lib; with Namet; use Namet; @@ -1862,12 +1863,16 @@ package body Freeze is ------------------- function Freeze_Entity (E : Entity_Id; N : Node_Id) return List_Id is - Loc : constant Source_Ptr := Sloc (N); - Comp : Entity_Id; - F_Node : Node_Id; - Indx : Node_Id; - Formal : Entity_Id; - Atype : Entity_Id; + GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the current Ghost mode in effect in case the entity being frozen + -- sets a different mode. + + Loc : constant Source_Ptr := Sloc (N); + Atype : Entity_Id; + Comp : Entity_Id; + F_Node : Node_Id; + Formal : Entity_Id; + Indx : Node_Id; Test_E : Entity_Id := E; -- This could use a comment ??? @@ -1929,6 +1934,9 @@ package body Freeze is -- call, but rather must go in the package holding the function, so that -- the backend can process it in the proper context. + procedure Restore_Globals; + -- Restore the values of all saved global variables + procedure Wrap_Imported_Subprogram (E : Entity_Id); -- If E is an entity for an imported subprogram with pre/post-conditions -- then this procedure will create a wrapper to ensure that proper run- @@ -4125,6 +4133,15 @@ package body Freeze is Append_List (Result, Decls); end Late_Freeze_Subprogram; + --------------------- + -- Restore_Globals -- + --------------------- + + procedure Restore_Globals is + begin + Ghost_Mode := GM; + end Restore_Globals; + ------------------------------ -- Wrap_Imported_Subprogram -- ------------------------------ @@ -4271,6 +4288,12 @@ package body Freeze is -- Start of processing for Freeze_Entity begin + -- The entity being frozen may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- freezing are properly flagged as ignored Ghost. + + Set_Ghost_Mode_For_Freeze (E, N); + -- We are going to test for various reasons why this entity need not be -- frozen here, but in the case of an Itype that's defined within a -- record, that test actually applies to the record. @@ -4286,6 +4309,7 @@ package body Freeze is -- Do not freeze if already frozen since we only need one freeze node if Is_Frozen (E) then + Restore_Globals; return No_List; -- It is improper to freeze an external entity within a generic because @@ -4300,6 +4324,7 @@ package body Freeze is Analyze_Aspects_At_Freeze_Point (E); end if; + Restore_Globals; return No_List; -- AI05-0213: A formal incomplete type does not freeze the actual. In @@ -4310,16 +4335,19 @@ package body Freeze is and then No (Full_View (Base_Type (E))) and then Ada_Version >= Ada_2012 then + Restore_Globals; return No_List; -- Formal subprograms are never frozen elsif Is_Formal_Subprogram (E) then + Restore_Globals; return No_List; -- Generic types are never frozen as they lack delayed semantic checks elsif Is_Generic_Type (E) then + Restore_Globals; return No_List; -- Do not freeze a global entity within an inner scope created during @@ -4353,6 +4381,7 @@ package body Freeze is then exit; else + Restore_Globals; return No_List; end if; end if; @@ -4388,12 +4417,16 @@ package body Freeze is end loop; if No (S) then + Restore_Globals; return No_List; end if; end; elsif Ekind (E) = E_Generic_Package then - return Freeze_Generic_Entities (E); + Result := Freeze_Generic_Entities (E); + + Restore_Globals; + return Result; end if; -- Add checks to detect proper initialization of scalars that may appear @@ -4475,6 +4508,7 @@ package body Freeze is if not Is_Internal (E) then if not Freeze_Profile (E) then + Restore_Globals; return Result; end if; end if; @@ -4499,6 +4533,7 @@ package body Freeze is if Late_Freezing then Late_Freeze_Subprogram (E); + Restore_Globals; return No_List; end if; @@ -4830,6 +4865,7 @@ package body Freeze is and then not Has_Delayed_Freeze (E)) then Check_Compile_Time_Size (E); + Restore_Globals; return No_List; end if; @@ -5102,6 +5138,7 @@ package body Freeze is if not Is_Frozen (Root_Type (E)) then Set_Is_Frozen (E, False); + Restore_Globals; return Result; end if; @@ -5237,6 +5274,7 @@ package body Freeze is and then not Present (Full_View (E)) then Set_Is_Frozen (E, False); + Restore_Globals; return Result; -- Case of full view present @@ -5328,6 +5366,7 @@ package body Freeze is Set_RM_Size (E, RM_Size (Full_View (E))); end if; + Restore_Globals; return Result; -- Case of underlying full view present @@ -5357,6 +5396,7 @@ package body Freeze is Check_Debug_Info_Needed (E); + Restore_Globals; return Result; -- Case of no full view present. If entity is derived or subtype, @@ -5370,6 +5410,7 @@ package body Freeze is else Set_Is_Frozen (E, False); + Restore_Globals; return No_List; end if; @@ -5418,6 +5459,7 @@ package body Freeze is -- generic processing), so we never need freeze nodes for them. if Is_Generic_Type (E) then + Restore_Globals; return Result; end if; @@ -6033,6 +6075,7 @@ package body Freeze is end if; end if; + Restore_Globals; return Result; end Freeze_Entity; diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb index 7d24ae03ed9..51ea9e89a18 100644 --- a/gcc/ada/frontend.adb +++ b/gcc/ada/frontend.adb @@ -33,6 +33,7 @@ with Elists; with Exp_Dbug; with Fmap; with Fname.UF; +with Ghost; use Ghost; with Inline; use Inline; with Lib; use Lib; with Lib.Load; use Lib.Load; @@ -421,14 +422,19 @@ begin Analyze_Inlined_Bodies; end if; - -- Remove entities from program that do not have any - -- execution time references. + -- Remove entities from program that do not have any execution + -- time references. if Debug_Flag_UU then Collect_Garbage_Entities; end if; Check_Elab_Calls; + + -- Remove any ignored Ghost code as it must not appear in the + -- executable. + + Remove_Ignored_Ghost_Code; end if; -- List library units if requested diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 6fa4f4cffc5..c24c22a0e01 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -297,6 +297,7 @@ GNAT_ADA_OBJS = \ ada/g-u3spch.o \ ada/get_spark_xrefs.o \ ada/get_targ.o \ + ada/ghost.o \ ada/gnat.o \ ada/gnatvsn.o \ ada/hostparm.o \ diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb new file mode 100644 index 00000000000..b69c74ee68f --- /dev/null +++ b/gcc/ada/ghost.adb @@ -0,0 +1,949 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- G H O S T -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2014-2015, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- +-- for more details. You should have received a copy of the GNU General -- +-- Public License distributed with GNAT; see file COPYING3. If not, go to -- +-- http://www.gnu.org/licenses for a complete copy of the license. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +with Alloc; use Alloc; +with Aspects; use Aspects; +with Atree; use Atree; +with Einfo; use Einfo; +with Elists; use Elists; +with Errout; use Errout; +with Lib; use Lib; +with Namet; use Namet; +with Nlists; use Nlists; +with Nmake; use Nmake; +with Opt; use Opt; +with Sem; use Sem; +with Sem_Aux; use Sem_Aux; +with Sem_Eval; use Sem_Eval; +with Sem_Res; use Sem_Res; +with Sem_Util; use Sem_Util; +with Sinfo; use Sinfo; +with Snames; use Snames; +with Table; + +package body Ghost is + + -- The following table contains the N_Compilation_Unit node for a unit that + -- is either subject to pragma Ghost with policy Ignore or contains ignored + -- Ghost code. The table is used in the removal of ignored Ghost code from + -- units. + + package Ignored_Ghost_Units is new Table.Table ( + Table_Component_Type => Node_Id, + Table_Index_Type => Int, + Table_Low_Bound => 0, + Table_Initial => Alloc.Ignored_Ghost_Units_Initial, + Table_Increment => Alloc.Ignored_Ghost_Units_Increment, + Table_Name => "Ignored_Ghost_Units"); + + ----------------------- + -- Local Subprograms -- + ----------------------- + + procedure Propagate_Ignored_Ghost_Code (N : Node_Id); + -- Subsidiary to Set_Ghost_Mode_xxx. Signal all enclosing scopes that they + -- now contain ignored Ghost code. Add the compilation unit containing N to + -- table Ignored_Ghost_Units for post processing. + + ---------------------------- + -- Add_Ignored_Ghost_Unit -- + ---------------------------- + + procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is + begin + pragma Assert (Nkind (Unit) = N_Compilation_Unit); + + -- Avoid duplicates in the table as pruning the same unit more than once + -- is wasteful. Since ignored Ghost code tends to be grouped up, check + -- the contents of the table in reverse. + + for Index in reverse Ignored_Ghost_Units.First .. + Ignored_Ghost_Units.Last + loop + -- The unit is already present in the table, do not add it again + + if Unit = Ignored_Ghost_Units.Table (Index) then + return; + end if; + end loop; + + -- If we get here, then this is the first time the unit is being added + + Ignored_Ghost_Units.Append (Unit); + end Add_Ignored_Ghost_Unit; + + ---------------------------- + -- Check_Ghost_Completion -- + ---------------------------- + + procedure Check_Ghost_Completion + (Partial_View : Entity_Id; + Full_View : Entity_Id) + is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(15)). + + if Is_Checked_Ghost_Entity (Partial_View) + and then Policy = Name_Ignore + then + Error_Msg_Sloc := Sloc (Full_View); + + Error_Msg_N ("incompatible ghost policies in effect", Partial_View); + Error_Msg_N ("\& declared with ghost policy Check", Partial_View); + Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View); + + elsif Is_Ignored_Ghost_Entity (Partial_View) + and then Policy = Name_Check + then + Error_Msg_Sloc := Sloc (Full_View); + + Error_Msg_N ("incompatible ghost policies in effect", Partial_View); + Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View); + Error_Msg_N ("\& completed # with ghost policy Check", Partial_View); + end if; + end Check_Ghost_Completion; + + ------------------------- + -- Check_Ghost_Context -- + ------------------------- + + procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is + procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id); + -- Verify that the Ghost policy at the point of declaration of entity Id + -- matches the policy at the point of reference. If this is not the case + -- emit an error at Err_N. + + function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; + -- Determine whether node Context denotes a Ghost-friendly context where + -- a Ghost entity can safely reside. + + ------------------------- + -- Is_OK_Ghost_Context -- + ------------------------- + + function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is + function Is_Ghost_Declaration (Decl : Node_Id) return Boolean; + -- Determine whether node Decl is a Ghost declaration or appears + -- within a Ghost declaration. + + function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean; + -- Determine whether statement or pragma N is Ghost or appears within + -- a Ghost statement or pragma. To qualify as such, N must either + -- 1) Occur within a ghost subprogram or package + -- 2) Denote a call to a ghost procedure + -- 3) Denote an assignment statement whose target is a ghost + -- variable. + -- 4) Denote a pragma that mentions a ghost entity + + -------------------------- + -- Is_Ghost_Declaration -- + -------------------------- + + function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is + Par : Node_Id; + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + + begin + -- Climb the parent chain looking for an object declaration + + Par := Decl; + while Present (Par) loop + if Is_Declaration (Par) then + + -- A declaration is Ghost when it appears within a Ghost + -- package or subprogram. + + if Ghost_Mode > None then + return True; + + -- Otherwise the declaration may not have been analyzed yet, + -- determine whether it is subject to aspect/pragma Ghost. + + else + return Is_Subject_To_Ghost (Par); + end if; + + -- Special cases + + -- A reference to a Ghost entity may appear as the default + -- expression of a formal parameter of a subprogram body. This + -- context must be treated as suitable because the relation + -- between the spec and the body has not been established and + -- the body is not marked as Ghost yet. The real check was + -- performed on the spec. + + elsif Nkind (Par) = N_Parameter_Specification + and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body + then + return True; + + -- References to Ghost entities may be relocated in internally + -- generated bodies. + + elsif Nkind (Par) = N_Subprogram_Body + and then not Comes_From_Source (Par) + then + Subp_Id := Corresponding_Spec (Par); + + -- The original context is an expression function that has + -- been split into a spec and a body. The context is OK as + -- long as the the initial declaration is Ghost. + + if Present (Subp_Id) then + Subp_Decl := + Original_Node (Unit_Declaration_Node (Subp_Id)); + + if Nkind (Subp_Decl) = N_Expression_Function then + return Is_Subject_To_Ghost (Subp_Decl); + end if; + end if; + + -- Otherwise this is either an internal body or an internal + -- completion. Both are OK because the real check was done + -- before expansion activities. + + return True; + end if; + + -- Prevent the search from going too far + + if Is_Body_Or_Package_Declaration (Par) then + return False; + end if; + + Par := Parent (Par); + end loop; + + return False; + end Is_Ghost_Declaration; + + ---------------------------------- + -- Is_Ghost_Statement_Or_Pragma -- + ---------------------------------- + + function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is + function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean; + -- Determine whether an arbitrary node denotes a reference to a + -- Ghost entity. + + ------------------------------- + -- Is_Ghost_Entity_Reference -- + ------------------------------- + + function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is + Ref : Node_Id; + + begin + Ref := N; + + -- When the reference extracts a subcomponent, recover the + -- related object (SPARK RM 6.9(1)). + + while Nkind_In (Ref, N_Explicit_Dereference, + N_Indexed_Component, + N_Selected_Component, + N_Slice) + loop + Ref := Prefix (Ref); + end loop; + + return + Is_Entity_Name (Ref) + and then Present (Entity (Ref)) + and then Is_Ghost_Entity (Entity (Ref)); + end Is_Ghost_Entity_Reference; + + -- Local variables + + Arg : Node_Id; + Stmt : Node_Id; + + -- Start of processing for Is_Ghost_Statement_Or_Pragma + + begin + if Nkind (N) = N_Pragma then + + -- A pragma is Ghost when it appears within a Ghost package or + -- subprogram. + + if Ghost_Mode > None then + return True; + end if; + + -- A pragma is Ghost when it mentions a Ghost entity + + Arg := First (Pragma_Argument_Associations (N)); + while Present (Arg) loop + if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then + return True; + end if; + + Next (Arg); + end loop; + end if; + + Stmt := N; + while Present (Stmt) loop + if Is_Statement (Stmt) then + + -- A statement is Ghost when it appears within a Ghost + -- package or subprogram. + + if Ghost_Mode > None then + return True; + + -- An assignment statement or a procedure call is Ghost when + -- the name denotes a Ghost entity. + + elsif Nkind_In (Stmt, N_Assignment_Statement, + N_Procedure_Call_Statement) + then + return Is_Ghost_Entity_Reference (Name (Stmt)); + end if; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Stmt) then + return False; + end if; + + Stmt := Parent (Stmt); + end loop; + + return False; + end Is_Ghost_Statement_Or_Pragma; + + -- Start of processing for Is_OK_Ghost_Context + + begin + -- The Ghost entity appears within an assertion expression + + if In_Assertion_Expr > 0 then + return True; + + -- The Ghost entity is part of a declaration or its completion + + elsif Is_Ghost_Declaration (Context) then + return True; + + -- The Ghost entity is referenced within a Ghost statement + + elsif Is_Ghost_Statement_Or_Pragma (Context) then + return True; + + -- Routine Expand_Record_Extension creates a parent subtype without + -- inserting it into the tree. There is no good way of recognizing + -- this special case as there is no parent. Try to approximate the + -- context. + + elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then + return True; + + else + return False; + end if; + end Is_OK_Ghost_Context; + + ------------------------ + -- Check_Ghost_Policy -- + ------------------------ + + procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + -- The Ghost policy in effect a the point of declaration and at the + -- point of use must match (SPARK RM 6.9(14)). + + if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then + Error_Msg_Sloc := Sloc (Err_N); + + Error_Msg_N ("incompatible ghost policies in effect", Err_N); + Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); + Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); + + elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then + Error_Msg_Sloc := Sloc (Err_N); + + Error_Msg_N ("incompatible ghost policies in effect", Err_N); + Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); + Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); + end if; + end Check_Ghost_Policy; + + -- Start of processing for Check_Ghost_Context + + begin + -- Once it has been established that the reference to the Ghost entity + -- is within a suitable context, ensure that the policy at the point of + -- declaration and at the point of use match. + + if Is_OK_Ghost_Context (Ghost_Ref) then + Check_Ghost_Policy (Ghost_Id, Ghost_Ref); + + -- Otherwise the Ghost entity appears in a non-Ghost context and affects + -- its behavior or value. + + else + Error_Msg_N + ("ghost entity cannot appear in this context (SPARK RM 6.9(12))", + Ghost_Ref); + end if; + end Check_Ghost_Context; + + ---------------------------- + -- Check_Ghost_Derivation -- + ---------------------------- + + procedure Check_Ghost_Derivation (Typ : Entity_Id) is + Parent_Typ : constant Entity_Id := Etype (Typ); + Iface : Entity_Id; + Iface_Elmt : Elmt_Id; + + begin + -- Allow untagged derivations from predefined types such as Integer as + -- those are not Ghost by definition. + + if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then + null; + + -- The parent type of a Ghost type extension must be Ghost + + elsif not Is_Ghost_Entity (Parent_Typ) then + Error_Msg_N ("type extension & cannot be ghost", Typ); + Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ); + return; + end if; + + -- All progenitors (if any) must be Ghost as well + + if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then + Iface_Elmt := First_Elmt (Interfaces (Typ)); + while Present (Iface_Elmt) loop + Iface := Node (Iface_Elmt); + + if not Is_Ghost_Entity (Iface) then + Error_Msg_N ("type extension & cannot be ghost", Typ); + Error_Msg_NE ("\interface type & is not ghost", Typ, Iface); + return; + end if; + + Next_Elmt (Iface_Elmt); + end loop; + end if; + end Check_Ghost_Derivation; + + -------------------------------- + -- Implements_Ghost_Interface -- + -------------------------------- + + function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is + Iface_Elmt : Elmt_Id; + + begin + -- Traverse the list of interfaces looking for a Ghost interface + + if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then + Iface_Elmt := First_Elmt (Interfaces (Typ)); + while Present (Iface_Elmt) loop + if Is_Ghost_Entity (Node (Iface_Elmt)) then + return True; + end if; + + Next_Elmt (Iface_Elmt); + end loop; + end if; + + return False; + end Implements_Ghost_Interface; + + ---------------- + -- Initialize -- + ---------------- + + procedure Initialize is + begin + Ignored_Ghost_Units.Init; + end Initialize; + + --------------------- + -- Is_Ghost_Entity -- + --------------------- + + function Is_Ghost_Entity (Id : Entity_Id) return Boolean is + begin + return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id); + end Is_Ghost_Entity; + + ------------------------- + -- Is_Subject_To_Ghost -- + ------------------------- + + function Is_Subject_To_Ghost (N : Node_Id) return Boolean is + function Enables_Ghostness (Arg : Node_Id) return Boolean; + -- Determine whether aspect or pragma argument Arg enables "ghostness" + + ----------------------- + -- Enables_Ghostness -- + ----------------------- + + function Enables_Ghostness (Arg : Node_Id) return Boolean is + Expr : Node_Id; + + begin + Expr := Arg; + + if Nkind (Expr) = N_Pragma_Argument_Association then + Expr := Get_Pragma_Arg (Expr); + end if; + + -- Determine whether the expression of the aspect is static and + -- denotes True. + + if Present (Expr) then + Preanalyze_And_Resolve (Expr); + + return + Is_OK_Static_Expression (Expr) + and then Is_True (Expr_Value (Expr)); + + -- Otherwise Ghost defaults to True + + else + return True; + end if; + end Enables_Ghostness; + + -- Local variables + + Id : constant Entity_Id := Defining_Entity (N); + Asp : Node_Id; + Decl : Node_Id; + Prev_Id : Entity_Id; + + -- Start of processing for Is_Subject_To_Ghost + + begin + -- The related entity of the declaration has not been analyzed yet, do + -- not inspect its attributes. + + if Ekind (Id) = E_Void then + null; + + elsif Is_Ghost_Entity (Id) then + return True; + + -- The completion of a type or a constant is not fully analyzed when the + -- reference to the Ghost entity is resolved. Because the completion is + -- not marked as Ghost yet, inspect the partial view. + + elsif Is_Record_Type (Id) + or else Ekind (Id) = E_Constant + or else (Nkind (N) = N_Object_Declaration + and then Constant_Present (N)) + then + Prev_Id := Incomplete_Or_Partial_View (Id); + + if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then + return True; + end if; + end if; + + -- Examine the aspect specifications (if any) looking for aspect Ghost + + if Permits_Aspect_Specifications (N) then + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + if Chars (Identifier (Asp)) = Name_Ghost then + return Enables_Ghostness (Expression (Asp)); + end if; + + Next (Asp); + end loop; + end if; + + Decl := Empty; + + -- When the context is a [generic] package declaration, pragma Ghost + -- resides in the visible declarations. + + if Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Decl := First (Visible_Declarations (Specification (N))); + + -- When the context is a package or a subprogram body, pragma Ghost + -- resides in the declarative part. + + elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then + Decl := First (Declarations (N)); + + -- Otherwise pragma Ghost appears in the declarations following N + + elsif Is_List_Member (N) then + Decl := Next (N); + end if; + + while Present (Decl) loop + if Nkind (Decl) = N_Pragma + and then Pragma_Name (Decl) = Name_Ghost + then + return + Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); + + -- A source construct ends the region where pragma Ghost may appear, + -- stop the traversal. + + elsif Comes_From_Source (Decl) then + exit; + end if; + + Next (Decl); + end loop; + + return False; + end Is_Subject_To_Ghost; + + ---------- + -- Lock -- + ---------- + + procedure Lock is + begin + Ignored_Ghost_Units.Locked := True; + Ignored_Ghost_Units.Release; + end Lock; + + ---------------------------------- + -- Propagate_Ignored_Ghost_Code -- + ---------------------------------- + + procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is + Nod : Node_Id; + Scop : Entity_Id; + + begin + -- Traverse the parent chain looking for blocks, packages and + -- subprograms or their respective bodies. + + Nod := Parent (N); + while Present (Nod) loop + Scop := Empty; + + if Nkind (Nod) = N_Block_Statement then + Scop := Entity (Identifier (Nod)); + + elsif Nkind_In (Nod, N_Package_Body, + N_Package_Declaration, + N_Subprogram_Body, + N_Subprogram_Declaration) + then + Scop := Defining_Entity (Nod); + end if; + + -- The current node denotes a scoping construct + + if Present (Scop) then + + -- Stop the traversal when the scope already contains ignored + -- Ghost code as all enclosing scopes have already been marked. + + if Contains_Ignored_Ghost_Code (Scop) then + exit; + + -- Otherwise mark this scope and keep climbing + + else + Set_Contains_Ignored_Ghost_Code (Scop); + end if; + end if; + + Nod := Parent (Nod); + end loop; + + -- The unit containing the ignored Ghost code must be post processed + -- before invoking the back end. + + Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N))); + end Propagate_Ignored_Ghost_Code; + + ------------------------------- + -- Remove_Ignored_Ghost_Code -- + ------------------------------- + + procedure Remove_Ignored_Ghost_Code is + procedure Prune_Tree (Root : Node_Id); + -- Remove all code marked as ignored Ghost from the tree of denoted by + -- Root. + + ---------------- + -- Prune_Tree -- + ---------------- + + procedure Prune_Tree (Root : Node_Id) is + procedure Prune (N : Node_Id); + -- Remove a given node from the tree by rewriting it into null + + function Prune_Node (N : Node_Id) return Traverse_Result; + -- Determine whether node N denotes an ignored Ghost construct. If + -- this is the case, rewrite N as a null statement. See the body for + -- special cases. + + ----------- + -- Prune -- + ----------- + + procedure Prune (N : Node_Id) is + begin + -- Destroy any aspects that may be associated with the node + + if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then + Remove_Aspects (N); + end if; + + Rewrite (N, Make_Null_Statement (Sloc (N))); + end Prune; + + ---------------- + -- Prune_Node -- + ---------------- + + function Prune_Node (N : Node_Id) return Traverse_Result is + Id : Entity_Id; + + begin + -- The node is either declared as ignored Ghost or is a byproduct + -- of expansion. Destroy it and stop the traversal on this branch. + + if Is_Ignored_Ghost_Node (N) then + Prune (N); + return Skip; + + -- Scoping constructs such as blocks, packages, subprograms and + -- bodies offer some flexibility with respect to pruning. + + elsif Nkind_In (N, N_Block_Statement, + N_Package_Body, + N_Package_Declaration, + N_Subprogram_Body, + N_Subprogram_Declaration) + then + if Nkind (N) = N_Block_Statement then + Id := Entity (Identifier (N)); + else + Id := Defining_Entity (N); + end if; + + -- The scoping construct contains both living and ignored Ghost + -- code, let the traversal prune all relevant nodes. + + if Contains_Ignored_Ghost_Code (Id) then + return OK; + + -- Otherwise the construct contains only living code and should + -- not be pruned. + + else + return Skip; + end if; + + -- Otherwise keep searching for ignored Ghost nodes + + else + return OK; + end if; + end Prune_Node; + + procedure Prune_Nodes is new Traverse_Proc (Prune_Node); + + -- Start of processing for Prune_Tree + + begin + Prune_Nodes (Root); + end Prune_Tree; + + -- Start of processing for Remove_Ignored_Ghost_Code + + begin + for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop + Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index))); + end loop; + end Remove_Ignored_Ghost_Code; + + -------------------- + -- Set_Ghost_Mode -- + -------------------- + + procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is + procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); + -- Set the value of global variable Ghost_Mode depending on the mode of + -- entity Id. + + procedure Set_Ghost_Mode_From_Policy; + -- Set the value of global variable Ghost_Mode depending on the current + -- Ghost policy in effect. + + -------------------------------- + -- Set_Ghost_Mode_From_Entity -- + -------------------------------- + + procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is + begin + if Is_Checked_Ghost_Entity (Id) then + Ghost_Mode := Check; + + elsif Is_Ignored_Ghost_Entity (Id) then + Ghost_Mode := Ignore; + + Set_Is_Ignored_Ghost_Node (N); + Propagate_Ignored_Ghost_Code (N); + end if; + end Set_Ghost_Mode_From_Entity; + + -------------------------------- + -- Set_Ghost_Mode_From_Policy -- + -------------------------------- + + procedure Set_Ghost_Mode_From_Policy is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + if Policy = Name_Check then + Ghost_Mode := Check; + + elsif Policy = Name_Ignore then + Ghost_Mode := Ignore; + + Set_Is_Ignored_Ghost_Node (N); + Propagate_Ignored_Ghost_Code (N); + end if; + end Set_Ghost_Mode_From_Policy; + + -- Local variables + + Nam : Node_Id; + + -- Start of processing for Set_Ghost_Mode + + begin + -- The input node denotes one of the many declaration kinds that may be + -- subject to pragma Ghost. + + if Is_Declaration (N) then + if Is_Subject_To_Ghost (N) then + Set_Ghost_Mode_From_Policy; + + -- The declaration denotes the completion of a deferred constant, + -- pragma Ghost appears on the partial declaration. + + elsif Nkind (N) = N_Object_Declaration + and then Constant_Present (N) + and then Present (Prev_Id) + then + Set_Ghost_Mode_From_Entity (Prev_Id); + + -- The declaration denotes the full view of a private type, pragma + -- Ghost appears on the partial declaration. + + elsif Nkind (N) = N_Full_Type_Declaration + and then Is_Private_Type (Defining_Entity (N)) + and then Present (Prev_Id) + then + Set_Ghost_Mode_From_Entity (Prev_Id); + end if; + + -- The input denotes an assignment or a procedure call. In this case + -- the Ghost mode is dictated by the name of the construct. + + elsif Nkind_In (N, N_Assignment_Statement, + N_Procedure_Call_Statement) + then + Nam := Name (N); + + -- When the reference extracts a subcomponent, recover the related + -- object (SPARK RM 6.9(1)). + + while Nkind_In (Nam, N_Explicit_Dereference, + N_Indexed_Component, + N_Selected_Component, + N_Slice) + loop + Nam := Prefix (Nam); + end loop; + + if Is_Entity_Name (Nam) + and then Present (Entity (Nam)) + then + Set_Ghost_Mode_From_Entity (Entity (Nam)); + end if; + + -- The input denotes a package or subprogram body + + elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then + if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id)) + or else Is_Subject_To_Ghost (N) + then + Set_Ghost_Mode_From_Policy; + end if; + end if; + end Set_Ghost_Mode; + + ------------------------------- + -- Set_Ghost_Mode_For_Freeze -- + ------------------------------- + + procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is + begin + if Is_Checked_Ghost_Entity (Id) then + Ghost_Mode := Check; + + elsif Is_Ignored_Ghost_Entity (Id) then + Ghost_Mode := Ignore; + + Propagate_Ignored_Ghost_Code (N); + end if; + end Set_Ghost_Mode_For_Freeze; + + ------------------------- + -- Set_Is_Ghost_Entity -- + ------------------------- + + procedure Set_Is_Ghost_Entity (Id : Entity_Id) is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + if Policy = Name_Check then + Set_Is_Checked_Ghost_Entity (Id); + + elsif Policy = Name_Ignore then + Set_Is_Ignored_Ghost_Entity (Id); + end if; + end Set_Is_Ghost_Entity; + +end Ghost; diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads new file mode 100644 index 00000000000..436e84fe616 --- /dev/null +++ b/gcc/ada/ghost.ads @@ -0,0 +1,115 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- G H O S T -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2014-2015, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- +-- for more details. You should have received a copy of the GNU General -- +-- Public License distributed with GNAT; see file COPYING3. If not, go to -- +-- http://www.gnu.org/licenses for a complete copy of the license. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains routines that deal with the static and runtime +-- semantics of Ghost entities. + +with Types; use Types; + +package Ghost is + + procedure Add_Ignored_Ghost_Unit (Unit : Node_Id); + -- Add a single ignored Ghost compilation unit to the internal table for + -- post processing. + + procedure Check_Ghost_Completion + (Partial_View : Entity_Id; + Full_View : Entity_Id); + -- Verify that the Ghost policy of a full view or a completion is the same + -- as the Ghost policy of the partial view. Emit an error if this is not + -- the case. + + procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id); + -- Determine whether node Ghost_Ref appears within a Ghost-friendly context + -- where Ghost entity Ghost_Id can safely reside. + + procedure Check_Ghost_Derivation (Typ : Entity_Id); + -- Verify that the parent type and all progenitors of derived type or type + -- extension Typ are Ghost. If this is not the case, issue an error. + + function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ implements at least one Ghost interface + + procedure Initialize; + -- Initialize internal tables + + function Is_Ghost_Entity (Id : Entity_Id) return Boolean; + -- Determine whether entity Id is Ghost. To qualify as such, the entity + -- must be subject to pragma Ghost. + + function Is_Subject_To_Ghost (N : Node_Id) return Boolean; + -- Determine whether declarative node N is subject to aspect or pragma + -- Ghost. Use this routine in cases where [source] pragma Ghost has not + -- been analyzed yet, but the context needs to establish the "ghostness" + -- of N. + + procedure Lock; + -- Lock internal tables before calling backend + + procedure Remove_Ignored_Ghost_Code; + -- Remove all code marked as ignored Ghost from the trees of all qualifying + -- units. + -- + -- WARNING: this is a separate front end pass, care should be taken to keep + -- it optimized. + + procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty); + -- Set the value of global variable Ghost_Mode depending on the following + -- scenarios: + -- + -- If N is a declaration, determine whether N is subject to pragma Ghost. + -- If this is the case, the Ghost_Mode is set based on the current Ghost + -- policy in effect. Special cases: + -- + -- N is the completion of a deferred constant, Prev_Id denotes the + -- entity of the partial declaration. + -- + -- N is the full view of a private type, Prev_Id denotes the entity + -- of the partial declaration. + -- + -- If N is an assignment statement or a procedure call, determine whether + -- the name of N denotes a reference to a Ghost entity. If this is the + -- case, the Global_Mode is set based on the mode of the name. + -- + -- If N denotes a package or a subprogram body, determine whether the + -- corresponding spec Prev_Id is a Ghost entity or the body is subject + -- to pragma Ghost. If this is the case, the Global_Mode is set based on + -- the current Ghost policy in effect. + -- + -- WARNING: the caller must save and restore the value of Ghost_Mode in a + -- a stack-like fasion as this routine may override the existing value. + + procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id); + -- Set the value of global variable Ghost_Mode depending on the mode of + -- entity Id. N denotes the context of the freeze. + -- + -- WARNING: the caller must save and restore the value of Ghost_Mode in a + -- a stack-like fasion as this routine may override the existing value. + + procedure Set_Is_Ghost_Entity (Id : Entity_Id); + -- Set the relevant ghost attribute of entity Id depending on the current + -- Ghost assertion policy in effect. + +end Ghost; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 9e77996a97c..983c120c09c 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -36,6 +36,7 @@ with Fmap; with Fname; use Fname; with Fname.UF; use Fname.UF; with Frontend; +with Ghost; with Gnatvsn; use Gnatvsn; with Inline; with Lib; use Lib; @@ -863,7 +864,6 @@ begin Lib.Xref.Initialize; Scan_Compiler_Arguments; Osint.Add_Default_Search_Dirs; - Atree.Initialize; Nlists.Initialize; Sinput.Initialize; @@ -876,6 +876,7 @@ begin SCOs.Initialize; Snames.Initialize; Stringt.Initialize; + Ghost.Initialize; Inline.Initialize; Par_SCO.Initialize; Sem_Ch8.Initialize; @@ -1291,12 +1292,13 @@ begin Atree.Lock; Elists.Lock; Fname.UF.Lock; + Ghost.Lock; Inline.Lock; Lib.Lock; + Namet.Lock; Nlists.Lock; Sem.Lock; Sinput.Lock; - Namet.Lock; Stringt.Lock; -- Here we call the back end to generate the output code diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index a913884a6d7..11c2d06dabf 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -1662,6 +1662,15 @@ package body Lib.Xref is J := 1; while J <= Xrefs.Last loop Ent := Xrefs.Table (J).Key.Ent; + + -- Do not generate reference information for an ignored Ghost + -- entity because neither the entity nor its references will + -- appear in the final tree. + + if Is_Ignored_Ghost_Entity (Ent) then + goto Orphan_Continue; + end if; + Get_Type_Reference (Ent, Tref, L, R); if Present (Tref) @@ -1744,6 +1753,7 @@ package body Lib.Xref is end; end if; + <> J := J + 1; end loop; end Handle_Orphan_Type_References; @@ -1752,7 +1762,6 @@ package body Lib.Xref is -- references, so we can sort them, and output them. Output_Refs : declare - Nrefs : constant Nat := Xrefs.Last; -- Number of references in table @@ -2114,6 +2123,15 @@ package body Lib.Xref is begin Ent := XE.Key.Ent; + + -- Do not generate reference information for an ignored Ghost + -- entity because neither the entity nor its references will + -- appear in the final tree. + + if Is_Ignored_Ghost_Entity (Ent) then + goto Continue; + end if; + Ctyp := Xref_Entity_Letters (Ekind (Ent)); -- Skip reference if it is the only reference to an entity, diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads index 5bbd4119f2d..8cac209ffd2 100644 --- a/gcc/ada/lib.ads +++ b/gcc/ada/lib.ads @@ -440,18 +440,25 @@ package Lib is -- do not have an entry for each possible field, since some of the fields -- can only be set by specialized interfaces (defined below). - function Version_Get (U : Unit_Number_Type) return Word_Hex_String; - -- Returns the version as a string with 8 hex digits (upper case letters) + function Compilation_Switches_Last return Nat; + -- Return the count of stored compilation switches - function Last_Unit return Unit_Number_Type; - -- Unit number of last allocated unit + procedure Disable_Switch_Storing; + -- Disable registration of switches by Store_Compilation_Switch. Used to + -- avoid registering switches added automatically by the gcc driver at the + -- end of the command line. - function Num_Units return Nat; - -- Number of units currently in unit table + function Earlier_In_Extended_Unit (S1, S2 : Source_Ptr) return Boolean; + -- Given two Sloc values for which In_Same_Extended_Unit is true, determine + -- if S1 appears before S2. Returns True if S1 appears before S2, and False + -- otherwise. The result is undefined if S1 and S2 are not in the same + -- extended unit. Note: this routine will not give reliable results if + -- called after Sprint has been called with -gnatD set. - procedure Remove_Unit (U : Unit_Number_Type); - -- Remove unit U from unit table. Currently this is effective only - -- if U is the last unit currently stored in the unit table. + procedure Enable_Switch_Storing; + -- Enable registration of switches by Store_Compilation_Switch. Used to + -- avoid registering switches added automatically by the gcc driver at the + -- beginning of the command line. function Entity_Is_In_Main_Unit (E : Entity_Id) return Boolean; -- Returns True if the entity E is declared in the main unit, or, in @@ -459,6 +466,45 @@ package Lib is -- within generic instantiations return True if the instantiation is -- itself "in the main unit" by this definition. Otherwise False. + function Exact_Source_Name (Loc : Source_Ptr) return String; + -- Return name of entity at location Loc exactly as written in the source. + -- this includes copying the wide character encodings exactly as they were + -- used in the source, so the caller must be aware of the possibility of + -- such encodings. + + function Get_Compilation_Switch (N : Pos) return String_Ptr; + -- Return the Nth stored compilation switch, or null if less than N + -- switches have been stored. Used by ASIS and back ends written in Ada. + + function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean; + -- Generic units must be separately compiled. Since we always use + -- macro substitution for generics, the resulting object file is a dummy + -- one with no code, but the ALI file has the normal form, and we need + -- this ALI file so that the binder can work out a correct order of + -- elaboration. + -- + -- However, ancient versions of GNAT used to not generate code or ALI + -- files for generic units, and this would yield complex order of + -- elaboration issues. These were fixed in GNAT 3.10. The support for not + -- compiling language-defined library generics was retained nonetheless + -- to facilitate bootstrap. Specifically, it is convenient to have + -- the same list of files to be compiled for all stages. So, if the + -- bootstrap compiler does not generate code for a given file, then + -- the stage1 compiler (and binder) also must deal with the case of + -- that file not being compiled. The predicate Generic_May_Lack_ALI is + -- True for those generic units for which missing ALI files are allowed. + + function Get_Cunit_Unit_Number (N : Node_Id) return Unit_Number_Type; + -- Return unit number of the unit whose N_Compilation_Unit node is the + -- one passed as an argument. This must always succeed since the node + -- could not have been built without making a unit table entry. + + function Get_Cunit_Entity_Unit_Number + (E : Entity_Id) return Unit_Number_Type; + -- Return unit number of the unit whose compilation unit spec entity is + -- the one passed as an argument. This must always succeed since the + -- entity could not have been built without making a unit table entry. + function Get_Source_Unit (N : Node_Or_Entity_Id) return Unit_Number_Type; pragma Inline (Get_Source_Unit); function Get_Source_Unit (S : Source_Ptr) return Unit_Number_Type; @@ -478,34 +524,6 @@ package Lib is -- template, so it returns the unit number containing the code that -- corresponds to the node N, or the source location S. - function In_Same_Source_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean; - pragma Inline (In_Same_Source_Unit); - -- Determines if the two nodes or entities N1 and N2 are in the same - -- source unit, the criterion being that Get_Source_Unit yields the - -- same value for each argument. - - function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean; - pragma Inline (In_Same_Code_Unit); - -- Determines if the two nodes or entities N1 and N2 are in the same - -- code unit, the criterion being that Get_Code_Unit yields the same - -- value for each argument. - - function In_Same_Extended_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean; - pragma Inline (In_Same_Extended_Unit); - -- Determines if two nodes or entities N1 and N2 are in the same - -- extended unit, where an extended unit is defined as a unit and all - -- its subunits (considered recursively, i.e. subunits of subunits are - -- included). Returns true if S1 and S2 are in the same extended unit - -- and False otherwise. - - function In_Same_Extended_Unit (S1, S2 : Source_Ptr) return Boolean; - pragma Inline (In_Same_Extended_Unit); - -- Determines if the two source locations S1 and S2 are in the same - -- extended unit, where an extended unit is defined as a unit and all - -- its subunits (considered recursively, i.e. subunits of subunits are - -- included). Returns true if S1 and S2 are in the same extended unit - -- and False otherwise. - function In_Extended_Main_Code_Unit (N : Node_Or_Entity_Id) return Boolean; -- Return True if the node is in the generated code of the extended main @@ -550,48 +568,67 @@ package Lib is function In_Predefined_Unit (S : Source_Ptr) return Boolean; -- Same function as above but argument is a source pointer - function Earlier_In_Extended_Unit (S1, S2 : Source_Ptr) return Boolean; - -- Given two Sloc values for which In_Same_Extended_Unit is true, determine - -- if S1 appears before S2. Returns True if S1 appears before S2, and False - -- otherwise. The result is undefined if S1 and S2 are not in the same - -- extended unit. Note: this routine will not give reliable results if - -- called after Sprint has been called with -gnatD set. - - function Exact_Source_Name (Loc : Source_Ptr) return String; - -- Return name of entity at location Loc exactly as written in the source. - -- this includes copying the wide character encodings exactly as they were - -- used in the source, so the caller must be aware of the possibility of - -- such encodings. - - function Compilation_Switches_Last return Nat; - -- Return the count of stored compilation switches + function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean; + pragma Inline (In_Same_Code_Unit); + -- Determines if the two nodes or entities N1 and N2 are in the same + -- code unit, the criterion being that Get_Code_Unit yields the same + -- value for each argument. - function Get_Compilation_Switch (N : Pos) return String_Ptr; - -- Return the Nth stored compilation switch, or null if less than N - -- switches have been stored. Used by ASIS and back ends written in Ada. + function In_Same_Extended_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean; + pragma Inline (In_Same_Extended_Unit); + -- Determines if two nodes or entities N1 and N2 are in the same + -- extended unit, where an extended unit is defined as a unit and all + -- its subunits (considered recursively, i.e. subunits of subunits are + -- included). Returns true if S1 and S2 are in the same extended unit + -- and False otherwise. - function Get_Cunit_Unit_Number (N : Node_Id) return Unit_Number_Type; - -- Return unit number of the unit whose N_Compilation_Unit node is the - -- one passed as an argument. This must always succeed since the node - -- could not have been built without making a unit table entry. + function In_Same_Extended_Unit (S1, S2 : Source_Ptr) return Boolean; + pragma Inline (In_Same_Extended_Unit); + -- Determines if the two source locations S1 and S2 are in the same + -- extended unit, where an extended unit is defined as a unit and all + -- its subunits (considered recursively, i.e. subunits of subunits are + -- included). Returns true if S1 and S2 are in the same extended unit + -- and False otherwise. - function Get_Cunit_Entity_Unit_Number - (E : Entity_Id) return Unit_Number_Type; - -- Return unit number of the unit whose compilation unit spec entity is - -- the one passed as an argument. This must always succeed since the - -- entity could not have been built without making a unit table entry. + function In_Same_Source_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean; + pragma Inline (In_Same_Source_Unit); + -- Determines if the two nodes or entities N1 and N2 are in the same + -- source unit, the criterion being that Get_Source_Unit yields the + -- same value for each argument. function Increment_Serial_Number return Nat; -- Increment Serial_Number field for current unit, and return the -- incremented value. - procedure Synchronize_Serial_Number; - -- This function increments the Serial_Number field for the current unit - -- but does not return the incremented value. This is used when there - -- is a situation where one path of control increments a serial number - -- (using Increment_Serial_Number), and the other path does not and it is - -- important to keep the serial numbers synchronized in the two cases (e.g. - -- when the references in a package and a client must be kept consistent). + procedure Initialize; + -- Initialize internal tables + + function Is_Loaded (Uname : Unit_Name_Type) return Boolean; + -- Determines if unit with given name is already loaded, i.e. there is + -- already an entry in the file table with this unit name for which the + -- corresponding file was found and parsed. Note that the Fatal_Error flag + -- of this entry must be checked before proceeding with further processing. + + function Last_Unit return Unit_Number_Type; + -- Unit number of last allocated unit + + procedure List (File_Names_Only : Boolean := False); + -- Lists units in active library (i.e. generates output consisting of a + -- sorted listing of the units represented in File table, except for the + -- main unit). If File_Names_Only is set to True, then the list includes + -- only file names, and no other information. Otherwise the unit name and + -- time stamp are also output. File_Names_Only also restricts the list to + -- exclude any predefined files. + + procedure Lock; + -- Lock internal tables before calling back end + + function Num_Units return Nat; + -- Number of units currently in unit table + + procedure Remove_Unit (U : Unit_Number_Type); + -- Remove unit U from unit table. Currently this is effective only if U is + -- the last unit currently stored in the unit table. procedure Replace_Linker_Option_String (S : String_Id; @@ -604,16 +641,6 @@ package Lib is -- which may influence the generated output file(s). Switch is the text of -- the switch to store (except that -fRTS gets changed back to --RTS). - procedure Enable_Switch_Storing; - -- Enable registration of switches by Store_Compilation_Switch. Used to - -- avoid registering switches added automatically by the gcc driver at the - -- beginning of the command line. - - procedure Disable_Switch_Storing; - -- Disable registration of switches by Store_Compilation_Switch. Used to - -- avoid registering switches added automatically by the gcc driver at the - -- end of the command line. - procedure Store_Linker_Option_String (S : String_Id); -- This procedure is called to register the string from a pragma -- Linker_Option. The argument is the Id of the string to register. @@ -622,14 +649,13 @@ package Lib is -- This procedure is called to register a pragma N for which a notes -- entry is required. - procedure Initialize; - -- Initialize internal tables - - procedure Lock; - -- Lock internal tables before calling back end - - procedure Unlock; - -- Unlock internal tables, in cases where the back end needs to modify them + procedure Synchronize_Serial_Number; + -- This function increments the Serial_Number field for the current unit + -- but does not return the incremented value. This is used when there + -- is a situation where one path of control increments a serial number + -- (using Increment_Serial_Number), and the other path does not and it is + -- important to keep the serial numbers synchronized in the two cases (e.g. + -- when the references in a package and a client must be kept consistent). procedure Tree_Read; -- Initializes internal tables from current tree file using the relevant @@ -639,43 +665,17 @@ package Lib is -- Writes out internal tables to current tree file using the relevant -- Table.Tree_Write routines. - function Is_Loaded (Uname : Unit_Name_Type) return Boolean; - -- Determines if unit with given name is already loaded, i.e. there is - -- already an entry in the file table with this unit name for which the - -- corresponding file was found and parsed. Note that the Fatal_Error flag - -- of this entry must be checked before proceeding with further processing. + procedure Unlock; + -- Unlock internal tables, in cases where the back end needs to modify them + + function Version_Get (U : Unit_Number_Type) return Word_Hex_String; + -- Returns the version as a string with 8 hex digits (upper case letters) procedure Version_Referenced (S : String_Id); -- This routine is called from Exp_Attr to register the use of a Version -- or Body_Version attribute. The argument is the external name used to -- access the version string. - procedure List (File_Names_Only : Boolean := False); - -- Lists units in active library (i.e. generates output consisting of a - -- sorted listing of the units represented in File table, except for the - -- main unit). If File_Names_Only is set to True, then the list includes - -- only file names, and no other information. Otherwise the unit name and - -- time stamp are also output. File_Names_Only also restricts the list to - -- exclude any predefined files. - - function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean; - -- Generic units must be separately compiled. Since we always use - -- macro substitution for generics, the resulting object file is a dummy - -- one with no code, but the ALI file has the normal form, and we need - -- this ALI file so that the binder can work out a correct order of - -- elaboration. - -- - -- However, ancient versions of GNAT used to not generate code or ALI - -- files for generic units, and this would yield complex order of - -- elaboration issues. These were fixed in GNAT 3.10. The support for not - -- compiling language-defined library generics was retained nonetheless - -- to facilitate bootstrap. Specifically, it is convenient to have - -- the same list of files to be compiled for all stages. So, if the - -- bootstrap compiler does not generate code for a given file, then - -- the stage1 compiler (and binder) also must deal with the case of - -- that file not being compiled. The predicate Generic_May_Lack_ALI is - -- True for those generic units for which missing ALI files are allowed. - procedure Write_Unit_Info (Unit_Num : Unit_Number_Type; Item : Node_Id; diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index ea2216822b0..a1ce246bb81 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -724,6 +724,14 @@ package Opt is -- True if the frontend finished its work and has called the backend to -- process the tree and generate the object file. + type Ghost_Mode_Type is (None, Check, Ignore); + -- Possible legal modes that can be set by aspect/pragma Ghost as well as + -- value None, which indicates that no such aspect/pragma applies. + + Ghost_Mode : Ghost_Mode_Type := None; + -- GNAT + -- Current Ghost mode setting + Global_Discard_Names : Boolean := False; -- GNAT, GNATBIND -- True if a pragma Discard_Names appeared as a configuration pragma for diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index babf5641e98..29ca1fa68d4 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -923,6 +923,12 @@ package body Rtsfind is end loop; end Save_Private_Visibility; + -- Local variables + + GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the current Ghost mode in effect to ensure a clean environment + -- when analyzing the unit. + -- Start of processing for Load_RTU begin @@ -932,6 +938,10 @@ package body Rtsfind is return; end if; + -- Provide a clean environment for the unit + + Ghost_Mode := None; + -- Note if secondary stack is used if U_Id = System_Secondary_Stack then @@ -1032,6 +1042,10 @@ package body Rtsfind is if Use_Setting then Set_Is_Potentially_Use_Visible (U.Entity, True); end if; + + -- Restore the original Ghost mode now that analysis has taken place + + Ghost_Mode := GM; end Load_RTU; -------------------- diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 442e89737ed..4451addbf39 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -95,6 +95,10 @@ package body Sem is ------------- procedure Analyze (N : Node_Id) is + GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the current Ghost mode in effect in case the construct sets a + -- different mode. + begin Debug_A_Entry ("analyzing ", N); @@ -108,7 +112,6 @@ package body Sem is -- Otherwise processing depends on the node kind case Nkind (N) is - when N_Abort_Statement => Analyze_Abort_Statement (N); @@ -622,10 +625,9 @@ package body Sem is -- the call to analyze them is generated when the full list is -- analyzed. - when - N_SCIL_Dispatch_Table_Tag_Init | - N_SCIL_Dispatching_Call | - N_SCIL_Membership_Test => + when N_SCIL_Dispatch_Table_Tag_Init | + N_SCIL_Dispatching_Call | + N_SCIL_Membership_Test => null; -- For the remaining node types, we generate compiler abort, because @@ -635,65 +637,63 @@ package body Sem is -- node appears only in the context of a type declaration, and is -- processed by the analyze routine for type declarations. - when - N_Abortable_Part | - N_Access_Definition | - N_Access_Function_Definition | - N_Access_Procedure_Definition | - N_Access_To_Object_Definition | - N_Aspect_Specification | - N_Case_Expression_Alternative | - N_Case_Statement_Alternative | - N_Compilation_Unit_Aux | - N_Component_Association | - N_Component_Clause | - N_Component_Definition | - N_Component_List | - N_Constrained_Array_Definition | - N_Contract | - N_Decimal_Fixed_Point_Definition | - N_Defining_Character_Literal | - N_Defining_Identifier | - N_Defining_Operator_Symbol | - N_Defining_Program_Unit_Name | - N_Delta_Constraint | - N_Derived_Type_Definition | - N_Designator | - N_Digits_Constraint | - N_Discriminant_Association | - N_Discriminant_Specification | - N_Elsif_Part | - N_Entry_Call_Statement | - N_Enumeration_Type_Definition | - N_Exception_Handler | - N_Floating_Point_Definition | - N_Formal_Decimal_Fixed_Point_Definition | - N_Formal_Derived_Type_Definition | - N_Formal_Discrete_Type_Definition | - N_Formal_Floating_Point_Definition | - N_Formal_Modular_Type_Definition | - N_Formal_Ordinary_Fixed_Point_Definition | - N_Formal_Private_Type_Definition | - N_Formal_Incomplete_Type_Definition | - N_Formal_Signed_Integer_Type_Definition | - N_Function_Specification | - N_Generic_Association | - N_Index_Or_Discriminant_Constraint | - N_Iteration_Scheme | - N_Mod_Clause | - N_Modular_Type_Definition | - N_Ordinary_Fixed_Point_Definition | - N_Parameter_Specification | - N_Pragma_Argument_Association | - N_Procedure_Specification | - N_Real_Range_Specification | - N_Record_Definition | - N_Signed_Integer_Type_Definition | - N_Unconstrained_Array_Definition | - N_Unused_At_Start | - N_Unused_At_End | - N_Variant => - + when N_Abortable_Part | + N_Access_Definition | + N_Access_Function_Definition | + N_Access_Procedure_Definition | + N_Access_To_Object_Definition | + N_Aspect_Specification | + N_Case_Expression_Alternative | + N_Case_Statement_Alternative | + N_Compilation_Unit_Aux | + N_Component_Association | + N_Component_Clause | + N_Component_Definition | + N_Component_List | + N_Constrained_Array_Definition | + N_Contract | + N_Decimal_Fixed_Point_Definition | + N_Defining_Character_Literal | + N_Defining_Identifier | + N_Defining_Operator_Symbol | + N_Defining_Program_Unit_Name | + N_Delta_Constraint | + N_Derived_Type_Definition | + N_Designator | + N_Digits_Constraint | + N_Discriminant_Association | + N_Discriminant_Specification | + N_Elsif_Part | + N_Entry_Call_Statement | + N_Enumeration_Type_Definition | + N_Exception_Handler | + N_Floating_Point_Definition | + N_Formal_Decimal_Fixed_Point_Definition | + N_Formal_Derived_Type_Definition | + N_Formal_Discrete_Type_Definition | + N_Formal_Floating_Point_Definition | + N_Formal_Modular_Type_Definition | + N_Formal_Ordinary_Fixed_Point_Definition | + N_Formal_Private_Type_Definition | + N_Formal_Incomplete_Type_Definition | + N_Formal_Signed_Integer_Type_Definition | + N_Function_Specification | + N_Generic_Association | + N_Index_Or_Discriminant_Constraint | + N_Iteration_Scheme | + N_Mod_Clause | + N_Modular_Type_Definition | + N_Ordinary_Fixed_Point_Definition | + N_Parameter_Specification | + N_Pragma_Argument_Association | + N_Procedure_Specification | + N_Real_Range_Specification | + N_Record_Definition | + N_Signed_Integer_Type_Definition | + N_Unconstrained_Array_Definition | + N_Unused_At_Start | + N_Unused_At_End | + N_Variant => raise Program_Error; end case; @@ -719,6 +719,11 @@ package body Sem is then Expand (N); end if; + + -- Restore the original Ghost mode once analysis and expansion have + -- taken place. + + Ghost_Mode := GM; end Analyze; -- Version with check(s) suppressed @@ -1297,6 +1302,51 @@ package body Sem is --------------- procedure Semantics (Comp_Unit : Node_Id) is + procedure Do_Analyze; + -- Perform the analysis of the compilation unit + + ---------------- + -- Do_Analyze -- + ---------------- + + procedure Do_Analyze is + GM : constant Ghost_Mode_Type := Ghost_Mode; + -- Save the current Ghost mode in effect in case the compilation unit + -- is withed from a unit with a different Ghost mode. + + List : Elist_Id; + + begin + List := Save_Scope_Stack; + Push_Scope (Standard_Standard); + + -- Set up a clean environment before analyzing + + Ghost_Mode := None; + Outer_Generic_Scope := Empty; + Scope_Suppress := Suppress_Options; + Scope_Stack.Table + (Scope_Stack.Last).Component_Alignment_Default := Calign_Default; + Scope_Stack.Table + (Scope_Stack.Last).Is_Active_Stack_Base := True; + + -- Now analyze the top level compilation unit node + + Analyze (Comp_Unit); + + -- Check for scope mismatch on exit from compilation + + pragma Assert (Current_Scope = Standard_Standard + or else Comp_Unit = Cunit (Main_Unit)); + + -- Then pop entry for Standard, and pop implicit types + + Pop_Scope; + Restore_Scope_Stack (List); + Ghost_Mode := GM; + end Do_Analyze; + + -- Local variables -- The following locations save the corresponding global flags and -- variables so that they can be restored on completion. This is needed @@ -1315,6 +1365,8 @@ package body Sem is S_Outer_Gen_Scope : constant Entity_Id := Outer_Generic_Scope; S_Style_Check : constant Boolean := Style_Check; + Already_Analyzed : constant Boolean := Analyzed (Comp_Unit); + Curunit : constant Unit_Number_Type := Get_Cunit_Unit_Number (Comp_Unit); -- New value of Current_Sem_Unit @@ -1344,43 +1396,6 @@ package body Sem is -- unit. All with'ed units are analyzed with config restrictions reset -- and we need to restore these saved values at the end. - procedure Do_Analyze; - -- Procedure to analyze the compilation unit - - ---------------- - -- Do_Analyze -- - ---------------- - - procedure Do_Analyze is - List : Elist_Id; - - begin - List := Save_Scope_Stack; - Push_Scope (Standard_Standard); - Scope_Suppress := Suppress_Options; - Scope_Stack.Table - (Scope_Stack.Last).Component_Alignment_Default := Calign_Default; - Scope_Stack.Table - (Scope_Stack.Last).Is_Active_Stack_Base := True; - Outer_Generic_Scope := Empty; - - -- Now analyze the top level compilation unit node - - Analyze (Comp_Unit); - - -- Check for scope mismatch on exit from compilation - - pragma Assert (Current_Scope = Standard_Standard - or else Comp_Unit = Cunit (Main_Unit)); - - -- Then pop entry for Standard, and pop implicit types - - Pop_Scope; - Restore_Scope_Stack (List); - end Do_Analyze; - - Already_Analyzed : constant Boolean := Analyzed (Comp_Unit); - -- Start of processing for Semantics begin diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index c193f1ad5ca..ca6c9639188 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -27,6 +27,7 @@ with Atree; use Atree; with Checks; use Checks; with Einfo; use Einfo; with Errout; use Errout; +with Ghost; use Ghost; with Lib; use Lib; with Lib.Xref; use Lib.Xref; with Namet; use Namet; @@ -56,7 +57,14 @@ package body Sem_Ch11 is procedure Analyze_Exception_Declaration (N : Node_Id) is Id : constant Entity_Id := Defining_Identifier (N); PF : constant Boolean := Is_Pure (Current_Scope); + begin + -- The exception declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + Generate_Definition (Id); Enter_Name (Id); Set_Ekind (Id, E_Exception); @@ -64,10 +72,10 @@ package body Sem_Ch11 is Set_Is_Statically_Allocated (Id); Set_Is_Pure (Id, PF); - -- An exception declared within a Ghost scope is automatically Ghost + -- An exception declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 53b626eea12..4b88e1d607a 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -33,6 +33,7 @@ with Exp_Disp; use Exp_Disp; with Fname; use Fname; with Fname.UF; use Fname.UF; with Freeze; use Freeze; +with Ghost; use Ghost; with Itypes; use Itypes; with Lib; use Lib; with Lib.Load; use Lib.Load; @@ -2991,6 +2992,11 @@ package body Sem_Ch12 is Decl : Node_Id; begin + -- The generic package declaration may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes generated + -- during analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); Check_SPARK_05_Restriction ("generic is not allowed", N); -- We introduce a renaming of the enclosing package, to have a usable @@ -3050,10 +3056,10 @@ package body Sem_Ch12 is Set_Etype (Id, Standard_Void_Type); Set_Contract (Id, Make_Contract (Sloc (Id))); - -- A generic package declared within a Ghost scope is rendered Ghost + -- A generic package declared within a Ghost region is rendered Ghost -- (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; @@ -3152,6 +3158,12 @@ package body Sem_Ch12 is Typ : Entity_Id; begin + -- The generic subprogram declaration may be subject to pragma Ghost + -- with policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged as + -- ignored Ghost. + + Set_Ghost_Mode (N); Check_SPARK_05_Restriction ("generic is not allowed", N); -- Create copy of generic unit, and save for instantiation. If the unit @@ -3259,10 +3271,10 @@ package body Sem_Ch12 is Set_Etype (Id, Standard_Void_Type); end if; - -- A generic subprogram declared within a Ghost scope is rendered Ghost + -- A generic subprogram declared within a Ghost region is rendered Ghost -- (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index c067539eb1c..61be2f9b602 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -39,6 +39,7 @@ with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Fname; use Fname; with Freeze; use Freeze; +with Ghost; use Ghost; with Itypes; use Itypes; with Layout; use Layout; with Lib; use Lib; @@ -532,8 +533,8 @@ package body Sem_Ch3 is function Find_Type_Of_Object (Obj_Def : Node_Id; Related_Nod : Node_Id) return Entity_Id; - -- Get type entity for object referenced by Obj_Def, attaching the - -- implicit types generated to Related_Nod + -- Get type entity for object referenced by Obj_Def, attaching the implicit + -- types generated to Related_Nod. procedure Floating_Point_Type_Declaration (T : Entity_Id; Def : Node_Id); -- Create a new float and apply the constraint to obtain subtype of it @@ -2552,9 +2553,15 @@ package body Sem_Ch3 is begin Prev := Find_Type_Name (N); - -- The full view, if present, now points to the current type - -- If there is an incomplete partial view, set a link to it, to - -- simplify the retrieval of primitive operations of the type. + -- The type declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N, Prev); + + -- The full view, if present, now points to the current type. If there + -- is an incomplete partial view, set a link to it, to simplify the + -- retrieval of primitive operations of the type. -- Ada 2005 (AI-50217): If the type was previously decorated when -- imported through a LIMITED WITH clause, it appears as incomplete @@ -2704,10 +2711,10 @@ package body Sem_Ch3 is Check_SPARK_05_Restriction ("controlled type is not allowed", N); end if; - -- A type declared within a Ghost scope is automatically Ghost + -- A type declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - if Comes_From_Source (T) and then Within_Ghost_Scope then + if Comes_From_Source (T) and then Ghost_Mode > None then Set_Is_Ghost_Entity (T); end if; @@ -2856,10 +2863,10 @@ package body Sem_Ch3 is Set_Is_First_Subtype (T, True); Set_Etype (T, T); - -- An incomplete type declared within a Ghost scope is automatically + -- An incomplete type declared within a Ghost region is automatically -- Ghost (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (T); end if; @@ -2970,13 +2977,19 @@ package body Sem_Ch3 is It : Interp; begin + -- The number declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + Generate_Definition (Id); Enter_Name (Id); - -- A number declared within a Ghost scope is automatically Ghost + -- A number declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; @@ -3393,6 +3406,12 @@ package body Sem_Ch3 is end if; end if; + -- The object declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N, Prev_Entity); + if Present (Prev_Entity) then Constant_Redeclaration (Id, N, T); @@ -3917,10 +3936,10 @@ package body Sem_Ch3 is Set_Ekind (Id, E_Variable); end if; - -- An object declared within a Ghost scope is automatically + -- An object declared within a Ghost region is automatically -- Ghost (SPARK RM 6.9(2)). - if Comes_From_Source (Id) and then Within_Ghost_Scope then + if Comes_From_Source (Id) and then Ghost_Mode > None then Set_Is_Ghost_Entity (Id); -- The Ghost policy in effect at the point of declaration @@ -4098,16 +4117,13 @@ package body Sem_Ch3 is Init_Esize (Id); Set_Optimize_Alignment_Flags (Id); - -- An object declared within a Ghost scope is automatically Ghost - -- (SPARK RM 6.9(2)). This property is also inherited when its type - -- is Ghost or the previous declaration of the deferred constant is - -- Ghost. + -- An object declared within a Ghost region is automatically Ghost + -- (SPARK RM 6.9(2)). if Comes_From_Source (Id) - and then (Is_Ghost_Entity (T) + and then (Ghost_Mode > None or else (Present (Prev_Entity) - and then Is_Ghost_Entity (Prev_Entity)) - or else Within_Ghost_Scope) + and then Is_Ghost_Entity (Prev_Entity))) then Set_Is_Ghost_Entity (Id); @@ -4353,6 +4369,12 @@ package body Sem_Ch3 is Parent_Base : Entity_Id; begin + -- The private extension declaration may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes generated + -- during analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + -- Ada 2005 (AI-251): Decorate all names in list of ancestor interfaces if Is_Non_Empty_List (Interface_List (N)) then @@ -4581,6 +4603,12 @@ package body Sem_Ch3 is R_Checks : Check_Result; begin + -- The subtype declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + Generate_Definition (Id); Set_Is_Pure (Id, Is_Pure (Current_Scope)); Init_Size_Align (Id); @@ -5456,12 +5484,13 @@ package body Sem_Ch3 is -- The constrained array type is a subtype of the unconstrained one - Set_Ekind (T, E_Array_Subtype); - Init_Size_Align (T); - Set_Etype (T, Implicit_Base); - Set_Scope (T, Current_Scope); - Set_Is_Constrained (T, True); - Set_First_Index (T, First (Discrete_Subtype_Definitions (Def))); + Set_Ekind (T, E_Array_Subtype); + Init_Size_Align (T); + Set_Etype (T, Implicit_Base); + Set_Scope (T, Current_Scope); + Set_Is_Constrained (T); + Set_First_Index (T, + First (Discrete_Subtype_Definitions (Def))); Set_Has_Delayed_Freeze (T); -- Complete setup of implicit base type @@ -5472,13 +5501,17 @@ package body Sem_Ch3 is Set_Has_Protected (Implicit_Base, Has_Protected (Element_Type)); Set_Component_Size (Implicit_Base, Uint_0); Set_Packed_Array_Impl_Type (Implicit_Base, Empty); - Set_Has_Controlled_Component - (Implicit_Base, - Has_Controlled_Component (Element_Type) - or else Is_Controlled (Element_Type)); - Set_Finalize_Storage_Only - (Implicit_Base, Finalize_Storage_Only - (Element_Type)); + Set_Has_Controlled_Component (Implicit_Base, + Has_Controlled_Component (Element_Type) + or else Is_Controlled (Element_Type)); + Set_Finalize_Storage_Only (Implicit_Base, + Finalize_Storage_Only (Element_Type)); + + -- Inherit the "ghostness" from the constrained array type + + if Is_Ghost_Entity (T) or else Ghost_Mode > None then + Set_Is_Ghost_Entity (Implicit_Base); + end if; -- Unconstrained array case @@ -5945,6 +5978,12 @@ package body Sem_Ch3 is Copy_Array_Base_Type_Attributes (Implicit_Base, Parent_Base); Set_Has_Delayed_Freeze (Implicit_Base, True); + + -- Inherit the "ghostness" from the parent base type + + if Is_Ghost_Entity (Parent_Base) or else Ghost_Mode > None then + Set_Is_Ghost_Entity (Implicit_Base); + end if; end Make_Implicit_Base; -- Start of processing for Build_Derived_Array_Type @@ -7720,34 +7759,6 @@ package body Sem_Ch3 is Derived_Type : Entity_Id; Derive_Subps : Boolean := True) is - function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean; - -- Determine whether type Typ implements at least one Ghost interface - - -------------------------------- - -- Implements_Ghost_Interface -- - -------------------------------- - - function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is - Iface_Elmt : Elmt_Id; - begin - -- Traverse the list of interfaces looking for a Ghost interface - - if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then - Iface_Elmt := First_Elmt (Interfaces (Typ)); - while Present (Iface_Elmt) loop - if Is_Ghost_Entity (Node (Iface_Elmt)) then - return True; - end if; - - Next_Elmt (Iface_Elmt); - end loop; - end if; - - return False; - end Implements_Ghost_Interface; - - -- Local variables - Discriminant_Specs : constant Boolean := Present (Discriminant_Specifications (N)); Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type); @@ -7775,8 +7786,6 @@ package body Sem_Ch3 is -- An empty Discs list means that there were no constraints in the -- subtype indication or that there was an error processing it. - -- Start of processing for Build_Derived_Record_Type - begin if Ekind (Parent_Type) = E_Record_Type_With_Private and then Present (Full_View (Parent_Type)) @@ -14630,6 +14639,12 @@ package body Sem_Ch3 is Set_Alias (New_Subp, Actual_Subp); end if; + -- Inherit the "ghostness" from the parent subprogram + + if Is_Ghost_Entity (Alias (New_Subp)) then + Set_Is_Ghost_Entity (New_Subp); + end if; + -- Derived subprograms of a tagged type must inherit the convention -- of the parent subprogram (a requirement of AI-117). Derived -- subprograms of untagged types simply get convention Ada by default. diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 1666917affb..5cd60dd7180 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -32,6 +32,7 @@ with Expander; use Expander; with Exp_Ch6; use Exp_Ch6; with Exp_Util; use Exp_Util; with Freeze; use Freeze; +with Ghost; use Ghost; with Lib; use Lib; with Lib.Xref; use Lib.Xref; with Namet; use Namet; @@ -278,6 +279,13 @@ package body Sem_Ch5 is -- proper use of a Ghost entity need to know the enclosing context. Analyze (Lhs); + + -- The left hand side of an assignment may reference an entity subject + -- to pragma Ghost with policy Ignore. Set the mode now to ensure that + -- any nodes generated during analysis and expansion are properly + -- flagged as ignored Ghost. + + Set_Ghost_Mode (N); Analyze (Rhs); -- Ensure that we never do an assignment on a variable marked as diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index fcca80b3878..5e987bcb16a 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -40,6 +40,7 @@ with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Fname; use Fname; with Freeze; use Freeze; +with Ghost; use Ghost; with Inline; use Inline; with Itypes; use Itypes; with Lib.Xref; use Lib.Xref; @@ -213,6 +214,12 @@ package body Sem_Ch6 is Scop : constant Entity_Id := Current_Scope; begin + -- The abstract subprogram declaration may be subject to pragma Ghost + -- with policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged as + -- ignored Ghost. + + Set_Ghost_Mode (N); Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N); Generate_Definition (Designator); @@ -223,10 +230,10 @@ package body Sem_Ch6 is Set_Categorization_From_Scope (Designator, Scop); - -- An abstract subprogram declared within a Ghost scope is automatically + -- An abstract subprogram declared within a Ghost region is rendered -- Ghost (SPARK RM 6.9(2)). - if Comes_From_Source (Designator) and then Within_Ghost_Scope then + if Comes_From_Source (Designator) and then Ghost_Mode > None then Set_Is_Ghost_Entity (Designator); end if; @@ -1257,7 +1264,7 @@ package body Sem_Ch6 is -- property is not directly inherited as the body may be subject -- to a different Ghost assertion policy. - if Is_Ghost_Entity (Gen_Id) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Gen_Id) or else Ghost_Mode > None then Set_Is_Ghost_Entity (Body_Id); -- The Ghost policy in effect at the point of declaration and at @@ -1606,6 +1613,13 @@ package body Sem_Ch6 is return; end if; + -- The name of the procedure call may reference an entity subject to + -- pragma Ghost with policy Ignore. Set the mode now to ensure that any + -- nodes generated during analysis and expansion are properly flagged as + -- ignored Ghost. + + Set_Ghost_Mode (N); + -- Otherwise analyze the parameters if Present (Actuals) then @@ -3113,6 +3127,13 @@ package body Sem_Ch6 is then if Is_Generic_Subprogram (Prev_Id) then Spec_Id := Prev_Id; + + -- The corresponding spec may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged + -- as ignored Ghost. + + Set_Ghost_Mode (N, Spec_Id); Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id)); Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id)); @@ -3150,9 +3171,24 @@ package body Sem_Ch6 is then if Is_Private_Concurrent_Primitive (Body_Id) then Spec_Id := Disambiguate_Spec; + + -- The corresponding spec may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged + -- as ignored Ghost. + + Set_Ghost_Mode (N, Spec_Id); + else Spec_Id := Find_Corresponding_Spec (N); + -- The corresponding spec may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged + -- as ignored Ghost. + + Set_Ghost_Mode (N, Spec_Id); + -- In GNATprove mode, if the body has no previous spec, create -- one so that the inlining machinery can operate properly. -- Transfer aspects, if any, to the new spec, so that they @@ -3294,6 +3330,13 @@ package body Sem_Ch6 is else Spec_Id := Corresponding_Spec (N); + + -- The corresponding spec may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged + -- as ignored Ghost. + + Set_Ghost_Mode (N, Spec_Id); end if; end if; @@ -3387,7 +3430,7 @@ package body Sem_Ch6 is -- property is not directly inherited as the body may be subject -- to a different Ghost assertion policy. - if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then Set_Is_Ghost_Entity (Body_Id); -- The Ghost policy in effect at the point of declaration and @@ -4261,6 +4304,12 @@ package body Sem_Ch6 is -- Indicates whether a null procedure declaration is a completion begin + -- The subprogram declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + -- Null procedures are not allowed in SPARK if Nkind (Specification (N)) = N_Procedure_Specification @@ -4294,12 +4343,12 @@ package body Sem_Ch6 is -- explicit pragma). Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma); - Set_SPARK_Pragma_Inherited (Designator, True); + Set_SPARK_Pragma_Inherited (Designator); - -- A subprogram declared within a Ghost scope is automatically Ghost + -- A subprogram declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - if Comes_From_Source (Designator) and then Within_Ghost_Scope then + if Comes_From_Source (Designator) and then Ghost_Mode > None then Set_Is_Ghost_Entity (Designator); end if; diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 1acef30dee0..0a80db82653 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -37,6 +37,7 @@ with Errout; use Errout; with Exp_Disp; use Exp_Disp; with Exp_Dist; use Exp_Dist; with Exp_Dbug; use Exp_Dbug; +with Ghost; use Ghost; with Lib; use Lib; with Lib.Xref; use Lib.Xref; with Namet; use Namet; @@ -634,6 +635,13 @@ package body Sem_Ch7 is end if; end if; + -- The corresponding spec of the package body may be subject to pragma + -- Ghost with policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged as + -- ignored Ghost. + + Set_Ghost_Mode (N, Spec_Id); + Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id)); Style.Check_Identifier (Body_Id, Spec_Id); @@ -731,7 +739,7 @@ package body Sem_Ch7 is -- property is not directly inherited as the body may be subject to a -- different Ghost assertion policy. - if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then Set_Is_Ghost_Entity (Body_Id); -- The Ghost policy in effect at the point of declaration and at the @@ -1001,6 +1009,12 @@ package body Sem_Ch7 is Indent; end if; + -- The package declaration may be subject to pragma Ghost with policy + -- Ignore. Set the mode now to ensure that any nodes generated during + -- analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + Generate_Definition (Id); Enter_Name (Id); Set_Ekind (Id, E_Package); @@ -1762,6 +1776,12 @@ package body Sem_Ch7 is Id : constant Entity_Id := Defining_Identifier (N); begin + -- The private type declaration may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes generated + -- during analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + Generate_Definition (Id); Set_Is_Pure (Id, PF); Init_Size_Align (Id); @@ -1775,10 +1795,10 @@ package body Sem_Ch7 is New_Private_Type (N, Id, N); Set_Depends_On_Private (Id); - -- A type declared within a Ghost scope is automatically Ghost + -- A type declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 2f22a9af685..8c7731488a0 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -32,6 +32,7 @@ with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Fname; use Fname; with Freeze; use Freeze; +with Ghost; use Ghost; with Impunit; use Impunit; with Lib; use Lib; with Lib.Load; use Lib.Load; @@ -552,6 +553,12 @@ package body Sem_Ch8 is Nam : constant Node_Id := Name (N); begin + -- The exception renaming declaration may be subject to pragma Ghost + -- with policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged as + -- ignored Ghost. + + Set_Ghost_Mode (N); Check_SPARK_05_Restriction ("exception renaming is not allowed", N); Enter_Name (Id); @@ -575,7 +582,7 @@ package body Sem_Ch8 is -- An exception renaming is Ghost if the renamed entity is Ghost or -- the construct appears within a Ghost scope. - if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; end if; @@ -665,6 +672,11 @@ package body Sem_Ch8 is return; end if; + -- The generic renaming declaration may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes generated + -- during analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); Check_SPARK_05_Restriction ("generic renaming is not allowed", N); Generate_Definition (New_P); @@ -711,7 +723,7 @@ package body Sem_Ch8 is -- An generic renaming is Ghost if the renamed entity is Ghost or the -- construct appears within a Ghost scope. - if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then Set_Is_Ghost_Entity (New_P); end if; @@ -850,6 +862,11 @@ package body Sem_Ch8 is return; end if; + -- The object renaming declaration may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes generated + -- during analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); Check_SPARK_05_Restriction ("object renaming is not allowed", N); Set_Is_Pure (Id, Is_Pure (Current_Scope)); @@ -1315,7 +1332,7 @@ package body Sem_Ch8 is if (Is_Entity_Name (Nam) and then Is_Ghost_Entity (Entity (Nam))) - or else Within_Ghost_Scope + or else Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; @@ -1371,6 +1388,12 @@ package body Sem_Ch8 is return; end if; + -- The package renaming declaration may be subject to pragma Ghost with + -- policy Ignore. Set the mode now to ensure that any nodes generated + -- during analysis and expansion are properly flagged as ignored Ghost. + + Set_Ghost_Mode (N); + -- Check for Text_IO special unit (we may be renaming a Text_IO child) Check_Text_IO_Special_Unit (Name (N)); @@ -1437,7 +1460,7 @@ package body Sem_Ch8 is -- A package renaming is Ghost if the renamed entity is Ghost or -- the construct appears within a Ghost scope. - if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then Set_Is_Ghost_Entity (New_P); end if; @@ -2559,6 +2582,13 @@ package body Sem_Ch8 is -- Start of processing for Analyze_Subprogram_Renaming begin + -- The subprogram renaming declaration may be subject to pragma Ghost + -- with policy Ignore. Set the mode now to ensure that any nodes + -- generated during analysis and expansion are properly flagged as + -- ignored Ghost. + + Set_Ghost_Mode (N); + -- We must test for the attribute renaming case before the Analyze -- call because otherwise Sem_Attr will complain that the attribute -- is missing an argument when it is analyzed. @@ -3027,7 +3057,7 @@ package body Sem_Ch8 is -- A subprogram renaming is Ghost if the renamed entity is Ghost or -- the construct appears within a Ghost scope. - if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then + if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then Set_Is_Ghost_Entity (New_S); end if; @@ -7184,6 +7214,12 @@ package body Sem_Ch8 is elsif Is_Floating_Point_Type (Etype (N)) then Check_Restriction (No_Floating_Point, N); end if; + + -- A Ghost type must appear in a specific context + + if Is_Ghost_Entity (Etype (N)) then + Check_Ghost_Context (Etype (N), N); + end if; end if; end Find_Type; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 74607e57655..dd2bc1be43e 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -41,6 +41,7 @@ with Errout; use Errout; with Exp_Dist; use Exp_Dist; with Exp_Util; use Exp_Util; with Freeze; use Freeze; +with Ghost; use Ghost; with Lib; use Lib; with Lib.Writ; use Lib.Writ; with Lib.Xref; use Lib.Xref; @@ -8412,7 +8413,7 @@ package body Sem_Prag is -- If previous error, avoid cascaded errors Check_Error_Detected; - Applies := True; + Applies := True; else Make_Inline (Subp); @@ -8434,8 +8435,7 @@ package body Sem_Prag is end if; if not Applies then - Error_Pragma_Arg - ("inappropriate argument for pragma%", Assoc); + Error_Pragma_Arg ("inappropriate argument for pragma%", Assoc); end if; Next (Assoc); @@ -10212,10 +10212,10 @@ package body Sem_Prag is Set_Refinement_Constituents (State_Id, New_Elmt_List); Set_Part_Of_Constituents (State_Id, New_Elmt_List); - -- An abstract state declared within a Ghost scope becomes + -- An abstract state declared within a Ghost region becomes -- Ghost (SPARK RM 6.9(2)). - if Within_Ghost_Scope then + if Ghost_Mode > None then Set_Is_Ghost_Entity (State_Id); end if; @@ -11907,7 +11907,7 @@ package body Sem_Prag is -- Pragma Check_Policy specifying a Ghost policy cannot -- occur within a ghost subprogram or package. - if Within_Ghost_Scope then + if Ghost_Mode > None then Error_Pragma ("pragma % cannot appear within ghost subprogram or " & "package"); @@ -14377,7 +14377,7 @@ package body Sem_Prag is -- region (SPARK RM 6.9(7)). if Is_False (Expr_Value (Expr)) - and then Within_Ghost_Scope + and then Ghost_Mode > None then Error_Pragma ("pragma % with value False cannot appear in enabled " @@ -14941,7 +14941,7 @@ package body Sem_Prag is -- Independent_Components -- ---------------------------- - -- pragma Independent_Components (array_or_record_LOCAL_NAME); + -- pragma Atomic_Components (array_or_record_LOCAL_NAME); when Pragma_Independent_Components => Independent_Components : declare E_Id : Node_Id; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index dedacd5af41..8f762d44b95 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -37,6 +37,7 @@ with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Fname; use Fname; with Freeze; use Freeze; +with Ghost; use Ghost; with Inline; use Inline; with Itypes; use Itypes; with Lib; use Lib; @@ -110,10 +111,6 @@ package body Sem_Res is Pref : Node_Id); -- Check that the type of the prefix of a dereference is not incomplete - procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id); - -- Determine whether node Ghost_Ref appears within a Ghost-friendly context - -- where Ghost entity Ghost_Id can safely reside. - function Check_Infinite_Recursion (N : Node_Id) return Boolean; -- Given a call node, N, which is known to occur immediately within the -- subprogram being called, determines whether it is a detectable case of @@ -694,193 +691,6 @@ package body Sem_Res is end if; end Check_Fully_Declared_Prefix; - ------------------------- - -- Check_Ghost_Context -- - ------------------------- - - procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is - procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id); - -- Verify that the Ghost policy at the point of declaration of entity Id - -- matches the policy at the point of reference. If this is not the case - -- emit an error at Err_N. - - function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; - -- Determine whether node Context denotes a Ghost-friendly context where - -- a Ghost entity can safely reside. - - ------------------------- - -- Is_OK_Ghost_Context -- - ------------------------- - - function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is - function Is_Ghost_Declaration (Decl : Node_Id) return Boolean; - -- Determine whether node Decl is a Ghost declaration or appears - -- within a Ghost declaration. - - -------------------------- - -- Is_Ghost_Declaration -- - -------------------------- - - function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is - Par : Node_Id; - Subp_Decl : Node_Id; - Subp_Id : Entity_Id; - - begin - -- Climb the parent chain looking for an object declaration - - Par := Decl; - while Present (Par) loop - case Nkind (Par) is - when N_Abstract_Subprogram_Declaration | - N_Exception_Declaration | - N_Exception_Renaming_Declaration | - N_Full_Type_Declaration | - N_Generic_Function_Renaming_Declaration | - N_Generic_Package_Declaration | - N_Generic_Package_Renaming_Declaration | - N_Generic_Procedure_Renaming_Declaration | - N_Generic_Subprogram_Declaration | - N_Number_Declaration | - N_Object_Declaration | - N_Object_Renaming_Declaration | - N_Package_Declaration | - N_Package_Renaming_Declaration | - N_Private_Extension_Declaration | - N_Private_Type_Declaration | - N_Subprogram_Declaration | - N_Subprogram_Renaming_Declaration | - N_Subtype_Declaration => - return Is_Subject_To_Ghost (Par); - - when others => - null; - end case; - - -- Special cases - - -- A reference to a Ghost entity may appear as the default - -- expression of a formal parameter of a subprogram body. This - -- context must be treated as suitable because the relation - -- between the spec and the body has not been established and - -- the body is not marked as Ghost yet. The real check was - -- performed on the spec. - - if Nkind (Par) = N_Parameter_Specification - and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body - then - return True; - - -- References to Ghost entities may be relocated in internally - -- generated bodies. - - elsif Nkind (Par) = N_Subprogram_Body - and then not Comes_From_Source (Par) - then - Subp_Id := Corresponding_Spec (Par); - - -- The original context is an expression function that has - -- been split into a spec and a body. The context is OK as - -- long as the the initial declaration is Ghost. - - if Present (Subp_Id) then - Subp_Decl := - Original_Node (Unit_Declaration_Node (Subp_Id)); - - if Nkind (Subp_Decl) = N_Expression_Function then - return Is_Subject_To_Ghost (Subp_Decl); - end if; - end if; - - -- Otherwise this is either an internal body or an internal - -- completion. Both are OK because the real check was done - -- before expansion activities. - - return True; - end if; - - -- Prevent the search from going too far - - if Is_Body_Or_Package_Declaration (Par) then - return False; - end if; - - Par := Parent (Par); - end loop; - - return False; - end Is_Ghost_Declaration; - - -- Start of processing for Is_OK_Ghost_Context - - begin - -- The Ghost entity appears within an assertion expression - - if In_Assertion_Expr > 0 then - return True; - - -- The Ghost entity is part of a declaration or its completion - - elsif Is_Ghost_Declaration (Context) then - return True; - - -- The Ghost entity is referenced within a Ghost statement - - elsif Is_Ghost_Statement_Or_Pragma (Context) then - return True; - - else - return False; - end if; - end Is_OK_Ghost_Context; - - ------------------------ - -- Check_Ghost_Policy -- - ------------------------ - - procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); - - begin - -- The Ghost policy in effect a the point of declaration and at the - -- point of use must match (SPARK RM 6.9(14)). - - if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then - Error_Msg_Sloc := Sloc (Err_N); - - Error_Msg_N ("incompatible ghost policies in effect", Err_N); - Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); - Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); - - elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then - Error_Msg_Sloc := Sloc (Err_N); - - Error_Msg_N ("incompatible ghost policies in effect", Err_N); - Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); - Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); - end if; - end Check_Ghost_Policy; - - -- Start of processing for Check_Ghost_Context - - begin - -- Once it has been established that the reference to the Ghost entity - -- is within a suitable context, ensure that the policy at the point of - -- declaration and at the point of use match. - - if Is_OK_Ghost_Context (Ghost_Ref) then - Check_Ghost_Policy (Ghost_Id, Ghost_Ref); - - -- Otherwise the Ghost entity appears in a non-Ghost context and affects - -- its behavior or value. - - else - Error_Msg_N - ("ghost entity cannot appear in this context (SPARK RM 6.9(12))", - Ghost_Ref); - end if; - end Check_Ghost_Context; - ------------------------------ -- Check_Infinite_Recursion -- ------------------------------ diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b0fcc17da47..51a67387416 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -70,7 +70,7 @@ with GNAT.HTable; use GNAT.HTable; package body Sem_Util is ---------------------------------------- - -- Global_Variables for New_Copy_Tree -- + -- Global Variables for New_Copy_Tree -- ---------------------------------------- -- These global variables are used by New_Copy_Tree. See description of the @@ -110,12 +110,6 @@ package body Sem_Util is -- and Build_Discriminal_Subtype_Of_Component. C is a list of constraints, -- Loc is the source location, T is the original subtype. - function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean; - -- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type - -- with discriminants whose default values are static, examine only the - -- components in the selected variant to determine whether all of them - -- have a default. - function Has_Enabled_Property (Item_Id : Entity_Id; Property : Name_Id) return Boolean; @@ -127,6 +121,12 @@ package body Sem_Util is -- T is a derived tagged type. Check whether the type extension is null. -- If the parent type is fully initialized, T can be treated as such. + function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean; + -- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type + -- with discriminants whose default values are static, examine only the + -- components in the selected variant to determine whether all of them + -- have a default. + ------------------------------ -- Abstract_Interface_List -- ------------------------------ @@ -2676,82 +2676,6 @@ package body Sem_Util is end if; end Check_Function_Writable_Actuals; - ---------------------------- - -- Check_Ghost_Completion -- - ---------------------------- - - procedure Check_Ghost_Completion - (Partial_View : Entity_Id; - Full_View : Entity_Id) - is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); - - begin - -- The Ghost policy in effect at the point of declaration and at the - -- point of completion must match (SPARK RM 6.9(15)). - - if Is_Checked_Ghost_Entity (Partial_View) - and then Policy = Name_Ignore - then - Error_Msg_Sloc := Sloc (Full_View); - - Error_Msg_N ("incompatible ghost policies in effect", Partial_View); - Error_Msg_N ("\& declared with ghost policy Check", Partial_View); - Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View); - - elsif Is_Ignored_Ghost_Entity (Partial_View) - and then Policy = Name_Check - then - Error_Msg_Sloc := Sloc (Full_View); - - Error_Msg_N ("incompatible ghost policies in effect", Partial_View); - Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View); - Error_Msg_N ("\& completed # with ghost policy Check", Partial_View); - end if; - end Check_Ghost_Completion; - - ---------------------------- - -- Check_Ghost_Derivation -- - ---------------------------- - - procedure Check_Ghost_Derivation (Typ : Entity_Id) is - Parent_Typ : constant Entity_Id := Etype (Typ); - Iface : Entity_Id; - Iface_Elmt : Elmt_Id; - - begin - -- Allow untagged derivations from predefined types such as Integer as - -- those are not Ghost by definition. - - if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then - null; - - -- The parent type of a Ghost type extension must be Ghost - - elsif not Is_Ghost_Entity (Parent_Typ) then - Error_Msg_N ("type extension & cannot be ghost", Typ); - Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ); - return; - end if; - - -- All progenitors (if any) must be Ghost as well - - if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then - Iface_Elmt := First_Elmt (Interfaces (Typ)); - while Present (Iface_Elmt) loop - Iface := Node (Iface_Elmt); - - if not Is_Ghost_Entity (Iface) then - Error_Msg_N ("type extension & cannot be ghost", Typ); - Error_Msg_NE ("\interface type & is not ghost", Typ, Iface); - return; - end if; - - Next_Elmt (Iface_Elmt); - end loop; - end if; - end Check_Ghost_Derivation; - -------------------------------- -- Check_Implicit_Dereference -- -------------------------------- @@ -9498,7 +9422,7 @@ package body Sem_Util is Pkg_Decl : Node_Id := Pkg; begin - if Ekind (Pkg) = E_Package then + if Present (Pkg) and then Ekind (Pkg) = E_Package then while Nkind (Pkg_Decl) /= N_Package_Specification loop Pkg_Decl := Parent (Pkg_Decl); end loop; @@ -10437,6 +10361,39 @@ package body Sem_Util is and then Is_Imported (Entity (Name (N))); end Is_CPP_Constructor_Call; + -------------------- + -- Is_Declaration -- + -------------------- + + function Is_Declaration (N : Node_Id) return Boolean is + begin + case Nkind (N) is + when N_Abstract_Subprogram_Declaration | + N_Exception_Declaration | + N_Exception_Renaming_Declaration | + N_Full_Type_Declaration | + N_Generic_Function_Renaming_Declaration | + N_Generic_Package_Declaration | + N_Generic_Package_Renaming_Declaration | + N_Generic_Procedure_Renaming_Declaration | + N_Generic_Subprogram_Declaration | + N_Number_Declaration | + N_Object_Declaration | + N_Object_Renaming_Declaration | + N_Package_Declaration | + N_Package_Renaming_Declaration | + N_Private_Extension_Declaration | + N_Private_Type_Declaration | + N_Subprogram_Declaration | + N_Subprogram_Renaming_Declaration | + N_Subtype_Declaration => + return True; + + when others => + return False; + end case; + end Is_Declaration; + ----------------- -- Is_Delegate -- ----------------- @@ -11209,110 +11166,6 @@ package body Sem_Util is end if; end Is_Fully_Initialized_Variant; - --------------------- - -- Is_Ghost_Entity -- - --------------------- - - function Is_Ghost_Entity (Id : Entity_Id) return Boolean is - begin - return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id); - end Is_Ghost_Entity; - - ---------------------------------- - -- Is_Ghost_Statement_Or_Pragma -- - ---------------------------------- - - function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is - function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean; - -- Determine whether an arbitrary node denotes a reference to a Ghost - -- entity. - - ------------------------------- - -- Is_Ghost_Entity_Reference -- - ------------------------------- - - function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is - Ref : Node_Id; - - begin - Ref := N; - - -- When the reference extracts a subcomponent, recover the related - -- object (SPARK RM 6.9(1)). - - while Nkind_In (Ref, N_Explicit_Dereference, - N_Indexed_Component, - N_Selected_Component, - N_Slice) - loop - Ref := Prefix (Ref); - end loop; - - return - Is_Entity_Name (Ref) - and then Present (Entity (Ref)) - and then Is_Ghost_Entity (Entity (Ref)); - end Is_Ghost_Entity_Reference; - - -- Local variables - - Arg : Node_Id; - Stmt : Node_Id; - - -- Start of processing for Is_Ghost_Statement_Or_Pragma - - begin - if Nkind (N) = N_Pragma then - - -- A pragma is Ghost when it appears within a Ghost package or - -- subprogram. - - if Within_Ghost_Scope then - return True; - end if; - - -- A pragma is Ghost when it mentions a Ghost entity - - Arg := First (Pragma_Argument_Associations (N)); - while Present (Arg) loop - if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then - return True; - end if; - - Next (Arg); - end loop; - end if; - - Stmt := N; - while Present (Stmt) loop - - -- A statement is Ghost when it appears within a Ghost package or - -- subprogram. - - if Is_Statement (Stmt) and then Within_Ghost_Scope then - return True; - - -- An assignment statement is Ghost when the target is a Ghost - -- variable. A procedure call is Ghost when the invoked procedure - -- is Ghost. - - elsif Nkind_In (Stmt, N_Assignment_Statement, - N_Procedure_Call_Statement) - then - return Is_Ghost_Entity_Reference (Name (Stmt)); - - -- Prevent the search from going too far - - elsif Is_Body_Or_Package_Declaration (Stmt) then - return False; - end if; - - Stmt := Parent (Stmt); - end loop; - - return False; - end Is_Ghost_Statement_Or_Pragma; - ---------------------------- -- Is_Inherited_Operation -- ---------------------------- @@ -12417,123 +12270,6 @@ package body Sem_Util is or else Nkind (N) = N_Procedure_Call_Statement; end Is_Statement; - ------------------------- - -- Is_Subject_To_Ghost -- - ------------------------- - - function Is_Subject_To_Ghost (N : Node_Id) return Boolean is - function Enables_Ghostness (Arg : Node_Id) return Boolean; - -- Determine whether aspect or pragma argument Arg enables "ghostness" - - ----------------------- - -- Enables_Ghostness -- - ----------------------- - - function Enables_Ghostness (Arg : Node_Id) return Boolean is - Expr : Node_Id; - - begin - Expr := Arg; - - if Nkind (Expr) = N_Pragma_Argument_Association then - Expr := Get_Pragma_Arg (Expr); - end if; - - -- Determine whether the expression of the aspect is static and - -- denotes True. - - if Present (Expr) then - Preanalyze_And_Resolve (Expr); - - return - Is_OK_Static_Expression (Expr) - and then Is_True (Expr_Value (Expr)); - - -- Otherwise Ghost defaults to True - - else - return True; - end if; - end Enables_Ghostness; - - -- Local variables - - Id : constant Entity_Id := Defining_Entity (N); - Asp : Node_Id; - Decl : Node_Id; - Prev_Id : Entity_Id; - - -- Start of processing for Is_Subject_To_Ghost - - begin - if Is_Ghost_Entity (Id) then - return True; - - -- The completion of a type or a constant is not fully analyzed when the - -- reference to the Ghost entity is resolved. Because the completion is - -- not marked as Ghost yet, inspect the partial view. - - elsif Is_Record_Type (Id) - or else Ekind (Id) = E_Constant - or else (Nkind (N) = N_Object_Declaration - and then Constant_Present (N)) - then - Prev_Id := Incomplete_Or_Partial_View (Id); - - if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then - return True; - end if; - end if; - - -- Examine the aspect specifications (if any) looking for aspect Ghost - - if Permits_Aspect_Specifications (N) then - Asp := First (Aspect_Specifications (N)); - while Present (Asp) loop - if Chars (Identifier (Asp)) = Name_Ghost then - return Enables_Ghostness (Expression (Asp)); - end if; - - Next (Asp); - end loop; - end if; - - Decl := Empty; - - -- When the context is a [generic] package declaration, pragma Ghost - -- resides in the visible declarations. - - if Nkind_In (N, N_Generic_Package_Declaration, - N_Package_Declaration) - then - Decl := First (Visible_Declarations (Specification (N))); - - -- Otherwise pragma Ghost appears in the declarations following N - - elsif Is_List_Member (N) then - Decl := Next (N); - end if; - - while Present (Decl) loop - if Nkind (Decl) = N_Pragma - and then Pragma_Name (Decl) = Name_Ghost - then - return - Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); - - -- A source construct ends the region where pragma Ghost may appear, - -- stop the traversal. - - elsif Comes_From_Source (Decl) then - exit; - end if; - - Next (Decl); - end loop; - - return False; - end Is_Subject_To_Ghost; - -------------------------------------------------- -- Is_Subprogram_Stub_Without_Prior_Declaration -- -------------------------------------------------- @@ -17265,22 +17001,6 @@ package body Sem_Util is Set_Entity (N, Val); end Set_Entity_With_Checks; - ------------------------- - -- Set_Is_Ghost_Entity -- - ------------------------- - - procedure Set_Is_Ghost_Entity (Id : Entity_Id) is - Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); - - begin - if Policy = Name_Check then - Set_Is_Checked_Ghost_Entity (Id); - - elsif Policy = Name_Ignore then - Set_Is_Ignored_Ghost_Entity (Id); - end if; - end Set_Is_Ghost_Entity; - ------------------------ -- Set_Name_Entity_Id -- ------------------------ @@ -18213,30 +17933,6 @@ package body Sem_Util is return List_1; end Visible_Ancestors; - ------------------------ - -- Within_Ghost_Scope -- - ------------------------ - - function Within_Ghost_Scope - (Id : Entity_Id := Current_Scope) return Boolean - is - S : Entity_Id; - - begin - -- Climb the scope stack looking for a Ghost scope - - S := Id; - while Present (S) and then S /= Standard_Standard loop - if Is_Ghost_Entity (S) then - return True; - end if; - - S := Scope (S); - end loop; - - return False; - end Within_Ghost_Scope; - ---------------------- -- Within_Init_Proc -- ---------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 040a7d65d4e..43f1089dca7 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -285,17 +285,6 @@ package Sem_Util is -- the one containing C2, that is known to refer to the same object (RM -- 6.4.1(6.17/3)). - procedure Check_Ghost_Completion - (Partial_View : Entity_Id; - Full_View : Entity_Id); - -- Verify that the Ghost policy of a full view or a completion is the same - -- as the Ghost policy of the partial view. Emit an error if this is not - -- the case. - - procedure Check_Ghost_Derivation (Typ : Entity_Id); - -- Verify that the parent type and all progenitors of derived type or type - -- extension Typ are Ghost. If this is not the case, issue an error. - procedure Check_Implicit_Dereference (N : Node_Id; Typ : Entity_Id); -- AI05-139-2: Accessors and iterators for containers. This procedure -- checks whether T is a reference type, and if so it adds an interprettion @@ -1213,6 +1202,9 @@ package Sem_Util is -- First determine whether type T is an interface and then check whether -- it is of protected, synchronized or task kind. + function Is_Declaration (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a declaration + function Is_Delegate (T : Entity_Id) return Boolean; -- Returns true if type T represents a delegate. A Delegate is the CIL -- object used to represent access-to-subprogram types. This is only @@ -1279,18 +1271,6 @@ package Sem_Util is -- means that the result returned is not crucial, but should err on the -- side of thinking things are fully initialized if it does not know. - function Is_Ghost_Entity (Id : Entity_Id) return Boolean; - -- Determine whether entity Id is Ghost. To qualify as such, the entity - -- must be subject to Convention Ghost. - - function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean; - -- Determine whether statement or pragma N is ghost. To qualify as such, N - -- must either - -- 1) Occur within a ghost subprogram or package - -- 2) Denote a call to a ghost procedure - -- 3) Denote an assignment statement whose target is a ghost variable - -- 4) Denote a pragma that mentions a ghost entity - function Is_Inherited_Operation (E : Entity_Id) return Boolean; -- E is a subprogram. Return True is E is an implicit operation inherited -- by a derived type declaration. @@ -1419,12 +1399,6 @@ package Sem_Util is -- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo). -- Note that a label is *not* a statement, and will return False. - function Is_Subject_To_Ghost (N : Node_Id) return Boolean; - -- Determine whether declarative node N is subject to aspect or pragma - -- Ghost. Use this routine in cases where [source] pragma Ghost has not - -- been analyzed yet, but the context needs to establish the "ghostness" - -- of N. - function Is_Subprogram_Stub_Without_Prior_Declaration (N : Node_Id) return Boolean; -- Return True if N is a subprogram stub with no prior subprogram @@ -1914,10 +1888,6 @@ package Sem_Util is -- If restriction No_Implementation_Identifiers is set, then it checks -- that the entity is not implementation defined. - procedure Set_Is_Ghost_Entity (Id : Entity_Id); - -- Set the relevant ghost attribute of entity Id depending on the current - -- Ghost assertion policy in effect. - procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id); pragma Inline (Set_Name_Entity_Id); -- Sets the Entity_Id value associated with the given name, which is the @@ -2045,12 +2015,6 @@ package Sem_Util is -- generate the list of visible ancestors; otherwise their partial -- view is added to the resulting list. - function Within_Ghost_Scope - (Id : Entity_Id := Current_Scope) return Boolean; - -- Determine whether an arbitrary entity is either a scope or within a - -- scope subject to convention Ghost or one that inherits "ghostness" from - -- an enclosing construct. - function Within_Init_Proc return Boolean; -- Determines if Current_Scope is within an init proc diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index ae7813593a1..7c4bbf9a98a 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -521,6 +521,32 @@ package Sinfo is -- simply ignore these nodes, since they are not relevant to the task -- of back annotating representation information. + ---------------- + -- Ghost Mode -- + ---------------- + + -- When a declaration is subject to pragma Ghost, it establishes a Ghost + -- region depending on the Ghost assertion policy in effect at the point + -- of declaration. This region is temporal and starts right before the + -- analysis of the Ghost declaration and ends after its expansion. The + -- values of global variable Opt.Ghost_Mode are as follows: + + -- 1. Check - All static semantics as defined in SPARK RM 6.9 are in + -- effect. + + -- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI + -- files, object files as well as the final executable. + + -- To achieve the runtime semantics of "Ignore", the compiler marks each + -- node created during an ignored Ghost region and signals all enclosing + -- scopes that such a node resides within. The compilation unit where the + -- node resides is also added to an auxiliary table for post processing. + + -- After the analysis and expansion of all compilation units takes place + -- as well as the instantiation of all inlined [generic] bodies, the GNAT + -- driver initiates a separate pass which removes all ignored Ghost code + -- from all units stored in the auxiliary table. + -------------------- -- GNATprove Mode -- -------------------- diff --git a/gcc/ada/treepr.adb b/gcc/ada/treepr.adb index 0f21b9973c0..9d09a57ddfe 100644 --- a/gcc/ada/treepr.adb +++ b/gcc/ada/treepr.adb @@ -1282,7 +1282,30 @@ package body Treepr is ----------------------- procedure Print_Node_Header (N : Node_Id) is - Notes : Boolean := False; + Enumerate : Boolean := False; + -- Flag set when enumerating multiple header flags + + procedure Print_Header_Flag (Flag : String); + -- Output one of the flags that appears in a node header. The routine + -- automatically handles enumeration of multiple flags. + + ----------------------- + -- Print_Header_Flag -- + ----------------------- + + procedure Print_Header_Flag (Flag : String) is + begin + if Enumerate then + Print_Char (','); + else + Enumerate := True; + Print_Char ('('); + end if; + + Print_Str (Flag); + end Print_Header_Flag; + + -- Start of processing for Print_Node_Header begin Print_Node_Ref (N); @@ -1293,34 +1316,25 @@ package body Treepr is return; end if; + Print_Char (' '); + if Comes_From_Source (N) then - Notes := True; - Print_Str (" (source"); + Print_Header_Flag ("source"); end if; if Analyzed (N) then - if not Notes then - Notes := True; - Print_Str (" ("); - else - Print_Str (","); - end if; - - Print_Str ("analyzed"); + Print_Header_Flag ("analyzed"); end if; if Error_Posted (N) then - if not Notes then - Notes := True; - Print_Str (" ("); - else - Print_Str (","); - end if; + Print_Header_Flag ("posted"); + end if; - Print_Str ("posted"); + if Is_Ignored_Ghost_Node (N) then + Print_Header_Flag ("ignored ghost"); end if; - if Notes then + if Enumerate then Print_Char (')'); end if; -- 2.30.2