Google Git
Sign in
gnu / gcc.git / refs/heads/trunk / . / gcc / ada / ghost.adb
blob: 74aeae50fe5fd18ec7ce993038f033010ca9f34b [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- G H O S T --
-- --
-- B o d y --
-- --
-- Copyright (C) 2014-2026, 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;
with Aspects; use Aspects;
with Atree; use Atree;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
with Elists; use Elists;
with Errout; use Errout;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
with Snames; use Snames;
with Stand; use Stand;
with Table;
package body Ghost is
---------------------
-- Data strictures --
---------------------
-- The following table contains all ignored Ghost nodes that must be
-- eliminated from the tree by routine Remove_Ignored_Ghost_Code.
package Ignored_Ghost_Nodes is new Table.Table (
Table_Component_Type => Node_Id,
Table_Index_Type => Int,
Table_Low_Bound => 0,
Table_Initial => Alloc.Ignored_Ghost_Nodes_Initial,
Table_Increment => Alloc.Ignored_Ghost_Nodes_Increment,
Table_Name => "Ignored_Ghost_Nodes");
---------------------
-- Local variables --
---------------------
Assertion_Level_Error_Msg : constant String :=
"incompatible assertion levels in effect";
Ghost_Policy_Error_Msg : constant String :=
"incompatible ghost policies in effect";
-----------------------
-- Local subprograms --
-----------------------
function Assertion_Level_To_Name (Level : Entity_Id) return Name_Id;
-- Returns No_Name if there is no Level or the name of the Level.
procedure Check_Valid_Ghost_Declaration (N : Node_Id);
-- Check that the declaration for a Ghost node N has a valid
-- Assertion_Policy and a valid Assertion_Level.
function Get_Ghost_Aspect (N : Node_Id) return Node_Id;
-- Returns the Ghost aspect for a given node if it has one.
function Get_Ghost_Pragma (N : Node_Id) return Node_Id;
-- Return the Ghost pragma following this node.
function Get_Ghost_Assertion_Level (N : Node_Id) return Entity_Id;
-- Returns the Assertion_Level entity if the node has a Ghost aspect and
-- the Ghost aspect is using an Assertion_Level.
function Ghost_Assertion_Level_In_Effect (Id : Entity_Id) return Entity_Id;
-- Returns the ghost level applicable for the given entity Id in a similar
-- manner as Ghost_Policy_In_Effect.
function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id;
-- Returns the ghost policy applicable for the given entity Id.
--
-- SPARK RM 6.9 (3):
--
-- An object declaration which occurs inside an expression in a ghost
-- declaration, statement, assertion pragma or specification aspect
-- declaration is a ghost declaration.
--
-- If this declaration does not have the Ghost aspect specified, the
-- assertion policy applicable to this declaration comes from the policy
-- applicable to the enclosing declaration, statement, assertion pragma
-- or specification aspect.
--
-- If the declaration occurs inside a ghost declaration, ghost statement,
-- assertion pragma or specification aspect and the assertion policy
-- applicable to this scope is Ignore, then the assertion policy applicable
-- to the declaration is also Ignore.
--
-- Otherwise, the assertion policy applicable to an object declaration
-- comes either from its assertion level if any, or from the ghost
-- policy at the point of declaration.
procedure Install_Ghost_Region
(Mode : Name_Id; N : Node_Id; Level : Entity_Id);
pragma Inline (Install_Ghost_Region);
-- Install a Ghost region comprised of mode Mode and ignored region start
-- node N and Level as the Assertion_Level that was associated with it.
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
-- 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_And_Set_Ghost_Region (N : Node_Id; Id : Entity_Id);
-- Install a new ghost region for N based on the active policy applied for
-- Id. Additionally if the policy is ignored mark and set the node as an
-- ignored ghost region.
procedure Mark_Ghost_Declaration_Or_Body
(N : Node_Id;
Mode : Name_Id;
Level : Entity_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. Additionally set level as the Ghost_Assertion_Level for all of
-- them.
procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id);
-- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for
-- later elimination.
------------------------------
-- Assertion_Level_From_Arg --
------------------------------
function Assertion_Level_From_Arg (Arg : Node_Id) return Entity_Id is
Expr : constant Node_Id := Get_Pragma_Arg (Arg);
Level : Entity_Id;
begin
-- Aspect Ghost without an expression uses Standard_Level_Default
if No (Expr) then
return Standard_Level_Default;
end if;
-- Check if the expression matches a static boolean expression first
Preanalyze_And_Resolve_Without_Errors (Expr);
if Is_OK_Static_Expression (Expr) then
if Is_True (Expr_Value (Expr)) then
return Standard_Level_Default;
else
-- Ghost => False is considered to be non-ghost
return Empty;
end if;
end if;
-- Alternatively the argument could be an Assertion_Level
if Nkind (Expr) = N_Identifier then
Level := Get_Assertion_Level (Chars (Expr));
if Present (Level) then
-- The identifier resolved to an assertion level. Override the
-- Any_Id from a failed resolution in pre-analysis.
Set_Entity (Expr, Level);
return Level;
end if;
end if;
-- We are dealing with a malformed ghost argument.
-- An error will be emitted when the pragma is analyzed.
return Empty;
end Assertion_Level_From_Arg;
-----------------------------
-- Assertion_Level_To_Name --
-----------------------------
function Assertion_Level_To_Name (Level : Entity_Id) return Name_Id is
begin
if No (Level) then
return No_Name;
end if;
return Chars (Level);
end Assertion_Level_To_Name;
----------------------------
-- Check_Ghost_Completion --
----------------------------
procedure Check_Ghost_Completion
(Prev_Id : Entity_Id;
Compl_Id : Entity_Id)
is
Policy : Name_Id;
begin
-- Nothing to do if one of the views is missing
if No (Prev_Id) or else No (Compl_Id) then
return;
end if;
Policy := Ghost_Policy_In_Effect (Prev_Id);
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(19)).
if Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
then
Error_Msg_N (Ghost_Policy_Error_Msg, Prev_Id);
Error_Msg_Sloc := Sloc (Prev_Id);
Error_Msg_N ("\& declared # with ghost policy `Check`", Prev_Id);
Error_Msg_Sloc := Sloc (Compl_Id);
Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id);
elsif Is_Ignored_Ghost_Entity (Prev_Id)
and then Policy = Name_Check
then
Error_Msg_N (Ghost_Policy_Error_Msg, Prev_Id);
Error_Msg_Sloc := Sloc (Prev_Id);
Error_Msg_N ("\& declared # with ghost policy `Ignore`", Prev_Id);
Error_Msg_Sloc := Sloc (Compl_Id);
Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id);
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; Ref : Node_Id);
-- Verify that the Ghost policy at the point of declaration of entity Id
-- matches the policy at the point of reference Ref. If this is not the
-- case emit an error at Ref.
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 (SPARK RM 6.9(13)).
function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean;
-- Return True iff N is enclosed in an aspect or pragma Predicate
-------------------------
-- Is_OK_Ghost_Context --
-------------------------
function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
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
--
-- * 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 ghost
-- reference. To qualify as such, Prag must either
--
-- * 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; Id : Entity_Id; Call_Arg : 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
--
-- * Denote a procedure call to a Ghost procedure
--
-- * Denote an assignment statement whose target is Ghost
-----------------------
-- Is_OK_Declaration --
-----------------------
function Is_OK_Declaration (Decl : Node_Id) return Boolean is
function In_Subprogram_Body_Profile (N : Node_Id) return Boolean;
-- Determine whether node N appears in the profile of a subprogram
-- body.
--------------------------------
-- In_Subprogram_Body_Profile --
--------------------------------
function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is
Spec : constant Node_Id := Parent (N);
begin
-- The node appears in a parameter specification in which case
-- it is either the parameter type or the default expression or
-- the node appears as the result definition of a function.
return
(Nkind (N) = N_Parameter_Specification
or else
(Nkind (Spec) = N_Function_Specification
and then N = Result_Definition (Spec)))
and then Nkind (Parent (Spec)) = N_Subprogram_Body;
end In_Subprogram_Body_Profile;
-- Local variables
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
-- Start of processing for Is_OK_Declaration
begin
if Is_Ghost_Declaration (Decl) then
return True;
-- Special cases
-- A reference to a Ghost entity may appear within the profile of
-- a subprogram body. This context is treated as suitable because
-- it duplicates the context of the corresponding spec. The real
-- check was already performed during the analysis of the spec.
elsif In_Subprogram_Body_Profile (Decl) then
return True;
-- A reference to a Ghost entity may appear within an expression
-- function which is still being analyzed. This context is treated
-- as suitable because it is not yet known whether the expression
-- function is an initial declaration or a completion. The real
-- check is performed when the expression function is expanded.
elsif Nkind (Decl) = N_Expression_Function
and then not Analyzed (Decl)
then
return True;
-- A reference to a Ghost entity may appear within the class-wide
-- precondition of a helper subprogram. This context is treated
-- as suitable because it was already verified when we were
-- analyzing the original class-wide precondition.
elsif Is_Subprogram (Current_Scope)
and then Present (Class_Preconditions_Subprogram (Current_Scope))
then
return True;
-- References to Ghost entities may be relocated in internally
-- generated bodies.
elsif Nkind (Decl) = N_Subprogram_Body
and then not Comes_From_Source (Decl)
then
Subp_Id := Corresponding_Spec (Decl);
if Present (Subp_Id) then
-- The context is the internally built _Wrapped_Statements
-- procedure, which is OK because the real check was done
-- before contract expansion activities.
if Chars (Subp_Id) = Name_uWrapped_Statements then
return True;
-- The context is the internally built predicate function,
-- which is OK because the real check was done before the
-- predicate function was generated.
elsif Is_Predicate_Function (Subp_Id) then
return True;
else
Subp_Decl :=
Original_Node (Unit_Declaration_Node (Subp_Id));
-- 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 initial declaration is Ghost.
if Nkind (Subp_Decl) = N_Expression_Function then
return Is_Ghost_Declaration (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.
else
return True;
end if;
end if;
return False;
end Is_OK_Declaration;
------------------
-- Is_OK_Pragma --
------------------
function Is_OK_Pragma (Prag : Node_Id) return Boolean
is
Prag_Id : Pragma_Id;
Prag_Nam : Name_Id;
begin
if Nkind (Prag) /= N_Pragma then
return False;
end if;
-- if the entitiy associated with the pragma is ignored then we do
-- not need to analyze the pragma.
if Is_Ignored_Ghost_Pragma (Prag) then
return True;
end if;
Prag_Id := Get_Pragma_Id (Prag);
Prag_Nam := Original_Aspect_Pragma_Name (Prag);
-- A pragma may not be analyzed, so that its Ghost status is
-- not determined yet, but it is guaranteed to be Ghost when
-- referencing a Ghost entity.
if Suppressed_Ghost_Policy_Check_Pragma (Prag_Id) then
return True;
-- An assertion expression pragma is Ghost when it contains a
-- reference to a Ghost entity (SPARK RM 6.9(13)), except for
-- predicate pragmas (SPARK RM 6.9(14)).
elsif Is_Valid_Assertion_Kind (Prag_Nam)
and then Assertion_Expression_Pragma (Prag_Id)
and then Prag_Id /= Pragma_Predicate
then
return True;
-- A pragma that applies to a Ghost construct or specifies an
-- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(4))
elsif Is_Ghost_Pragma (Prag) then
return True;
-- Several pragmas that may apply to a non-Ghost entity are
-- treated as Ghost when they contain a reference to a Ghost
-- entity (SPARK RM 6.9(18)).
elsif Prag_Nam
in Name_Global
| Name_Depends
| Name_Initializes
| Name_Refined_Global
| Name_Refined_Depends
| Name_Refined_State
then
return True;
end if;
return False;
end Is_OK_Pragma;
---------------------
-- Is_OK_Statement --
---------------------
function Is_OK_Statement
(Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean
is
procedure Check_Assignment_Levels (Assignee : Entity_Id);
-- Check that a ghost entity on the RHS of the assignment is
-- assertion level dependent on the LHS.
procedure Check_Procedure_Call_Policies (Callee : Entity_Id);
-- Check that
-- * the a checked call argument is not modified by an ignored
-- procedure call.
-- * the level of the modified call argument depends on the level
-- of the call.
function Is_Modified_By_Call
(Call : Node_Id; Call_Arg : Node_Id; Callee : Entity_Id)
return Boolean;
-- Check that Call_Arg was used in the call and that the formal
-- for that argument was either out or in-out.
-----------------------------
-- Check_Assignment_Levels --
-----------------------------
procedure Check_Assignment_Levels (Assignee : Entity_Id) is
Assignee_Level : constant Entity_Id :=
Ghost_Assertion_Level (Assignee);
Id_Level : constant Entity_Id :=
Ghost_Assertion_Level (Id);
begin
-- SPARK RM 6.9 (13) A ghost entity E shall only be referenced
-- within an assignment statement whose target is a ghost
-- variable that is assertion-level-dependent on E.
if not Is_Assertion_Level_Dependent (Assignee_Level, Id_Level)
then
Error_Msg_N (Assertion_Level_Error_Msg, Ghost_Ref);
Error_Msg_Name_1 := Chars (Id_Level);
Error_Msg_N ("\& has assertion level %", Ghost_Ref);
Error_Msg_Name_1 := Chars (Assignee_Level);
Error_Msg_Node_2 := Assignee;
Error_Msg_NE ("\& is modifying & with %", Ghost_Ref, Id);
Error_Msg_Name_1 := Chars (Id_Level);
Error_Msg_NE
("\assertion level of & should depend on %",
Ghost_Ref,
Assignee);
end if;
end Check_Assignment_Levels;
-----------------------------------
-- Check_Procedure_Call_Policies --
-----------------------------------
procedure Check_Procedure_Call_Policies (Callee : Entity_Id) is
Id_Level : constant Entity_Id := Ghost_Assertion_Level (Id);
Id_Policy : constant Name_Id := Ghost_Policy_In_Effect (Id);
Call_Level : Entity_Id;
Call_Policy : Name_Id;
begin
if No (Callee) then
return;
end if;
-- Checks apply only if we are processing a call argument that
-- is modified by the call.
if No (Call_Arg)
or else not Is_Modified_By_Call (Stmt, Call_Arg, Callee)
then
return;
end if;
Call_Policy := Ghost_Policy_In_Effect (Callee);
Call_Level := Ghost_Assertion_Level (Callee);
if Id_Policy = Name_Check
and then Call_Policy = Name_Ignore
then
Error_Msg_Sloc := Sloc (Ghost_Ref);
Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref);
Error_Msg_NE ("\& has ghost policy `Check`", Ghost_Ref, Id);
Error_Msg_NE
("\& is modified # by a procedure with `Ignore`",
Ghost_Ref,
Id);
end if;
-- An out or in out mode actual parameter and the subprogram
-- shall have matching assertion levels SPARK RM 6.9 (15).
if Id_Level /= Call_Level then
Error_Msg_N (Assertion_Level_Error_Msg, Ghost_Ref);
Error_Msg_Name_1 := Chars (Id_Level);
Error_Msg_N ("\& has assertion level %", Ghost_Ref);
Error_Msg_Name_1 := Chars (Call_Level);
Error_Msg_Node_2 := Callee;
Error_Msg_N
("\& is modified by & with %", Ghost_Ref);
Error_Msg_N
("\the levels of the call and call arguments must match",
Ghost_Ref);
end if;
end Check_Procedure_Call_Policies;
-------------------------
-- Is_Modified_By_Call --
-------------------------
function Is_Modified_By_Call
(Call : Node_Id; Call_Arg : Node_Id; Callee : Entity_Id)
return Boolean
is
Form : Node_Id;
Act : Node_Id;
begin
Act := First_Actual (Call);
Form := First_Formal (Callee);
while Present (Form) and then Present (Act) loop
if Act = Call_Arg then
return
Ekind (Form) in E_Out_Parameter | E_In_Out_Parameter;
end if;
Next_Formal (Form);
Next_Actual (Act);
end loop;
return False;
end Is_Modified_By_Call;
-- Start of processing for Is_OK_Statement
begin
-- An assignment statement is Ghost when the target is a Ghost
-- entity.
if Nkind (Stmt) = N_Assignment_Statement then
if Is_Ghost_Assignment (Stmt) then
Check_Assignment_Levels
(Get_Enclosing_Ghost_Entity (Name (Stmt)));
return True;
end if;
-- A procedure call is Ghost when it calls a Ghost procedure
elsif Nkind (Stmt) = N_Procedure_Call_Statement then
if Is_Ghost_Procedure_Call (Stmt) then
Check_Procedure_Call_Policies (Get_Subprogram_Entity (Stmt));
return True;
end if;
-- Special cases
-- An if statement is a suitable context for a Ghost entity if it
-- is the byproduct of assertion expression expansion. Note that
-- the assertion expression may not be related to a Ghost entity,
-- but it may still contain references to Ghost entities.
elsif Nkind (Stmt) = N_If_Statement
and then Comes_From_Check_Or_Contract (Stmt)
then
return True;
end if;
return False;
end Is_OK_Statement;
-- Local variables
Par : Node_Id;
Prev : Node_Id;
-- Start of processing for Is_OK_Ghost_Context
begin
-- 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.
if No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
return True;
-- Otherwise climb the parent chain looking for a suitable Ghost
-- context.
else
Par := Context;
Prev := Empty;
while Present (Par) loop
-- It is not possible to check correct use of Ghost entities
-- in generic instantiations until after the generic has been
-- resolved. Postpone that verification to after resolution.
if Nkind (Par) = N_Generic_Association then
return True;
-- A reference to a Ghost entity can appear within an aspect
-- specification (SPARK RM 6.9(13)). The precise checking will
-- occur when analyzing the corresponding pragma. We make an
-- exception for predicate aspects other than Ghost_Predicate
-- that only allow referencing a Ghost entity when the
-- corresponding type declaration is Ghost (SPARK RM 6.9(14)).
elsif Nkind (Par) = N_Aspect_Specification
and then
(Get_Aspect_Id (Par) = Aspect_Ghost_Predicate
or else not Same_Aspect
(Get_Aspect_Id (Par), Aspect_Predicate))
then
return True;
-- A Ghost type may be referenced in a use or use_type clause
-- (SPARK RM 6.9(13)).
elsif Present (Parent (Par))
and then Nkind (Parent (Par)) in N_Use_Package_Clause
| N_Use_Type_Clause
then
return True;
-- The context is an attribute definition clause for a Ghost
-- entity.
elsif Nkind (Parent (Par)) = N_Attribute_Definition_Clause
and then Par = Name (Parent (Par))
then
return True;
-- The context is the instantiation or renaming of a Ghost
-- entity.
elsif Nkind (Parent (Par)) in N_Generic_Instantiation
| N_Renaming_Declaration
| N_Generic_Renaming_Declaration
and then Par = Name (Parent (Par))
then
return True;
-- In the case of the renaming of a ghost object, the type
-- itself may be ghost.
elsif Nkind (Parent (Par)) = N_Object_Renaming_Declaration
and then (Par = Subtype_Mark (Parent (Par))
or else Par = Access_Definition (Parent (Par)))
then
return True;
-- It is always legal to use a ghost prefix. More complex
-- scenarios are analyzed for the selector.
elsif Nkind (Par) = N_Selected_Component
and then Prefix (Par) = Prev
then
return True;
elsif Is_OK_Declaration (Par) then
return True;
elsif Is_OK_Pragma (Par) then
return True;
elsif Is_OK_Statement (Par, Ghost_Id, Prev) then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Prev := Par;
Par := Parent (Par);
end loop;
-- The expansion of assertion expression pragmas and attribute Old
-- may cause a legal Ghost entity reference to become illegal due
-- to node relocation. Check the In_Assertion_Expr counter as last
-- resort to try and infer the original legal context.
if In_Assertion_Expr > 0 then
return True;
-- Otherwise the context is not suitable for a reference to a
-- Ghost entity.
else
return False;
end if;
end if;
end Is_OK_Ghost_Context;
------------------------
-- Check_Ghost_Policy --
------------------------
procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is
function Is_From_Aspect_Iterable (Ref : Node_Id) return Boolean;
-- Returns true when the node is contained within an Iterable aspect.
function Is_From_Aspect_Iterable (Ref : Node_Id) return Boolean is
P : Node_Id := Parent (Ref);
begin
while Present (P) loop
if Nkind (P) = N_Aspect_Specification then
return Get_Aspect_Id (P) = Aspect_Iterable;
end if;
P := Parent (P);
end loop;
return False;
end Is_From_Aspect_Iterable;
-- Local variables
Applic_Policy : Ghost_Mode_Type := Ghost_Config.Ghost_Mode;
Ghost_Region : constant Node_Id := Ghost_Config.Current_Region;
-- Start of processing for Check_Ghost_Policy
begin
-- The policy is allowed to change within renaming and instantiation
-- statements.
if No (Ghost_Region)
or else Nkind (Ghost_Region)
in N_Object_Renaming_Declaration
| N_Package_Instantiation
| N_Procedure_Instantiation
| N_Subprogram_Renaming_Declaration
then
return;
end if;
-- The applied policy for procedure calls is the policy in effect at
-- the moment of the call.
if Ekind (Id) in E_Procedure then
Applic_Policy := Name_To_Ghost_Mode (Ghost_Policy_In_Effect (Id));
end if;
-- The Ghost policy in effect a the point of declaration and at the
-- point of use must match (SPARK RM 6.9(18)).
if Is_Checked_Ghost_Entity (Id)
and then Applic_Policy = Ignore
and then Known_To_Be_Assigned (Ref)
then
Error_Msg_N (Ghost_Policy_Error_Msg, Ref);
Error_Msg_Sloc := Sloc (Id);
Error_Msg_NE ("\& declared # with ghost policy `Check`", Ref, Id);
Error_Msg_Sloc := Sloc (Ref);
Error_Msg_NE ("\& used # with ghost policy `Ignore`", Ref, Id);
end if;
-- A ghost entity E shall not be referenced within an aspect
-- specification [(including an aspect-specifying pragma)] which
-- specifies an aspect of an entity that is either non-ghost or not
-- assertion-level-dependent on E except in the following cases the
-- specified aspect is either Global, Depends, Refined_Global,
-- Refined_Depends, Initializes, Refined_State, or Iterable (SPARK RM
-- 6.9(14)).
if No (Ghost_Region)
or else (Nkind (Ghost_Region) = N_Pragma
and then Get_Pragma_Id (Ghost_Region)
in Pragma_Global
| Pragma_Depends
| Pragma_Refined_Global
| Pragma_Refined_Depends
| Pragma_Initializes
| Pragma_Refined_State)
or else Is_From_Aspect_Iterable (Ref)
then
return;
end if;
if Is_Ignored_Ghost_Entity (Id) and then Applic_Policy = Check then
Error_Msg_N (Ghost_Policy_Error_Msg, Ref);
Error_Msg_Sloc := Sloc (Id);
Error_Msg_NE ("\& declared # with ghost policy `Ignore`", Ref, Id);
Error_Msg_Sloc := Sloc (Ref);
Error_Msg_NE ("\& used # with ghost policy `Check`", Ref, Id);
end if;
end Check_Ghost_Policy;
-----------------------------------
-- In_Aspect_Or_Pragma_Predicate --
-----------------------------------
function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean is
Par : Node_Id := N;
begin
while Present (Par) loop
if Nkind (Par) = N_Pragma
and then Get_Pragma_Id (Par) = Pragma_Predicate
then
return True;
elsif Nkind (Par) = N_Aspect_Specification
and then Same_Aspect (Get_Aspect_Id (Par), Aspect_Predicate)
then
return True;
-- Stop the search when it's clear it cannot be inside an aspect
-- or pragma.
elsif Is_Declaration (Par)
or else Is_Statement (Par)
or else Is_Body (Par)
then
return False;
end if;
Par := Parent (Par);
end loop;
return False;
end In_Aspect_Or_Pragma_Predicate;
-- Start of processing for Check_Ghost_Context
begin
if Ghost_Context_Checks_Disabled then
return;
end if;
-- Class-wide pre/postconditions of ignored pragmas are preanalyzed
-- to report errors on wrong conditions; however, ignored pragmas may
-- also have references to ghost entities and we must disable checking
-- their context to avoid reporting spurious errors.
if Inside_Class_Condition_Preanalysis then
return;
end if;
-- When assertions are enabled, compiler generates code for ghost
-- entities, that is not subject to Ghost policy.
if not Comes_From_Source (Ghost_Ref) then
return;
end if;
-- If the Ghost entity appears in a non-Ghost context and affects
-- its behavior or value (SPARK RM 6.9(13,14)).
if not Is_OK_Ghost_Context (Ghost_Ref) then
Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
-- When the Ghost entity appears in a pragma Predicate, explain the
-- reason for this being illegal, and suggest a fix instead.
if In_Aspect_Or_Pragma_Predicate (Ghost_Ref) then
Error_Msg_N
("\as predicates are checked in membership tests, "
& "the type and its predicate must be both ghost",
Ghost_Ref);
Error_Msg_N
("\either make the type ghost "
& "or use a Ghost_Predicate "
& "or use a type invariant on a private type", Ghost_Ref);
end if;
end if;
-- 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 Present (Ghost_Id) then
Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
end if;
end Check_Ghost_Context;
------------------------------------------------
-- Check_Ghost_Context_In_Generic_Association --
------------------------------------------------
procedure Check_Ghost_Context_In_Generic_Association
(Actual : Node_Id;
Formal : Entity_Id)
is
function Emit_Error_On_Ghost_Reference
(N : Node_Id)
return Traverse_Result;
-- Determine wether N denotes a reference to a ghost entity, and if so
-- issue an error.
-----------------------------------
-- Emit_Error_On_Ghost_Reference --
-----------------------------------
function Emit_Error_On_Ghost_Reference
(N : Node_Id)
return Traverse_Result
is
begin
if Is_Entity_Name (N)
and then Present (Entity (N))
and then Is_Ghost_Entity (Entity (N))
then
Error_Msg_N ("ghost entity cannot appear in this context", N);
Error_Msg_Sloc := Sloc (Formal);
Error_Msg_NE ("\formal & was not declared as ghost #", N, Formal);
return Abandon;
end if;
return OK;
end Emit_Error_On_Ghost_Reference;
procedure Check_Ghost_References is
new Traverse_Proc (Emit_Error_On_Ghost_Reference);
-- Start of processing for Check_Ghost_Context_In_Generic_Association
begin
-- The context is ghost when it appears within a Ghost package or
-- subprogram.
if Ghost_Config.Ghost_Mode > None then
return;
-- The context is ghost if Formal is explicitly marked as ghost
elsif Is_Ghost_Entity (Formal) then
return;
else
Check_Ghost_References (Actual);
end if;
end Check_Ghost_Context_In_Generic_Association;
-----------------------------------
-- Check_Valid_Ghost_Declaration --
-----------------------------------
procedure Check_Valid_Ghost_Declaration (N : Node_Id) is
procedure Check_Valid_Assertion_Level (Id : Entity_Id; Ref : Node_Id);
-- Check that the the assertion level of the declared entity is
-- compatible with assertion level of the ghost region.
---------------------------------
-- Check_Valid_Assertion_Level --
---------------------------------
procedure Check_Valid_Assertion_Level (Id : Entity_Id; Ref : Node_Id) is
Id_Level : constant Entity_Id := Ghost_Assertion_Level (Id);
Region_Level : constant Entity_Id :=
Ghost_Config.Ghost_Mode_Assertion_Level;
begin
-- This check is not applied for generic isntantiations
if Is_Generic_Instance (Id) then
return;
end if;
if not Is_Assertion_Level_Dependent (Id_Level, Region_Level) then
Error_Msg_Sloc := Sloc (Ref);
Error_Msg_N (Assertion_Level_Error_Msg, Ref);
Error_Msg_Name_1 := Chars (Id_Level);
Error_Msg_NE ("\& has assertion level %", Ref, Id);
Error_Msg_Name_1 := Chars (Region_Level);
Error_Msg_NE ("\& is declared within a region with %", Ref, Id);
Error_Msg_Name_1 := Chars (Region_Level);
Error_Msg_NE ("\assertion level of & should depend on %", Ref, Id);
end if;
end Check_Valid_Assertion_Level;
-- Local variables
Id : constant Entity_Id := Defining_Entity (N);
-- Start of processing for Check_Valid_Ghost_Declaration
begin
if not Is_Ghost_Entity (Id) or else Ghost_Config.Ghost_Mode = None
then
return;
end if;
Check_Valid_Assertion_Level (Id, N);
end Check_Valid_Ghost_Declaration;
---------------------------------------------
-- Check_Ghost_Formal_Procedure_Or_Package --
---------------------------------------------
procedure Check_Ghost_Formal_Procedure_Or_Package
(N : Node_Id;
Actual : Entity_Id;
Formal : Entity_Id;
Is_Default : Boolean := False)
is
begin
if not Is_Ghost_Entity (Formal) then
return;
end if;
if Present (Actual) and then Is_Ghost_Entity (Actual) then
return;
end if;
if Is_Default then
Error_Msg_N ("ghost procedure expected as default", N);
Error_Msg_NE ("\formal & is declared as ghost", N, Formal);
else
if Ekind (Formal) = E_Procedure then
Error_Msg_N ("ghost procedure expected for actual", N);
else
Error_Msg_N ("ghost package expected for actual", N);
end if;
Error_Msg_Sloc := Sloc (Formal);
Error_Msg_NE ("\formal & was declared as ghost #", N, Formal);
end if;
end Check_Ghost_Formal_Procedure_Or_Package;
---------------------------------
-- Check_Ghost_Formal_Variable --
---------------------------------
procedure Check_Ghost_Formal_Variable
(Actual : Node_Id;
Formal : Entity_Id;
Is_Default : Boolean := False)
is
Actual_Obj : constant Entity_Id := Get_Enclosing_Ghost_Entity (Actual);
begin
if not Is_Ghost_Entity (Formal) then
return;
end if;
if No (Actual_Obj)
or else not Is_Ghost_Entity (Actual_Obj)
then
if Is_Default then
Error_Msg_N ("ghost object expected as default", Actual);
Error_Msg_NE ("\formal & is declared as ghost", Actual, Formal);
else
Error_Msg_N ("ghost object expected for mutable actual", Actual);
Error_Msg_Sloc := Sloc (Formal);
Error_Msg_NE ("\formal & was declared as ghost #", Actual, Formal);
end if;
end if;
end Check_Ghost_Formal_Variable;
----------------------------
-- Check_Ghost_Overriding --
----------------------------
procedure Check_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id)
is
Deriv_Typ : Entity_Id;
Over_Subp : Entity_Id;
begin
if No (Subp) or else No (Overridden_Subp) then
return;
end if;
Over_Subp := Ultimate_Alias (Overridden_Subp);
Deriv_Typ := Find_Dispatching_Type (Subp);
-- A Ghost primitive of a non-Ghost type extension cannot override an
-- inherited non-Ghost primitive (SPARK RM 6.9(10)).
if Is_Ghost_Entity (Subp)
and then Present (Deriv_Typ)
and then not Is_Ghost_Entity (Deriv_Typ)
and then not Is_Ghost_Entity (Over_Subp)
and then not Is_Abstract_Subprogram (Over_Subp)
then
Error_Msg_N ("incompatible overriding in effect", Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N ("\overridden # with ghost subprogram", Subp);
end if;
-- A non-Ghost primitive of a type extension cannot override an
-- inherited Ghost primitive (SPARK RM 6.9(10)).
if Is_Ghost_Entity (Over_Subp)
and then not Is_Ghost_Entity (Subp)
and then not Is_Abstract_Subprogram (Subp)
then
Error_Msg_N ("incompatible overriding in effect", Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N ("\& declared # as ghost subprogram", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
end if;
if Present (Deriv_Typ)
and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
then
-- When a tagged type is either non-Ghost or checked Ghost and
-- one of its primitives overrides an inherited operation, the
-- overridden operation of the ancestor type must be ignored Ghost
-- if the primitive is ignored Ghost (SPARK RM 6.9(21)).
if Is_Ignored_Ghost_Entity (Subp) then
-- Both the parent subprogram and overriding subprogram are
-- ignored Ghost.
if Is_Ignored_Ghost_Entity (Over_Subp) then
null;
-- The parent subprogram carries policy Check
elsif Is_Checked_Ghost_Entity (Over_Subp) then
Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N
("\& declared # with ghost policy `Check`", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N
("\overridden # with ghost policy `Ignore`", Subp);
-- The parent subprogram is non-Ghost
else
Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N
("\overridden # with ghost policy `Ignore`", Subp);
end if;
-- When a tagged type is either non-Ghost or checked Ghost and
-- one of its primitives overrides an inherited operation, the
-- the primitive of the tagged type must be ignored Ghost if the
-- overridden operation is ignored Ghost (SPARK RM 6.9(21)).
elsif Is_Ignored_Ghost_Entity (Over_Subp) then
-- Both the parent subprogram and the overriding subprogram are
-- ignored Ghost.
if Is_Ignored_Ghost_Entity (Subp) then
null;
-- The overriding subprogram carries policy Check
elsif Is_Checked_Ghost_Entity (Subp) then
Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N
("\& declared # with ghost policy `Ignore`", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N
("\overridden # with Ghost policy `Check`", Subp);
-- The overriding subprogram is non-Ghost
else
Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
Error_Msg_Sloc := Sloc (Over_Subp);
Error_Msg_N
("\& declared # with ghost policy `Ignore`", Subp);
Error_Msg_Sloc := Sloc (Subp);
Error_Msg_N
("\overridden # with non-ghost subprogram", Subp);
end if;
end if;
end if;
end Check_Ghost_Overriding;
---------------------------
-- Check_Ghost_Primitive --
---------------------------
procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
Prim_Level : Entity_Id;
Typ_Level : Entity_Id;
begin
if not Is_Tagged_Type (Typ) then
return;
end if;
-- The Ghost policy in effect at the point of declaration of a primitive
-- operation and a tagged type must match (SPARK RM 6.9(21)).
if Is_Checked_Ghost_Entity (Prim)
and then Is_Ignored_Ghost_Entity (Typ)
then
Error_Msg_N (Ghost_Policy_Error_Msg, Prim);
Error_Msg_Sloc := Sloc (Typ);
Error_Msg_NE
("\tagged type & declared # with ghost policy `Ignore`",
Prim, Typ);
Error_Msg_Sloc := Sloc (Prim);
Error_Msg_N
("\primitive subprogram & declared # with ghost policy `Check`",
Prim);
end if;
Prim_Level := Ghost_Assertion_Level (Prim);
Typ_Level := Ghost_Assertion_Level (Typ);
if not Is_Assertion_Level_Dependent (Prim_Level, Typ_Level) then
Error_Msg_N (Assertion_Level_Error_Msg, Prim);
Error_Msg_Name_1 := Chars (Typ_Level);
Error_Msg_Sloc := Sloc (Typ);
Error_Msg_NE ("\tagged type & declared # with %", Prim, Typ);
Error_Msg_Name_1 := Chars (Prim_Level);
Error_Msg_Sloc := Sloc (Prim);
Error_Msg_NE
("\primitive subprogram & declared # with %", Prim, Prim);
Error_Msg_Name_1 := Chars (Typ_Level);
Error_Msg_NE
("\assertion level of & should depend on %", Prim, Prim);
end if;
end Check_Ghost_Primitive;
----------------------------
-- Check_Ghost_Refinement --
----------------------------
procedure Check_Ghost_Refinement
(State : Node_Id;
State_Id : Entity_Id;
Constit : Node_Id;
Constit_Id : Entity_Id)
is
State_Level : Entity_Id;
Constit_Level : Entity_Id;
begin
-- Only check ghost states
if not Is_Ghost_Entity (State_Id) then
return;
end if;
-- A constituent of a Ghost abstract state must be a Ghost entity
-- (SPARK RM 7.2.2(12)).
if not Is_Ghost_Entity (Constit_Id) then
SPARK_Msg_NE
("constituent of ghost state & must be ghost",
Constit, State_Id);
end if;
-- The Ghost policy in effect at the point of an ignored abstract state
-- cannot be check (SPARK RM 6.9(20)).
if Is_Ignored_Ghost_Entity (State_Id)
and then Is_Checked_Ghost_Entity (Constit_Id)
then
SPARK_Msg_N (Ghost_Policy_Error_Msg, State);
Error_Msg_Sloc := Sloc (State_Id);
SPARK_Msg_NE
("\abstract state & declared # with ghost policy `Ignore`",
State, State_Id);
Error_Msg_Sloc := Sloc (Constit_Id);
SPARK_Msg_NE
("\constituent & declared # with ghost policy `Check`",
State, Constit_Id);
end if;
State_Level := Ghost_Assertion_Level (State_Id);
Constit_Level := Ghost_Assertion_Level (Constit_Id);
if not Is_Assertion_Level_Dependent (Constit_Level, State_Level) then
SPARK_Msg_N (Assertion_Level_Error_Msg, State);
Error_Msg_Name_1 := Chars (State_Level);
Error_Msg_Sloc := Sloc (State_Id);
SPARK_Msg_NE ("\abstract state & declared # with %", State, State_Id);
Error_Msg_Name_1 := Chars (Constit_Level);
Error_Msg_Sloc := Sloc (Constit_Id);
SPARK_Msg_NE ("\constituent & declared # with %", State, Constit_Id);
Error_Msg_Name_1 := Chars (State_Level);
SPARK_Msg_NE
("\assertion level of & should depend on %", State, Constit_Id);
end if;
end Check_Ghost_Refinement;
----------------------
-- Check_Ghost_Type --
----------------------
procedure Check_Ghost_Type (Typ : Entity_Id) is
Conc_Typ : Entity_Id;
Full_Typ : Entity_Id;
begin
if Is_Ghost_Entity (Typ)
and then Comes_From_Source (Typ)
then
Conc_Typ := Empty;
Full_Typ := Typ;
if Is_Single_Concurrent_Type (Typ) then
Conc_Typ := Anonymous_Object (Typ);
Full_Typ := Conc_Typ;
elsif Has_Protected (Typ)
or else Has_Task (Typ)
then
Conc_Typ := Typ;
end if;
-- A Ghost type cannot be concurrent (SPARK RM 6.9(22)). Verify this
-- legality rule first to give a finer-grained diagnostic.
if Present (Conc_Typ) then
Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ);
end if;
-- A Ghost type cannot be effectively volatile (SPARK RM 6.9(9))
if Is_Effectively_Volatile (Full_Typ) then
Error_Msg_N ("ghost type & cannot be volatile", Full_Typ);
end if;
end if;
end Check_Ghost_Type;
----------------------
-- Get_Ghost_Aspect --
----------------------
function Get_Ghost_Aspect (N : Node_Id) return Node_Id is
Asp : Node_Id;
begin
if not Permits_Aspect_Specifications (N) then
return Empty;
end if;
Asp := First (Aspect_Specifications (N));
while Present (Asp) loop
if Chars (Identifier (Asp)) = Name_Ghost then
return Asp;
end if;
Next (Asp);
end loop;
return Empty;
end Get_Ghost_Aspect;
----------------------
-- Get_Ghost_Pragma --
----------------------
function Get_Ghost_Pragma (N : Node_Id) return Node_Id is
Decl : Node_Id := Empty;
begin
-- When the context is a [generic] package declaration, pragma Ghost
-- resides in the visible declarations.
if Nkind (N) in 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 (N) in 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 Decl;
-- A source construct ends the region where pragma Ghost may appear,
-- stop the traversal. Check the original node as source constructs
-- may be rewritten into something else by expansion.
elsif Comes_From_Source (Original_Node (Decl)) then
exit;
end if;
Next (Decl);
end loop;
return Empty;
end Get_Ghost_Pragma;
-------------------------------
-- Get_Ghost_Assertion_Level --
-------------------------------
function Get_Ghost_Assertion_Level (N : Node_Id) return Entity_Id is
Ghost_Asp : constant Node_Id := Get_Ghost_Aspect (N);
Ghost_Prag : Node_Id;
begin
if Present (Ghost_Asp) then
return Assertion_Level_From_Arg (Expression (Ghost_Asp));
end if;
Ghost_Prag := Get_Ghost_Pragma (N);
if Present (Ghost_Prag) then
return
Assertion_Level_From_Arg
(First (Pragma_Argument_Associations (Ghost_Prag)));
end if;
return Empty;
end Get_Ghost_Assertion_Level;
-------------------------------------
-- Ghost_Assertion_Level_In_Effect --
-------------------------------------
function Ghost_Assertion_Level_In_Effect (Id : Entity_Id) return Entity_Id
is
begin
if Ghost_Config.Is_Inside_Statement_Or_Pragma
and then Is_Implicit_Ghost (Id)
then
return Ghost_Config.Ghost_Mode_Assertion_Level;
else
return Ghost_Assertion_Level (Id);
end if;
end Ghost_Assertion_Level_In_Effect;
----------------------------
-- Ghost_Policy_In_Effect --
----------------------------
function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id is
Level : constant Entity_Id := Ghost_Assertion_Level (Id);
Level_Nam : constant Name_Id :=
(if No (Level) then No_Name else Chars (Level));
begin
if Present (Ghost_Config.Ignored_Ghost_Region) then
return Name_Ignore;
elsif Ghost_Config.Is_Inside_Statement_Or_Pragma
and then Is_Implicit_Ghost (Id)
then
case Ghost_Config.Ghost_Mode is
when Check =>
return Name_Check;
when Ignore =>
return Name_Ignore;
when None =>
return No_Name;
end case;
else
return Policy_In_Effect (Name_Ghost, Level_Nam);
end if;
end Ghost_Policy_In_Effect;
--------------------------------
-- 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_Nodes.Init;
-- Set the soft link which enables Atree.Mark_New_Ghost_Node to record
-- an ignored Ghost node or entity.
Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access);
end Initialize;
--------------------------
-- Install_Ghost_Region --
--------------------------
procedure Install_Ghost_Region
(Mode : Ghost_Mode_Type;
N : Node_Id;
Level : Entity_Id)
is
begin
-- The context is already within an ignored Ghost region. Maintain the
-- start of the outermost ignored Ghost region.
if Present (Ghost_Config.Ignored_Ghost_Region) then
null;
-- The current region is the outermost ignored Ghost region. Save its
-- starting node.
elsif Present (N) and then Mode = Ignore then
Ghost_Config.Ignored_Ghost_Region := N;
-- Otherwise the current region is not ignored, nothing to save
else
Ghost_Config.Ignored_Ghost_Region := Empty;
end if;
Ghost_Config.Current_Region := N;
Ghost_Config.Ghost_Mode := Mode;
Ghost_Config.Ghost_Mode_Assertion_Level := Level;
if Nkind (Ghost_Config.Current_Region)
in N_Statement_Other_Than_Procedure_Call
| N_Procedure_Call_Statement
| N_Pragma
then
Ghost_Config.Is_Inside_Statement_Or_Pragma := True;
end if;
end Install_Ghost_Region;
procedure Install_Ghost_Region
(Mode : Name_Id; N : Node_Id; Level : Entity_Id) is
begin
Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N, Level);
end Install_Ghost_Region;
-------------------------
-- Is_Compatible_Level --
-------------------------
function Is_Assertion_Level_Dependent
(Self : Entity_Id; Other : Entity_Id) return Boolean is
begin
return
Self = Standard_Level_Default
or else Other = Standard_Level_Default
or else Is_Same_Or_Depends_On_Level (Self, Other)
or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static);
end Is_Assertion_Level_Dependent;
-------------------------
-- 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 := Get_Enclosing_Ghost_Entity (Name (N));
return Present (Id) and then Is_Ghost_Entity (Id);
end if;
return False;
end Is_Ghost_Assignment;
----------------------------------
-- Is_Ghost_Attribute_Reference --
----------------------------------
function Is_Ghost_Attribute_Reference (N : Node_Id) return Boolean is
begin
return Nkind (N) = N_Attribute_Reference
and then Attribute_Name (N) = Name_Initialized;
end Is_Ghost_Attribute_Reference;
--------------------------
-- 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 := Get_Enclosing_Ghost_Entity (Name (N));
return Present (Id) and then Is_Ghost_Entity (Id);
end if;
return False;
end Is_Ghost_Procedure_Call;
---------------------------
-- Is_Ignored_Ghost_Unit --
---------------------------
function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean is
function Ultimate_Original_Node (Nod : Node_Id) return Node_Id;
-- Obtain the original node of arbitrary node Nod following a potential
-- chain of rewritings.
----------------------------
-- Ultimate_Original_Node --
----------------------------
function Ultimate_Original_Node (Nod : Node_Id) return Node_Id is
Res : Node_Id := Nod;
begin
while Is_Rewrite_Substitution (Res) loop
Res := Original_Node (Res);
end loop;
return Res;
end Ultimate_Original_Node;
-- Start of processing for Is_Ignored_Ghost_Unit
begin
-- Inspect the original node of the unit in case removal of ignored
-- Ghost code has already taken place.
return
Nkind (N) = N_Compilation_Unit
and then Is_Ignored_Ghost_Entity_In_Codegen
(Defining_Entity (Ultimate_Original_Node (Unit (N))));
end Is_Ignored_Ghost_Unit;
-------------------------
-- 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
begin
-- Ghostness is enabled if the argument implies a default assertion
-- level or it is explicitly a reference to an assertion level.
return Present (Assertion_Level_From_Arg (Arg));
end Enables_Ghostness;
-- Local variables
Id : constant Entity_Id := Defining_Entity (N);
Asp : Node_Id;
Prag : 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
Asp := Get_Ghost_Aspect (N);
if Present (Asp) then
return Enables_Ghostness (Expression (Asp));
end if;
-- Examine the following pragmas for an applicable Ghost pragma
Prag := Get_Ghost_Pragma (N);
if Present (Prag) then
return
Enables_Ghostness (First (Pragma_Argument_Associations (Prag)));
end if;
return False;
end Is_Subject_To_Ghost;
----------
-- Lock --
----------
procedure Lock is
begin
Ignored_Ghost_Nodes.Release;
Ignored_Ghost_Nodes.Locked := True;
end Lock;
-----------------------------------
-- Mark_And_Set_Ghost_Assignment --
-----------------------------------
procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is
-- A ghost assignment is an assignment whose left-hand side denotes a
-- ghost object. Subcomponents are not marked "ghost", so we need to
-- find the containing "whole" object. So, for "P.X.Comp (J) := ...",
-- where P is a package, X is a record, and Comp is an array, we need
-- to check the ghost flags of X.
procedure Check_Assignment_Policies (Assignee : Entity_Id);
-- Check that:
-- * A checked ghost assignment is not used in an ignored ghost
-- region.
-- * The level of the ghost region depends on the level of the
-- ghost assignment.
-------------------------------
-- Check_Assignment_Policies --
-------------------------------
procedure Check_Assignment_Policies (Assignee : Entity_Id) is
Assignee_Policy : constant Name_Id :=
Ghost_Policy_In_Effect (Assignee);
Assignee_Level : constant Entity_Id :=
Ghost_Assertion_Level (Assignee);
Region_Policy : constant Ghost_Mode_Type := Ghost_Config.Ghost_Mode;
Region_Level : constant Entity_Id :=
Ghost_Config.Ghost_Mode_Assertion_Level;
begin
if Assignee_Policy = Name_Check and then Region_Policy = Ignore then
Error_Msg_N (Ghost_Policy_Error_Msg, N);
Error_Msg_NE ("\& has ghost policy `Check`", N, Assignee);
Error_Msg_NE
("\& is modified in a region with `Ignore`", N, Assignee);
end if;
-- If an assignment to a part of a ghost variable occurs in a ghost
-- entity, then the variable should be assertion-level-dependent on
-- this entity (SPARK RM 6.9(18)).
if Present (Region_Level)
and then not Is_Assertion_Level_Dependent
(Assignee_Level, Region_Level)
then
Error_Msg_N (Assertion_Level_Error_Msg, N);
Error_Msg_Name_1 := Chars (Assignee_Level);
Error_Msg_NE ("\& has assertion level %", N, Assignee);
Error_Msg_Name_1 := Chars (Region_Level);
Error_Msg_NE
("\& is modified within a region with %", N, Assignee);
Error_Msg_Name_1 := Chars (Region_Level);
Error_Msg_NE
("\assertion level of & should depend on %", N, Assignee);
end if;
end Check_Assignment_Policies;
-- Local variables
Orig_Lhs : constant Node_Id := Name (N);
Id : Entity_Id;
Lhs : Node_Id;
-- Start of processing for Mark_And_Set_Ghost_Assignment
begin
-- Cases where full analysis is needed, involving array indexing
-- which would otherwise be missing array-bounds checks:
if not Analyzed (Orig_Lhs)
and then
((Nkind (Orig_Lhs) = N_Indexed_Component
and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component
and then Nkind (Prefix (Prefix (Orig_Lhs))) =
N_Indexed_Component)
or else
(Nkind (Orig_Lhs) = N_Selected_Component
and then Nkind (Prefix (Orig_Lhs)) = N_Indexed_Component
and then Nkind (Prefix (Prefix (Orig_Lhs))) =
N_Selected_Component
and then Nkind (Parent (N)) /= N_Loop_Statement))
then
Analyze (Orig_Lhs);
end if;
-- Make sure Lhs is at least preanalyzed, so we can tell whether
-- it denotes a ghost variable. In some cases we need to do a full
-- analysis, or else the back end gets confused. Note that in the
-- preanalysis case, we are preanalyzing a copy of the left-hand
-- side name, temporarily attached to the tree.
Lhs :=
(if Analyzed (Orig_Lhs) then Orig_Lhs else New_Copy_Tree (Orig_Lhs));
if not Analyzed (Lhs) then
Set_Name (N, Lhs);
Set_Parent (Lhs, N);
Preanalyze_Without_Errors (Lhs);
Set_Name (N, Orig_Lhs);
end if;
Id := Get_Enclosing_Ghost_Entity (Lhs);
if Present (Id) and then Is_Ghost_Entity (Id) then
Check_Assignment_Policies (Id);
end if;
Mark_And_Set_Ghost_Region (N, Id);
end Mark_And_Set_Ghost_Assignment;
-----------------------------
-- Mark_And_Set_Ghost_Body --
-----------------------------
procedure Mark_And_Set_Ghost_Body (N : Node_Id; Spec_Id : Entity_Id) is
Body_Id : constant Entity_Id := Defining_Entity (N);
Level : Entity_Id := Empty;
Policy : Name_Id := No_Name;
begin
-- A body becomes Ghost when it is subject to aspect or pragma Ghost
if Is_Subject_To_Ghost (N) then
if Present (Spec_Id) then
Policy := Ghost_Policy_In_Effect (Spec_Id);
Level := Ghost_Assertion_Level_In_Effect (Spec_Id);
else
Policy := Ghost_Policy_In_Effect (Body_Id);
Level := Ghost_Assertion_Level_In_Effect (Body_Id);
end if;
-- A body declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
elsif Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- 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;
Level := Ghost_Assertion_Level (Spec_Id);
end if;
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(18)).
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, Level);
-- Install the appropriate Ghost region
Install_Ghost_Region (Policy, N, Level);
end Mark_And_Set_Ghost_Body;
-----------------------------------
-- Mark_And_Set_Ghost_Completion --
-----------------------------------
procedure Mark_And_Set_Ghost_Completion
(N : Node_Id;
Prev_Id : Entity_Id)
is
Compl_Id : constant Entity_Id := Defining_Entity (N);
Level : Entity_Id := Empty;
Policy : Name_Id := No_Name;
begin
-- A completion elaborated in a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
if Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- The completion becomes Ghost when its initial declaration is also
-- Ghost.
elsif Is_Checked_Ghost_Entity (Prev_Id) then
Policy := Name_Check;
Level := Ghost_Assertion_Level (Prev_Id);
elsif Is_Ignored_Ghost_Entity (Prev_Id) then
Policy := Name_Ignore;
Level := Ghost_Assertion_Level (Prev_Id);
end if;
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(18)).
Check_Ghost_Completion
(Prev_Id => Prev_Id,
Compl_Id => Compl_Id);
-- Mark the completion as Ghost
Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
-- Install the appropriate Ghost region
Install_Ghost_Region (Policy, N, Level);
end Mark_And_Set_Ghost_Completion;
------------------------------------
-- Mark_And_Set_Ghost_Declaration --
------------------------------------
procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is
Level : Entity_Id := Empty;
Par_Id : Entity_Id;
Policy : Name_Id := No_Name;
begin
-- A declaration becomes Ghost when it is subject to aspect or pragma
-- Ghost.
Level := Get_Ghost_Assertion_Level (N);
-- A valid assertion level from an explicit pragma or aspect ghost
-- indicates the explicit ghostlyness of the declaration. Otherwise the
-- ghostliness of the declaration should be handled by other means like
-- the region.
if Present (Level) then
-- Default to the Ignore policy inside ignored ghost regions.
-- Similarly to how we do it in Ghost_Policy_In_Effect.
-- SPARK RM 6.9 (3)
if Present (Ghost_Config.Ignored_Ghost_Region) then
Policy := Name_Ignore;
else
Policy :=
Policy_In_Effect (Name_Ghost, Assertion_Level_To_Name (Level));
end if;
-- A declaration elaborated in a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
elsif Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- A child package or subprogram declaration becomes Ghost when its
-- parent is Ghost (SPARK RM 6.9(2)).
elsif Nkind (N)
in 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;
Level := Ghost_Assertion_Level (Par_Id);
end if;
-- Mark the declaration and its formals as Ghost
Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
Check_Valid_Ghost_Declaration (N);
-- Install the appropriate Ghost region
Install_Ghost_Region (Policy, N, Level);
end Mark_And_Set_Ghost_Declaration;
--------------------------------------
-- Mark_And_Set_Ghost_Instantiation --
--------------------------------------
procedure Mark_And_Set_Ghost_Instantiation
(N : Node_Id;
Gen_Id : Entity_Id)
is
procedure Check_Ghost_Actuals;
-- Check the context of ghost actuals
-------------------------
-- Check_Ghost_Actuals --
-------------------------
procedure Check_Ghost_Actuals is
Assoc : Node_Id := First (Generic_Associations (N));
Act : Node_Id;
begin
while Present (Assoc) loop
if Nkind (Assoc) /= N_Others_Choice then
Act := Explicit_Generic_Actual_Parameter (Assoc);
-- Within a nested instantiation, a defaulted actual is an
-- empty association, so nothing to check.
if No (Act) then
null;
elsif Comes_From_Source (Act)
and then Nkind (Act) in N_Has_Etype
and then Present (Etype (Act))
and then Is_Ghost_Entity (Etype (Act))
then
Check_Ghost_Context (Etype (Act), Act);
end if;
end if;
Next (Assoc);
end loop;
end Check_Ghost_Actuals;
-- Local variables
Level : Entity_Id := Empty;
Policy : Name_Id := No_Name;
begin
-- An instantiation becomes Ghost when it is subject to pragma Ghost
if Is_Subject_To_Ghost (N) then
Policy := Ghost_Policy_In_Effect (Gen_Id);
-- An instantiation declaration within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
elsif Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- Inherit the "ghostness" of the generic unit, but the current Ghost
-- policy is the relevant one for the instantiation.
elsif Is_Ghost_Entity (Gen_Id) then
Policy := Ghost_Policy_In_Effect (Gen_Id);
if Policy = No_Name then
Policy := Name_Ignore;
end if;
Level := Ghost_Assertion_Level (Gen_Id);
end if;
-- Mark the instantiation as Ghost
Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
-- Install the appropriate Ghost region
Install_Ghost_Region (Policy, N, Level);
-- Check Ghost actuals. Given that this routine is unconditionally
-- invoked with subprogram and package instantiations, this check
-- verifies the context of all the ghost entities passed in generic
-- instantiations.
Check_Ghost_Actuals;
end Mark_And_Set_Ghost_Instantiation;
------------------------------------------
-- Check_Procedure_Call_Argument_Levels --
------------------------------------------
procedure Check_Procedure_Call_Argument_Levels (N : Node_Id) is
procedure Check_Argument_Levels
(Actual : Entity_Id; Actual_Ref : Node_Id);
-- Check that the ghost assertion level of an actual is an assertion
-- level which depends on the ghost region where the procedure call
-- is located.
---------------------------
-- Check_Argument_Levels --
---------------------------
procedure Check_Argument_Levels
(Actual : Entity_Id; Actual_Ref : Node_Id)
is
Actual_Level : constant Entity_Id := Ghost_Assertion_Level (Actual);
Region_Level : constant Entity_Id :=
Ghost_Config.Ghost_Mode_Assertion_Level;
begin
-- If an assignment to a part of a ghost variable occurs in a ghost
-- entity, then the variable should be assertion-level-dependent on
-- this entity [This includes both assignment statements and passing
-- a ghost variable as an out or in out mode actual parameter.]
-- (SPARK RM 6.9(18)).
if Present (Region_Level)
and then not Is_Assertion_Level_Dependent
(Actual_Level, Region_Level)
then
Error_Msg_N (Assertion_Level_Error_Msg, Actual_Ref);
Error_Msg_Name_1 := Chars (Actual_Level);
Error_Msg_N ("\& has assertion level %", Actual_Ref);
Error_Msg_Name_1 := Chars (Region_Level);
Error_Msg_N ("\& is modified within a region with %", Actual_Ref);
Error_Msg_Name_1 := Chars (Region_Level);
Error_Msg_N
("\assertion level of & should depend on %", Actual_Ref);
end if;
end Check_Argument_Levels;
-- Local variables
Actual : Node_Id;
Actual_Id : Entity_Id;
Formal : Node_Id;
Id : Entity_Id;
Orig_Actual : Node_Id;
-- Start of processing for Check_Procedure_Call_Argument_Levels
begin
if Nkind (N) not in N_Procedure_Call_Statement then
return;
end if;
-- Handle the access-to-subprogram case
if Ekind (Etype (Name (N))) = E_Subprogram_Type then
Id := Etype (Name (N));
else
Id := Get_Enclosing_Ghost_Entity (Name (N));
end if;
-- Check for context if we are able to derive the called subprogram and
-- we are not dealing with an expanded construct.
if Present (Id)
and then Can_Have_Formals (Id)
and then Comes_From_Source (N)
and then Ghost_Config.Ghost_Mode /= None
then
Orig_Actual := First_Actual (N);
Formal := First_Formal (Id);
while Present (Orig_Actual) and then Present (Formal) loop
-- Similarly to Mark_And_Set_Ghost_Procedure_Call we need to
-- analyze the call argument first to get its level for this
-- analysis.
Actual :=
(if Analyzed (Orig_Actual)
then Orig_Actual
else New_Copy_Tree (Orig_Actual));
if not Analyzed (Actual) then
Preanalyze_Without_Errors (Actual);
end if;
if Ekind (Formal) in E_Out_Parameter | E_In_Out_Parameter then
Actual_Id := Get_Enclosing_Ghost_Entity (Actual);
if Present (Actual_Id) then
Check_Argument_Levels (Actual_Id, Orig_Actual);
end if;
end if;
Next_Formal (Formal);
Next_Actual (Orig_Actual);
end loop;
end if;
end Check_Procedure_Call_Argument_Levels;
---------------------------------------
-- Mark_And_Set_Ghost_Procedure_Call --
---------------------------------------
procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is
Id : Entity_Id;
begin
-- A procedure call becomes Ghost when the procedure being invoked is
-- Ghost. Install the Ghost mode of the procedure.
Id := Get_Enclosing_Ghost_Entity (Name (N));
Mark_And_Set_Ghost_Region (N, Id);
end Mark_And_Set_Ghost_Procedure_Call;
-------------------------------
-- Mark_And_Set_Ghost_Region --
-------------------------------
procedure Mark_And_Set_Ghost_Region (N : Node_Id; Id : Entity_Id) is
Id_Policy : Name_Id;
begin
-- Nothing to do if we are not dealing with a ghost entity
if No (Id) or else not Is_Ghost_Entity (Id) then
return;
end if;
Id_Policy := Ghost_Policy_In_Effect (Id);
if Id_Policy = Name_Check then
Install_Ghost_Region (Check, N, Ghost_Assertion_Level (Id));
elsif Id_Policy = Name_Ignore then
Install_Ghost_Region (Ignore, N, Ghost_Assertion_Level (Id));
Set_Is_Ignored_Ghost_Node (N);
Record_Ignored_Ghost_Node (N);
end if;
end Mark_And_Set_Ghost_Region;
-----------------------
-- Mark_Ghost_Clause --
-----------------------
procedure Mark_Ghost_Clause (N : Node_Id) is
Nam : Node_Id := Empty;
begin
if Nkind (N) = N_Use_Package_Clause then
Nam := Name (N);
elsif Nkind (N) = N_Use_Type_Clause then
Nam := Subtype_Mark (N);
elsif Nkind (N) = N_With_Clause then
Nam := Name (N);
end if;
if Present (Nam)
and then Is_Entity_Name (Nam)
and then Present (Entity (Nam))
and then Is_Ignored_Ghost_Entity_In_Codegen (Entity (Nam))
then
Set_Is_Ignored_Ghost_Node (N);
Record_Ignored_Ghost_Node (N);
end if;
end Mark_Ghost_Clause;
------------------------------------
-- Mark_Ghost_Declaration_Or_Body --
------------------------------------
procedure Mark_Ghost_Declaration_Or_Body
(N : Node_Id;
Mode : Name_Id;
Level : Entity_Id)
is
Id : constant Entity_Id := Defining_Entity (N);
Mark_Formals : Boolean := False;
Param : Node_Id;
Param_Id : Entity_Id;
procedure Mark_And_Set_Is_Checked_Ghost_Entity (E : Entity_Id);
-- Sets Is_Checked_Ghost_Entity, unsets Is_Ignored_Ghost_Entity
procedure Mark_And_Set_Is_Ignored_Ghost_Entity (E : Entity_Id);
-- Sets Is_Ignored_Ghost_Entity, unsets Is_Checked_Ghost_Entity
------------------------------------------
-- Mark_And_Set_Is_Checked_Ghost_Entity --
------------------------------------------
procedure Mark_And_Set_Is_Checked_Ghost_Entity (E : Entity_Id) is
begin
Set_Is_Checked_Ghost_Entity (E, True);
Set_Is_Ignored_Ghost_Entity (E, False);
end Mark_And_Set_Is_Checked_Ghost_Entity;
------------------------------------------
-- Mark_And_Set_Is_Ignored_Ghost_Entity --
------------------------------------------
procedure Mark_And_Set_Is_Ignored_Ghost_Entity (E : Entity_Id) is
begin
Set_Is_Checked_Ghost_Entity (E, False);
Set_Is_Ignored_Ghost_Entity (E, True);
end Mark_And_Set_Is_Ignored_Ghost_Entity;
-- Start of processing for Mark_Ghost_Declaration_Or_Body
begin
Set_Ghost_Assertion_Level (Id, Level);
if Mode = Name_Check then
Mark_Formals := True;
Mark_And_Set_Is_Checked_Ghost_Entity (Id);
elsif Mode = Name_Ignore then
Mark_Formals := True;
Mark_And_Set_Is_Ignored_Ghost_Entity (Id);
Set_Is_Ignored_Ghost_Node (N);
Record_Ignored_Ghost_Node (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 (N) in 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);
Set_Ghost_Assertion_Level (Param_Id, Level);
if Mode = Name_Check then
Mark_And_Set_Is_Checked_Ghost_Entity (Param_Id);
elsif Mode = Name_Ignore then
Mark_And_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
Mark_Ghost_Pragma (N, Check);
elsif Is_Ignored_Ghost_Entity (Id) then
Mark_Ghost_Pragma (N, Ignore);
end if;
end Mark_Ghost_Pragma;
procedure Mark_Ghost_Pragma (N : Node_Id; Mode : Ghost_Mode_Type) is
begin
if Mode = Check then
Set_Is_Checked_Ghost_Pragma (N, True);
Set_Is_Ignored_Ghost_Pragma (N, False);
else
Set_Is_Checked_Ghost_Pragma (N, False);
Set_Is_Ignored_Ghost_Pragma (N, True);
Set_Is_Ignored_Ghost_Node (N);
Record_Ignored_Ghost_Node (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;
Level : constant Entity_Id := Ghost_Assertion_Level (Id);
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, Level);
end Mark_Ghost_Renaming;
------------------------
-- Name_To_Ghost_Mode --
------------------------
function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is
begin
if Mode = Name_Check then
return Check;
elsif Mode = Name_Ignore then
return Ignore;
-- Otherwise the mode must denote one of the following:
--
-- * Disable indicates that the Ghost policy in effect is Disable
--
-- * None or No_Name indicates that the associated construct is not
-- subject to any Ghost annotation.
else
pragma Assert (Mode in Name_Disable | Name_None | No_Name);
return None;
end if;
end Name_To_Ghost_Mode;
-------------------------------
-- Record_Ignored_Ghost_Node --
-------------------------------
procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id) is
begin
-- Save all "top level" ignored Ghost nodes which can be safely replaced
-- with a null statement. Note that there is need to save other kinds of
-- nodes because those will always be enclosed by some top level ignored
-- Ghost node.
if Is_Body (N)
or else Is_Declaration (N)
or else Nkind (N) in N_Generic_Instantiation
| N_Push_Pop_xxx_Label
| N_Raise_xxx_Error
| N_Representation_Clause
| N_Statement_Other_Than_Procedure_Call
| N_Call_Marker
| N_Freeze_Entity
| N_Freeze_Generic_Entity
| N_Itype_Reference
| N_Pragma
| N_Procedure_Call_Statement
| N_Use_Package_Clause
| N_Use_Type_Clause
| N_Variable_Reference_Marker
| N_With_Clause
then
-- Only ignored Ghost nodes must be recorded in the table
pragma Assert (Is_Ignored_Ghost_Node (N));
Ignored_Ghost_Nodes.Append (N);
end if;
end Record_Ignored_Ghost_Node;
-------------------------------
-- Remove_Ignored_Ghost_Code --
-------------------------------
procedure Remove_Ignored_Ghost_Code is
procedure Remove_Ignored_Ghost_Node (N : Node_Id);
-- Eliminate ignored Ghost node N from the tree
-------------------------------
-- Remove_Ignored_Ghost_Node --
-------------------------------
procedure Remove_Ignored_Ghost_Node (N : Node_Id) is
begin
-- The generation and processing of ignored Ghost nodes may cause the
-- same node to be saved multiple times. Reducing the number of saves
-- to one involves costly solutions such as a hash table or the use
-- of a flag shared by all nodes. To solve this problem, the removal
-- machinery allows for multiple saves, but does not eliminate a node
-- which has already been eliminated.
if Nkind (N) = N_Null_Statement then
null;
-- Otherwise the ignored Ghost node must be eliminated
else
-- Only ignored Ghost nodes must be eliminated from the tree
pragma Assert (Is_Ignored_Ghost_Node (N));
-- Eliminate the node by rewriting it into null. Another option
-- is to remove it from the tree, however multiple corner cases
-- emerge which have be dealt individually.
Rewrite (N, Make_Null_Statement (Sloc (N)));
end if;
end Remove_Ignored_Ghost_Node;
-- Start of processing for Remove_Ignored_Ghost_Code
begin
for Index in Ignored_Ghost_Nodes.First .. Ignored_Ghost_Nodes.Last loop
Remove_Ignored_Ghost_Node (Ignored_Ghost_Nodes.Table (Index));
end loop;
end Remove_Ignored_Ghost_Code;
--------------------------
-- Restore_Ghost_Region --
--------------------------
procedure Restore_Ghost_Region (Config : Ghost_Config_Type) is
begin
Ghost_Config := Config;
end Restore_Ghost_Region;
--------------------
-- Set_Ghost_Mode --
--------------------
procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
-- Install the Ghost mode of entity Id
--------------------------------
-- Set_Ghost_Mode_From_Entity --
--------------------------------
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
Level : constant Entity_Id := Ghost_Assertion_Level (Id);
begin
if Is_Checked_Ghost_Entity (Id) then
Install_Ghost_Region (Check, N, Level);
elsif Is_Ignored_Ghost_Entity (Id) then
Install_Ghost_Region (Ignore, N, Level);
else
Install_Ghost_Region (None, N, Level);
end if;
end Set_Ghost_Mode_From_Entity;
-- Local variables
Id : Entity_Id;
Level : Entity_Id;
-- Start of processing for Set_Ghost_Mode
begin
-- The Ghost mode of an assignment statement depends on the Ghost mode
-- of the target.
if Nkind (N) = N_Assignment_Statement then
Id := Get_Enclosing_Ghost_Entity (Name (N));
if Present (Id) then
Set_Ghost_Mode_From_Entity (Id);
end if;
-- The Ghost mode of a body or a declaration depends on the Ghost mode
-- of its defining entity.
elsif Is_Body (N) or else Is_Declaration (N) then
Set_Ghost_Mode_From_Entity (Defining_Entity (N));
-- The Ghost mode of an entity depends on the entity itself
elsif Nkind (N) in N_Entity then
Set_Ghost_Mode_From_Entity (N);
-- The Ghost mode of a [generic] freeze node depends on the Ghost mode
-- of the entity being frozen.
elsif Nkind (N) in N_Freeze_Entity | N_Freeze_Generic_Entity then
Set_Ghost_Mode_From_Entity (Entity (N));
-- 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
Level := Pragma_Ghost_Assertion_Level (N);
if Is_Checked_Ghost_Pragma (N) then
-- Still install an ignored ghost region if the pragma is attached
-- to a checked ghost entity, but the pragma itself is explicitly
-- ignored.
if Is_Ignored (N) then
Install_Ghost_Region (Ignore, N, Level);
else
Install_Ghost_Region (Check, N, Level);
end if;
elsif Is_Ignored_Ghost_Pragma (N) then
Install_Ghost_Region (Ignore, N, Level);
else
if Is_Checked (N) then
Install_Ghost_Region (Check, N, Level);
else
Install_Ghost_Region (None, N, Level);
end if;
end if;
-- The Ghost mode of a procedure call depends on the Ghost mode of the
-- procedure being invoked.
elsif Nkind (N) = N_Procedure_Call_Statement then
Id := Get_Enclosing_Ghost_Entity (Name (N));
if Present (Id) then
Set_Ghost_Mode_From_Entity (Id);
end if;
end if;
end Set_Ghost_Mode;
-------------------------
-- Set_Is_Ghost_Entity --
-------------------------
procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
Policy : constant Name_Id := Ghost_Policy_In_Effect (Id);
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;