gcc/ada/ghost.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                                G H O S T                                 --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   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 with Alloc;    use Alloc;
  27 with Aspects;  use Aspects;
  28 with Atree;    use Atree;
  29 with Einfo;    use Einfo;
  30 with Elists;   use Elists;
  31 with Errout;   use Errout;
  32 with Lib;      use Lib;
  33 with Namet;    use Namet;
  34 with Nlists;   use Nlists;
  35 with Nmake;    use Nmake;
  36 with Opt;      use Opt;
  37 with Sem;      use Sem;
  38 with Sem_Aux;  use Sem_Aux;
  39 with Sem_Disp; use Sem_Disp;
  40 with Sem_Eval; use Sem_Eval;
  41 with Sem_Prag; use Sem_Prag;
  42 with Sem_Res;  use Sem_Res;
  43 with Sem_Util; use Sem_Util;
  44 with Sinfo;    use Sinfo;
  45 with Snames;   use Snames;
  46 with Table;
  47
  48 package body Ghost is
  49
  50    --  The following table contains the N_Compilation_Unit node for a unit that
  51    --  is either subject to pragma Ghost with policy Ignore or contains ignored
  52    --  Ghost code. The table is used in the removal of ignored Ghost code from
  53    --  units.
  54
  55    package Ignored_Ghost_Units is new Table.Table (
  56      Table_Component_Type => Node_Id,
  57      Table_Index_Type     => Int,
  58      Table_Low_Bound      => 0,
  59      Table_Initial        => Alloc.Ignored_Ghost_Units_Initial,
  60      Table_Increment      => Alloc.Ignored_Ghost_Units_Increment,
  61      Table_Name           => "Ignored_Ghost_Units");
  62
  63    -----------------------
  64    -- Local Subprograms --
  65    -----------------------
  66
  67    function Ghost_Entity (N : Node_Id) return Entity_Id;
  68    --  Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
  69    --  a reference to a Ghost entity. Return Empty if there is no such entity.
  70
  71    function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
  72    --  Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether
  73    --  declaration or body N is subject to aspect or pragma Ghost. Use this
  74    --  routine in cases where [source] pragma Ghost has not been analyzed yet,
  75    --  but the context needs to establish the "ghostness" of N.
  76
  77    procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
  78    --  Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
  79    --  Signal all enclosing scopes that they now contain ignored Ghost code.
  80    --  Add the compilation unit containing N to table Ignored_Ghost_Units for
  81    --  post processing.
  82
  83    ----------------------------
  84    -- Add_Ignored_Ghost_Unit --
  85    ----------------------------
  86
  87    procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is
  88    begin
  89       pragma Assert (Nkind (Unit) = N_Compilation_Unit);
  90
  91       --  Avoid duplicates in the table as pruning the same unit more than once
  92       --  is wasteful. Since ignored Ghost code tends to be grouped up, check
  93       --  the contents of the table in reverse.
  94
  95       for Index in reverse Ignored_Ghost_Units.First ..
  96                            Ignored_Ghost_Units.Last
  97       loop
  98          --  If the unit is already present in the table, do not add it again
  99
 100          if Unit = Ignored_Ghost_Units.Table (Index) then
 101             return;
 102          end if;
 103       end loop;
 104
 105       --  If we get here, then this is the first time the unit is being added
 106
 107       Ignored_Ghost_Units.Append (Unit);
 108    end Add_Ignored_Ghost_Unit;
 109
 110    ----------------------------
 111    -- Check_Ghost_Completion --
 112    ----------------------------
 113
 114    procedure Check_Ghost_Completion
 115      (Partial_View : Entity_Id;
 116       Full_View    : Entity_Id)
 117    is
 118       Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
 119
 120    begin
 121       --  The Ghost policy in effect at the point of declaration and at the
 122       --  point of completion must match (SPARK RM 6.9(14)).
 123
 124       if Is_Checked_Ghost_Entity (Partial_View)
 125         and then Policy = Name_Ignore
 126       then
 127          Error_Msg_Sloc := Sloc (Full_View);
 128
 129          Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
 130          Error_Msg_N ("\& declared with ghost policy `Check`", Partial_View);
 131          Error_Msg_N ("\& completed # with ghost policy `Ignore`",
 132                                                                Partial_View);
 133
 134       elsif Is_Ignored_Ghost_Entity (Partial_View)
 135         and then Policy = Name_Check
 136       then
 137          Error_Msg_Sloc := Sloc (Full_View);
 138
 139          Error_Msg_N ("incompatible ghost policies in effect",  Partial_View);
 140          Error_Msg_N ("\& declared with ghost policy `Ignore`", Partial_View);
 141          Error_Msg_N ("\& completed # with ghost policy `Check`",
 142                                                                 Partial_View);
 143       end if;
 144    end Check_Ghost_Completion;
 145
 146    -------------------------
 147    -- Check_Ghost_Context --
 148    -------------------------
 149
 150    procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
 151       procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
 152       --  Verify that the Ghost policy at the point of declaration of entity Id
 153       --  matches the policy at the point of reference. If this is not the case
 154       --  emit an error at Err_N.
 155
 156       function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
 157       --  Determine whether node Context denotes a Ghost-friendly context where
 158       --  a Ghost entity can safely reside (SPARK RM 6.9(10)).
 159
 160       -------------------------
 161       -- Is_OK_Ghost_Context --
 162       -------------------------
 163
 164       function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
 165          function Is_OK_Declaration (Decl : Node_Id) return Boolean;
 166          --  Determine whether node Decl is a suitable context for a reference
 167          --  to a Ghost entity. To qualify as such, Decl must either
 168          --    1) Be subject to pragma Ghost
 169          --    2) Rename a Ghost entity
 170
 171          function Is_OK_Pragma (Prag : Node_Id) return Boolean;
 172          --  Determine whether node Prag is a suitable context for a reference
 173          --  to a Ghost entity. To qualify as such, Prag must either
 174          --    1) Be an assertion expression pragma
 175          --    2) Denote pragma Global, Depends, Initializes, Refined_Global,
 176          --       Refined_Depends or Refined_State
 177          --    3) Specify an aspect of a Ghost entity
 178          --    4) Contain a reference to a Ghost entity
 179
 180          function Is_OK_Statement (Stmt : Node_Id) return Boolean;
 181          --  Determine whether node Stmt is a suitable context for a reference
 182          --  to a Ghost entity. To qualify as such, Stmt must either
 183          --    1) Denote a call to a Ghost procedure
 184          --    2) Denote an assignment statement whose target is Ghost
 185
 186          -----------------------
 187          -- Is_OK_Declaration --
 188          -----------------------
 189
 190          function Is_OK_Declaration (Decl : Node_Id) return Boolean is
 191             function In_Subprogram_Body_Profile (N : Node_Id) return Boolean;
 192             --  Determine whether node N appears in the profile of a subprogram
 193             --  body.
 194
 195             function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
 196             --  Determine whether node Ren_Decl denotes a renaming declaration
 197             --  with a Ghost name.
 198
 199             --------------------------------
 200             -- In_Subprogram_Body_Profile --
 201             --------------------------------
 202
 203             function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is
 204                Spec : constant Node_Id := Parent (N);
 205
 206             begin
 207                --  The node appears in a parameter specification in which case
 208                --  it is either the parameter type or the default expression or
 209                --  the node appears as the result definition of a function.
 210
 211                return
 212                  (Nkind (N) = N_Parameter_Specification
 213                    or else
 214                      (Nkind (Spec) = N_Function_Specification
 215                        and then N = Result_Definition (Spec)))
 216                    and then Nkind (Parent (Spec)) = N_Subprogram_Body;
 217             end In_Subprogram_Body_Profile;
 218
 219             -----------------------
 220             -- Is_Ghost_Renaming --
 221             -----------------------
 222
 223             function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is
 224                Nam_Id : Entity_Id;
 225
 226             begin
 227                if Is_Renaming_Declaration (Ren_Decl) then
 228                   Nam_Id := Ghost_Entity (Name (Ren_Decl));
 229
 230                   return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
 231                end if;
 232
 233                return False;
 234             end Is_Ghost_Renaming;
 235
 236             --  Local variables
 237
 238             Subp_Decl : Node_Id;
 239             Subp_Id   : Entity_Id;
 240
 241          --  Start of processing for Is_OK_Declaration
 242
 243          begin
 244             if Is_Declaration (Decl) then
 245
 246                --  A renaming declaration is Ghost when it renames a Ghost
 247                --  entity.
 248
 249                if Is_Ghost_Renaming (Decl) then
 250                   return True;
 251
 252                --  The declaration may not have been analyzed yet, determine
 253                --  whether it is subject to pragma Ghost.
 254
 255                elsif Is_Subject_To_Ghost (Decl) then
 256                   return True;
 257                end if;
 258
 259             --  Special cases
 260
 261             --  A reference to a Ghost entity may appear within the profile of
 262             --  a subprogram body. This context is treated as suitable because
 263             --  it duplicates the context of the corresponding spec. The real
 264             --  check was already performed during the analysis of the spec.
 265
 266             elsif In_Subprogram_Body_Profile (Decl) then
 267                return True;
 268
 269             --  A reference to a Ghost entity may appear within an expression
 270             --  function which is still being analyzed. This context is treated
 271             --  as suitable because it is not yet known whether the expression
 272             --  function is an initial declaration or a completion. The real
 273             --  check is performed when the expression function is expanded.
 274
 275             elsif Nkind (Decl) = N_Expression_Function
 276               and then not Analyzed (Decl)
 277             then
 278                return True;
 279
 280             --  References to Ghost entities may be relocated in internally
 281             --  generated bodies.
 282
 283             elsif Nkind (Decl) = N_Subprogram_Body
 284               and then not Comes_From_Source (Decl)
 285             then
 286                Subp_Id := Corresponding_Spec (Decl);
 287
 288                if Present (Subp_Id) then
 289
 290                   --  The context is the internally built _Postconditions
 291                   --  procedure, which is OK because the real check was done
 292                   --  before expansion activities.
 293
 294                   if Chars (Subp_Id) = Name_uPostconditions then
 295                      return True;
 296
 297                   else
 298                      Subp_Decl :=
 299                        Original_Node (Unit_Declaration_Node (Subp_Id));
 300
 301                      --  The original context is an expression function that
 302                      --  has been split into a spec and a body. The context is
 303                      --  OK as long as the initial declaration is Ghost.
 304
 305                      if Nkind (Subp_Decl) = N_Expression_Function then
 306                         return Is_Subject_To_Ghost (Subp_Decl);
 307                      end if;
 308                   end if;
 309
 310                --  Otherwise this is either an internal body or an internal
 311                --  completion. Both are OK because the real check was done
 312                --  before expansion activities.
 313
 314                else
 315                   return True;
 316                end if;
 317             end if;
 318
 319             return False;
 320          end Is_OK_Declaration;
 321
 322          ------------------
 323          -- Is_OK_Pragma --
 324          ------------------
 325
 326          function Is_OK_Pragma (Prag : Node_Id) return Boolean is
 327             procedure Check_Policies (Prag_Nam : Name_Id);
 328             --  Verify that the Ghost policy in effect is the same as the
 329             --  assertion policy for pragma name Prag_Nam. Emit an error if
 330             --  this is not the case.
 331
 332             --------------------
 333             -- Check_Policies --
 334             --------------------
 335
 336             procedure Check_Policies (Prag_Nam : Name_Id) is
 337                AP : constant Name_Id := Check_Kind (Prag_Nam);
 338                GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
 339
 340             begin
 341                --  If the Ghost policy in effect at the point of a Ghost entity
 342                --  reference is Ignore, then the assertion policy of the pragma
 343                --  must be Ignore (SPARK RM 6.9(18)).
 344
 345                if GP = Name_Ignore and then AP /= Name_Ignore then
 346                   Error_Msg_N
 347                     ("incompatible ghost policies in effect",
 348                      Ghost_Ref);
 349                   Error_Msg_NE
 350                     ("\ghost entity & has policy `Ignore`",
 351                      Ghost_Ref, Ghost_Id);
 352
 353                   Error_Msg_Name_1 := AP;
 354                   Error_Msg_N
 355                     ("\assertion expression has policy %", Ghost_Ref);
 356                end if;
 357             end Check_Policies;
 358
 359             --  Local variables
 360
 361             Arg      : Node_Id;
 362             Arg_Id   : Entity_Id;
 363             Prag_Id  : Pragma_Id;
 364             Prag_Nam : Name_Id;
 365
 366          --  Start of processing for Is_OK_Pragma
 367
 368          begin
 369             if Nkind (Prag) = N_Pragma then
 370                Prag_Id  := Get_Pragma_Id (Prag);
 371                Prag_Nam := Original_Aspect_Pragma_Name (Prag);
 372
 373                --  A pragma that applies to a Ghost construct or specifies an
 374                --  aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
 375
 376                if Is_Ghost_Pragma (Prag) then
 377                   return True;
 378
 379                --  An assertion expression pragma is Ghost when it contains a
 380                --  reference to a Ghost entity (SPARK RM 6.9(10)).
 381
 382                elsif Assertion_Expression_Pragma (Prag_Id) then
 383
 384                   --  Ensure that the assertion policy and the Ghost policy are
 385                   --  compatible (SPARK RM 6.9(18)).
 386
 387                   Check_Policies (Prag_Nam);
 388                   return True;
 389
 390                --  Several pragmas that may apply to a non-Ghost entity are
 391                --  treated as Ghost when they contain a reference to a Ghost
 392                --  entity (SPARK RM 6.9(11)).
 393
 394                elsif Nam_In (Prag_Nam, Name_Global,
 395                                        Name_Depends,
 396                                        Name_Initializes,
 397                                        Name_Refined_Global,
 398                                        Name_Refined_Depends,
 399                                        Name_Refined_State)
 400                then
 401                   return True;
 402
 403                --  Otherwise a normal pragma is Ghost when it encloses a Ghost
 404                --  name (SPARK RM 6.9(3)).
 405
 406                else
 407                   Arg := First (Pragma_Argument_Associations (Prag));
 408                   while Present (Arg) loop
 409                      Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
 410
 411                      if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
 412                         return True;
 413                      end if;
 414
 415                      Next (Arg);
 416                   end loop;
 417                end if;
 418             end if;
 419
 420             return False;
 421          end Is_OK_Pragma;
 422
 423          ---------------------
 424          -- Is_OK_Statement --
 425          ---------------------
 426
 427          function Is_OK_Statement (Stmt : Node_Id) return Boolean is
 428             Nam_Id : Entity_Id;
 429
 430          begin
 431             --  An assignment statement or a procedure call is Ghost when the
 432             --  name denotes a Ghost entity.
 433
 434             if Nkind_In (Stmt, N_Assignment_Statement,
 435                                N_Procedure_Call_Statement)
 436             then
 437                Nam_Id := Ghost_Entity (Name (Stmt));
 438
 439                return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
 440
 441             --  Special cases
 442
 443             --  An if statement is a suitable context for a Ghost entity if it
 444             --  is the byproduct of assertion expression expansion. Note that
 445             --  the assertion expression may not be related to a Ghost entity,
 446             --  but it may still contain references to Ghost entities.
 447
 448             elsif Nkind (Stmt) = N_If_Statement
 449               and then Nkind (Original_Node (Stmt)) = N_Pragma
 450               and then Assertion_Expression_Pragma
 451                          (Get_Pragma_Id (Original_Node (Stmt)))
 452             then
 453                return True;
 454             end if;
 455
 456             return False;
 457          end Is_OK_Statement;
 458
 459          --  Local variables
 460
 461          Par : Node_Id;
 462
 463       --  Start of processing for Is_OK_Ghost_Context
 464
 465       begin
 466          --  The context is Ghost when it appears within a Ghost package or
 467          --  subprogram.
 468
 469          if Ghost_Mode > None then
 470             return True;
 471
 472          --  Routine Expand_Record_Extension creates a parent subtype without
 473          --  inserting it into the tree. There is no good way of recognizing
 474          --  this special case as there is no parent. Try to approximate the
 475          --  context.
 476
 477          elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
 478             return True;
 479
 480          --  Otherwise climb the parent chain looking for a suitable Ghost
 481          --  context.
 482
 483          else
 484             Par := Context;
 485             while Present (Par) loop
 486                if Is_Ignored_Ghost_Node (Par) then
 487                   return True;
 488
 489                --  A reference to a Ghost entity can appear within an aspect
 490                --  specification (SPARK RM 6.9(10)).
 491
 492                elsif Nkind (Par) = N_Aspect_Specification then
 493                   return True;
 494
 495                elsif Is_OK_Declaration (Par) then
 496                   return True;
 497
 498                elsif Is_OK_Pragma (Par) then
 499                   return True;
 500
 501                elsif Is_OK_Statement (Par) then
 502                   return True;
 503
 504                --  Prevent the search from going too far
 505
 506                elsif Is_Body_Or_Package_Declaration (Par) then
 507                   exit;
 508                end if;
 509
 510                Par := Parent (Par);
 511             end loop;
 512
 513             --  The expansion of assertion expression pragmas and attribute Old
 514             --  may cause a legal Ghost entity reference to become illegal due
 515             --  to node relocation. Check the In_Assertion_Expr counter as last
 516             --  resort to try and infer the original legal context.
 517
 518             if In_Assertion_Expr > 0 then
 519                return True;
 520
 521             --  Otherwise the context is not suitable for a reference to a
 522             --  Ghost entity.
 523
 524             else
 525                return False;
 526             end if;
 527          end if;
 528       end Is_OK_Ghost_Context;
 529
 530       ------------------------
 531       -- Check_Ghost_Policy --
 532       ------------------------
 533
 534       procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
 535          Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
 536
 537       begin
 538          --  The Ghost policy in effect a the point of declaration and at the
 539          --  point of use must match (SPARK RM 6.9(13)).
 540
 541          if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
 542             Error_Msg_Sloc := Sloc (Err_N);
 543
 544             Error_Msg_N  ("incompatible ghost policies in effect", Err_N);
 545             Error_Msg_NE ("\& declared with ghost policy `Check`", Err_N, Id);
 546             Error_Msg_NE ("\& used # with ghost policy `Ignore`",  Err_N, Id);
 547
 548          elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
 549             Error_Msg_Sloc := Sloc (Err_N);
 550
 551             Error_Msg_N  ("incompatible ghost policies in effect",  Err_N);
 552             Error_Msg_NE ("\& declared with ghost policy `Ignore`", Err_N, Id);
 553             Error_Msg_NE ("\& used # with ghost policy `Check`",    Err_N, Id);
 554          end if;
 555       end Check_Ghost_Policy;
 556
 557    --  Start of processing for Check_Ghost_Context
 558
 559    begin
 560       --  Once it has been established that the reference to the Ghost entity
 561       --  is within a suitable context, ensure that the policy at the point of
 562       --  declaration and at the point of use match.
 563
 564       if Is_OK_Ghost_Context (Ghost_Ref) then
 565          Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
 566
 567       --  Otherwise the Ghost entity appears in a non-Ghost context and affects
 568       --  its behavior or value (SPARK RM 6.9(11,12)).
 569
 570       else
 571          Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
 572       end if;
 573    end Check_Ghost_Context;
 574
 575    ----------------------------
 576    -- Check_Ghost_Overriding --
 577    ----------------------------
 578
 579    procedure Check_Ghost_Overriding
 580      (Subp            : Entity_Id;
 581       Overridden_Subp : Entity_Id)
 582    is
 583       Deriv_Typ : Entity_Id;
 584       Over_Subp : Entity_Id;
 585
 586    begin
 587       if Present (Subp) and then Present (Overridden_Subp) then
 588          Over_Subp := Ultimate_Alias (Overridden_Subp);
 589          Deriv_Typ := Find_Dispatching_Type (Subp);
 590
 591          --  A Ghost primitive of a non-Ghost type extension cannot override an
 592          --  inherited non-Ghost primitive (SPARK RM 6.9(8)).
 593
 594          if Is_Ghost_Entity (Subp)
 595            and then Present (Deriv_Typ)
 596            and then not Is_Ghost_Entity (Deriv_Typ)
 597            and then not Is_Ghost_Entity (Over_Subp)
 598          then
 599             Error_Msg_N ("incompatible overriding in effect", Subp);
 600
 601             Error_Msg_Sloc := Sloc (Over_Subp);
 602             Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
 603
 604             Error_Msg_Sloc := Sloc (Subp);
 605             Error_Msg_N ("\overridden # with ghost subprogram", Subp);
 606          end if;
 607
 608          --  A non-Ghost primitive of a type extension cannot override an
 609          --  inherited Ghost primitive (SPARK RM 6.9(8)).
 610
 611          if not Is_Ghost_Entity (Subp)
 612            and then Is_Ghost_Entity (Over_Subp)
 613          then
 614             Error_Msg_N ("incompatible overriding in effect", Subp);
 615
 616             Error_Msg_Sloc := Sloc (Over_Subp);
 617             Error_Msg_N ("\& declared # as ghost subprogram", Subp);
 618
 619             Error_Msg_Sloc := Sloc (Subp);
 620             Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
 621          end if;
 622
 623          if Present (Deriv_Typ)
 624            and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
 625          then
 626             --  When a tagged type is either non-Ghost or checked Ghost and
 627             --  one of its primitives overrides an inherited operation, the
 628             --  overridden operation of the ancestor type must be ignored Ghost
 629             --  if the primitive is ignored Ghost (SPARK RM 6.9(17)).
 630
 631             if Is_Ignored_Ghost_Entity (Subp) then
 632
 633                --  Both the parent subprogram and overriding subprogram are
 634                --  ignored Ghost.
 635
 636                if Is_Ignored_Ghost_Entity (Over_Subp) then
 637                   null;
 638
 639                --  The parent subprogram carries policy Check
 640
 641                elsif Is_Checked_Ghost_Entity (Over_Subp) then
 642                   Error_Msg_N
 643                     ("incompatible ghost policies in effect", Subp);
 644
 645                   Error_Msg_Sloc := Sloc (Over_Subp);
 646                   Error_Msg_N
 647                     ("\& declared # with ghost policy `Check`", Subp);
 648
 649                   Error_Msg_Sloc := Sloc (Subp);
 650                   Error_Msg_N
 651                     ("\overridden # with ghost policy `Ignore`", Subp);
 652
 653                --  The parent subprogram is non-Ghost
 654
 655                else
 656                   Error_Msg_N
 657                     ("incompatible ghost policies in effect", Subp);
 658
 659                   Error_Msg_Sloc := Sloc (Over_Subp);
 660                   Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
 661
 662                   Error_Msg_Sloc := Sloc (Subp);
 663                   Error_Msg_N
 664                     ("\overridden # with ghost policy `Ignore`", Subp);
 665                end if;
 666
 667             --  When a tagged type is either non-Ghost or checked Ghost and
 668             --  one of its primitives overrides an inherited operation, the
 669             --  the primitive of the tagged type must be ignored Ghost if the
 670             --  overridden operation is ignored Ghost (SPARK RM 6.9(17)).
 671
 672             elsif Is_Ignored_Ghost_Entity (Over_Subp) then
 673
 674                --  Both the parent subprogram and the overriding subprogram are
 675                --  ignored Ghost.
 676
 677                if Is_Ignored_Ghost_Entity (Subp) then
 678                   null;
 679
 680                --  The overriding subprogram carries policy Check
 681
 682                elsif Is_Checked_Ghost_Entity (Subp) then
 683                   Error_Msg_N
 684                     ("incompatible ghost policies in effect", Subp);
 685
 686                   Error_Msg_Sloc := Sloc (Over_Subp);
 687                   Error_Msg_N
 688                     ("\& declared # with ghost policy `Ignore`", Subp);
 689
 690                   Error_Msg_Sloc := Sloc (Subp);
 691                   Error_Msg_N
 692                     ("\overridden # with Ghost policy `Check`", Subp);
 693
 694                --  The overriding subprogram is non-Ghost
 695
 696                else
 697                   Error_Msg_N
 698                     ("incompatible ghost policies in effect", Subp);
 699
 700                   Error_Msg_Sloc := Sloc (Over_Subp);
 701                   Error_Msg_N
 702                     ("\& declared # with ghost policy `Ignore`", Subp);
 703
 704                   Error_Msg_Sloc := Sloc (Subp);
 705                   Error_Msg_N
 706                     ("\overridden # with non-ghost subprogram", Subp);
 707                end if;
 708             end if;
 709          end if;
 710       end if;
 711    end Check_Ghost_Overriding;
 712
 713    ---------------------------
 714    -- Check_Ghost_Primitive --
 715    ---------------------------
 716
 717    procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
 718    begin
 719       --  The Ghost policy in effect at the point of declaration of a primitive
 720       --  operation and a tagged type must match (SPARK RM 6.9(16)).
 721
 722       if Is_Tagged_Type (Typ) then
 723          if Is_Checked_Ghost_Entity (Prim)
 724            and then Is_Ignored_Ghost_Entity (Typ)
 725          then
 726             Error_Msg_N ("incompatible ghost policies in effect", Prim);
 727
 728             Error_Msg_Sloc := Sloc (Typ);
 729             Error_Msg_NE
 730               ("\tagged type & declared # with ghost policy `Ignore`",
 731                Prim, Typ);
 732
 733             Error_Msg_Sloc := Sloc (Prim);
 734             Error_Msg_N
 735               ("\primitive subprogram & declared # with ghost policy `Check`",
 736                Prim);
 737
 738          elsif Is_Ignored_Ghost_Entity (Prim)
 739            and then Is_Checked_Ghost_Entity (Typ)
 740          then
 741             Error_Msg_N ("incompatible ghost policies in effect", Prim);
 742
 743             Error_Msg_Sloc := Sloc (Typ);
 744             Error_Msg_NE
 745               ("\tagged type & declared # with ghost policy `Check`",
 746                Prim, Typ);
 747
 748             Error_Msg_Sloc := Sloc (Prim);
 749             Error_Msg_N
 750               ("\primitive subprogram & declared # with ghost policy `Ignore`",
 751                Prim);
 752          end if;
 753       end if;
 754    end Check_Ghost_Primitive;
 755
 756    ----------------------------
 757    -- Check_Ghost_Refinement --
 758    ----------------------------
 759
 760    procedure Check_Ghost_Refinement
 761      (State      : Node_Id;
 762       State_Id   : Entity_Id;
 763       Constit    : Node_Id;
 764       Constit_Id : Entity_Id)
 765    is
 766    begin
 767       if Is_Ghost_Entity (State_Id) then
 768          if Is_Ghost_Entity (Constit_Id) then
 769
 770             --  The Ghost policy in effect at the point of abstract state
 771             --  declaration and constituent must match (SPARK RM 6.9(15)).
 772
 773             if Is_Checked_Ghost_Entity (State_Id)
 774               and then Is_Ignored_Ghost_Entity (Constit_Id)
 775             then
 776                Error_Msg_Sloc := Sloc (Constit);
 777                SPARK_Msg_N ("incompatible ghost policies in effect", State);
 778
 779                SPARK_Msg_NE
 780                  ("\abstract state & declared with ghost policy `Check`",
 781                   State, State_Id);
 782                SPARK_Msg_NE
 783                  ("\constituent & declared # with ghost policy `Ignore`",
 784                   State, Constit_Id);
 785
 786             elsif Is_Ignored_Ghost_Entity (State_Id)
 787               and then Is_Checked_Ghost_Entity (Constit_Id)
 788             then
 789                Error_Msg_Sloc := Sloc (Constit);
 790                SPARK_Msg_N ("incompatible ghost policies in effect", State);
 791
 792                SPARK_Msg_NE
 793                  ("\abstract state & declared with ghost policy `Ignore`",
 794                   State, State_Id);
 795                SPARK_Msg_NE
 796                  ("\constituent & declared # with ghost policy `Check`",
 797                   State, Constit_Id);
 798             end if;
 799
 800             --  A constituent of a Ghost abstract state must be a Ghost entity
 801             --  (SPARK RM 7.2.2(12)).
 802
 803          else
 804             SPARK_Msg_NE
 805               ("constituent of ghost state & must be ghost",
 806                Constit, State_Id);
 807          end if;
 808       end if;
 809    end Check_Ghost_Refinement;
 810
 811    ------------------
 812    -- Ghost_Entity --
 813    ------------------
 814
 815    function Ghost_Entity (N : Node_Id) return Entity_Id is
 816       Ref : Node_Id;
 817
 818    begin
 819       --  When the reference extracts a subcomponent, recover the related
 820       --  object (SPARK RM 6.9(1)).
 821
 822       Ref := N;
 823       while Nkind_In (Ref, N_Explicit_Dereference,
 824                            N_Indexed_Component,
 825                            N_Selected_Component,
 826                            N_Slice)
 827       loop
 828          Ref := Prefix (Ref);
 829       end loop;
 830
 831       if Is_Entity_Name (Ref) then
 832          return Entity (Ref);
 833       else
 834          return Empty;
 835       end if;
 836    end Ghost_Entity;
 837
 838    --------------------------------
 839    -- Implements_Ghost_Interface --
 840    --------------------------------
 841
 842    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
 843       Iface_Elmt : Elmt_Id;
 844
 845    begin
 846       --  Traverse the list of interfaces looking for a Ghost interface
 847
 848       if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
 849          Iface_Elmt := First_Elmt (Interfaces (Typ));
 850          while Present (Iface_Elmt) loop
 851             if Is_Ghost_Entity (Node (Iface_Elmt)) then
 852                return True;
 853             end if;
 854
 855             Next_Elmt (Iface_Elmt);
 856          end loop;
 857       end if;
 858
 859       return False;
 860    end Implements_Ghost_Interface;
 861
 862    ----------------
 863    -- Initialize --
 864    ----------------
 865
 866    procedure Initialize is
 867    begin
 868       Ignored_Ghost_Units.Init;
 869    end Initialize;
 870
 871    -------------------------
 872    -- Is_Subject_To_Ghost --
 873    -------------------------
 874
 875    function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
 876       function Enables_Ghostness (Arg : Node_Id) return Boolean;
 877       --  Determine whether aspect or pragma argument Arg enables "ghostness"
 878
 879       -----------------------
 880       -- Enables_Ghostness --
 881       -----------------------
 882
 883       function Enables_Ghostness (Arg : Node_Id) return Boolean is
 884          Expr : Node_Id;
 885
 886       begin
 887          Expr := Arg;
 888
 889          if Nkind (Expr) = N_Pragma_Argument_Association then
 890             Expr := Get_Pragma_Arg (Expr);
 891          end if;
 892
 893          --  Determine whether the expression of the aspect or pragma is static
 894          --  and denotes True.
 895
 896          if Present (Expr) then
 897             Preanalyze_And_Resolve (Expr);
 898
 899             return
 900               Is_OK_Static_Expression (Expr)
 901                 and then Is_True (Expr_Value (Expr));
 902
 903          --  Otherwise Ghost defaults to True
 904
 905          else
 906             return True;
 907          end if;
 908       end Enables_Ghostness;
 909
 910       --  Local variables
 911
 912       Id      : constant Entity_Id := Defining_Entity (N);
 913       Asp     : Node_Id;
 914       Decl    : Node_Id;
 915       Prev_Id : Entity_Id;
 916
 917    --  Start of processing for Is_Subject_To_Ghost
 918
 919    begin
 920       --  The related entity of the declaration has not been analyzed yet, do
 921       --  not inspect its attributes.
 922
 923       if Ekind (Id) = E_Void then
 924          null;
 925
 926       elsif Is_Ghost_Entity (Id) then
 927          return True;
 928
 929       --  The completion of a type or a constant is not fully analyzed when the
 930       --  reference to the Ghost entity is resolved. Because the completion is
 931       --  not marked as Ghost yet, inspect the partial view.
 932
 933       elsif Is_Record_Type (Id)
 934         or else Ekind (Id) = E_Constant
 935         or else (Nkind (N) = N_Object_Declaration
 936                   and then Constant_Present (N))
 937       then
 938          Prev_Id := Incomplete_Or_Partial_View (Id);
 939
 940          if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
 941             return True;
 942          end if;
 943       end if;
 944
 945       --  Examine the aspect specifications (if any) looking for aspect Ghost
 946
 947       if Permits_Aspect_Specifications (N) then
 948          Asp := First (Aspect_Specifications (N));
 949          while Present (Asp) loop
 950             if Chars (Identifier (Asp)) = Name_Ghost then
 951                return Enables_Ghostness (Expression (Asp));
 952             end if;
 953
 954             Next (Asp);
 955          end loop;
 956       end if;
 957
 958       Decl := Empty;
 959
 960       --  When the context is a [generic] package declaration, pragma Ghost
 961       --  resides in the visible declarations.
 962
 963       if Nkind_In (N, N_Generic_Package_Declaration,
 964                       N_Package_Declaration)
 965       then
 966          Decl := First (Visible_Declarations (Specification (N)));
 967
 968       --  When the context is a package or a subprogram body, pragma Ghost
 969       --  resides in the declarative part.
 970
 971       elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
 972          Decl := First (Declarations (N));
 973
 974       --  Otherwise pragma Ghost appears in the declarations following N
 975
 976       elsif Is_List_Member (N) then
 977          Decl := Next (N);
 978       end if;
 979
 980       while Present (Decl) loop
 981          if Nkind (Decl) = N_Pragma
 982            and then Pragma_Name (Decl) = Name_Ghost
 983          then
 984             return
 985               Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
 986
 987          --  A source construct ends the region where pragma Ghost may appear,
 988          --  stop the traversal. Check the original node as source constructs
 989          --  may be rewritten into something else by expansion.
 990
 991          elsif Comes_From_Source (Original_Node (Decl)) then
 992             exit;
 993          end if;
 994
 995          Next (Decl);
 996       end loop;
 997
 998       return False;
 999    end Is_Subject_To_Ghost;
