===================================================================
@@ -1627,22 +1627,6 @@
-- cannot just be passed on to the back end in untransformed state.
procedure Expand_N_Assignment_Statement (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Crep : constant Boolean := Change_Of_Representation (N);
Lhs : constant Node_Id := Name (N);
Loc : constant Source_Ptr := Sloc (N);
@@ -1650,12 +1634,12 @@
Typ : constant Entity_Id := Underlying_Type (Etype (Lhs));
Exp : Node_Id;
- -- Start of processing for Expand_N_Assignment_Statement
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
- -- The assignment statement may be Ghost if the left hand side is Ghost.
+ -- The assignment statement is Ghost when the left hand side is Ghost.
-- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- are properly marked as Ghost.
Set_Ghost_Mode (N);
@@ -1668,7 +1652,7 @@
if Componentwise_Assignment (N) then
Expand_Assign_Record (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -1763,7 +1747,7 @@
Rewrite (N, Call);
Analyze (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end;
@@ -1914,7 +1898,7 @@
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2134,7 +2118,7 @@
if not Crep then
Expand_Bit_Packed_Element_Set (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Change of representation case
@@ -2186,7 +2170,7 @@
-- Nothing to do for valuetypes
-- ??? Set_Scope_Is_Transient (False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
elsif Is_Tagged_Type (Typ)
@@ -2242,7 +2226,7 @@
-- expansion, since they would be missed in -gnatc mode ???
Error_Msg_N ("assignment not available on limited type", N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2413,7 +2397,7 @@
-- it with all checks suppressed.
Analyze (N, Suppress => All_Checks);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end Tagged_Case;
@@ -2431,7 +2415,7 @@
end loop;
Expand_Assign_Array (N, Actual_Rhs);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end;
@@ -2439,7 +2423,7 @@
elsif Is_Record_Type (Typ) then
Expand_Assign_Record (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Scalar types. This is where we perform the processing related to the
@@ -2552,11 +2536,11 @@
end if;
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
exception
when RE_Not_Available =>
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end Expand_N_Assignment_Statement;
===================================================================
@@ -303,9 +303,8 @@
--------------------------
procedure Expand_Pragma_Check (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Cond : constant Node_Id := Arg2 (N);
- Nam : constant Name_Id := Chars (Arg1 (N));
+ Cond : constant Node_Id := Arg2 (N);
+ Nam : constant Name_Id := Chars (Arg1 (N));
Msg : Node_Id;
Loc : constant Source_Ptr := Sloc (First_Node (Cond));
@@ -329,16 +328,6 @@
return;
end if;
- -- Set the Ghost mode in effect from the pragma. In general both the
- -- assertion policy and the Ghost policy of pragma Check must agree,
- -- but there are cases where this can be circumvented. For instance,
- -- a living subtype with an ignored predicate may be declared in one
- -- packade, an ignored Ghost object in another and the compilation may
- -- use -gnata to enable assertions.
- -- ??? Ghost predicates are under redesign
-
- Set_Ghost_Mode (N);
-
-- Since this check is active, we rewrite the pragma into a
-- corresponding if statement, and then analyze the statement.
@@ -502,11 +491,6 @@
Error_Msg_N ("?A?check will fail at run time", N);
end if;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_Pragma_Check;
---------------------------------
@@ -992,8 +976,9 @@
Aggr : constant Node_Id :=
Expression (First (Pragma_Argument_Associations (CCs)));
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Case_Guard : Node_Id;
CG_Checks : Node_Id;
CG_Stmts : List_Id;
@@ -1027,12 +1012,20 @@
return;
end if;
- -- The contract cases may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- The contract cases is Ghost when it applies to a Ghost entity. Set
+ -- the mode now to ensure that any nodes generated during expansion are
+ -- properly flagged as Ghost.
Set_Ghost_Mode (CCs);
+ -- The expansion of contract cases is quite distributed as it produces
+ -- various statements to evaluate the case guards and consequences. To
+ -- preserve the original context, set the Is_Assertion_Expr flag. This
+ -- aids the Ghost legality checks when verifying the placement of a
+ -- reference to a Ghost entity.
+
+ In_Assertion_Expr := In_Assertion_Expr + 1;
+
Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
-- Create the counter which tracks the number of case guards that
@@ -1258,10 +1251,8 @@
Append_To (Stmts, Conseq_Checks);
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ In_Assertion_Expr := In_Assertion_Expr - 1;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Contract_Cases;
---------------------------------------
@@ -1361,22 +1352,6 @@
-------------------------------------
procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
Check : Node_Id;
Expr : Node_Id;
@@ -1384,7 +1359,7 @@
List : List_Id;
Pack_Id : Entity_Id;
- -- Start of processing for Expand_Pragma_Initial_Condition
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
if Nkind (Spec_Or_Body) = N_Package_Body then
@@ -1424,9 +1399,9 @@
Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
- -- The initial condition be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- The initial condition is Ghost when it applies to a Ghost entity. Set
+ -- the mode now to ensure that any nodes generated during expansion are
+ -- properly flagged as Ghost.
Set_Ghost_Mode (Init_Cond);
@@ -1442,7 +1417,7 @@
-- runtime check as it will repeat the illegality.
if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -1461,7 +1436,7 @@
Append_To (List, Check);
Analyze (Check);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Initial_Condition;
------------------------------------
@@ -1811,7 +1786,7 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_Pragma_Loop_Variant
@@ -1825,9 +1800,9 @@
return;
end if;
- -- The loop variant may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- The loop variant is Ghost when it applies to a Ghost entity. Set
+ -- the mode now to ensure that any nodes generated during expansion
+ -- are properly flagged as Ghost.
Set_Ghost_Mode (N);
@@ -1892,10 +1867,7 @@
-- corresponding declarations and statements. We leave it in the tree
-- for documentation purposes. It will be ignored by the backend.
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Loop_Variant;
--------------------------------
===================================================================
@@ -2556,9 +2556,8 @@
-----------------------------------
procedure Analyze_Full_Type_Declaration (N : Node_Id) is
- Def : constant Node_Id := Type_Definition (N);
- Def_Id : constant Entity_Id := Defining_Identifier (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Def : constant Node_Id := Type_Definition (N);
+ Def_Id : constant Entity_Id := Defining_Identifier (N);
T : Entity_Id;
Prev : Entity_Id;
@@ -2576,9 +2575,6 @@
-- list later in Sem_Disp.Check_Operation_From_Incomplete_Type (which
-- is called from Process_Incomplete_Dependents).
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------------------
-- Check_Ops_From_Incomplete_Type --
------------------------------------
@@ -2616,26 +2612,11 @@
end if;
end Check_Ops_From_Incomplete_Type;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Start of processing for Analyze_Full_Type_Declaration
begin
Prev := Find_Type_Name (N);
- -- 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.
@@ -2773,7 +2754,6 @@
end if;
if Etype (T) = Any_Type then
- Restore_Globals;
return;
end if;
@@ -2914,8 +2894,6 @@
Analyze_Aspect_Specifications (N, Def_Id);
end if;
end if;
-
- Restore_Globals;
end Analyze_Full_Type_Declaration;
----------------------------------
@@ -2923,18 +2901,12 @@
----------------------------------
procedure Analyze_Incomplete_Type_Decl (N : Node_Id) is
- F : constant Boolean := Is_Pure (Current_Scope);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- T : Entity_Id;
+ F : constant Boolean := Is_Pure (Current_Scope);
+ T : Entity_Id;
begin
Check_SPARK_05_Restriction ("incomplete type is not allowed", N);
- -- The incomplete type declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during analysis and expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
Generate_Definition (Defining_Identifier (N));
-- Process an incomplete declaration. The identifier must not have been
@@ -2984,11 +2956,6 @@
Set_Private_Dependents (T, New_Elmt_List);
Set_Is_Pure (T, F);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Incomplete_Type_Decl;
-----------------------------------
@@ -3063,37 +3030,13 @@
--------------------------------
procedure Analyze_Number_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
E : constant Node_Id := Expression (N);
Id : constant Entity_Id := Defining_Identifier (N);
Index : Interp_Index;
It : Interp;
T : Entity_Id;
- -- Start of processing for Analyze_Number_Declaration
-
begin
- -- The number declaration may be subject to pragma Ghost with policy
- -- 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);
@@ -3113,8 +3056,6 @@
Set_Etype (Id, Universal_Integer);
Set_Ekind (Id, E_Named_Integer);
Set_Is_Frozen (Id, True);
-
- Restore_Globals;
return;
end if;
@@ -3216,8 +3157,6 @@
Set_Ekind (Id, E_Constant);
Set_Never_Set_In_Source (Id, True);
Set_Is_True_Constant (Id, True);
-
- Restore_Globals;
return;
end if;
@@ -3231,8 +3170,6 @@
Rewrite (E, Make_Integer_Literal (Sloc (N), 1));
Set_Etype (E, Any_Type);
end if;
-
- Restore_Globals;
end Analyze_Number_Declaration;
-----------------------------
@@ -3406,9 +3343,8 @@
--------------------------------
procedure Analyze_Object_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Identifier (N);
+ Loc : constant Source_Ptr := Sloc (N);
+ Id : constant Entity_Id := Defining_Identifier (N);
Act_T : Entity_Id;
T : Entity_Id;
@@ -3437,9 +3373,6 @@
-- Any other relevant delayed aspects on object declarations ???
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
-----------------
-- Count_Tasks --
-----------------
@@ -3518,14 +3451,9 @@
return False;
end Delayed_Aspect_Present;
- ---------------------
- -- Restore_Globals --
- ---------------------
+ -- Local variables
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Analyze_Object_Declaration
@@ -3580,9 +3508,10 @@
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.
+ -- The object declaration is Ghost when it is subject to pragma Ghost or
+ -- completes a deferred Ghost constant. Set the mode now to ensure that
+ -- any nodes generated during analysis and expansion are properly marked
+ -- as Ghost.
Set_Ghost_Mode (N, Prev_Entity);
@@ -3866,7 +3795,7 @@
and then Analyzed (N)
and then No (Expression (N))
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -4139,7 +4068,7 @@
Freeze_Before (N, T);
Set_Is_Frozen (Id);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
@@ -4522,7 +4451,7 @@
Check_No_Hidden_State (Id);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Object_Declaration;
---------------------------
@@ -4543,19 +4472,12 @@
-------------------------------------------
procedure Analyze_Private_Extension_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Indic : constant Node_Id := Subtype_Indication (N);
- T : constant Entity_Id := Defining_Identifier (N);
+ Indic : constant Node_Id := Subtype_Indication (N);
+ T : constant Entity_Id := Defining_Identifier (N);
Parent_Base : Entity_Id;
Parent_Type : Entity_Id;
begin
- -- The private extension declaration may be subject to pragma Ghost with
- -- 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
@@ -4769,11 +4691,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, T);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Private_Extension_Declaration;
---------------------------------
@@ -4784,18 +4701,11 @@
(N : Node_Id;
Skip : Boolean := False)
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
R_Checks : Check_Result;
T : Entity_Id;
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);
@@ -5393,11 +5303,6 @@
end if;
Analyze_Dimension (N);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Subtype_Declaration;
--------------------------------
===================================================================
@@ -4177,26 +4177,27 @@
-- Encode entity names in package body
procedure Expand_N_Package_Body (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Spec_Ent : constant Entity_Id := Corresponding_Spec (N);
- Fin_Id : Entity_Id;
+ Spec_Id : constant Entity_Id := Corresponding_Spec (N);
+ Fin_Id : Entity_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
- -- The package body may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as ignored Ghost.
+ -- The package body is Ghost when the corresponding spec is Ghost. Set
+ -- the mode now to ensure that any nodes generated during expansion are
+ -- properly marked as Ghost.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Spec_Id);
-- This is done only for non-generic packages
- if Ekind (Spec_Ent) = E_Package then
+ if Ekind (Spec_Id) = E_Package then
Push_Scope (Corresponding_Spec (N));
-- Build dispatch tables of library level tagged types
if Tagged_Type_Expansion
- and then Is_Library_Level_Entity (Spec_Ent)
+ and then Is_Library_Level_Entity (Spec_Id)
then
Build_Static_Dispatch_Tables (N);
end if;
@@ -4207,7 +4208,7 @@
-- assertion expression must be verified at the end of the body
-- statements.
- if Present (Get_Pragma (Spec_Ent, Pragma_Initial_Condition)) then
+ if Present (Get_Pragma (Spec_Id, Pragma_Initial_Condition)) then
Expand_Pragma_Initial_Condition (N);
end if;
@@ -4215,13 +4216,13 @@
end if;
Set_Elaboration_Flag (N, Corresponding_Spec (N));
- Set_In_Package_Body (Spec_Ent, False);
+ Set_In_Package_Body (Spec_Id, False);
-- Set to encode entity names in package body before gigi is called
Qualify_Entity_Names (N);
- if Ekind (Spec_Ent) /= E_Generic_Package then
+ if Ekind (Spec_Id) /= E_Generic_Package then
Build_Finalizer
(N => N,
Clean_Stmts => No_List,
@@ -4244,10 +4245,7 @@
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Body;
----------------------------------
@@ -4260,7 +4258,6 @@
-- appear.
procedure Expand_N_Package_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Entity (N);
Spec : constant Node_Id := Specification (N);
Decls : List_Id;
@@ -4304,12 +4301,6 @@
return;
end if;
- -- The package declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- For a package declaration that implies no associated body, generate
-- task activation call and RACW supporting bodies now (since we won't
-- have a specific separate compilation unit for that).
@@ -4383,11 +4374,6 @@
Set_Finalizer (Id, Fin_Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Package_Declaration;
-----------------------------
===================================================================
@@ -90,9 +90,8 @@
------------------------
procedure Analyze_Assignment (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Lhs : constant Node_Id := Name (N);
- Rhs : constant Node_Id := Expression (N);
+ Lhs : constant Node_Id := Name (N);
+ Rhs : constant Node_Id := Expression (N);
T1 : Entity_Id;
T2 : Entity_Id;
Decl : Node_Id;
@@ -107,9 +106,6 @@
-- the assignment, and at the end of processing before setting any new
-- current values in place.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
procedure Set_Assignment_Type
(Opnd : Node_Id;
Opnd_Type : in out Entity_Id);
@@ -215,15 +211,6 @@
end if;
end Kill_Lhs;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-------------------------
-- Set_Assignment_Type --
-------------------------
@@ -282,6 +269,10 @@
end if;
end Set_Assignment_Type;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Assignment
begin
@@ -293,10 +284,9 @@
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.
+ -- An assignment statement is Ghost when the left hand side denotes a
+ -- Ghost entity. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly marked as Ghost.
Set_Ghost_Mode (N);
Analyze (Rhs);
@@ -391,7 +381,7 @@
Error_Msg_N
("no valid types for left-hand side for assignment", Lhs);
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
@@ -467,14 +457,14 @@
"specified??", Lhs);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
end;
Diagnose_Non_Variable_Lhs (Lhs);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Error of assigning to limited type. We do however allow this in
@@ -495,7 +485,7 @@
Explain_Limited_Type (T1, Lhs);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Enforce RM 3.9.3 (8): the target of an assignment operation cannot be
@@ -534,7 +524,7 @@
then
Error_Msg_N ("invalid use of incomplete type", Lhs);
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -552,7 +542,7 @@
if Rhs = Error then
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -561,7 +551,7 @@
if not Covers (T1, T2) then
Wrong_Type (Rhs, Etype (Lhs));
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -589,7 +579,7 @@
if T1 = Any_Type or else T2 = Any_Type then
Kill_Lhs;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -682,7 +672,7 @@
-- to reset Is_True_Constant, and desirable for xref purposes.
Note_Possible_Modification (Lhs, Sure => True);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- If we know the right hand side is non-null, then we convert to the
@@ -889,7 +879,7 @@
end;
Analyze_Dimension (N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Assignment;
-----------------------------
===================================================================
@@ -6424,34 +6424,17 @@
Expr : Node_Id;
Mem : Boolean := False) return Node_Id
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Loc : constant Source_Ptr := Sloc (Expr);
Call : Node_Id;
PFM : Entity_Id;
- -- Start of processing for Make_Predicate_Call
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
pragma Assert (Present (Predicate_Function (Typ)));
- -- The related type may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that the call is properly flagged as
- -- ignored Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the call is properly marked as Ghost.
Set_Ghost_Mode_From_Entity (Typ);
@@ -6466,7 +6449,7 @@
Name => New_Occurrence_Of (PFM, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Call;
end if;
end if;
@@ -6479,7 +6462,7 @@
New_Occurrence_Of (Predicate_Function (Typ), Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Call;
end Make_Predicate_Call;
===================================================================
@@ -571,7 +571,7 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
@@ -637,10 +637,9 @@
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.
+ -- A package body is Ghost when the corresponding spec is Ghost. 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);
@@ -942,10 +941,7 @@
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Package_Body_Helper;
------------------------------
@@ -1021,22 +1017,6 @@
---------------------------------
procedure Analyze_Package_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Id : constant Node_Id := Defining_Entity (N);
Body_Required : Boolean;
@@ -1048,8 +1028,6 @@
PF : Boolean;
-- True when in the context of a declared pure library unit
- -- Start of processing for Analyze_Package_Declaration
-
begin
if Debug_Flag_C then
Write_Str ("==> package spec ");
@@ -1060,12 +1038,6 @@
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);
@@ -1102,7 +1074,6 @@
-- package Pkg is ...
if From_Limited_With (Id) then
- Restore_Globals;
return;
end if;
@@ -1163,8 +1134,6 @@
Write_Location (Sloc (N));
Write_Eol;
end if;
-
- Restore_Globals;
end Analyze_Package_Declaration;
-----------------------------------
@@ -1851,17 +1820,10 @@
--------------------------------------
procedure Analyze_Private_Type_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Id : constant Entity_Id := Defining_Identifier (N);
PF : constant Boolean := Is_Pure (Enclosing_Lib_Unit_Entity);
begin
- -- The private type declaration may be subject to pragma Ghost with
- -- 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);
@@ -1885,11 +1847,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Private_Type_Declaration;
----------------------------------
===================================================================
@@ -390,12 +390,12 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
CCase : Node_Id;
Restore_Scope : Boolean := False;
@@ -454,10 +454,7 @@
Error_Msg_N ("wrong syntax for constract cases", N);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
@@ -1715,11 +1712,12 @@
(N : Node_Id;
Expr_Val : out Boolean)
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
- Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1));
+ Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
-- Set the Ghost mode in effect from the pragma. Due to the delayed
-- analysis of the pragma, the Ghost mode at point of declaration and
@@ -1758,10 +1756,7 @@
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_External_Property_In_Decl_Part;
---------------------------------
@@ -2264,11 +2259,12 @@
--------------------------------------------
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
-- Set the Ghost mode in effect from the pragma. Due to the delayed
-- analysis of the pragma, the Ghost mode at point of declaration and
@@ -2283,11 +2279,7 @@
-- is not desired at this point.
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
@@ -10808,18 +10800,12 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Expr : Node_Id;
New_Args : List_Id;
-- Start of processing for Assert
begin
- -- Ensure that analysis and expansion produce Ghost nodes if the
- -- pragma itself is Ghost.
-
- Set_Ghost_Mode (N);
-
-- Assert is an Ada 2005 RM-defined pragma
if Prag_Id = Pragma_Assert then
@@ -10892,11 +10878,6 @@
Pragma_Argument_Associations => New_Args));
Analyze (N);
-
- -- Restore the original Ghost mode once analysis and expansion
- -- have taken place.
-
- Ghost_Mode := GM;
end Assert;
----------------------
@@ -11551,15 +11532,17 @@
-- allowed, since they have special meaning for Check_Policy.
when Pragma_Check => Check : declare
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Cname : Name_Id;
Eloc : Source_Ptr;
Expr : Node_Id;
Str : Node_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
- -- Ensure that analysis and expansion produce Ghost nodes if the
- -- pragma itself is Ghost.
+ -- Pragma Check is Ghost when it applies to a Ghost entity. Set
+ -- the mode now to ensure that any nodes generated during analysis
+ -- and expansion are marked as Ghost.
Set_Ghost_Mode (N);
@@ -11758,10 +11741,7 @@
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- -- Restore the original Ghost mode once analysis and expansion
- -- have taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Check;
--------------------------
@@ -15699,7 +15679,6 @@
-- [,[Message =>] String_Expression]);
when Pragma_Invariant => Invariant : declare
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Discard : Boolean;
Typ : Entity_Id;
Type_Id : Node_Id;
@@ -15793,11 +15772,6 @@
if Class_Present (N) then
Set_Has_Inheritable_Invariants (Typ);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion
- -- have taken place.
-
- Ghost_Mode := GM;
end Invariant;
----------------------
@@ -22450,11 +22424,12 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
@@ -22500,11 +22475,7 @@
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
===================================================================
@@ -3135,7 +3135,6 @@
------------------------------------------
procedure Analyze_Generic_Package_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Decls : constant List_Id :=
Visible_Declarations (Specification (N));
@@ -3146,11 +3145,6 @@
Save_Parent : 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
@@ -3302,11 +3296,6 @@
end if;
end;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Generic_Package_Declaration;
--------------------------------------------
@@ -3314,7 +3303,6 @@
--------------------------------------------
procedure Analyze_Generic_Subprogram_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Formals : List_Id;
Id : Entity_Id;
New_N : Node_Id;
@@ -3324,12 +3312,6 @@
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
@@ -3478,11 +3460,6 @@
Generate_Reference_To_Formals (Id);
List_Inherited_Pre_Post_Aspects (Id);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Generic_Subprogram_Declaration;
-----------------------------------
===================================================================
@@ -29,6 +29,7 @@
with Elists; use Elists;
with Expander; use Expander;
with Fname; use Fname;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
with Nlists; use Nlists;
@@ -95,9 +96,7 @@
-------------
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.
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
Debug_A_Entry ("analyzing ", N);
@@ -109,6 +108,14 @@
return;
end if;
+ -- A declaration may be subject to pragma Ghost. Set the mode now to
+ -- ensure that any nodes generated during analysis and expansion are
+ -- marked as Ghost.
+
+ if Is_Declaration (N) then
+ Set_Ghost_Mode (N);
+ end if;
+
-- Otherwise processing depends on the node kind
case Nkind (N) is
@@ -720,10 +727,7 @@
Expand (N);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze;
-- Version with check(s) suppressed
@@ -1310,9 +1314,7 @@
----------------
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.
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
List : Elist_Id;
@@ -1343,7 +1345,7 @@
Pop_Scope;
Restore_Scope_Stack (List);
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Do_Analyze;
-- Local variables
===================================================================
@@ -925,9 +925,7 @@
-- 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.
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Load_RTU
@@ -1043,9 +1041,7 @@
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
- -- Restore the original Ghost mode now that analysis has taken place
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Load_RTU;
--------------------
===================================================================
@@ -1870,10 +1870,6 @@
-------------------
function Freeze_Entity (E : Entity_Id; N : Node_Id) return List_Id is
- 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;
@@ -1945,9 +1941,6 @@
-- 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-
@@ -4492,15 +4485,6 @@
Append_List (Result, Decls);
end Late_Freeze_Subprogram;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
------------------------------
-- Wrap_Imported_Subprogram --
------------------------------
@@ -4644,12 +4628,16 @@
end if;
end Wrap_Imported_Subprogram;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- 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.
+ -- The entity being frozen may be subject to pragma Ghost. Set the mode
+ -- now to ensure that any nodes generated during freezing are properly
+ -- flagged as Ghost.
Set_Ghost_Mode_From_Entity (E);
@@ -4668,7 +4656,7 @@
-- Do not freeze if already frozen since we only need one freeze node
if Is_Frozen (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- It is improper to freeze an external entity within a generic because
@@ -4683,7 +4671,7 @@
Analyze_Aspects_At_Freeze_Point (E);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- AI05-0213: A formal incomplete type does not freeze the actual. In
@@ -4694,19 +4682,19 @@
and then No (Full_View (Base_Type (E)))
and then Ada_Version >= Ada_2012
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- Formal subprograms are never frozen
elsif Is_Formal_Subprogram (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- Generic types are never frozen as they lack delayed semantic checks
elsif Is_Generic_Type (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
-- Do not freeze a global entity within an inner scope created during
@@ -4740,7 +4728,7 @@
then
exit;
else
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
end if;
@@ -4776,7 +4764,7 @@
end loop;
if No (S) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
end;
@@ -4784,7 +4772,7 @@
elsif Ekind (E) = E_Generic_Package then
Result := Freeze_Generic_Entities (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
@@ -4867,7 +4855,7 @@
if not Is_Internal (E) then
if not Freeze_Profile (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
end if;
@@ -4892,7 +4880,7 @@
if Late_Freezing then
Late_Freeze_Subprogram (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
@@ -5055,7 +5043,7 @@
and then not Has_Delayed_Freeze (E))
then
Check_Compile_Time_Size (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
@@ -5330,7 +5318,7 @@
if not Is_Frozen (Root_Type (E)) then
Set_Is_Frozen (E, False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
@@ -5466,7 +5454,7 @@
and then not Present (Full_View (E))
then
Set_Is_Frozen (E, False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
-- Case of full view present
@@ -5558,7 +5546,7 @@
Set_RM_Size (E, RM_Size (Full_View (E)));
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
-- Case of underlying full view present
@@ -5588,7 +5576,7 @@
Check_Debug_Info_Needed (E);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
-- Case of no full view present. If entity is derived or subtype,
@@ -5602,7 +5590,7 @@
else
Set_Is_Frozen (E, False);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return No_List;
end if;
@@ -5651,7 +5639,7 @@
-- generic processing), so we never need freeze nodes for them.
if Is_Generic_Type (E) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
@@ -6267,7 +6255,7 @@
end if;
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end Freeze_Entity;
===================================================================
@@ -1314,7 +1314,6 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (Typ);
Prag : constant Node_Id :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
@@ -1324,6 +1323,8 @@
Expr : Node_Id;
Stmt : Node_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Build_Default_Init_Cond_Procedure_Body
begin
@@ -1341,8 +1342,8 @@
return;
end if;
- -- Ensure that the analysis and expansion produce Ghost nodes if the
- -- type itself is Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now
+ -- to ensure that the analysis and expansion produce Ghost nodes.
Set_Ghost_Mode_From_Entity (Typ);
@@ -1412,11 +1413,7 @@
Set_Corresponding_Spec (Body_Decl, Proc_Id);
Insert_After_And_Analyze (Declaration_Node (Typ), Body_Decl);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Build_Default_Init_Cond_Procedure_Body;
-- Local variables
@@ -1465,10 +1462,12 @@
---------------------------------------------------
procedure Build_Default_Init_Cond_Procedure_Declaration (Typ : Entity_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Loc : constant Source_Ptr := Sloc (Typ);
- Prag : constant Node_Id :=
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Prag : constant Node_Id :=
Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Proc_Id : Entity_Id;
begin
@@ -1485,8 +1484,8 @@
return;
end if;
- -- Ensure that the analysis and expansion produce Ghost nodes if the
- -- type itself is Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the analysis and expansion produce Ghost nodes.
Set_Ghost_Mode_From_Entity (Typ);
@@ -1520,10 +1519,7 @@
Defining_Identifier => Make_Temporary (Loc, 'I'),
Parameter_Type => New_Occurrence_Of (Typ, Loc))))));
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Build_Default_Init_Cond_Procedure_Declaration;
---------------------------
===================================================================
@@ -1990,6 +1990,10 @@
return;
end Resolution_Failed;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Resolve
begin
@@ -1997,6 +2001,14 @@
return;
end if;
+ -- A declaration may be subject to pragma Ghost. Set the mode now to
+ -- ensure that any nodes generated during analysis and expansion are
+ -- marked as Ghost.
+
+ if Is_Declaration (N) then
+ Set_Ghost_Mode (N);
+ end if;
+
-- Access attribute on remote subprogram cannot be used for a non-remote
-- access-to-subprogram type.
@@ -2112,6 +2124,7 @@
if Analyzed (N) then
Debug_A_Exit ("resolving ", N, " (done, already analyzed)");
Analyze_Dimension (N);
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Any case of Any_Type as the Etype value means that we had a
@@ -2119,6 +2132,7 @@
elsif Etype (N) = Any_Type then
Debug_A_Exit ("resolving ", N, " (done, Etype = Any_Type)");
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2550,6 +2564,7 @@
then
Resolve (N, Full_View (Typ));
Set_Etype (N, Typ);
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Check for an aggregate. Sometimes we can get bogus aggregates
@@ -2658,6 +2673,7 @@
if Address_Integer_Convert_OK (Typ, Etype (N)) then
Rewrite (N, Unchecked_Convert_To (Typ, Relocate_Node (N)));
Analyze_And_Resolve (N, Typ);
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2720,12 +2736,14 @@
end if;
Resolution_Failed;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Test if we have more than one interpretation for the context
elsif Ambiguous then
Resolution_Failed;
+ Ghost_Mode := Save_Ghost_Mode;
return;
-- Only one intepretation
@@ -2813,6 +2831,7 @@
-- Rewrite_Renamed_Operator.
if Analyzed (N) then
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
@@ -2962,6 +2981,7 @@
if Nkind (N) not in N_Subexpr then
Debug_A_Exit ("resolving ", N, " (done)");
Expand (N);
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -2996,6 +3016,8 @@
Expand (N);
end if;
+
+ Ghost_Mode := Save_Ghost_Mode;
end Resolve;
-------------
===================================================================
@@ -31,7 +31,6 @@
with Exp_Ch7; use Exp_Ch7;
with Exp_Intr; use Exp_Intr;
with Exp_Util; use Exp_Util;
-with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
@@ -1190,9 +1189,8 @@
-- end if;
procedure Expand_N_Exception_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Identifier (N);
- Loc : constant Source_Ptr := Sloc (N);
+ Id : constant Entity_Id := Defining_Identifier (N);
+ Loc : constant Source_Ptr := Sloc (N);
Ex_Id : Entity_Id;
Flag_Id : Entity_Id;
L : List_Id;
@@ -1279,12 +1277,6 @@
return;
end if;
- -- The exception declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- Definition of the external name: nam : constant String := "A.B.NAME";
Ex_Id :=
@@ -1391,11 +1383,6 @@
Insert_List_After_And_Analyze (N, L);
end if;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Exception_Declaration;
---------------------------------------------
===================================================================
@@ -67,6 +67,12 @@
-- Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
-- a reference to a Ghost entity. Return Empty if there is no such entity.
+ function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
+ -- Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether
+ -- declaration or body N is subject to aspect or pragma Ghost. Use this
+ -- routine in cases where [source] pragma Ghost has not been analyzed yet,
+ -- but the context needs to establish the "ghostness" of N.
+
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
-- Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
-- Signal all enclosing scopes that they now contain ignored Ghost code.
@@ -407,15 +413,27 @@
-- Special cases
- -- An if statement is a suitable context for a Ghost entity if it
- -- is the byproduct of assertion expression expansion.
+ elsif Nkind (Stmt) = N_If_Statement then
- elsif Nkind (Stmt) = N_If_Statement
- and then Nkind (Original_Node (Stmt)) = N_Pragma
- and then Assertion_Expression_Pragma
- (Get_Pragma_Id (Original_Node (Stmt)))
- then
- return True;
+ -- An if statement is a suitable context for a Ghost entity if
+ -- it is the byproduct of assertion expression expansion. Note
+ -- that the assertion expression may not be related to a Ghost
+ -- entity, but it may still contain references to Ghost
+ -- entities.
+
+ if Nkind (Original_Node (Stmt)) = N_Pragma
+ and then Assertion_Expression_Pragma
+ (Get_Pragma_Id (Original_Node (Stmt)))
+ then
+ return True;
+
+ -- The expansion of pragma Contract_Cases produces various if
+ -- statements to evaluate all case guards. This is a suitable
+ -- context as Contract_Cases is an assertion expression.
+
+ elsif In_Assertion_Expr > 0 then
+ return True;
+ end if;
end if;
return False;
@@ -517,12 +535,10 @@
Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
-- Otherwise the Ghost entity appears in a non-Ghost context and affects
- -- its behavior or value.
+ -- its behavior or value (SPARK RM 6.9(11,12)).
else
- Error_Msg_N
- ("ghost entity cannot appear in this context (SPARK RM 6.9(11))",
- Ghost_Ref);
+ Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
end if;
end Check_Ghost_Context;
@@ -701,8 +717,8 @@
Expr := Get_Pragma_Arg (Expr);
end if;
- -- Determine whether the expression of the aspect is static and
- -- denotes True.
+ -- Determine whether the expression of the aspect or pragma is static
+ -- and denotes True.
if Present (Expr) then
Preanalyze_And_Resolve (Expr);
===================================================================
@@ -4917,20 +4917,17 @@
---------------------------------------
procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
begin
- -- The procedure call may be Ghost if the name is Ghost. Set the mode
- -- now to ensure that any nodes generated during expansion are properly
- -- flagged as ignored Ghost.
+ -- The procedure call is Ghost when the name is Ghost. Set the mode now
+ -- to ensure that any nodes generated during expansion are properly set
+ -- as Ghost.
Set_Ghost_Mode (N);
- Expand_Call (N);
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Expand_Call (N);
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Procedure_Call_Statement;
--------------------------------------
@@ -5005,10 +5002,9 @@
-- Wrap thread body
procedure Expand_N_Subprogram_Body (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Loc : constant Source_Ptr := Sloc (N);
- HSS : constant Node_Id := Handled_Statement_Sequence (N);
- Body_Id : Entity_Id;
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+ HSS : constant Node_Id := Handled_Statement_Sequence (N);
+ Loc : constant Source_Ptr := Sloc (N);
Except_H : Node_Id;
L : List_Id;
Spec_Id : Entity_Id;
@@ -5019,9 +5015,6 @@
-- the latter test is not critical, it does not matter if we add a few
-- extra returns, since they get eliminated anyway later on.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
----------------
-- Add_Return --
----------------
@@ -5094,24 +5087,26 @@
end if;
end Add_Return;
- ---------------------
- -- Restore_Globals --
- ---------------------
+ -- Local varaibles
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Subprogram_Body
begin
- -- The subprogram body may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are flagged as ignored Ghost.
+ if Present (Corresponding_Spec (N)) then
+ Spec_Id := Corresponding_Spec (N);
+ else
+ Spec_Id := Body_Id;
+ end if;
- Set_Ghost_Mode (N);
+ -- The subprogram body is Ghost when it is stand alone and subject to
+ -- pragma Ghost or the corresponding spec is Ghost. To accomodate both
+ -- cases, set the mode now to ensure that any nodes generated during
+ -- expansion are marked as Ghost.
+ Set_Ghost_Mode (N, Spec_Id);
+
-- Set L to either the list of declarations if present, or to the list
-- of statements if no declarations are present. This is used to insert
-- new stuff at the start.
@@ -5164,16 +5159,6 @@
end;
end if;
- -- Find entity for subprogram
-
- Body_Id := Defining_Entity (N);
-
- if Present (Corresponding_Spec (N)) then
- Spec_Id := Corresponding_Spec (N);
- else
- Spec_Id := Body_Id;
- end if;
-
-- Need poll on entry to subprogram if polling enabled. We only do this
-- for non-empty subprograms, since it does not seem necessary to poll
-- for a dummy null subprogram.
@@ -5288,7 +5273,7 @@
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
@@ -5424,7 +5409,7 @@
Unest_Bodies.Append ((Spec_Id, N));
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Body;
-----------------------------------
@@ -5451,21 +5436,14 @@
-- If the declaration is for a null procedure, emit null body
procedure Expand_N_Subprogram_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Subp : constant Entity_Id := Defining_Entity (N);
- Scop : constant Entity_Id := Scope (Subp);
+ Loc : constant Source_Ptr := Sloc (N);
+ Subp : constant Entity_Id := Defining_Entity (N);
+ Scop : constant Entity_Id := Scope (Subp);
Prot_Bod : Node_Id;
Prot_Decl : Node_Id;
Prot_Id : Entity_Id;
begin
- -- The subprogram declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- In SPARK, subprogram declarations are only allowed in package
-- specifications.
@@ -5566,11 +5544,6 @@
Set_Is_Inlined (Subp, False);
end;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Subprogram_Declaration;
--------------------------------
===================================================================
@@ -66,12 +66,6 @@
-- 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
===================================================================
@@ -50,13 +50,15 @@
---------------------------------------------
procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Decl : Node_Id;
begin
- -- The exception renaming declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes
- -- generated during expansion are properly flagged as ignored Ghost.
+ -- The exception renaming declaration is Ghost when it is subject to
+ -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set
+ -- the mode now to ensure that any nodes generated during expansion are
+ -- properly marked as Ghost.
Set_Ghost_Mode (N);
@@ -66,10 +68,7 @@
Insert_Action (N, Decl);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Exception_Renaming_Declaration;
------------------------------------------
@@ -159,14 +158,15 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Object_Renaming_Declaration
begin
- -- The object renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during expansion are properly flagged as ignored Ghost.
+ -- The object renaming declaration is Ghost when it is subject to pragma
+ -- Ghost or renames a Ghost entity. To accomodate both cases, set the
+ -- mode now to ensure that any nodes generated during expansion are
+ -- properly marked as Ghost.
Set_Ghost_Mode (N);
@@ -213,10 +213,7 @@
Insert_Action (N, Decl);
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Object_Renaming_Declaration;
-------------------------------------------
@@ -224,13 +221,15 @@
-------------------------------------------
procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
Decl : Node_Id;
begin
- -- The package renaming declaration may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during expansion are properly flagged as ignored Ghost.
+ -- The package renaming declaration is Ghost when it is subject to
+ -- pragma Ghost or renames a Ghost entity. To accomodate both cases,
+ -- set the mode now to ensure that any nodes generated during expansion
+ -- are properly marked as Ghost.
Set_Ghost_Mode (N);
@@ -273,10 +272,7 @@
end if;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Renaming_Declaration;
----------------------------------------------
@@ -326,15 +322,16 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Nam : constant Node_Id := Name (N);
+ Nam : constant Node_Id := Name (N);
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Expand_N_Subprogram_Renaming_Declaration
begin
- -- The subprogram renaming declaration may be subject to pragma Ghost
- -- with policy Ignore. Set the mode now to ensure that any nodes created
- -- during expansion are properly flagged as ignored Ghost.
+ -- The subprogram renaming declaration is Ghost when it is subject to
+ -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set
+ -- the mode now to ensure that any nodes created during expansion are
+ -- properly flagged as ignored Ghost.
Set_Ghost_Mode (N);
@@ -402,10 +399,7 @@
end;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Renaming_Declaration;
end Exp_Ch8;
===================================================================
@@ -209,18 +209,11 @@
---------------------------------------------
procedure Analyze_Abstract_Subprogram_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Scop : constant Entity_Id := Current_Scope;
- Subp_Id : constant Entity_Id :=
+ Scop : constant Entity_Id := Current_Scope;
+ Subp_Id : constant Entity_Id :=
Analyze_Subprogram_Specification (Specification (N));
begin
- -- The abstract subprogram declaration may be subject to pragma Ghost
- -- 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 (Subp_Id);
@@ -261,11 +254,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Subp_Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Abstract_Subprogram_Declaration;
---------------------------------
@@ -1547,15 +1535,10 @@
----------------------------
procedure Analyze_Procedure_Call (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
procedure Analyze_Call_And_Resolve;
-- Do Analyze and Resolve calls for procedure call
-- At end, check illegal order dependence.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------------
-- Analyze_Call_And_Resolve --
------------------------------
@@ -1570,15 +1553,6 @@
end if;
end Analyze_Call_And_Resolve;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Local variables
Actuals : constant List_Id := Parameter_Associations (N);
@@ -1587,6 +1561,8 @@
Actual : Node_Id;
New_N : Node_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Procedure_Call
begin
@@ -1618,10 +1594,9 @@
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.
+ -- A procedure call is Ghost when its name denotes a Ghost procedure.
+ -- Set the mode now to ensure that any nodes generated during analysis
+ -- and expansion are properly marked as Ghost.
Set_Ghost_Mode (N);
@@ -1657,7 +1632,7 @@
and then Is_Record_Type (Etype (Entity (P)))
and then Remote_AST_I_Dereference (P)
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
elsif Is_Entity_Name (P)
@@ -1794,7 +1769,7 @@
Error_Msg_N ("invalid procedure or entry call", N);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Procedure_Call;
------------------------------
@@ -2275,7 +2250,6 @@
-- the subprogram, or to perform conformance checks.
procedure Analyze_Subprogram_Body_Helper (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
Loc : constant Source_Ptr := Sloc (N);
Body_Spec : Node_Id := Specification (N);
Body_Id : Entity_Id := Defining_Entity (Body_Spec);
@@ -2351,9 +2325,6 @@
-- Determine whether subprogram Subp_Id is a primitive of a concurrent
-- type that implements an interface and has a private view.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
procedure Set_Trivial_Subprogram (N : Node_Id);
-- Sets the Is_Trivial_Subprogram flag in both spec and body of the
-- subprogram whose body is being analyzed. N is the statement node
@@ -2930,15 +2901,6 @@
return False;
end Is_Private_Concurrent_Primitive;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
----------------------------
-- Set_Trivial_Subprogram --
----------------------------
@@ -3046,6 +3008,10 @@
end if;
end Verify_Overriding_Indicator;
+ -- Local variables
+
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- Start of processing for Analyze_Subprogram_Body_Helper
begin
@@ -3065,10 +3031,10 @@
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.
+ -- A subprogram body is Ghost when it is stand alone and subject
+ -- to pragma Ghost or when the corresponding spec is Ghost. Set
+ -- the mode now to ensure that any nodes generated during analysis
+ -- and expansion are properly marked as Ghost.
Set_Ghost_Mode (N, Spec_Id);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
@@ -3081,7 +3047,7 @@
Check_Missing_Return;
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
@@ -3089,7 +3055,7 @@
-- enter name will post error.
Enter_Name (Body_Id);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -3100,7 +3066,7 @@
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
@@ -3112,20 +3078,20 @@
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.
+ -- A subprogram body is Ghost when it is stand alone and
+ -- subject to pragma Ghost or when the corresponding spec is
+ -- Ghost. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly marked as Ghost.
Set_Ghost_Mode (N, Spec_Id);
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.
+ -- A subprogram body is Ghost when it is stand alone and
+ -- subject to pragma Ghost or when the corresponding spec is
+ -- Ghost. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly marked as Ghost.
Set_Ghost_Mode (N, Spec_Id);
@@ -3179,7 +3145,7 @@
-- If this is a duplicate body, no point in analyzing it
if Error_Posted (N) then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -3212,10 +3178,10 @@
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.
+ -- A subprogram body is Ghost when it is stand alone and subject
+ -- to pragma Ghost or when the corresponding spec is Ghost. Set
+ -- the mode now to ensure that any nodes generated during analysis
+ -- and expansion are properly marked as Ghost.
Set_Ghost_Mode (N, Spec_Id);
end if;
@@ -3292,7 +3258,7 @@
if Is_Abstract_Subprogram (Spec_Id) then
Error_Msg_N ("an abstract subprogram cannot have a body", N);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
else
@@ -3362,7 +3328,7 @@
if not Conformant
and then not Mode_Conformant (Body_Id, Spec_Id)
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
@@ -3569,7 +3535,7 @@
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return;
end if;
@@ -4034,7 +4000,7 @@
end if;
end;
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
end Analyze_Subprogram_Body_Helper;
---------------------------------
@@ -4139,37 +4105,13 @@
------------------------------------
procedure Analyze_Subprogram_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
Scop : constant Entity_Id := Current_Scope;
Designator : Entity_Id;
Is_Completion : Boolean;
-- Indicates whether a null procedure declaration is a completion
- -- Start of processing for Analyze_Subprogram_Declaration
-
begin
- -- The subprogram declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- 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
@@ -4191,7 +4133,6 @@
-- The null procedure acts as a body, nothing further is needed
if Is_Completion then
- Restore_Globals;
return;
end if;
end if;
@@ -4372,8 +4313,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Designator);
end if;
-
- Restore_Globals;
end Analyze_Subprogram_Declaration;
--------------------------------------
===================================================================
@@ -3645,10 +3645,6 @@
-- 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 :=
@@ -3711,9 +3707,6 @@
-- 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 --
------------------------------
@@ -4398,15 +4391,6 @@
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;
@@ -4436,6 +4420,8 @@
TSD_Aggr_List : List_Id;
TSD_Tags_List : List_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- The following name entries are used by Make_DT to generate a number
-- of entities related to a tagged type. These entities may be generated
-- in a scope other than that of the tagged type declaration, and if
@@ -4477,9 +4463,9 @@
begin
pragma Assert (Is_Frozen (Typ));
- -- The tagged type being processed may be subject to pragma Ghost with
- -- policy Ignore. Set the mode now to ensure that any nodes generated
- -- during dispatch table creation are properly flagged as ignored Ghost.
+ -- The tagged type being processed may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during dispatch table
+ -- creation are properly marked as Ghost.
Set_Ghost_Mode (Declaration_Node (Typ), Typ);
@@ -4491,12 +4477,12 @@
or else Convention (Typ) = Convention_CIL
or else Convention (Typ) = Convention_Java
then
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
elsif No_Run_Time_Mode then
Error_Msg_CRT ("tagged types", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
elsif not RTE_Available (RE_Tag) then
@@ -4512,7 +4498,7 @@
Analyze_List (Result, Suppress => All_Checks);
Error_Msg_CRT ("tagged types", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
@@ -4523,14 +4509,14 @@
if RTE_Available (RE_Interface_Data) then
if Max_Predef_Prims /= 15 then
Error_Msg_N ("run-time library configuration error", Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
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;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end if;
end if;
@@ -6264,7 +6250,7 @@
Register_CG_Node (Typ);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
end Make_DT;
===================================================================
@@ -550,17 +550,10 @@
-- there is more than one element in the list.
procedure Analyze_Exception_Renaming (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Entity (N);
- Nam : constant Node_Id := Name (N);
+ Id : constant Entity_Id := Defining_Entity (N);
+ 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);
@@ -595,11 +588,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Exception_Renaming;
---------------------------
@@ -669,8 +657,7 @@
(N : Node_Id;
K : Entity_Kind)
is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- New_P : constant Entity_Id := Defining_Entity (N);
+ New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
Inst : Boolean := False;
@@ -681,11 +668,6 @@
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);
@@ -756,11 +738,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, New_P);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Generic_Renaming;
-----------------------------
@@ -867,10 +844,6 @@
return False;
end In_Generic_Scope;
- -- Local variables
-
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Analyze_Object_Renaming
begin
@@ -878,11 +851,6 @@
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));
@@ -1394,11 +1362,6 @@
-- Deal with dimensions
Analyze_Dimension (N);
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Object_Renaming;
------------------------------
@@ -1406,39 +1369,15 @@
------------------------------
procedure Analyze_Package_Renaming (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
-
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
- -- Local variables
-
New_P : constant Entity_Id := Defining_Entity (N);
Old_P : Entity_Id;
Spec : Node_Id;
- -- Start of processing for Analyze_Package_Renaming
-
begin
if Name (N) = Error then
return;
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));
@@ -1538,7 +1477,6 @@
-- subtypes again, so they are compatible with types in their class.
if not Is_Generic_Instance (Old_P) then
- Restore_Globals;
return;
else
Spec := Specification (Unit_Declaration_Node (Old_P));
@@ -1580,8 +1518,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, New_P);
end if;
-
- Restore_Globals;
end Analyze_Package_Renaming;
-------------------------------
@@ -2628,20 +2564,12 @@
-- defaulted formal subprogram when the actual for a related formal
-- type is class-wide.
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Inst_Node : Node_Id := Empty;
+ Inst_Node : Node_Id := Empty;
New_S : Entity_Id;
-- 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.
@@ -3559,11 +3487,6 @@
Analyze (N);
end if;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Subprogram_Renaming;
-------------------------
===================================================================
@@ -55,17 +55,10 @@
-----------------------------------
procedure Analyze_Exception_Declaration (N : Node_Id) is
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Id : constant Entity_Id := Defining_Identifier (N);
- PF : constant Boolean := Is_Pure (Current_Scope);
+ 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);
@@ -83,11 +76,6 @@
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Analyze_Exception_Declaration;
--------------------------------
===================================================================
@@ -7763,12 +7763,13 @@
function Build_Invariant_Procedure_Declaration
(Typ : Entity_Id) return Node_Id
is
- Loc : constant Source_Ptr := Sloc (Typ);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Loc : constant Source_Ptr := Sloc (Typ);
Decl : Node_Id;
Obj_Id : Entity_Id;
SId : Entity_Id;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
begin
-- Check for duplicate definitions
@@ -7776,9 +7777,8 @@
return Empty;
end if;
- -- The related type may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that the predicate functions are properly
- -- flagged as ignored Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the predicate functions are properly marked as Ghost.
Set_Ghost_Mode_From_Entity (Typ);
@@ -7810,11 +7810,8 @@
Defining_Identifier => Obj_Id,
Parameter_Type => New_Occurrence_Of (Typ, Loc)))));
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
+ Ghost_Mode := Save_Ghost_Mode;
- Ghost_Mode := GM;
-
return Decl;
end Build_Invariant_Procedure_Declaration;
@@ -8563,7 +8560,7 @@
-- Local variables
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-- Start of processing for Build_Predicate_Functions
@@ -8576,9 +8573,8 @@
return;
end if;
- -- The related type may be subject to pragma Ghost with policy Ignore.
- -- Set the mode now to ensure that the predicate functions are properly
- -- flagged as ignored Ghost.
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the predicate functions are properly marked as Ghost.
Set_Ghost_Mode_From_Entity (Typ);
@@ -8927,10 +8923,7 @@
end;
end if;
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
+ Ghost_Mode := Save_Ghost_Mode;
end Build_Predicate_Functions;
-----------------------------------------
===================================================================
@@ -4786,21 +4786,14 @@
-- Local declarations
- Def_Id : constant Entity_Id := Defining_Identifier (N);
- B_Id : constant Entity_Id := Base_Type (Def_Id);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Def_Id : constant Entity_Id := Defining_Identifier (N);
+ B_Id : constant Entity_Id := Base_Type (Def_Id);
FN : Node_Id;
Par_Id : Entity_Id;
-- Start of processing for Expand_N_Full_Type_Declaration
begin
- -- The type declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
if Is_Access_Type (Def_Id) then
Build_Master (Def_Id);
@@ -4924,11 +4917,6 @@
end if;
end;
end if;
-
- -- Restore the original Ghost mode once analysis and expansion have
- -- taken place.
-
- Ghost_Mode := GM;
end Expand_N_Full_Type_Declaration;
---------------------------------
@@ -4936,13 +4924,12 @@
---------------------------------
procedure Expand_N_Object_Declaration (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Def_Id : constant Entity_Id := Defining_Identifier (N);
- Expr : constant Node_Id := Expression (N);
- GM : constant Ghost_Mode_Type := Ghost_Mode;
- Obj_Def : constant Node_Id := Object_Definition (N);
- Typ : constant Entity_Id := Etype (Def_Id);
- Base_Typ : constant Entity_Id := Base_Type (Typ);
+ Loc : constant Source_Ptr := Sloc (N);
+ Def_Id : constant Entity_Id := Defining_Identifier (N);
+ Expr : constant Node_Id := Expression (N);
+ Obj_Def : constant Node_Id := Object_Definition (N);
+ Typ : constant Entity_Id := Etype (Def_Id);
+ Base_Typ : constant Entity_Id := Base_Type (Typ);
Expr_Q : Node_Id;
function Build_Equivalent_Aggregate return Boolean;
@@ -4954,9 +4941,6 @@
-- Generate all default initialization actions for object Def_Id. Any
-- new code is inserted after node After.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
function Rewrite_As_Renaming return Boolean;
-- Indicate whether to rewrite a declaration with initialization into an
-- object renaming declaration (see below).
@@ -5387,15 +5371,6 @@
end if;
end Default_Initialize_Object;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-------------------------
-- Rewrite_As_Renaming --
-------------------------
@@ -5439,12 +5414,6 @@
return;
end if;
- -- The object declaration may be subject to pragma Ghost with policy
- -- Ignore. Set the mode now to ensure that any nodes generated during
- -- expansion are properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- First we do special processing for objects of a tagged type where
-- this is the point at which the type is frozen. The creation of the
-- dispatch table and the initialization procedure have to be deferred
@@ -5613,7 +5582,6 @@
and then Is_Build_In_Place_Function_Call (Expr_Q)
then
Make_Build_In_Place_Call_In_Object_Declaration (N, Expr_Q);
- Restore_Globals;
-- The previous call expands the expression initializing the
-- built-in-place object into further code that will be analyzed
@@ -5858,7 +5826,6 @@
end;
end if;
- Restore_Globals;
return;
-- Common case of explicit object initialization
@@ -5974,7 +5941,6 @@
-- to avoid its management in the backend
Set_Expression (N, Empty);
- Restore_Globals;
return;
-- Handle initialization of limited tagged types
@@ -6196,13 +6162,10 @@
end;
end if;
- Restore_Globals;
-
-- Exception on library entity not available
exception
when RE_Not_Available =>
- Restore_Globals;
return;
end Expand_N_Object_Declaration;
@@ -7523,10 +7486,6 @@
-- 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 Process_RACW_Types (Typ : Entity_Id);
-- Validate and generate stubs for all RACW types associated with type
-- Typ.
@@ -7535,9 +7494,6 @@
-- Associate type Typ's Finalize_Address primitive with the finalization
-- masters of pending access-to-Typ types.
- procedure Restore_Globals;
- -- Restore the values of all saved global variables
-
------------------------
-- Process_RACW_Types --
------------------------
@@ -7618,26 +7574,19 @@
end if;
end Process_Pending_Access_Types;
- ---------------------
- -- Restore_Globals --
- ---------------------
-
- procedure Restore_Globals is
- begin
- Ghost_Mode := GM;
- end Restore_Globals;
-
-- Local variables
Def_Id : constant Entity_Id := Entity (N);
Result : Boolean := False;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
-- 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.
+ -- The type being frozen may be subject to pragma Ghost. Set the mode
+ -- now to ensure that any nodes generated during freezing are properly
+ -- marked as Ghost.
Set_Ghost_Mode (N, Def_Id);
@@ -7954,12 +7903,12 @@
Process_Pending_Access_Types (Def_Id);
Freeze_Stream_Operations (N, Def_Id);
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return Result;
exception
when RE_Not_Available =>
- Restore_Globals;
+ Ghost_Mode := Save_Ghost_Mode;
return False;
end Freeze_Type;