Mercurial > hg > CbC > CbC_gcc
comparison gcc/ada/ghost.ads @ 111:04ced10e8804
gcc 7
| author | kono |
|---|---|
| date | Fri, 27 Oct 2017 22:46:09 +0900 |
| parents | |
| children | 84e7813d76e9 |
comparison
equal
deleted
inserted
replaced
| 68:561a7518be6b | 111:04ced10e8804 |
|---|---|
| 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; |