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-2016, 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
 105      (N    : Node_Id;
 106       Mode : out Ghost_Mode_Type);
 107    --  Mark assignment statement N as Ghost when:
 108    --
 109    --    * The left hand side denotes a Ghost entity
 110    --
 111    --  Install the Ghost mode of the assignment statement. Mode is the Ghost
 112    --  mode in effect prior to processing the assignment. This routine starts
 113    --  a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
 114
 115    procedure Mark_And_Set_Ghost_Body
 116      (N       : Node_Id;
 117       Spec_Id : Entity_Id;
 118       Mode    : out Ghost_Mode_Type);
 119    --  Mark package or subprogram body N as Ghost when:
 120    --
 121    --    * The body is subject to pragma Ghost
 122    --
 123    --    * The body completes a previous declaration whose spec denoted by
 124    --      Spec_Id is a Ghost entity.
 125    --
 126    --    * The body appears within a Ghost region
 127    --
 128    --  Install the Ghost mode of the body. Mode is the Ghost mode prior to
 129    --  processing the body. This routine starts a Ghost region and must be
 130    --  used in conjunction with Restore_Ghost_Mode.
 131
 132    procedure Mark_And_Set_Ghost_Completion
 133      (N       : Node_Id;
 134       Prev_Id : Entity_Id;
 135       Mode    : out Ghost_Mode_Type);
 136    --  Mark completion N of a deferred constant or private type [extension]
 137    --  Ghost when:
 138    --
 139    --    * The entity of the previous declaration denoted by Prev_Id is Ghost
 140    --
 141    --    * The completion appears within a Ghost region
 142    --
 143    --  Install the Ghost mode of the completion. Mode is the Ghost mode prior
 144    --  to processing the completion. This routine starts a Ghost region and
 145    --  must be used in conjunction with Restore_Ghost_Mode.
 146
 147    procedure Mark_And_Set_Ghost_Declaration
 148      (N    : Node_Id;
 149       Mode : out Ghost_Mode_Type);
 150    --  Mark declaration N as Ghost when:
 151    --
 152    --    * The declaration is subject to pragma Ghost
 153    --
 154    --    * The declaration denotes a child package or subprogram and the parent
 155    --      is a Ghost unit.
 156    --
 157    --    * The declaration appears within a Ghost region
 158    --
 159    --  Install the Ghost mode of the declaration. Mode is the Ghost mode prior
 160    --  to processing the declaration. This routine starts a Ghost region and
 161    --  must be used in conjunction with Restore_Ghost_Mode.
 162
 163    procedure Mark_And_Set_Ghost_Instantiation
 164      (N      : Node_Id;
 165       Gen_Id : Entity_Id;
 166       Mode   : out Ghost_Mode_Type);
 167    --  Mark instantiation N as Ghost when:
 168    --
 169    --    * The instantiation is subject to pragma Ghost
 170    --
 171    --    * The generic template denoted by Gen_Id is Ghost
 172    --
 173    --    * The instantiation appears within a Ghost region
 174    --
 175    --  Install the Ghost mode of the instantiation. Mode is the Ghost mode
 176    --  prior to processing the instantiation. This routine starts a Ghost
 177    --  region and must be used in conjunction with Restore_Ghost_Mode.
 178
 179    procedure Mark_And_Set_Ghost_Procedure_Call
 180      (N    : Node_Id;
 181       Mode : out Ghost_Mode_Type);
 182    --  Mark procedure call N as Ghost when:
 183    --
 184    --    * The procedure being invoked is a Ghost entity
 185    --
 186    --  Install the Ghost mode of the procedure call. Mode is the Ghost mode
 187    --  prior to processing the procedure call. This routine starts a Ghost
 188    --  region and must be used in conjunction with Restore_Ghost_Mode.
 189
 190    procedure Mark_Ghost_Clause (N : Node_Id);
 191    --  Mark use package, use type, or with clause N as Ghost when:
 192    --
 193    --    * The clause mentions a Ghost entity
 194
 195    procedure Mark_Ghost_Pragma
 196      (N  : Node_Id;
 197       Id : Entity_Id);
 198    --  Mark pragma N as Ghost when:
 199    --
 200    --    * The pragma encloses Ghost entity Id
 201    --
 202    --    * The pragma is associated with Ghost entity Id
 203
 204    procedure Mark_Ghost_Renaming
 205      (N  : Node_Id;
 206       Id : Entity_Id);
 207    --  Mark renaming declaration N as Ghost when:
 208    --
 209    --    * Renamed entity Id denotes a Ghost entity
 210
 211    procedure Remove_Ignored_Ghost_Code;
 212    --  Remove all code marked as ignored Ghost from the trees of all qualifying
 213    --  units (SPARK RM 6.9(4)).
 214    --
 215    --  WARNING: this is a separate front end pass, care should be taken to keep
 216    --  it optimized.
 217
 218    procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type);
 219    --  Terminate a Ghost region by restoring the Ghost mode prior to the
 220    --  region denoted by Mode. This routine must be used in conjunction
 221    --  with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
 222
 223    procedure Set_Ghost_Mode
 224      (N    : Node_Or_Entity_Id;
 225       Mode : out Ghost_Mode_Type);
 226    --  Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior
 227    --  to processing the node. This routine starts a Ghost region and must be
 228    --  used in conjunction with Restore_Ghost_Mode.
 229
 230    procedure Set_Is_Ghost_Entity (Id : Entity_Id);
 231    --  Set the relevant Ghost attributes of entity Id depending on the current
 232    --  Ghost assertion policy in effect.
 233
 234 end Ghost;