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_Overriding
  49      (Subp            : Entity_Id;
  50       Overridden_Subp : Entity_Id);
  51    --  Verify that the Ghost policy of parent subprogram Overridden_Subp is
  52    --  compatible with the Ghost policy of overriding subprogram Subp. Emit
  53    --  an error if this is not the case.
  54
  55    procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
  56    --  Verify that the Ghost policy of primitive operation Prim is the same as
  57    --  the Ghost policy of tagged type Typ. Emit an error if this is not the
  58    --  case.
  59
  60    procedure Check_Ghost_Refinement
  61      (State      : Node_Id;
  62       State_Id   : Entity_Id;
  63       Constit    : Node_Id;
  64       Constit_Id : Entity_Id);
  65    --  Verify that the Ghost policy of constituent Constit_Id is compatible
  66    --  with the Ghost policy of abstract state State_I.
  67
  68    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
  69    --  Determine whether type Typ implements at least one Ghost interface
  70
  71    procedure Initialize;
  72    --  Initialize internal tables
  73
  74    procedure Lock;
  75    --  Lock internal tables before calling backend
  76
  77    procedure Mark_Full_View_As_Ghost
  78      (Priv_Typ : Entity_Id;
  79       Full_Typ : Entity_Id);
  80    --  Set all Ghost-related attributes of type Full_Typ depending on the Ghost
  81    --  mode of incomplete or private type Priv_Typ.
  82
  83    procedure Mark_Pragma_As_Ghost
  84      (Prag       : Node_Id;
  85       Context_Id : Entity_Id);
  86    --  Set all Ghost-related attributes of pragma Prag if its context denoted
  87    --  by Id is a Ghost entity.
  88
  89    procedure Mark_Renaming_As_Ghost
  90      (Ren_Decl : Node_Id;
  91       Nam_Id   : Entity_Id);
  92    --  Set all Ghost-related attributes of renaming declaration Ren_Decl if its
  93    --  renamed name denoted by Nam_Id is a Ghost entity.
  94
  95    procedure Remove_Ignored_Ghost_Code;
  96    --  Remove all code marked as ignored Ghost from the trees of all qualifying
  97    --  units (SPARK RM 6.9(4)).
  98    --
  99    --  WARNING: this is a separate front end pass, care should be taken to keep
 100    --  it optimized.
 101
 102    procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
 103    --  Set the value of global variable Ghost_Mode depending on the following
 104    --  scenarios:
 105    --
 106    --    If N is a declaration, determine whether N is subject to pragma Ghost.
 107    --    If this is the case, the Ghost_Mode is set based on the current Ghost
 108    --    policy in effect. Special cases:
 109    --
 110    --      N is the completion of a deferred constant, the Ghost_Mode is set
 111    --      based on the mode of partial declaration entity denoted by Id.
 112    --
 113    --      N is the full view of a private type, the Ghost_Mode is set based
 114    --      on the mode of the partial declaration entity denoted by Id.
 115    --
 116    --    If N is an assignment statement or a procedure call, the Ghost_Mode is
 117    --    set based on the mode of the name.
 118    --
 119    --    If N denotes a package or a subprogram body, the Ghost_Mode is set to
 120    --    the current Ghost policy in effect if the body is subject to Ghost or
 121    --    the corresponding spec denoted by Id is a Ghost entity.
 122    --
 123    --    If N is a pragma, the Ghost_Mode is set based on the mode of the
 124    --    pragma.
 125    --
 126    --    If N is a freeze node, the Global_Mode is set based on the mode of
 127    --    entity Id.
 128    --
 129    --  WARNING: the caller must save and restore the value of Ghost_Mode in a
 130    --  a stack-like fasion as this routine may override the existing value.
 131
 132    procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
 133    --  Set the valye of global variable Ghost_Mode depending on the mode of
 134    --  entity Id.
 135    --
 136    --  WARNING: the caller must save and restore the value of Ghost_Mode in a
 137    --  a stack-like fasion as this routine may override the existing value.
 138
 139    procedure Set_Is_Ghost_Entity (Id : Entity_Id);
 140    --  Set the relevant Ghost attributes of entity Id depending on the current
 141    --  Ghost assertion policy in effect.
 142
 143 end Ghost;