1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT COMPILER COMPONENTS                         --
4--                                                                          --
5--                                G H O S T                                 --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--          Copyright (C) 2014-2015, Free Software Foundation, Inc.         --
10--                                                                          --
11-- GNAT is free software;  you can  redistribute it  and/or modify it under --
12-- terms of the  GNU General Public License as published  by the Free Soft- --
13-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
14-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
15-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
16-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
17-- for  more details.  You should have  received  a copy of the GNU General --
18-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
19-- http://www.gnu.org/licenses for a complete copy of the license.          --
20--                                                                          --
21-- GNAT was originally developed  by the GNAT team at  New York University. --
22-- Extensive contributions were provided by Ada Core Technologies Inc.      --
23--                                                                          --
24------------------------------------------------------------------------------
25
26--  This package contains routines that deal with the static and runtime
27--  semantics of Ghost entities.
28
29with Types; use Types;
30
31package Ghost is
32
33   procedure Add_Ignored_Ghost_Unit (Unit : Node_Id);
34   --  Add a single ignored Ghost compilation unit to the internal table for
35   --  post processing.
36
37   procedure Check_Ghost_Completion
38     (Partial_View : Entity_Id;
39      Full_View    : Entity_Id);
40   --  Verify that the Ghost policy of a full view or a completion is the same
41   --  as the Ghost policy of the partial view. Emit an error if this is not
42   --  the case.
43
44   procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
45   --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
46   --  where Ghost entity Ghost_Id can safely reside.
47
48   procedure Check_Ghost_Derivation (Typ : Entity_Id);
49   --  Verify that the parent type and all progenitors of derived type or type
50   --  extension Typ are Ghost. If this is not the case, issue an error.
51
52   procedure Check_Ghost_Overriding
53     (Subp            : Entity_Id;
54      Overridden_Subp : Entity_Id);
55   --  Verify that the Ghost policy of parent subprogram Overridden_Subp is the
56   --  same as the Ghost policy of overriding subprogram Subp. Emit an error if
57   --  this is not the case.
58
59   function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
60   --  Determine whether type Typ implements at least one Ghost interface
61
62   procedure Initialize;
63   --  Initialize internal tables
64
65   procedure Lock;
66   --  Lock internal tables before calling backend
67
68   procedure Mark_Full_View_As_Ghost
69     (Priv_Typ : Entity_Id;
70      Full_Typ : Entity_Id);
71   --  Set all Ghost-related attributes of type Full_Typ depending on the Ghost
72   --  mode of incomplete or private type Priv_Typ.
73
74   procedure Mark_Pragma_As_Ghost
75     (Prag       : Node_Id;
76      Context_Id : Entity_Id);
77   --  Set all Ghost-related attributes of pragma Prag if its context denoted
78   --  by Id is a Ghost entity.
79
80   procedure Mark_Renaming_As_Ghost
81     (Ren_Decl : Node_Id;
82      Nam_Id   : Entity_Id);
83   --  Set all Ghost-related attributes of renaming declaration Ren_Decl if its
84   --  renamed name denoted by Nam_Id is a Ghost entity.
85
86   procedure Remove_Ignored_Ghost_Code;
87   --  Remove all code marked as ignored Ghost from the trees of all qualifying
88   --  units.
89   --
90   --  WARNING: this is a separate front end pass, care should be taken to keep
91   --  it optimized.
92
93   procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
94   --  Set the value of global variable Ghost_Mode depending on the following
95   --  scenarios:
96   --
97   --    If N is a declaration, determine whether N is subject to pragma Ghost.
98   --    If this is the case, the Ghost_Mode is set based on the current Ghost
99   --    policy in effect. Special cases:
100   --
101   --      N is the completion of a deferred constant, the Ghost_Mode is set
102   --      based on the mode of partial declaration entity denoted by Id.
103   --
104   --      N is the full view of a private type, the Ghost_Mode is set based
105   --      on the mode of the partial declaration entity denoted by Id.
106   --
107   --    If N is an assignment statement or a procedure call, the Ghost_Mode is
108   --    set based on the mode of the name.
109   --
110   --    If N denotes a package or a subprogram body, the Ghost_Mode is set to
111   --    the current Ghost policy in effect if the body is subject to Ghost or
112   --    the corresponding spec denoted by Id is a Ghost entity.
113   --
114   --    If N is a pragma, the Ghost_Mode is set based on the mode of the
115   --    pragma.
116   --
117   --    If N is a freeze node, the Global_Mode is set based on the mode of
118   --    entity Id.
119   --
120   --  WARNING: the caller must save and restore the value of Ghost_Mode in a
121   --  a stack-like fasion as this routine may override the existing value.
122
123   procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
124   --  Set the valye of global variable Ghost_Mode depending on the mode of
125   --  entity Id.
126   --
127   --  WARNING: the caller must save and restore the value of Ghost_Mode in a
128   --  a stack-like fasion as this routine may override the existing value.
129
130   procedure Set_Is_Ghost_Entity (Id : Entity_Id);
131   --  Set the relevant Ghost attributes of entity Id depending on the current
132   --  Ghost assertion policy in effect.
133
134end Ghost;
135