Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/ghost.ads @ 132:d34655255c78

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
update gcc-8.2
author mir3636
date Thu, 25 Oct 2018 10:21:07 +0900
parents 84e7813d76e9
children 1830386684a0
comparison
equal deleted inserted replaced
130:e108057fa461 132:d34655255c78
4 -- -- 4 -- --
5 -- G H O S T -- 5 -- G H O S T --
6 -- -- 6 -- --
7 -- S p e c -- 7 -- S p e c --
8 -- -- 8 -- --
9 -- Copyright (C) 2014-2017, Free Software Foundation, Inc. -- 9 -- Copyright (C) 2014-2018, Free Software Foundation, Inc. --
10 -- -- 10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under -- 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- -- 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- -- 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- -- 14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
29 with Opt; use Opt; 29 with Opt; use Opt;
30 with Types; use Types; 30 with Types; use Types;
31 31
32 package Ghost is 32 package Ghost is
33 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 34 procedure Check_Ghost_Completion
39 (Prev_Id : Entity_Id; 35 (Prev_Id : Entity_Id;
40 Compl_Id : Entity_Id); 36 Compl_Id : Entity_Id);
41 -- Verify that the Ghost policy of initial entity Prev_Id is compatible 37 -- 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 38 -- with the Ghost policy of completing entity Compl_Id. Emit an error if
66 Constit : Node_Id; 62 Constit : Node_Id;
67 Constit_Id : Entity_Id); 63 Constit_Id : Entity_Id);
68 -- Verify that the Ghost policy of constituent Constit_Id is compatible 64 -- Verify that the Ghost policy of constituent Constit_Id is compatible
69 -- with the Ghost policy of abstract state State_I. 65 -- with the Ghost policy of abstract state State_I.
70 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; 71 function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
72 -- Determine whether type Typ implements at least one Ghost interface 72 -- Determine whether type Typ implements at least one Ghost interface
73 73
74 procedure Initialize; 74 procedure Initialize;
75 -- Initialize internal tables 75 -- Initialize internal tables
76 76
77 procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); 77 procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
78 -- Set the value of global variable Ghost_Mode depending on the Ghost 78 pragma Inline (Install_Ghost_Region);
79 -- policy denoted by Mode. 79 -- Install a Ghost region described by mode Mode and ignored region start
80 -- node N.
80 81
81 function Is_Ghost_Assignment (N : Node_Id) return Boolean; 82 function Is_Ghost_Assignment (N : Node_Id) return Boolean;
82 -- Determine whether arbitrary node N denotes an assignment statement whose 83 -- Determine whether arbitrary node N denotes an assignment statement whose
83 -- target is a Ghost entity. 84 -- target is a Ghost entity.
84 85
105 -- Mark assignment statement N as Ghost when: 106 -- Mark assignment statement N as Ghost when:
106 -- 107 --
107 -- * The left hand side denotes a Ghost entity 108 -- * The left hand side denotes a Ghost entity
108 -- 109 --
109 -- Install the Ghost mode of the assignment statement. This routine starts 110 -- 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 -- a Ghost region and must be used with routine Restore_Ghost_Region.
111 112
112 procedure Mark_And_Set_Ghost_Body 113 procedure Mark_And_Set_Ghost_Body
113 (N : Node_Id; 114 (N : Node_Id;
114 Spec_Id : Entity_Id); 115 Spec_Id : Entity_Id);
115 -- Mark package or subprogram body N as Ghost when: 116 -- Mark package or subprogram body N as Ghost when:
120 -- Spec_Id is a Ghost entity. 121 -- Spec_Id is a Ghost entity.
121 -- 122 --
122 -- * The body appears within a Ghost region 123 -- * The body appears within a Ghost region
123 -- 124 --
124 -- Install the Ghost mode of the body. This routine starts a Ghost region 125 -- 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 -- and must be used with routine Restore_Ghost_Region.
126 127
127 procedure Mark_And_Set_Ghost_Completion 128 procedure Mark_And_Set_Ghost_Completion
128 (N : Node_Id; 129 (N : Node_Id;
129 Prev_Id : Entity_Id); 130 Prev_Id : Entity_Id);
130 -- Mark completion N of a deferred constant or private type [extension] 131 -- Mark completion N of a deferred constant or private type [extension]
133 -- * The entity of the previous declaration denoted by Prev_Id is Ghost 134 -- * The entity of the previous declaration denoted by Prev_Id is Ghost
134 -- 135 --
135 -- * The completion appears within a Ghost region 136 -- * The completion appears within a Ghost region
136 -- 137 --
137 -- Install the Ghost mode of the completion. This routine starts a Ghost 138 -- 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 -- region and must be used with routine Restore_Ghost_Region.
139 140
140 procedure Mark_And_Set_Ghost_Declaration (N : Node_Id); 141 procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
141 -- Mark declaration N as Ghost when: 142 -- Mark declaration N as Ghost when:
142 -- 143 --
143 -- * The declaration is subject to pragma Ghost 144 -- * The declaration is subject to pragma Ghost
146 -- is a Ghost unit. 147 -- is a Ghost unit.
147 -- 148 --
148 -- * The declaration appears within a Ghost region 149 -- * The declaration appears within a Ghost region
149 -- 150 --
150 -- Install the Ghost mode of the declaration. This routine starts a Ghost 151 -- 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 -- region and must be used with routine Restore_Ghost_Region.
152 153
153 procedure Mark_And_Set_Ghost_Instantiation 154 procedure Mark_And_Set_Ghost_Instantiation
154 (N : Node_Id; 155 (N : Node_Id;
155 Gen_Id : Entity_Id); 156 Gen_Id : Entity_Id);
156 -- Mark instantiation N as Ghost when: 157 -- Mark instantiation N as Ghost when:
160 -- * The generic template denoted by Gen_Id is Ghost 161 -- * The generic template denoted by Gen_Id is Ghost
161 -- 162 --
162 -- * The instantiation appears within a Ghost region 163 -- * The instantiation appears within a Ghost region
163 -- 164 --
164 -- Install the Ghost mode of the instantiation. This routine starts a Ghost 165 -- 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 -- region and must be used with routine Restore_Ghost_Region.
166 167
167 procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id); 168 procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
168 -- Mark procedure call N as Ghost when: 169 -- Mark procedure call N as Ghost when:
169 -- 170 --
170 -- * The procedure being invoked is a Ghost entity 171 -- * The procedure being invoked is a Ghost entity
171 -- 172 --
172 -- Install the Ghost mode of the procedure call. This routine starts a 173 -- 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 -- Ghost region and must be used with routine Restore_Ghost_Region.
174 175
175 procedure Mark_Ghost_Clause (N : Node_Id); 176 procedure Mark_Ghost_Clause (N : Node_Id);
176 -- Mark use package, use type, or with clause N as Ghost when: 177 -- Mark use package, use type, or with clause N as Ghost when:
177 -- 178 --
178 -- * The clause mentions a Ghost entity 179 -- * The clause mentions a Ghost entity
198 -- units (SPARK RM 6.9(4)). 199 -- units (SPARK RM 6.9(4)).
199 -- 200 --
200 -- WARNING: this is a separate front end pass, care should be taken to keep 201 -- WARNING: this is a separate front end pass, care should be taken to keep
201 -- it optimized. 202 -- it optimized.
202 203
203 procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type); 204 procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
204 -- Terminate a Ghost region by restoring the Ghost mode prior to the 205 pragma Inline (Restore_Ghost_Region);
205 -- region denoted by Mode. This routine must be used in conjunction 206 -- Restore a Ghost region to a previous state described by mode Mode and
206 -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode. 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
207 213
208 procedure Set_Ghost_Mode (N : Node_Or_Entity_Id); 214 procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
209 -- Install the Ghost mode of arbitrary node N. This routine starts a Ghost 215 -- 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. 216 -- region and must be used with routine Restore_Ghost_Region.
211 217
212 procedure Set_Is_Ghost_Entity (Id : Entity_Id); 218 procedure Set_Is_Ghost_Entity (Id : Entity_Id);
213 -- Set the relevant Ghost attributes of entity Id depending on the current 219 -- Set the relevant Ghost attributes of entity Id depending on the current
214 -- Ghost assertion policy in effect. 220 -- Ghost assertion policy in effect.
215 221