------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- G H O S T --
-- --
-- B o d y --
-- --
-- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
-- for more details. You should have received a copy of the GNU General --
-- Public License distributed with GNAT; see file COPYING3. If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
with Alloc; use Alloc;
with Aspects; use Aspects;
with Atree; use Atree;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Opt; use Opt;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Eval; use Sem_Eval;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Snames; use Snames;
with Table;
package body Ghost is
-- The following table contains the N_Compilation_Unit node for a unit that
-- is either subject to pragma Ghost with policy Ignore or contains ignored
-- Ghost code. The table is used in the removal of ignored Ghost code from
-- units.
package Ignored_Ghost_Units is new Table.Table (
Table_Component_Type => Node_Id,
Table_Index_Type => Int,
Table_Low_Bound => 0,
Table_Initial => Alloc.Ignored_Ghost_Units_Initial,
Table_Increment => Alloc.Ignored_Ghost_Units_Increment,
Table_Name => "Ignored_Ghost_Units");
-----------------------
-- Local Subprograms --
-----------------------
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
-- Subsidiary to Set_Ghost_Mode_xxx. Signal all enclosing scopes that they
-- now contain ignored Ghost code. Add the compilation unit containing N to
-- table Ignored_Ghost_Units for post processing.
----------------------------
-- Add_Ignored_Ghost_Unit --
----------------------------
procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is
begin
pragma Assert (Nkind (Unit) = N_Compilation_Unit);
-- Avoid duplicates in the table as pruning the same unit more than once
-- is wasteful. Since ignored Ghost code tends to be grouped up, check
-- the contents of the table in reverse.
for Index in reverse Ignored_Ghost_Units.First ..
Ignored_Ghost_Units.Last
loop
-- If the unit is already present in the table, do not add it again
if Unit = Ignored_Ghost_Units.Table (Index) then
return;
end if;
end loop;
-- If we get here, then this is the first time the unit is being added
Ignored_Ghost_Units.Append (Unit);
end Add_Ignored_Ghost_Unit;
----------------------------
-- Check_Ghost_Completion --
----------------------------
procedure Check_Ghost_Completion
(Partial_View : Entity_Id;
Full_View : Entity_Id)
is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Partial_View)
and then Policy = Name_Ignore
then
Error_Msg_Sloc := Sloc (Full_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Check", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
end if;
end Check_Ghost_Completion;
-------------------------
-- Check_Ghost_Context --
-------------------------
procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
-- Verify that the Ghost policy at the point of declaration of entity Id
-- matches the policy at the point of reference. If this is not the case
-- emit an error at Err_N.
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
-- Determine whether node Context denotes a Ghost-friendly context where
-- a Ghost entity can safely reside.
-------------------------
-- Is_OK_Ghost_Context --
-------------------------
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
-- Determine whether node Decl is a Ghost declaration or appears
-- within a Ghost declaration.
function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
-- Determine whether statement or pragma N is Ghost or appears within
-- a Ghost statement or pragma. To qualify as such, N must either
-- 1) Occur within a ghost subprogram or package
-- 2) Denote a call to a ghost procedure
-- 3) Denote an assignment statement whose target is a ghost
-- variable.
-- 4) Denote a pragma that mentions a ghost entity
--------------------------
-- Is_Ghost_Declaration --
--------------------------
function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
Par : Node_Id;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
begin
-- Climb the parent chain looking for an object declaration
Par := Decl;
while Present (Par) loop
if Is_Declaration (Par) then
-- A declaration is Ghost when it appears within a Ghost
-- package or subprogram.
if Ghost_Mode > None then
return True;
-- Otherwise the declaration may not have been analyzed yet,
-- determine whether it is subject to aspect/pragma Ghost.
else
return Is_Subject_To_Ghost (Par);
end if;
-- Special cases
-- A reference to a Ghost entity may appear as the default
-- expression of a formal parameter of a subprogram body. This
-- context must be treated as suitable because the relation
-- between the spec and the body has not been established and
-- the body is not marked as Ghost yet. The real check was
-- performed on the spec.
elsif Nkind (Par) = N_Parameter_Specification
and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
then
return True;
-- References to Ghost entities may be relocated in internally
-- generated bodies.
elsif Nkind (Par) = N_Subprogram_Body
and then not Comes_From_Source (Par)
then
Subp_Id := Corresponding_Spec (Par);
-- The original context is an expression function that has
-- been split into a spec and a body. The context is OK as
-- long as the the initial declaration is Ghost.
if Present (Subp_Id) then
Subp_Decl :=
Original_Node (Unit_Declaration_Node (Subp_Id));
if Nkind (Subp_Decl) = N_Expression_Function then
return Is_Subject_To_Ghost (Subp_Decl);
end if;
end if;
-- Otherwise this is either an internal body or an internal
-- completion. Both are OK because the real check was done
-- before expansion activities.
return True;
end if;
-- Prevent the search from going too far
if Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Par := Parent (Par);
end loop;
return False;
end Is_Ghost_Declaration;
----------------------------------
-- Is_Ghost_Statement_Or_Pragma --
----------------------------------
function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a reference to a
-- Ghost entity.
-------------------------------
-- Is_Ghost_Entity_Reference --
-------------------------------
function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
Ref : Node_Id;
begin
-- When the reference extracts a subcomponent, recover the
-- related object (SPARK RM 6.9(1)).
Ref := N;
while Nkind_In (Ref, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Ref := Prefix (Ref);
end loop;
return
Is_Entity_Name (Ref)
and then Present (Entity (Ref))
and then Is_Ghost_Entity (Entity (Ref));
end Is_Ghost_Entity_Reference;
-- Local variables
Arg : Node_Id;
Stmt : Node_Id;
-- Start of processing for Is_Ghost_Statement_Or_Pragma
begin
if Nkind (N) = N_Pragma then
-- A pragma is Ghost when it appears within a Ghost package or
-- subprogram.
if Ghost_Mode > None then
return True;
end if;
-- A pragma is Ghost when it mentions a Ghost entity
Arg := First (Pragma_Argument_Associations (N));
while Present (Arg) loop
if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
return True;
end if;
Next (Arg);
end loop;
end if;
Stmt := N;
while Present (Stmt) loop
if Is_Statement (Stmt) then
-- A statement is Ghost when it appears within a Ghost
-- package or subprogram.
if Ghost_Mode > None then
return True;
-- An assignment statement or a procedure call is Ghost when
-- the name denotes a Ghost entity.
elsif Nkind_In (Stmt, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
return Is_Ghost_Entity_Reference (Name (Stmt));
end if;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Stmt) then
return False;
end if;
Stmt := Parent (Stmt);
end loop;
return False;
end Is_Ghost_Statement_Or_Pragma;
-- Start of processing for Is_OK_Ghost_Context
begin
-- The Ghost entity appears within an assertion expression
if In_Assertion_Expr > 0 then
return True;
-- The Ghost entity is part of a declaration or its completion
elsif Is_Ghost_Declaration (Context) then
return True;
-- The Ghost entity is referenced within a Ghost statement
elsif Is_Ghost_Statement_Or_Pragma (Context) then
return True;
-- Routine Expand_Record_Extension creates a parent subtype without
-- inserting it into the tree. There is no good way of recognizing
-- this special case as there is no parent. Try to approximate the
-- context.
elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
return True;
else
return False;
end if;
end Is_OK_Ghost_Context;
------------------------
-- Check_Ghost_Policy --
------------------------
procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
-- The Ghost policy in effect a the point of declaration and at the
-- point of use must match (SPARK RM 6.9(14)).
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
end if;
end Check_Ghost_Policy;
-- Start of processing for Check_Ghost_Context
begin
-- Once it has been established that the reference to the Ghost entity
-- is within a suitable context, ensure that the policy at the point of
-- declaration and at the point of use match.
if Is_OK_Ghost_Context (Ghost_Ref) then
Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
-- Otherwise the Ghost entity appears in a non-Ghost context and affects
-- its behavior or value.
else
Error_Msg_N
("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
Ghost_Ref);
end if;
end Check_Ghost_Context;
----------------------------
-- Check_Ghost_Derivation --
----------------------------
procedure Check_Ghost_Derivation (Typ : Entity_Id) is
Parent_Typ : constant Entity_Id := Etype (Typ);
Iface : Entity_Id;
Iface_Elmt : Elmt_Id;
begin
-- Allow untagged derivations from predefined types such as Integer as
-- those are not Ghost by definition.
if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
null;
-- The parent type of a Ghost type extension must be Ghost
elsif not Is_Ghost_Entity (Parent_Typ) then
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
return;
end if;
-- All progenitors (if any) must be Ghost as well
if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
Iface_Elmt := First_Elmt (Interfaces (Typ));
while Present (Iface_Elmt) loop
Iface := Node (Iface_Elmt);
if not Is_Ghost_Entity (Iface) then
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
return;
end if;
Next_Elmt (Iface_Elmt);
end loop;
end if;
end Check_Ghost_Derivation;
--------------------------------
-- Implements_Ghost_Interface --
--------------------------------
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
Iface_Elmt : Elmt_Id;
begin
-- Traverse the list of interfaces looking for a Ghost interface
if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
Iface_Elmt := First_Elmt (Interfaces (Typ));
while Present (Iface_Elmt) loop
if Is_Ghost_Entity (Node (Iface_Elmt)) then
return True;
end if;
Next_Elmt (Iface_Elmt);
end loop;
end if;
return False;
end Implements_Ghost_Interface;
----------------
-- Initialize --
----------------
procedure Initialize is
begin
Ignored_Ghost_Units.Init;
end Initialize;
---------------------
-- Is_Ghost_Entity --
---------------------
function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
begin
return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
end Is_Ghost_Entity;
-------------------------
-- Is_Subject_To_Ghost --
-------------------------
function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
function Enables_Ghostness (Arg : Node_Id) return Boolean;
-- Determine whether aspect or pragma argument Arg enables "ghostness"
-----------------------
-- Enables_Ghostness --
-----------------------
function Enables_Ghostness (Arg : Node_Id) return Boolean is
Expr : Node_Id;
begin
Expr := Arg;
if Nkind (Expr) = N_Pragma_Argument_Association then
Expr := Get_Pragma_Arg (Expr);
end if;
-- Determine whether the expression of the aspect is static and
-- denotes True.
if Present (Expr) then
Preanalyze_And_Resolve (Expr);
return
Is_OK_Static_Expression (Expr)
and then Is_True (Expr_Value (Expr));
-- Otherwise Ghost defaults to True
else
return True;
end if;
end Enables_Ghostness;
-- Local variables
Id : constant Entity_Id := Defining_Entity (N);
Asp : Node_Id;
Decl : Node_Id;
Prev_Id : Entity_Id;
-- Start of processing for Is_Subject_To_Ghost
begin
-- The related entity of the declaration has not been analyzed yet, do
-- not inspect its attributes.
if Ekind (Id) = E_Void then
null;
elsif Is_Ghost_Entity (Id) then
return True;
-- The completion of a type or a constant is not fully analyzed when the
-- reference to the Ghost entity is resolved. Because the completion is
-- not marked as Ghost yet, inspect the partial view.
elsif Is_Record_Type (Id)
or else Ekind (Id) = E_Constant
or else (Nkind (N) = N_Object_Declaration
and then Constant_Present (N))
then
Prev_Id := Incomplete_Or_Partial_View (Id);
if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
return True;
end if;
end if;
-- Examine the aspect specifications (if any) looking for aspect Ghost
if Permits_Aspect_Specifications (N) then
Asp := First (Aspect_Specifications (N));
while Present (Asp) loop
if Chars (Identifier (Asp)) = Name_Ghost then
return Enables_Ghostness (Expression (Asp));
end if;
Next (Asp);
end loop;
end if;
Decl := Empty;
-- When the context is a [generic] package declaration, pragma Ghost
-- resides in the visible declarations.
if Nkind_In (N, N_Generic_Package_Declaration,
N_Package_Declaration)
then
Decl := First (Visible_Declarations (Specification (N)));
-- When the context is a package or a subprogram body, pragma Ghost
-- resides in the declarative part.
elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
Decl := First (Declarations (N));
-- Otherwise pragma Ghost appears in the declarations following N
elsif Is_List_Member (N) then
Decl := Next (N);
end if;
while Present (Decl) loop
if Nkind (Decl) = N_Pragma
and then Pragma_Name (Decl) = Name_Ghost
then
return
Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
-- A source construct ends the region where pragma Ghost may appear,
-- stop the traversal.
elsif Comes_From_Source (Decl) then
exit;
end if;
Next (Decl);
end loop;
return False;
end Is_Subject_To_Ghost;
----------
-- Lock --
----------
procedure Lock is
begin
Ignored_Ghost_Units.Locked := True;
Ignored_Ghost_Units.Release;
end Lock;
----------------------------------
-- Propagate_Ignored_Ghost_Code --
----------------------------------
procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is
Nod : Node_Id;
Scop : Entity_Id;
begin
-- Traverse the parent chain looking for blocks, packages and
-- subprograms or their respective bodies.
Nod := Parent (N);
while Present (Nod) loop
Scop := Empty;
if Nkind (Nod) = N_Block_Statement then
Scop := Entity (Identifier (Nod));
elsif Nkind_In (Nod, N_Package_Body,
N_Package_Declaration,
N_Subprogram_Body,
N_Subprogram_Declaration)
then
Scop := Defining_Entity (Nod);
end if;
-- The current node denotes a scoping construct
if Present (Scop) then
-- Stop the traversal when the scope already contains ignored
-- Ghost code as all enclosing scopes have already been marked.
if Contains_Ignored_Ghost_Code (Scop) then
exit;
-- Otherwise mark this scope and keep climbing
else
Set_Contains_Ignored_Ghost_Code (Scop);
end if;
end if;
Nod := Parent (Nod);
end loop;
-- The unit containing the ignored Ghost code must be post processed
-- before invoking the back end.
Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N)));
end Propagate_Ignored_Ghost_Code;
-------------------------------
-- Remove_Ignored_Ghost_Code --
-------------------------------
procedure Remove_Ignored_Ghost_Code is
procedure Prune_Tree (Root : Node_Id);
-- Remove all code marked as ignored Ghost from the tree of denoted by
-- Root.
----------------
-- Prune_Tree --
----------------
procedure Prune_Tree (Root : Node_Id) is
procedure Prune (N : Node_Id);
-- Remove a given node from the tree by rewriting it into null
function Prune_Node (N : Node_Id) return Traverse_Result;
-- Determine whether node N denotes an ignored Ghost construct. If
-- this is the case, rewrite N as a null statement. See the body for
-- special cases.
-----------
-- Prune --
-----------
procedure Prune (N : Node_Id) is
begin
-- Destroy any aspects that may be associated with the node
if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
Remove_Aspects (N);
end if;
Rewrite (N, Make_Null_Statement (Sloc (N)));
end Prune;
----------------
-- Prune_Node --
----------------
function Prune_Node (N : Node_Id) return Traverse_Result is
Id : Entity_Id;
begin
-- The node is either declared as ignored Ghost or is a byproduct
-- of expansion. Destroy it and stop the traversal on this branch.
if Is_Ignored_Ghost_Node (N) then
Prune (N);
return Skip;
-- Scoping constructs such as blocks, packages, subprograms and
-- bodies offer some flexibility with respect to pruning.
elsif Nkind_In (N, N_Block_Statement,
N_Package_Body,
N_Package_Declaration,
N_Subprogram_Body,
N_Subprogram_Declaration)
then
if Nkind (N) = N_Block_Statement then
Id := Entity (Identifier (N));
else
Id := Defining_Entity (N);
end if;
-- The scoping construct contains both living and ignored Ghost
-- code, let the traversal prune all relevant nodes.
if Contains_Ignored_Ghost_Code (Id) then
return OK;
-- Otherwise the construct contains only living code and should
-- not be pruned.
else
return Skip;
end if;
-- Otherwise keep searching for ignored Ghost nodes
else
return OK;
end if;
end Prune_Node;
procedure Prune_Nodes is new Traverse_Proc (Prune_Node);
-- Start of processing for Prune_Tree
begin
Prune_Nodes (Root);
end Prune_Tree;
-- Start of processing for Remove_Ignored_Ghost_Code
begin
for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
end loop;
end Remove_Ignored_Ghost_Code;
--------------------
-- Set_Ghost_Mode --
--------------------
procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
-- Set the value of global variable Ghost_Mode depending on the mode of
-- entity Id.
procedure Set_Ghost_Mode_From_Policy;
-- Set the value of global variable Ghost_Mode depending on the current
-- Ghost policy in effect.
--------------------------------
-- Set_Ghost_Mode_From_Entity --
--------------------------------
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
begin
if Is_Checked_Ghost_Entity (Id) then
Ghost_Mode := Check;
elsif Is_Ignored_Ghost_Entity (Id) then
Ghost_Mode := Ignore;
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_From_Entity;
--------------------------------
-- Set_Ghost_Mode_From_Policy --
--------------------------------
procedure Set_Ghost_Mode_From_Policy is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
if Policy = Name_Check then
Ghost_Mode := Check;
elsif Policy = Name_Ignore then
Ghost_Mode := Ignore;
Set_Is_Ignored_Ghost_Node (N);
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_From_Policy;
-- Local variables
Nam : Node_Id;
-- Start of processing for Set_Ghost_Mode
begin
-- The input node denotes one of the many declaration kinds that may be
-- subject to pragma Ghost.
if Is_Declaration (N) then
if Is_Subject_To_Ghost (N) then
Set_Ghost_Mode_From_Policy;
-- The declaration denotes the completion of a deferred constant,
-- pragma Ghost appears on the partial declaration.
elsif Nkind (N) = N_Object_Declaration
and then Constant_Present (N)
and then Present (Prev_Id)
then
Set_Ghost_Mode_From_Entity (Prev_Id);
-- The declaration denotes the full view of a private type, pragma
-- Ghost appears on the partial declaration.
elsif Nkind (N) = N_Full_Type_Declaration
and then Is_Private_Type (Defining_Entity (N))
and then Present (Prev_Id)
then
Set_Ghost_Mode_From_Entity (Prev_Id);
end if;
-- The input denotes an assignment or a procedure call. In this case
-- the Ghost mode is dictated by the name of the construct.
elsif Nkind_In (N, N_Assignment_Statement,
N_Procedure_Call_Statement)
then
-- When the reference extracts a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
Nam := Name (N);
while Nkind_In (Nam, N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
loop
Nam := Prefix (Nam);
end loop;
if Is_Entity_Name (Nam)
and then Present (Entity (Nam))
then
Set_Ghost_Mode_From_Entity (Entity (Nam));
end if;
-- The input denotes a package or subprogram body
elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id))
or else Is_Subject_To_Ghost (N)
then
Set_Ghost_Mode_From_Policy;
end if;
end if;
end Set_Ghost_Mode;
-------------------------------
-- Set_Ghost_Mode_For_Freeze --
-------------------------------
procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is
begin
if Is_Checked_Ghost_Entity (Id) then
Ghost_Mode := Check;
elsif Is_Ignored_Ghost_Entity (Id) then
Ghost_Mode := Ignore;
Propagate_Ignored_Ghost_Code (N);
end if;
end Set_Ghost_Mode_For_Freeze;
-------------------------
-- Set_Is_Ghost_Entity --
-------------------------
procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
if Policy = Name_Check then
Set_Is_Checked_Ghost_Entity (Id);
elsif Policy = Name_Ignore then
Set_Is_Ignored_Ghost_Entity (Id);
end if;
end Set_Is_Ghost_Entity;
end Ghost;