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    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
  53    --  Determine whether type Typ implements at least one Ghost interface
  54
  55    procedure Initialize;
  56    --  Initialize internal tables
  57
  58    function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
  59    --  Determine whether entity Id is Ghost. To qualify as such, the entity
  60    --  must be subject to pragma Ghost.
  61
  62    function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
  63    --  Determine whether declarative node N is subject to aspect or pragma
  64    --  Ghost. Use this routine in cases where [source] pragma Ghost has not
  65    --  been analyzed yet, but the context needs to establish the "ghostness"
  66    --  of N.
  67
  68    procedure Lock;
  69    --  Lock internal tables before calling backend
  70
  71    procedure Remove_Ignored_Ghost_Code;
  72    --  Remove all code marked as ignored Ghost from the trees of all qualifying
  73    --  units.
  74    --
  75    --  WARNING: this is a separate front end pass, care should be taken to keep
  76    --  it optimized.
  77
  78    procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty);
  79    --  Set the value of global variable Ghost_Mode depending on the following
  80    --  scenarios:
  81    --
  82    --    If N is a declaration, determine whether N is subject to pragma Ghost.
  83    --    If this is the case, the Ghost_Mode is set based on the current Ghost
  84    --    policy in effect. Special cases:
  85    --
  86    --      N is the completion of a deferred constant, Prev_Id denotes the
  87    --      entity of the partial declaration.
  88    --
  89    --      N is the full view of a private type, Prev_Id denotes the entity
  90    --      of the partial declaration.
  91    --
  92    --    If N is an assignment statement or a procedure call, determine whether
  93    --    the name of N denotes a reference to a Ghost entity. If this is the
  94    --    case, the Global_Mode is set based on the mode of the name.
  95    --
  96    --    If N denotes a package or a subprogram body, determine whether the
  97    --    corresponding spec Prev_Id is a Ghost entity or the body is subject
  98    --    to pragma Ghost. If this is the case, the Global_Mode is set based on
  99    --    the current Ghost policy in effect.
 100    --
 101    --  WARNING: the caller must save and restore the value of Ghost_Mode in a
 102    --  a stack-like fasion as this routine may override the existing value.
 103
 104    procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id);
 105    --  Set the value of global variable Ghost_Mode depending on the mode of
 106    --  entity Id. N denotes the context of the freeze.
 107    --
 108    --  WARNING: the caller must save and restore the value of Ghost_Mode in a
 109    --  a stack-like fasion as this routine may override the existing value.
 110
 111    procedure Set_Is_Ghost_Entity (Id : Entity_Id);
 112    --  Set the relevant ghost attribute of entity Id depending on the current
 113    --  Ghost assertion policy in effect.
 114
 115 end Ghost;