gcc/ada/ghost.ads

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