https://gcc.gnu.org/g:bad0a5c562991a8b1e515cd498347b314bc2e8a9
commit r16-2752-gbad0a5c562991a8b1e515cd498347b314bc2e8a9 Author: Viljar Indus <in...@adacore.com> Date: Wed Jul 23 11:59:10 2025 +0300 ada: Keep Ghost_Mode related variables in a record Simplify the storing process for ghost mode related variables and make the process more extendable if new ghost mode related features are added. gcc/ada/ChangeLog: * atree.adb: update references to Ghost_Mode. * exp_ch3.adb: use a structure type to store all of the existing ghost mode related state variables. * exp_disp.adb: Likewise. * exp_spark.adb: Likewise. * exp_util.adb: Likewise. * expander.adb: Likewise. * freeze.adb: Likewise and replace references to existing ghost mode variables. * ghost.adb (Install_Ghost_Region): install the changes of the region in to the new Ghost_Config structure. (Restore_Ghost_Region): Use the new Ghost_Config instead. In general replace all references to the existing ghost mode variables with the new structure equivalent. * ghost.ads (Restore_Ghost_Region): update the spec. * opt.ads (Ghost_Config_Type): A new type that has two of the previous ghost code related global variables as memembers - Ghost_Mode and Ignored_Ghost_Region. (Ghost_Config) New variable to store the previous Ghost_Mode and Ignored_Ghost_Region info. * rtsfind.adb: Replace references to existing ghost mode variables. * sem.adb: Likewise. * sem_ch12.adb: Likewise. * sem_ch13.adb: Likewise. * sem_ch3.adb: Likewise. * sem_ch5.adb: Likewise. * sem_ch6.adb: Likewise. * sem_ch7.adb: Likewise. * sem_prag.adb: Likewise. * sem_util.adb: Likewise. Diff: --- gcc/ada/atree.adb | 4 ++-- gcc/ada/exp_ch3.adb | 7 +++---- gcc/ada/exp_disp.adb | 5 ++--- gcc/ada/exp_spark.adb | 5 ++--- gcc/ada/exp_util.adb | 25 ++++++++++-------------- gcc/ada/expander.adb | 5 ++--- gcc/ada/freeze.adb | 13 ++++++------- gcc/ada/ghost.adb | 33 ++++++++++++++++---------------- gcc/ada/ghost.ads | 2 +- gcc/ada/opt.ads | 21 ++++++++++++-------- gcc/ada/rtsfind.adb | 15 ++++++++------- gcc/ada/sem.adb | 10 ++++------ gcc/ada/sem_ch12.adb | 24 ++++++++++------------- gcc/ada/sem_ch13.adb | 10 ++++------ gcc/ada/sem_ch3.adb | 10 ++++------ gcc/ada/sem_ch5.adb | 7 +++---- gcc/ada/sem_ch6.adb | 19 ++++++++---------- gcc/ada/sem_ch7.adb | 9 ++++----- gcc/ada/sem_prag.adb | 53 ++++++++++++++++++++++----------------------------- gcc/ada/sem_util.adb | 7 +++---- 20 files changed, 128 insertions(+), 156 deletions(-) diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 20ca189ad8c3..0ff3d6e34a8f 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -1802,12 +1802,12 @@ package body Atree is -- The Ghost node is created within a Ghost region - if Ghost_Mode = Check then + if Ghost_Config.Ghost_Mode = Check then if Nkind (N) in N_Entity then Set_Is_Checked_Ghost_Entity (N); end if; - elsif Ghost_Mode = Ignore then + elsif Ghost_Config.Ghost_Mode = Ignore then if Nkind (N) in N_Entity then Set_Is_Ignored_Ghost_Entity (N); end if; diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 6cf7c9c97076..00b3aae0bd9e 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -9601,8 +9601,7 @@ package body Exp_Ch3 is Def_Id : constant Entity_Id := Entity (N); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Result : Boolean := False; @@ -9956,13 +9955,13 @@ package body Exp_Ch3 is end if; end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); return Result; exception when RE_Not_Available => - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); return False; end Freeze_Type; diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 619ac407cb0a..1c09e204275e 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -4593,8 +4593,7 @@ package body Exp_Disp is Name_TSD : constant Name_Id := New_External_Name (Tname, 'B', Suffix_Index => -1); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit AI : Elmt_Id; @@ -6526,7 +6525,7 @@ package body Exp_Disp is Register_CG_Node (Typ); <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); return Result; end Make_DT; diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index a75a507388bc..0f9203410f2f 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -1128,8 +1128,7 @@ package body Exp_SPARK is Wrapper_Decl_List : List_Id; Wrapper_Body_List : List_Id := No_List; - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit begin @@ -1253,7 +1252,7 @@ package body Exp_SPARK is end if; end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end SPARK_Freeze_Type; end Exp_SPARK; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 5a6fca081a69..1b2de4f248d8 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -2311,8 +2311,7 @@ package body Exp_Util is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit DIC_Prag : Node_Id; @@ -2558,7 +2557,7 @@ package body Exp_Util is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Build_DIC_Procedure_Body; ------------------------------------- @@ -2575,8 +2574,7 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit DIC_Prag : Node_Id; @@ -2783,7 +2781,7 @@ package body Exp_Util is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Build_DIC_Procedure_Declaration; ------------------------------------ @@ -3709,8 +3707,7 @@ package body Exp_Util is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Dummy : Entity_Id; @@ -4058,7 +4055,7 @@ package body Exp_Util is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Build_Invariant_Procedure_Body; ------------------------------------------- @@ -4075,8 +4072,7 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Proc_Decl : Node_Id; @@ -4292,7 +4288,7 @@ package body Exp_Util is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Build_Invariant_Procedure_Declaration; ------------------------ @@ -10640,8 +10636,7 @@ package body Exp_Util is is Loc : constant Source_Ptr := Sloc (Expr); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Call : Node_Id; @@ -10685,7 +10680,7 @@ package body Exp_Util is Name => New_Occurrence_Of (Func_Id, Loc), Parameter_Associations => Param_Assocs); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); return Call; end Make_Predicate_Call; diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb index 3d7b0d77f119..25f49505399b 100644 --- a/gcc/ada/expander.adb +++ b/gcc/ada/expander.adb @@ -84,8 +84,7 @@ package body Expander is -- Ghost mode. procedure Expand (N : Node_Id) is - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit begin @@ -559,7 +558,7 @@ package body Expander is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Expand; --------------------------- diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index afe0fda0671c..2ebffff7a5fa 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2878,8 +2878,7 @@ package body Freeze is is Loc : constant Source_Ptr := Sloc (N); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Atype : Entity_Id; @@ -8360,12 +8359,12 @@ package body Freeze is -- and Per-Object Expressions" will suppress the insertion, and the -- freeze node will be dropped on the floor. - if Saved_GM = Ignore - and then Ghost_Mode /= Ignore - and then Present (Ignored_Ghost_Region) + if Saved_Ghost_Config.Ghost_Mode = Ignore + and then Ghost_Config.Ghost_Mode /= Ignore + and then Present (Ghost_Config.Ignored_Ghost_Region) then Insert_Actions - (Assoc_Node => Ignored_Ghost_Region, + (Assoc_Node => Ghost_Config.Ignored_Ghost_Region, Ins_Actions => Result, Spec_Expr_OK => True); @@ -8373,7 +8372,7 @@ package body Freeze is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); return Result; end Freeze_Entity; diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 6f648f2af922..f9c285316cd5 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -447,7 +447,7 @@ package body Ghost is -- The context is Ghost when it appears within a Ghost package or -- subprogram. - if Ghost_Mode > None then + if Ghost_Config.Ghost_Mode > None then return True; -- Routine Expand_Record_Extension creates a parent subtype without @@ -719,7 +719,7 @@ package body Ghost is -- The context is ghost when it appears within a Ghost package or -- subprogram. - if Ghost_Mode > None then + if Ghost_Config.Ghost_Mode > None then return; -- The context is ghost if Formal is explicitly marked as ghost @@ -1130,22 +1130,22 @@ package body Ghost is -- The context is already within an ignored Ghost region. Maintain the -- start of the outermost ignored Ghost region. - if Present (Ignored_Ghost_Region) then + if Present (Ghost_Config.Ignored_Ghost_Region) then null; -- The current region is the outermost ignored Ghost region. Save its -- starting node. elsif Present (N) and then Mode = Ignore then - Ignored_Ghost_Region := N; + Ghost_Config.Ignored_Ghost_Region := N; -- Otherwise the current region is not ignored, nothing to save else - Ignored_Ghost_Region := Empty; + Ghost_Config.Ignored_Ghost_Region := Empty; end if; - Ghost_Mode := Mode; + Ghost_Config.Ghost_Mode := Mode; end Install_Ghost_Region; procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is @@ -1504,10 +1504,10 @@ package body Ghost is -- A body declared within a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - elsif Ghost_Mode = Check then + elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; - elsif Ghost_Mode = Ignore then + elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; -- Inherit the "ghostness" of the previous declaration when the body @@ -1553,10 +1553,10 @@ package body Ghost is -- A completion elaborated in a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - if Ghost_Mode = Check then + if Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; - elsif Ghost_Mode = Ignore then + elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; -- The completion becomes Ghost when its initial declaration is also @@ -1603,10 +1603,10 @@ package body Ghost is -- A declaration elaborated in a Ghost region is automatically Ghost -- (SPARK RM 6.9(2)). - elsif Ghost_Mode = Check then + elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; - elsif Ghost_Mode = Ignore then + elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; -- A child package or subprogram declaration becomes Ghost when its @@ -1698,10 +1698,10 @@ package body Ghost is -- An instantiation declaration within a Ghost region is automatically -- Ghost (SPARK RM 6.9(2)). - elsif Ghost_Mode = Check then + elsif Ghost_Config.Ghost_Mode = Check then Policy := Name_Check; - elsif Ghost_Mode = Ignore then + elsif Ghost_Config.Ghost_Mode = Ignore then Policy := Name_Ignore; -- Inherit the "ghostness" of the generic unit, but the current Ghost @@ -2018,10 +2018,9 @@ package body Ghost is -- Restore_Ghost_Region -- -------------------------- - procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is + procedure Restore_Ghost_Region (Config : Ghost_Config_Type) is begin - Ghost_Mode := Mode; - Ignored_Ghost_Region := N; + Ghost_Config := Config; end Restore_Ghost_Region; -------------------- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 3863e50a4176..62c809c8fd34 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -243,7 +243,7 @@ package Ghost is -- WARNING: this is a separate front end pass, care should be taken to keep -- it optimized. - procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id); + procedure Restore_Ghost_Region (Config : Ghost_Config_Type); pragma Inline (Restore_Ghost_Region); -- Restore a Ghost region to a previous state described by mode Mode and -- ignored region start node N. This routine must be used in conjunction diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index e595b0841195..73f9fe8e8f71 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -746,9 +746,20 @@ package Opt is -- 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; + type Ghost_Config_Type is record + Ghost_Mode : Ghost_Mode_Type := None; + -- The current Ghost mode in effect + + Ignored_Ghost_Region : Node_Id := Empty; + -- The start of the current ignored Ghost region. This value must always + -- reflect the starting node of the outermost ignored Ghost region. If a + -- nested ignored Ghost region is entered, the value must remain + -- unchanged. + end record; + + Ghost_Config : Ghost_Config_Type; -- GNAT - -- The current Ghost mode in effect + -- All relevant Ghost mode settings Global_Discard_Names : Boolean := False; -- GNAT, GNATBIND @@ -810,12 +821,6 @@ package Opt is -- use of -gnateu, causing subsequent unrecognized switches to result in -- a warning rather than an error. - Ignored_Ghost_Region : Node_Id := Empty; - -- GNAT - -- The start of the current ignored Ghost region. This value must always - -- reflect the starting node of the outermost ignored Ghost region. If a - -- nested ignored Ghost region is entered, the value must remain unchanged. - Implicit_Packing : Boolean := False; -- GNAT -- If set True, then a Size attribute clause on an array is allowed to diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index 86713ff955ab..f47aacc77487 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -1030,8 +1030,7 @@ package body Rtsfind is U : RT_Unit_Table_Record renames RT_Unit_Table (U_Id); Priv_Par : constant Elist_Id := New_Elmt_List; Lib_Unit : Node_Id; - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; @@ -1099,7 +1098,7 @@ package body Rtsfind is procedure Restore_SPARK_Context is begin Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Restore_SPARK_Context; @@ -1289,7 +1288,7 @@ package body Rtsfind is declare LibUnit : constant Node_Id := Unit (Cunit (U.Unum)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_GM : constant Ghost_Mode_Type := Ghost_Config.Ghost_Mode; Clause : Node_Id; Withn : Node_Id; @@ -1308,13 +1307,13 @@ package body Rtsfind is -- later, after ignored ghost code is converted to a null -- statement. - Ghost_Mode := None; + Ghost_Config.Ghost_Mode := None; Withn := Make_With_Clause (Standard_Location, Name => Make_Unit_Name (U, Defining_Unit_Name (Specification (LibUnit)))); - Ghost_Mode := Saved_GM; + Ghost_Config.Ghost_Mode := Saved_GM; Set_Corresponding_Spec (Withn, U.Entity); Set_First_Name (Withn); @@ -1627,7 +1626,9 @@ package body Rtsfind is -- is pulled within an ignored Ghost context because all this code will -- disappear. - if U_Id = System_Secondary_Stack and then Ghost_Mode /= Ignore then + if U_Id = System_Secondary_Stack + and then Ghost_Config.Ghost_Mode /= Ignore + then Sec_Stack_Used := True; end if; diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index e168d62eafbb..944ece119785 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -104,8 +104,7 @@ package body Sem is -- Ghost mode. procedure Analyze (N : Node_Id) is - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit begin @@ -842,7 +841,7 @@ package body Sem is Expand_SPARK_Potential_Renaming (N); end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze; -- Version with check(s) suppressed @@ -1440,8 +1439,7 @@ package body Sem is -- the Ghost mode. procedure Do_Analyze is - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; -- Save Ghost and SPARK mode-related data to restore on exit @@ -1489,7 +1487,7 @@ package body Sem is Style_Max_Line_Length := Saved_ML; Style_Check_Max_Line_Length := Saved_CML; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; end Do_Analyze; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index b5c9e88adbbf..1ba76dc74cee 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -4900,8 +4900,7 @@ package body Sem_Ch12 is Loc : constant Source_Ptr := Sloc (N); Is_Abbrev : constant Boolean := Is_Abbreviated_Instance (Defining_Entity (N)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; @@ -5680,7 +5679,7 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); Style_Check := Saved_Style_Check; @@ -5695,7 +5694,7 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); Style_Check := Saved_Style_Check; end Analyze_Package_Instantiation; @@ -6340,8 +6339,7 @@ package body Sem_Ch12 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; @@ -6736,7 +6734,7 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); exception @@ -6750,7 +6748,7 @@ package body Sem_Ch12 is end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Subprogram_Instantiation; @@ -12874,8 +12872,7 @@ package body Sem_Ch12 is -- the package body. Saved_CS : constant Config_Switches_Type := Save_Config_Switches; - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_LSST : constant Suppress_Stack_Entry_Ptr := @@ -13405,7 +13402,7 @@ package body Sem_Ch12 is Expander_Mode_Restore; Restore_Config_Switches (Saved_CS); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); Restore_Warnings (Saved_Warn); end Instantiate_Package_Body; @@ -13436,8 +13433,7 @@ package body Sem_Ch12 is -- the subprogram body. Saved_CS : constant Config_Switches_Type := Save_Config_Switches; - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_LSST : constant Suppress_Stack_Entry_Ptr := @@ -13740,7 +13736,7 @@ package body Sem_Ch12 is Expander_Mode_Restore; Restore_Config_Switches (Saved_CS); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); Restore_SPARK_Mode (Saved_SM, Saved_SMP); Restore_Warnings (Saved_Warn); end Instantiate_Subprogram_Body; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index b7ada50456a4..f29690b43f81 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -10282,8 +10282,7 @@ package body Sem_Ch13 is procedure Build_Predicate_Function (Typ : Entity_Id; N : Node_Id) is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Expr : Node_Id; @@ -11090,7 +11089,7 @@ package body Sem_Ch13 is end; end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); if Restore_Scope then Pop_Scope; @@ -11110,8 +11109,7 @@ package body Sem_Ch13 is is Loc : constant Source_Ptr := Sloc (Typ); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Func_Decl : Node_Id; @@ -11192,7 +11190,7 @@ package body Sem_Ch13 is Insert_After (Parent (Typ), Func_Decl); Analyze (Func_Decl); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); return Func_Decl; end Build_Predicate_Function_Declaration; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 37261695eacb..9f69e4f6cb8d 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -4386,8 +4386,7 @@ package body Sem_Ch3 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Prev_Entity : Entity_Id := Empty; @@ -5475,7 +5474,7 @@ package body Sem_Ch3 is Check_No_Hidden_State (Id); end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Object_Declaration; --------------------------- @@ -21707,8 +21706,7 @@ package body Sem_Ch3 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Full_Indic : Node_Id; @@ -22401,7 +22399,7 @@ package body Sem_Ch3 is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Process_Full_View; ----------------------------------- diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 0661e64d095d..9e4936bd6293 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -385,8 +385,7 @@ package body Sem_Ch5 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit T1 : Entity_Id; @@ -1193,7 +1192,7 @@ package body Sem_Ch5 is Analyze_Dimension (N); <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); -- If the right-hand side contains target names, expansion has been -- disabled to prevent expansion that might move target names out of @@ -2108,7 +2107,7 @@ package body Sem_Ch5 is -- A label declared within a Ghost region becomes Ghost (SPARK RM -- 6.9(2)). - if Ghost_Mode > None then + if Ghost_Config.Ghost_Mode > None then Set_Is_Ghost_Entity (Id); end if; end Analyze_Implicit_Label_Declaration; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 709f6254b5ec..b7ddc4b7a6a6 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1372,8 +1372,7 @@ package body Sem_Ch6 is Loc : constant Source_Ptr := Sloc (N); Spec : constant Node_Id := Specification (N); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; -- Save the Ghost and SPARK mode-related data to restore on exit @@ -1529,7 +1528,7 @@ package body Sem_Ch6 is <<Leave>> Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Null_Procedure; ----------------------------- @@ -1624,8 +1623,7 @@ package body Sem_Ch6 is Loc : constant Source_Ptr := Sloc (N); P : constant Node_Id := Name (N); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Actual : Node_Id; @@ -1890,7 +1888,7 @@ package body Sem_Ch6 is end if; <<Leave>> - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Procedure_Call; ------------------------------ @@ -3608,8 +3606,7 @@ package body Sem_Ch6 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_EA : constant Boolean := Expander_Active; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; @@ -3836,7 +3833,7 @@ package body Sem_Ch6 is -- user entities, as internally generated entitities might still need -- to be expanded (e.g. those generated for types). - if Present (Ignored_Ghost_Region) + if Present (Ghost_Config.Ignored_Ghost_Region) and then Comes_From_Source (Body_Id) then Expander_Active := False; @@ -5022,12 +5019,12 @@ package body Sem_Ch6 is end if; <<Leave>> - if Present (Ignored_Ghost_Region) then + if Present (Ghost_Config.Ignored_Ghost_Region) then Expander_Active := Saved_EA; end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Subprogram_Body_Helper; ------------------------------------ diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index c2e60aaae113..d28bafb3378c 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -714,8 +714,7 @@ package body Sem_Ch7 is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; Saved_EA : constant Boolean := Expander_Active; Saved_ISMP : constant Boolean := Ignore_SPARK_Mode_Pragmas_In_Instance; @@ -836,7 +835,7 @@ package body Sem_Ch7 is -- user entities, as internally generated entities might still need -- to be expanded (e.g. those generated for types). - if Present (Ignored_Ghost_Region) + if Present (Ghost_Config.Ignored_Ghost_Region) and then Comes_From_Source (Body_Id) then Expander_Active := False; @@ -1149,12 +1148,12 @@ package body Sem_Ch7 is end if; end if; - if Present (Ignored_Ghost_Region) then + if Present (Ghost_Config.Ignored_Ghost_Region) then Expander_Active := Saved_EA; end if; Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Package_Body_Helper; --------------------------------- diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 2717c38cdfde..ecb4e22b4f18 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -436,8 +436,7 @@ package body Sem_Prag is Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Errors : Nat; @@ -492,7 +491,7 @@ package body Sem_Prag is End_Scope; end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end if; Set_Is_Analyzed_Pragma (N); @@ -607,8 +606,7 @@ package body Sem_Prag is CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit CCase : Node_Id; @@ -695,7 +693,7 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Contract_Cases_In_Decl_Part; ---------------------------------- @@ -2464,8 +2462,7 @@ package body Sem_Prag is Exceptional_Contracts : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Exceptional_Contract : Node_Id; @@ -2556,7 +2553,7 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Exceptional_Cases_In_Decl_Part; ------------------------------------- @@ -2772,8 +2769,7 @@ package body Sem_Prag is Exit_Contracts : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Exit_Contract : Node_Id; @@ -2863,7 +2859,7 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Exit_Cases_In_Decl_Part; -------------------------------------------- @@ -3688,8 +3684,7 @@ package body Sem_Prag is Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit begin @@ -3713,7 +3708,7 @@ package body Sem_Prag is Preanalyze_And_Resolve (Expr, Standard_Boolean); Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Initial_Condition_In_Decl_Part; -------------------------------------- @@ -12987,7 +12982,9 @@ package body Sem_Prag is -- An abstract state declared within a Ghost region becomes -- Ghost (SPARK RM 6.9(2)). - if Ghost_Mode > None or else Is_Ghost_Entity (Pack_Id) then + if Ghost_Config.Ghost_Mode > None + or else Is_Ghost_Entity (Pack_Id) + then Set_Is_Ghost_Entity (State_Id); end if; @@ -14302,7 +14299,7 @@ package body Sem_Prag is -- cannot occur within a Ghost subprogram or package -- (SPARK RM 6.9(16)). - if Ghost_Mode > None then + if Ghost_Config.Ghost_Mode > None then Error_Pragma ("pragma % cannot appear within ghost subprogram or " & "package"); @@ -14888,8 +14885,7 @@ package body Sem_Prag is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Cname : Name_Id; @@ -15100,7 +15096,7 @@ package body Sem_Prag is In_Assertion_Expr := In_Assertion_Expr - 1; end if; - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Check; -------------------------- @@ -18720,7 +18716,7 @@ package body Sem_Prag is -- region (SPARK RM 6.9(6)). if Is_False (Expr_Value (Expr)) - and then Ghost_Mode > None + and then Ghost_Config.Ghost_Mode > None then Error_Pragma ("pragma % with value False cannot appear in enabled " @@ -28323,8 +28319,7 @@ package body Sem_Prag is Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Errors : Nat; @@ -28417,7 +28412,7 @@ package body Sem_Prag is Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Pre_Post_Condition_In_Decl_Part; --------------------------------------- @@ -28437,8 +28432,7 @@ package body Sem_Prag is Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Errors : Nat; @@ -28561,7 +28555,7 @@ package body Sem_Prag is Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end if; Set_Is_Analyzed_Pragma (N); @@ -31803,8 +31797,7 @@ package body Sem_Prag is Variants : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit Variant : Node_Id; @@ -31899,7 +31892,7 @@ package body Sem_Prag is Set_Is_Analyzed_Pragma (N); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Analyze_Subprogram_Variant_In_Decl_Part; ------------------------------------ diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b2b4fed8c1e9..73558c13b89f 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -1963,8 +1963,7 @@ package body Sem_Util is -- Local variables - Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; - Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config; -- Save the Ghost-related attributes to restore on exit -- Start of processing for Build_Elaboration_Entity @@ -2060,7 +2059,7 @@ package body Sem_Util is Set_Has_Qualified_Name (Elab_Ent); Set_Has_Fully_Qualified_Name (Elab_Ent); - Restore_Ghost_Region (Saved_GM, Saved_IGR); + Restore_Ghost_Region (Saved_Ghost_Config); end Build_Elaboration_Entity; -------------------------------- @@ -22574,7 +22573,7 @@ package body Sem_Util is -- Mark the Ghost and SPARK mode in effect if Modes then - if Ghost_Mode = Ignore then + if Ghost_Config.Ghost_Mode = Ignore then Set_Is_Ignored_Ghost_Node (N); end if;