1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
|
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- G H O S T --
-- --
-- S p e c --
-- --
-- Copyright (C) 2014-2024, 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. --
-- --
------------------------------------------------------------------------------
-- This package contains routines that deal with the static and runtime
-- semantics of Ghost entities.
with Namet; use Namet;
with Opt; use Opt;
with Types; use Types;
package Ghost is
procedure Check_Ghost_Completion
(Prev_Id : Entity_Id;
Compl_Id : Entity_Id);
-- Verify that the Ghost policy of initial entity Prev_Id is compatible
-- with the Ghost policy of completing entity Compl_Id. Emit an error if
-- this is not the case.
procedure Check_Ghost_Context
(Ghost_Id : Entity_Id;
Ghost_Ref : Node_Id);
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
procedure Check_Ghost_Context_In_Generic_Association
(Actual : Node_Id;
Formal : Entity_Id);
-- Check that if Actual contains references to ghost entities, generic
-- formal parameter Formal is ghost (SPARK RM 6.9(10)).
procedure Check_Ghost_Formal_Procedure_Or_Package
(N : Node_Id;
Actual : Entity_Id;
Formal : Entity_Id;
Is_Default : Boolean := False);
-- Verify that if generic formal procedure (resp. package) Formal is ghost,
-- then Actual is not Empty and also a ghost procedure (resp. package)
-- (SPARK RM 6.9(13-14)). The error if any is located on N. If
-- Is_Default is False, N and Actual represent the actual parameter in an
-- instantiation. Otherwise, they represent the default subprogram of a
-- formal subprogram declaration.
procedure Check_Ghost_Formal_Variable
(Actual : Node_Id;
Formal : Entity_Id;
Is_Default : Boolean := False);
-- Verify that if Formal (either an IN OUT generic formal parameter, or an
-- IN generic formal parameter of access-to-variable type) is ghost, then
-- Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when
-- Actual is the default expression of the formal object declaration.
procedure Check_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id);
-- Verify that the Ghost policy of parent subprogram Overridden_Subp is
-- compatible with the Ghost policy of overriding subprogram Subp. Emit
-- an error if this is not the case.
procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
-- Verify that the Ghost policy of primitive operation Prim is the same as
-- the Ghost policy of tagged type Typ. Emit an error if this is not the
-- case.
procedure Check_Ghost_Refinement
(State : Node_Id;
State_Id : Entity_Id;
Constit : Node_Id;
Constit_Id : Entity_Id);
-- Verify that the Ghost policy of constituent Constit_Id is compatible
-- with the Ghost policy of abstract state State_I.
procedure Check_Ghost_Type (Typ : Entity_Id);
-- Verify that Ghost type Typ is neither concurrent, nor effectively
-- volatile.
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
procedure Initialize;
-- Initialize internal tables
procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
pragma Inline (Install_Ghost_Region);
-- Install a Ghost region described by mode Mode and ignored region start
-- node N.
function Is_Ghost_Assignment (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes an assignment statement whose
-- target is a Ghost entity.
function Is_Ghost_Attribute_Reference (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes an attribute reference which
-- denotes a Ghost attribute.
function Is_Ghost_Declaration (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a declaration which defines
-- a Ghost entity.
function Is_Ghost_Pragma (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a pragma which encloses a
-- Ghost entity or is associated with a Ghost entity.
function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a procedure call invoking a
-- Ghost procedure.
function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean;
-- Determine whether compilation unit N is subject to pragma Ghost with
-- policy Ignore.
procedure Lock;
-- Lock internal tables before calling backend
procedure Mark_And_Set_Ghost_Assignment (N : Node_Id);
-- Mark assignment statement N as Ghost when:
--
-- * The left hand side denotes a Ghost entity
--
-- Install the Ghost mode of the assignment statement. This routine starts
-- a Ghost region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Body
(N : Node_Id;
Spec_Id : Entity_Id);
-- Mark package or subprogram body N as Ghost when:
--
-- * The body is subject to pragma Ghost
--
-- * The body completes a previous declaration whose spec denoted by
-- Spec_Id is a Ghost entity.
--
-- * The body appears within a Ghost region
--
-- Install the Ghost mode of the body. This routine starts a Ghost region
-- and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Completion
(N : Node_Id;
Prev_Id : Entity_Id);
-- Mark completion N of a deferred constant or private type [extension]
-- Ghost when:
--
-- * The entity of the previous declaration denoted by Prev_Id is Ghost
--
-- * The completion appears within a Ghost region
--
-- Install the Ghost mode of the completion. This routine starts a Ghost
-- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
-- Mark declaration N as Ghost when:
--
-- * The declaration is subject to pragma Ghost
--
-- * The declaration denotes a child package or subprogram and the parent
-- is a Ghost unit.
--
-- * The declaration appears within a Ghost region
--
-- Install the Ghost mode of the declaration. This routine starts a Ghost
-- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Instantiation
(N : Node_Id;
Gen_Id : Entity_Id);
-- Mark instantiation N as Ghost when:
--
-- * The instantiation is subject to pragma Ghost
--
-- * The generic template denoted by Gen_Id is Ghost
--
-- * The instantiation appears within a Ghost region
--
-- Install the Ghost mode of the instantiation. This routine starts a Ghost
-- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
-- Mark procedure call N as Ghost when:
--
-- * The procedure being invoked is a Ghost entity
--
-- Install the Ghost mode of the procedure call. This routine starts a
-- Ghost region and must be used with routine Restore_Ghost_Region.
procedure Mark_Ghost_Clause (N : Node_Id);
-- Mark use package, use type, or with clause N as Ghost when:
--
-- * The clause mentions a Ghost entity
procedure Mark_Ghost_Pragma
(N : Node_Id;
Id : Entity_Id);
-- Mark pragma N as Ghost when:
--
-- * The pragma encloses Ghost entity Id
--
-- * The pragma is associated with Ghost entity Id
procedure Mark_Ghost_Pragma
(N : Node_Id;
Mode : Ghost_Mode_Type);
-- Mark pragma N as Ghost with the corresponding Mode
procedure Mark_Ghost_Renaming
(N : Node_Id;
Id : Entity_Id);
-- Mark renaming declaration N as Ghost when:
--
-- * Renamed entity Id denotes a Ghost entity
function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type;
pragma Inline (Name_To_Ghost_Mode);
-- Convert a Ghost mode denoted by name Mode into its respective enumerated
-- value.
procedure Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
-- units (SPARK RM 6.9(4)).
--
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
pragma Inline (Restore_Ghost_Region);
-- Restore a Ghost region to a previous state described by mode Mode and
-- ignored region start node N. This routine must be used in conjunction
-- with the following routines:
--
-- Install_Ghost_Region
-- Mark_And_Set_xxx
-- Set_Ghost_Mode
procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
-- Install the Ghost mode of arbitrary node N. This routine starts a Ghost
-- region and must be used with routine Restore_Ghost_Region.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant Ghost attributes of entity Id depending on the current
-- Ghost assertion policy in effect.
end Ghost;
|
