From: Viljar Indus <[email protected]>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
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 20ca189ad8c..0ff3d6e34a8 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 6cf7c9c9707..00b3aae0bd9 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 619ac407cb0..1c09e204275 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 a75a507388b..0f9203410f2 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 5a6fca081a6..1b2de4f248d 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 3d7b0d77f11..25f49505399 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 afe0fda0671..2ebffff7a5f 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 6f648f2af92..f9c285316cd 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 3863e50a417..62c809c8fd3 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 e595b084119..73f9fe8e8f7 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 86713ff955a..f47aacc7748 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 e168d62eafb..944ece11978 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 b5c9e88adbb..1ba76dc74ce 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 b7ada50456a..f29690b43f8 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 37261695eac..9f69e4f6cb8 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 0661e64d095..9e4936bd629 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 709f6254b5e..b7ddc4b7a6a 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 c2e60aaae11..d28bafb3378 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 2717c38cdfd..ecb4e22b4f1 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 b2b4fed8c1e..73558c13b89 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;
--
2.43.0
