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