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