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-2015, 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 Types; use Types;
  30
  31 package Ghost is
  32
  33    procedure Add_Ignored_Ghost_Unit (Unit : Node_Id);
  34    --  Add a single ignored Ghost compilation unit to the internal table for
  35    --  post processing.
  36
  37    procedure Check_Ghost_Completion
  38      (Partial_View : Entity_Id;
  39       Full_View    : Entity_Id);
  40    --  Verify that the Ghost policy of a full view or a completion is the same
  41    --  as the Ghost policy of the partial view. Emit an error if this is not
  42    --  the case.
  43
  44    procedure Check_Ghost_Context (Ghost_Id : Entity_Id; 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_Derivation (Typ : Entity_Id);
  49    --  Verify that the parent type and all progenitors of derived type or type
  50    --  extension Typ are Ghost. If this is not the case, issue an error.
  51
  52    procedure Check_Ghost_Overriding
  53      (Subp            : Entity_Id;
  54       Overridden_Subp : Entity_Id);
  55    --  Verify that the Ghost policy of parent subprogram Overridden_Subp is the
  56    --  same as the Ghost policy of overriding subprogram Subp. Emit an error if
  57    --  this is not the case.
  58
  59    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
  60    --  Determine whether type Typ implements at least one Ghost interface
  61
  62    procedure Initialize;
  63    --  Initialize internal tables
  64
  65    function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
  66    --  Determine whether entity Id is Ghost. To qualify as such, the entity
  67    --  must be subject to pragma Ghost.
  68
  69    function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
  70    --  Determine whether declarative node N is subject to aspect or pragma
  71    --  Ghost. Use this routine in cases where [source] pragma Ghost has not
  72    --  been analyzed yet, but the context needs to establish the "ghostness"
  73    --  of N.
  74
  75    procedure Lock;
  76    --  Lock internal tables before calling backend
  77
  78    procedure Mark_Full_View_As_Ghost
  79      (Priv_Typ : Entity_Id;
  80       Full_Typ : Entity_Id);
  81    --  Set all Ghost-related attributes of type Full_Typ depending on the Ghost
  82    --  mode of incomplete or private type Priv_Typ.
  83
  84    procedure Mark_Pragma_As_Ghost
  85      (Prag       : Node_Id;
  86       Context_Id : Entity_Id);
  87    --  Set all Ghost-related attributes of pragma Prag if its context denoted
  88    --  by Id is a Ghost entity.
  89
  90    procedure Mark_Renaming_As_Ghost
  91      (Ren_Decl : Node_Id;
  92       Nam_Id   : Entity_Id);
  93    --  Set all Ghost-related attributes of renaming declaration Ren_Decl if its
  94    --  renamed name denoted by Nam_Id is a Ghost entity.
  95
  96    procedure Remove_Ignored_Ghost_Code;
  97    --  Remove all code marked as ignored Ghost from the trees of all qualifying
  98    --  units.
  99    --
 100    --  WARNING: this is a separate front end pass, care should be taken to keep
 101    --  it optimized.
 102
 103    procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
 104    --  Set the value of global variable Ghost_Mode depending on the following
 105    --  scenarios:
 106    --
 107    --    If N is a declaration, determine whether N is subject to pragma Ghost.
 108    --    If this is the case, the Ghost_Mode is set based on the current Ghost
 109    --    policy in effect. Special cases:
 110    --
 111    --      N is the completion of a deferred constant, the Ghost_Mode is set
 112    --      based on the mode of partial declaration entity denoted by Id.
 113    --
 114    --      N is the full view of a private type, the Ghost_Mode is set based
 115    --      on the mode of the partial declaration entity denoted by Id.
 116    --
 117    --    If N is an assignment statement or a procedure call, the Ghost_Mode is
 118    --    set based on the mode of the name.
 119    --
 120    --    If N denotes a package or a subprogram body, the Ghost_Mode is set to
 121    --    the current Ghost policy in effect if the body is subject to Ghost or
 122    --    the corresponding spec denoted by Id is a Ghost entity.
 123    --
 124    --    If N is a pragma, the Ghost_Mode is set based on the mode of the
 125    --    pragma.
 126    --
 127    --    If N is a freeze node, the Global_Mode is set based on the mode of
 128    --    entity Id.
 129    --
 130    --  WARNING: the caller must save and restore the value of Ghost_Mode in a
 131    --  a stack-like fasion as this routine may override the existing value.
 132
 133    procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
 134    --  Set the valye of global variable Ghost_Mode depending on the mode of
 135    --  entity Id.
 136    --
 137    --  WARNING: the caller must save and restore the value of Ghost_Mode in a
 138    --  a stack-like fasion as this routine may override the existing value.
 139
 140    procedure Set_Is_Ghost_Entity (Id : Entity_Id);
 141    --  Set the relevant Ghost attributes of entity Id depending on the current
 142    --  Ghost assertion policy in effect.
 143
 144 end Ghost;