1000
1001    ----------
1002    -- Lock --
1003    ----------
1004
1005    procedure Lock is
1006    begin
1007       Ignored_Ghost_Units.Locked := True;
1008       Ignored_Ghost_Units.Release;
1009    end Lock;
1010
1011    -----------------------------
1012    -- Mark_Full_View_As_Ghost --
1013    -----------------------------
1014
1015    procedure Mark_Full_View_As_Ghost
1016      (Priv_Typ : Entity_Id;
1017       Full_Typ : Entity_Id)
1018    is
1019       Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
1020
1021    begin
1022       if Is_Checked_Ghost_Entity (Priv_Typ) then
1023          Set_Is_Checked_Ghost_Entity (Full_Typ);
1024
1025       elsif Is_Ignored_Ghost_Entity (Priv_Typ) then
1026          Set_Is_Ignored_Ghost_Entity (Full_Typ);
1027          Set_Is_Ignored_Ghost_Node (Full_Decl);
1028          Propagate_Ignored_Ghost_Code (Full_Decl);
1029       end if;
1030    end Mark_Full_View_As_Ghost;
1031
1032    --------------------------
1033    -- Mark_Pragma_As_Ghost --
1034    --------------------------
1035
1036    procedure Mark_Pragma_As_Ghost
1037      (Prag       : Node_Id;
1038       Context_Id : Entity_Id)
1039    is
1040    begin
1041       if Is_Checked_Ghost_Entity (Context_Id) then
1042          Set_Is_Ghost_Pragma (Prag);
1043
1044       elsif Is_Ignored_Ghost_Entity (Context_Id) then
1045          Set_Is_Ghost_Pragma (Prag);
1046          Set_Is_Ignored_Ghost_Node (Prag);
1047          Propagate_Ignored_Ghost_Code (Prag);
1048       end if;
1049    end Mark_Pragma_As_Ghost;
1050
1051    ----------------------------
1052    -- Mark_Renaming_As_Ghost --
1053    ----------------------------
1054
1055    procedure Mark_Renaming_As_Ghost
1056      (Ren_Decl : Node_Id;
1057       Nam_Id   : Entity_Id)
1058    is
1059       Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
1060
1061    begin
1062       if Is_Checked_Ghost_Entity (Nam_Id) then
1063          Set_Is_Checked_Ghost_Entity (Ren_Id);
1064
1065       elsif Is_Ignored_Ghost_Entity (Nam_Id) then
1066          Set_Is_Ignored_Ghost_Entity (Ren_Id);
1067          Set_Is_Ignored_Ghost_Node (Ren_Decl);
1068          Propagate_Ignored_Ghost_Code (Ren_Decl);
1069       end if;
1070    end Mark_Renaming_As_Ghost;
1071
1072    ----------------------------------
1073    -- Propagate_Ignored_Ghost_Code --
1074    ----------------------------------
1075
1076    procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is
1077       Nod  : Node_Id;
1078       Scop : Entity_Id;
1079
1080    begin
1081       --  Traverse the parent chain looking for blocks, packages and
1082       --  subprograms or their respective bodies.
1083
1084       Nod := Parent (N);
1085       while Present (Nod) loop
1086          Scop := Empty;
1087
1088          if Nkind (Nod) = N_Block_Statement then
1089             Scop := Entity (Identifier (Nod));
1090
1091          elsif Nkind_In (Nod, N_Package_Body,
1092                               N_Package_Declaration,
1093                               N_Subprogram_Body,
1094                               N_Subprogram_Declaration)
1095          then
1096             Scop := Defining_Entity (Nod);
1097          end if;
1098
1099          --  The current node denotes a scoping construct
1100
1101          if Present (Scop) then
1102
1103             --  Stop the traversal when the scope already contains ignored
1104             --  Ghost code as all enclosing scopes have already been marked.
1105
1106             if Contains_Ignored_Ghost_Code (Scop) then
1107                exit;
1108
1109             --  Otherwise mark this scope and keep climbing
1110
1111             else
1112                Set_Contains_Ignored_Ghost_Code (Scop);
1113             end if;
1114          end if;
1115
1116          Nod := Parent (Nod);
1117       end loop;
1118
1119       --  The unit containing the ignored Ghost code must be post processed
1120       --  before invoking the back end.
1121
1122       Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N)));
1123    end Propagate_Ignored_Ghost_Code;
1124
1125    -------------------------------
1126    -- Remove_Ignored_Ghost_Code --
1127    -------------------------------
1128
1129    procedure Remove_Ignored_Ghost_Code is
1130       procedure Prune_Tree (Root : Node_Id);
1131       --  Remove all code marked as ignored Ghost from the tree of denoted by
1132       --  Root.
1133
1134       ----------------
1135       -- Prune_Tree --
1136       ----------------
1137
1138       procedure Prune_Tree (Root : Node_Id) is
1139          procedure Prune (N : Node_Id);
1140          --  Remove a given node from the tree by rewriting it into null
1141
1142          function Prune_Node (N : Node_Id) return Traverse_Result;
1143          --  Determine whether node N denotes an ignored Ghost construct. If
1144          --  this is the case, rewrite N as a null statement. See the body for
1145          --  special cases.
1146
1147          -----------
1148          -- Prune --
1149          -----------
1150
1151          procedure Prune (N : Node_Id) is
1152          begin
1153             --  Destroy any aspects that may be associated with the node
1154
1155             if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
1156                Remove_Aspects (N);
1157             end if;
1158
1159             Rewrite (N, Make_Null_Statement (Sloc (N)));
1160          end Prune;
1161
1162          ----------------
1163          -- Prune_Node --
1164          ----------------
1165
1166          function Prune_Node (N : Node_Id) return Traverse_Result is
1167             Id : Entity_Id;
1168
1169          begin
1170             --  The node is either declared as ignored Ghost or is a byproduct
1171             --  of expansion. Destroy it and stop the traversal on this branch.
1172
1173             if Is_Ignored_Ghost_Node (N) then
1174                Prune (N);
1175                return Skip;
1176
1177             --  Scoping constructs such as blocks, packages, subprograms and
1178             --  bodies offer some flexibility with respect to pruning.
1179
1180             elsif Nkind_In (N, N_Block_Statement,
1181                                N_Package_Body,
1182                                N_Package_Declaration,
1183                                N_Subprogram_Body,
1184                                N_Subprogram_Declaration)
1185             then
1186                if Nkind (N) = N_Block_Statement then
1187                   Id := Entity (Identifier (N));
1188                else
1189                   Id := Defining_Entity (N);
1190                end if;
1191
1192                --  The scoping construct contains both living and ignored Ghost
1193                --  code, let the traversal prune all relevant nodes.
1194
1195                if Contains_Ignored_Ghost_Code (Id) then
1196                   return OK;
1197
1198                --  Otherwise the construct contains only living code and should
1199                --  not be pruned.
1200
1201                else
1202                   return Skip;
1203                end if;
1204
1205             --  Otherwise keep searching for ignored Ghost nodes
1206
1207             else
1208                return OK;
1209             end if;
1210          end Prune_Node;
1211
1212          procedure Prune_Nodes is new Traverse_Proc (Prune_Node);
1213
1214       --  Start of processing for Prune_Tree
1215
1216       begin
1217          Prune_Nodes (Root);
1218       end Prune_Tree;
1219
1220    --  Start of processing for Remove_Ignored_Ghost_Code
1221
1222    begin
1223       for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
1224          Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
1225       end loop;
1226    end Remove_Ignored_Ghost_Code;
1227
1228    --------------------
1229    -- Set_Ghost_Mode --
1230    --------------------
1231
1232    procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty) is
1233       procedure Set_From_Entity (Ent_Id : Entity_Id);
1234       --  Set the value of global variable Ghost_Mode depending on the mode of
1235       --  entity Ent_Id.
1236
1237       procedure Set_From_Policy;
1238       --  Set the value of global variable Ghost_Mode depending on the current
1239       --  Ghost policy in effect.
1240
1241       ---------------------
1242       -- Set_From_Entity --
1243       ---------------------
1244
1245       procedure Set_From_Entity (Ent_Id : Entity_Id) is
1246       begin
1247          Set_Ghost_Mode_From_Entity (Ent_Id);
1248
1249          if Is_Ignored_Ghost_Entity (Ent_Id) then
1250             Set_Is_Ignored_Ghost_Node (N);
1251             Propagate_Ignored_Ghost_Code (N);
1252          end if;
1253       end Set_From_Entity;
1254
1255       ---------------------
1256       -- Set_From_Policy --
1257       ---------------------
1258
1259       procedure Set_From_Policy is
1260          Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
1261
1262       begin
1263          if Policy = Name_Check then
1264             Ghost_Mode := Check;
1265
1266          elsif Policy = Name_Ignore then
1267             Ghost_Mode := Ignore;
1268
1269             Set_Is_Ignored_Ghost_Node (N);
1270             Propagate_Ignored_Ghost_Code (N);
1271          end if;
1272       end Set_From_Policy;
1273
1274       --  Local variables
1275
1276       Nam_Id : Entity_Id;
1277
1278    --  Start of processing for Set_Ghost_Mode
1279
1280    begin
1281       --  The input node denotes one of the many declaration kinds that may be
1282       --  subject to pragma Ghost.
1283
1284       if Is_Declaration (N) then
1285          if Is_Subject_To_Ghost (N) then
1286             Set_From_Policy;
1287
1288          --  The declaration denotes the completion of a deferred constant,
1289          --  pragma Ghost appears on the partial declaration.
1290
1291          elsif Nkind (N) = N_Object_Declaration
1292            and then Constant_Present (N)
1293            and then Present (Id)
1294          then
1295             Set_From_Entity (Id);
1296
1297          --  The declaration denotes the full view of a private type, pragma
1298          --  Ghost appears on the partial declaration.
1299
1300          elsif Nkind (N) = N_Full_Type_Declaration
1301            and then Is_Private_Type (Defining_Entity (N))
1302            and then Present (Id)
1303          then
1304             Set_From_Entity (Id);
1305          end if;
1306
1307       --  The input denotes an assignment or a procedure call. In this case
1308       --  the Ghost mode is dictated by the name of the construct.
1309
1310       elsif Nkind_In (N, N_Assignment_Statement,
1311                          N_Procedure_Call_Statement)
1312       then
1313          Nam_Id := Ghost_Entity (Name (N));
1314
1315          if Present (Nam_Id) then
1316             Set_From_Entity (Nam_Id);
1317          end if;
1318
1319       --  The input denotes a package or subprogram body
1320
1321       elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
1322          if (Present (Id) and then Is_Ghost_Entity (Id))
1323            or else Is_Subject_To_Ghost (N)
1324          then
1325             Set_From_Policy;
1326          end if;
1327
1328       --  The input denotes a pragma
1329
1330       elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
1331          if Is_Ignored_Ghost_Node (N) then
1332             Ghost_Mode := Ignore;
1333          else
1334             Ghost_Mode := Check;
1335          end if;
1336
1337       --  The input denotes a freeze node
1338
1339       elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
1340          Set_From_Entity (Id);
1341       end if;
1342    end Set_Ghost_Mode;
1343
1344    --------------------------------
1345    -- Set_Ghost_Mode_From_Entity --
1346    --------------------------------
1347
1348    procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
1349    begin
1350       if Is_Checked_Ghost_Entity (Id) then
1351          Ghost_Mode := Check;
1352       elsif Is_Ignored_Ghost_Entity (Id) then
1353          Ghost_Mode := Ignore;
1354       end if;
1355    end Set_Ghost_Mode_From_Entity;
1356
1357    -------------------------
1358    -- Set_Is_Ghost_Entity --
1359    -------------------------
1360
1361    procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
1362       Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
1363    begin
1364       if Policy = Name_Check then
1365          Set_Is_Checked_Ghost_Entity (Id);
1366       elsif Policy = Name_Ignore then
1367          Set_Is_Ignored_Ghost_Entity (Id);
1368       end if;
1369    end Set_Is_Ghost_Entity;
1370
1371 end Ghost;