|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT COMPILER COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- G H O S T --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2014-2019, Free Software Foundation, Inc. --
|
|
111
|
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
|
|
|
29 with Opt; use Opt;
|
|
|
30 with Types; use Types;
|
|
|
31
|
|
|
32 package 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
|
|
131
|
67 procedure Check_Ghost_Type (Typ : Entity_Id);
|
|
|
68 -- Verify that Ghost type Typ is neither concurrent, nor effectively
|
|
|
69 -- volatile.
|
|
|
70
|
|
111
|
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
|
|
131
|
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.
|
|
111
|
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
|
|
131
|
111 -- a Ghost region and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
131
|
126 -- and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
131
|
139 -- region and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
131
|
152 -- region and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
131
|
166 -- region and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
131
|
174 -- Ghost region and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
131
|
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
|
|
111
|
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
|
|
131
|
216 -- region and must be used with routine Restore_Ghost_Region.
|
|
111
|
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
|
|
|
222 end Ghost;
|
