1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT COMPILER COMPONENTS                         --
4--                                                                          --
5--                                G H O S T                                 --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--          Copyright (C) 2014-2021, 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 Opt;   use Opt;
30with Types; use Types;
31
32package Ghost is
33
34   procedure Check_Ghost_Completion
35     (Prev_Id  : Entity_Id;
36      Compl_Id : Entity_Id);
37   --  Verify that the Ghost policy of initial entity Prev_Id is compatible
38   --  with the Ghost policy of completing entity Compl_Id. Emit an error if
39   --  this is not the case.
40
41   procedure Check_Ghost_Context
42     (Ghost_Id  : Entity_Id;
43      Ghost_Ref : Node_Id);
44   --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
45   --  where Ghost entity Ghost_Id can safely reside.
46
47   procedure Check_Ghost_Overriding
48     (Subp            : Entity_Id;
49      Overridden_Subp : Entity_Id);
50   --  Verify that the Ghost policy of parent subprogram Overridden_Subp is
51   --  compatible with the Ghost policy of overriding subprogram Subp. Emit
52   --  an error if this is not the case.
53
54   procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
55   --  Verify that the Ghost policy of primitive operation Prim is the same as
56   --  the Ghost policy of tagged type Typ. Emit an error if this is not the
57   --  case.
58
59   procedure Check_Ghost_Refinement
60     (State      : Node_Id;
61      State_Id   : Entity_Id;
62      Constit    : Node_Id;
63      Constit_Id : Entity_Id);
64   --  Verify that the Ghost policy of constituent Constit_Id is compatible
65   --  with the Ghost policy of abstract state State_I.
66
67   procedure Check_Ghost_Type (Typ : Entity_Id);
68   --  Verify that Ghost type Typ is neither concurrent, nor effectively
69   --  volatile.
70
71   function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
72   --  Determine whether type Typ implements at least one Ghost interface
73
74   procedure Initialize;
75   --  Initialize internal tables
76
77   procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
78   pragma Inline (Install_Ghost_Region);
79   --  Install a Ghost region described by mode Mode and ignored region start
80   --  node N.
81
82   function Is_Ghost_Assignment (N : Node_Id) return Boolean;
83   --  Determine whether arbitrary node N denotes an assignment statement whose
84   --  target is a Ghost entity.
85
86   function Is_Ghost_Declaration (N : Node_Id) return Boolean;
87   --  Determine whether arbitrary node N denotes a declaration which defines
88   --  a Ghost entity.
89
90   function Is_Ghost_Pragma (N : Node_Id) return Boolean;
91   --  Determine whether arbitrary node N denotes a pragma which encloses a
92   --  Ghost entity or is associated with a Ghost entity.
93
94   function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
95   --  Determine whether arbitrary node N denotes a procedure call invoking a
96   --  Ghost procedure.
97
98   function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean;
99   --  Determine whether compilation unit N is subject to pragma Ghost with
100   --  policy Ignore.
101
102   procedure Lock;
103   --  Lock internal tables before calling backend
104
105   procedure Mark_And_Set_Ghost_Assignment (N : Node_Id);
106   --  Mark assignment statement N as Ghost when:
107   --
108   --    * The left hand side denotes a Ghost entity
109   --
110   --  Install the Ghost mode of the assignment statement. This routine starts
111   --  a Ghost region and must be used with routine Restore_Ghost_Region.
112
113   procedure Mark_And_Set_Ghost_Body
114     (N       : Node_Id;
115      Spec_Id : Entity_Id);
116   --  Mark package or subprogram body N as Ghost when:
117   --
118   --    * The body is subject to pragma Ghost
119   --
120   --    * The body completes a previous declaration whose spec denoted by
121   --      Spec_Id is a Ghost entity.
122   --
123   --    * The body appears within a Ghost region
124   --
125   --  Install the Ghost mode of the body. This routine starts a Ghost region
126   --  and must be used with routine Restore_Ghost_Region.
127
128   procedure Mark_And_Set_Ghost_Completion
129     (N       : Node_Id;
130      Prev_Id : Entity_Id);
131   --  Mark completion N of a deferred constant or private type [extension]
132   --  Ghost when:
133   --
134   --    * The entity of the previous declaration denoted by Prev_Id is Ghost
135   --
136   --    * The completion appears within a Ghost region
137   --
138   --  Install the Ghost mode of the completion. This routine starts a Ghost
139   --  region and must be used with routine Restore_Ghost_Region.
140
141   procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
142   --  Mark declaration N as Ghost when:
143   --
144   --    * The declaration is subject to pragma Ghost
145   --
146   --    * The declaration denotes a child package or subprogram and the parent
147   --      is a Ghost unit.
148   --
149   --    * The declaration appears within a Ghost region
150   --
151   --  Install the Ghost mode of the declaration. This routine starts a Ghost
152   --  region and must be used with routine Restore_Ghost_Region.
153
154   procedure Mark_And_Set_Ghost_Instantiation
155     (N      : Node_Id;
156      Gen_Id : Entity_Id);
157   --  Mark instantiation N as Ghost when:
158   --
159   --    * The instantiation is subject to pragma Ghost
160   --
161   --    * The generic template denoted by Gen_Id is Ghost
162   --
163   --    * The instantiation appears within a Ghost region
164   --
165   --  Install the Ghost mode of the instantiation. This routine starts a Ghost
166   --  region and must be used with routine Restore_Ghost_Region.
167
168   procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
169   --  Mark procedure call N as Ghost when:
170   --
171   --    * The procedure being invoked is a Ghost entity
172   --
173   --  Install the Ghost mode of the procedure call. This routine starts a
174   --  Ghost region and must be used with routine Restore_Ghost_Region.
175
176   procedure Mark_Ghost_Clause (N : Node_Id);
177   --  Mark use package, use type, or with clause N as Ghost when:
178   --
179   --    * The clause mentions a Ghost entity
180
181   procedure Mark_Ghost_Pragma
182     (N  : Node_Id;
183      Id : Entity_Id);
184   --  Mark pragma N as Ghost when:
185   --
186   --    * The pragma encloses Ghost entity Id
187   --
188   --    * The pragma is associated with Ghost entity Id
189
190   procedure Mark_Ghost_Renaming
191     (N  : Node_Id;
192      Id : Entity_Id);
193   --  Mark renaming declaration N as Ghost when:
194   --
195   --    * Renamed entity Id denotes a Ghost entity
196
197   procedure Remove_Ignored_Ghost_Code;
198   --  Remove all code marked as ignored Ghost from the trees of all qualifying
199   --  units (SPARK RM 6.9(4)).
200   --
201   --  WARNING: this is a separate front end pass, care should be taken to keep
202   --  it optimized.
203
204   procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
205   pragma Inline (Restore_Ghost_Region);
206   --  Restore a Ghost region to a previous state described by mode Mode and
207   --  ignored region start node N. This routine must be used in conjunction
208   --  with the following routines:
209   --
210   --    Install_Ghost_Region
211   --    Mark_And_Set_xxx
212   --    Set_Ghost_Mode
213
214   procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
215   --  Install the Ghost mode of arbitrary node N. This routine starts a Ghost
216   --  region and must be used with routine Restore_Ghost_Region.
217
218   procedure Set_Is_Ghost_Entity (Id : Entity_Id);
219   --  Set the relevant Ghost attributes of entity Id depending on the current
220   --  Ghost assertion policy in effect.
221
222end Ghost;
223