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-2018, 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;
  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 Namet;    use Namet;
  33 with Nlists;   use Nlists;
  34 with Nmake;    use Nmake;
  35 with Sem;      use Sem;
  36 with Sem_Aux;  use Sem_Aux;
  37 with Sem_Disp; use Sem_Disp;
  38 with Sem_Eval; use Sem_Eval;
  39 with Sem_Prag; use Sem_Prag;
  40 with Sem_Res;  use Sem_Res;
  41 with Sem_Util; use Sem_Util;
  42 with Sinfo;    use Sinfo;
  43 with Snames;   use Snames;
  44 with Table;
  45
  46 package body Ghost is
  47
  48    ---------------------
  49    -- Data strictures --
  50    ---------------------
  51
  52    --  The following table contains all ignored Ghost nodes that must be
  53    --  eliminated from the tree by routine Remove_Ignored_Ghost_Code.
  54
  55    package Ignored_Ghost_Nodes 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_Nodes_Initial,
  60      Table_Increment      => Alloc.Ignored_Ghost_Nodes_Increment,
  61      Table_Name           => "Ignored_Ghost_Nodes");
  62
  63    -----------------------
  64    -- Local subprograms --
  65    -----------------------
  66
  67    function Ghost_Entity (N : Node_Id) return Entity_Id;
  68    --  Find the entity of a reference to a Ghost entity. Return Empty if there
  69    --  is no such entity.
  70
  71    procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
  72    pragma Inline (Install_Ghost_Mode);
  73    --  Install Ghost mode Mode as the Ghost mode in effect
  74
  75    procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id);
  76    pragma Inline (Install_Ghost_Region);
  77    --  Install a Ghost region comprised of mode Mode and ignored region start
  78    --  node N.
  79
  80    function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
  81    --  Determine whether declaration or body N is subject to aspect or pragma
  82    --  Ghost. This routine must be used in cases where pragma Ghost has not
  83    --  been analyzed yet, but the context needs to establish the "ghostness"
  84    --  of N.
  85
  86    procedure Mark_Ghost_Declaration_Or_Body
  87      (N    : Node_Id;
  88       Mode : Name_Id);
  89    --  Mark the defining entity of declaration or body N as Ghost depending on
  90    --  mode Mode. Mark all formals parameters when N denotes a subprogram or a
  91    --  body.
  92
  93    function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type;
  94    pragma Inline (Name_To_Ghost_Mode);
  95    --  Convert a Ghost mode denoted by name Mode into its respective enumerated
  96    --  value.
  97
  98    procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id);
  99    --  Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for
 100    --  later elimination.
 101
 102    ----------------------------
 103    -- Check_Ghost_Completion --
 104    ----------------------------
 105
 106    procedure Check_Ghost_Completion
 107      (Prev_Id  : Entity_Id;
 108       Compl_Id : Entity_Id)
 109    is
 110       Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
 111
 112    begin
 113       --  Nothing to do if one of the views is missing
 114
 115       if No (Prev_Id) or else No (Compl_Id) then
 116          null;
 117
 118       --  The Ghost policy in effect at the point of declaration and at the
 119       --  point of completion must match (SPARK RM 6.9(14)).
 120
 121       elsif Is_Checked_Ghost_Entity (Prev_Id)
 122         and then Policy = Name_Ignore
 123       then
 124          Error_Msg_Sloc := Sloc (Compl_Id);
 125
 126          Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
 127          Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id);
 128          Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id);
 129
 130       elsif Is_Ignored_Ghost_Entity (Prev_Id)
 131         and then Policy = Name_Check
 132       then
 133          Error_Msg_Sloc := Sloc (Compl_Id);
 134
 135          Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
 136          Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id);
 137          Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id);
 138       end if;
 139    end Check_Ghost_Completion;
 140
 141    -------------------------
 142    -- Check_Ghost_Context --
 143    -------------------------
 144
 145    procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
 146       procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id);
 147       --  Verify that the Ghost policy at the point of declaration of entity Id
 148       --  matches the policy at the point of reference Ref. If this is not the
 149       --  case emit an error at Ref.
 150
 151       function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
 152       --  Determine whether node Context denotes a Ghost-friendly context where
 153       --  a Ghost entity can safely reside (SPARK RM 6.9(10)).
 154
 155       -------------------------
 156       -- Is_OK_Ghost_Context --
 157       -------------------------
 158
 159       function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
 160          function Is_OK_Declaration (Decl : Node_Id) return Boolean;
 161          --  Determine whether node Decl is a suitable context for a reference
 162          --  to a Ghost entity. To qualify as such, Decl must either
 163          --
 164          --    * Define a Ghost entity
 165          --
 166          --    * Be subject to pragma Ghost
 167
 168          function Is_OK_Pragma (Prag : Node_Id) return Boolean;
 169          --  Determine whether node Prag is a suitable context for a reference
 170          --  to a Ghost entity. To qualify as such, Prag must either
 171          --
 172          --    * Be an assertion expression pragma
 173          --
 174          --    * Denote pragma Global, Depends, Initializes, Refined_Global,
 175          --      Refined_Depends or Refined_State.
 176          --
 177          --    * Specify an aspect of a Ghost entity
 178          --
 179          --    * Contain a reference to a Ghost entity
 180
 181          function Is_OK_Statement (Stmt : Node_Id) return Boolean;
 182          --  Determine whether node Stmt is a suitable context for a reference
 183          --  to a Ghost entity. To qualify as such, Stmt must either
 184          --
 185          --    * Denote a procedure call to a Ghost procedure
 186          --
 187          --    * Denote an assignment statement whose target is Ghost
 188
 189          -----------------------
 190          -- Is_OK_Declaration --
 191          -----------------------
 192
 193          function Is_OK_Declaration (Decl : Node_Id) return Boolean is
 194             function In_Subprogram_Body_Profile (N : Node_Id) return Boolean;
 195             --  Determine whether node N appears in the profile of a subprogram
 196             --  body.
 197
 198             --------------------------------
 199             -- In_Subprogram_Body_Profile --
 200             --------------------------------
 201
 202             function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is
 203                Spec : constant Node_Id := Parent (N);
 204
 205             begin
 206                --  The node appears in a parameter specification in which case
 207                --  it is either the parameter type or the default expression or
 208                --  the node appears as the result definition of a function.
 209
 210                return
 211                  (Nkind (N) = N_Parameter_Specification
 212                    or else
 213                      (Nkind (Spec) = N_Function_Specification
 214                        and then N = Result_Definition (Spec)))
 215                    and then Nkind (Parent (Spec)) = N_Subprogram_Body;
 216             end In_Subprogram_Body_Profile;
 217
 218             --  Local variables
 219
 220             Subp_Decl : Node_Id;
 221             Subp_Id   : Entity_Id;
 222
 223          --  Start of processing for Is_OK_Declaration
 224
 225          begin
 226             if Is_Ghost_Declaration (Decl) then
 227                return True;
 228
 229             --  Special cases
 230
 231             --  A reference to a Ghost entity may appear within the profile of
 232             --  a subprogram body. This context is treated as suitable because
 233             --  it duplicates the context of the corresponding spec. The real
 234             --  check was already performed during the analysis of the spec.
 235
 236             elsif In_Subprogram_Body_Profile (Decl) then
 237                return True;
 238
 239             --  A reference to a Ghost entity may appear within an expression
 240             --  function which is still being analyzed. This context is treated
 241             --  as suitable because it is not yet known whether the expression
 242             --  function is an initial declaration or a completion. The real
 243             --  check is performed when the expression function is expanded.
 244
 245             elsif Nkind (Decl) = N_Expression_Function
 246               and then not Analyzed (Decl)
 247             then
 248                return True;
 249
 250             --  References to Ghost entities may be relocated in internally
 251             --  generated bodies.
 252
 253             elsif Nkind (Decl) = N_Subprogram_Body
 254               and then not Comes_From_Source (Decl)
 255             then
 256                Subp_Id := Corresponding_Spec (Decl);
 257
 258                if Present (Subp_Id) then
 259
 260                   --  The context is the internally built _Postconditions
 261                   --  procedure, which is OK because the real check was done
 262                   --  before expansion activities.
 263
 264                   if Chars (Subp_Id) = Name_uPostconditions then
 265                      return True;
 266
 267                   --  The context is the internally built predicate function,
 268                   --  which is OK because the real check was done before the
 269                   --  predicate function was generated.
 270
 271                   elsif Is_Predicate_Function (Subp_Id) then
 272                      return True;
 273
 274                   else
 275                      Subp_Decl :=
 276                        Original_Node (Unit_Declaration_Node (Subp_Id));
 277
 278                      --  The original context is an expression function that
 279                      --  has been split into a spec and a body. The context is
 280                      --  OK as long as the initial declaration is Ghost.
 281
 282                      if Nkind (Subp_Decl) = N_Expression_Function then
 283                         return Is_Ghost_Declaration (Subp_Decl);
 284                      end if;
 285                   end if;
 286
 287                --  Otherwise this is either an internal body or an internal
 288                --  completion. Both are OK because the real check was done
 289                --  before expansion activities.
 290
 291                else
 292                   return True;
 293                end if;
 294             end if;
 295
 296             return False;
 297          end Is_OK_Declaration;
 298
 299          ------------------
 300          -- Is_OK_Pragma --
 301          ------------------
 302
 303          function Is_OK_Pragma (Prag : Node_Id) return Boolean is
 304             procedure Check_Policies (Prag_Nam : Name_Id);
 305             --  Verify that the Ghost policy in effect is the same as the
 306             --  assertion policy for pragma name Prag_Nam. Emit an error if
 307             --  this is not the case.
 308
 309             --------------------
 310             -- Check_Policies --
 311             --------------------
 312
 313             procedure Check_Policies (Prag_Nam : Name_Id) is
 314                AP : constant Name_Id := Check_Kind (Prag_Nam);
 315                GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
 316
 317             begin
 318                --  If the Ghost policy in effect at the point of a Ghost entity
 319                --  reference is Ignore, then the assertion policy of the pragma
 320                --  must be Ignore (SPARK RM 6.9(18)).
 321
 322                if GP = Name_Ignore and then AP /= Name_Ignore then
 323                   Error_Msg_N
 324                     ("incompatible ghost policies in effect",
 325                      Ghost_Ref);
 326                   Error_Msg_NE
 327                     ("\ghost entity & has policy `Ignore`",
 328                      Ghost_Ref, Ghost_Id);
 329
 330                   Error_Msg_Name_1 := AP;
 331                   Error_Msg_N
 332                     ("\assertion expression has policy %", Ghost_Ref);
 333                end if;
 334             end Check_Policies;
 335
 336             --  Local variables
 337
 338             Prag_Id  : Pragma_Id;
 339             Prag_Nam : Name_Id;
 340
 341          --  Start of processing for Is_OK_Pragma
 342
 343          begin
 344             if Nkind (Prag) = N_Pragma then
 345                Prag_Id  := Get_Pragma_Id (Prag);
 346                Prag_Nam := Original_Aspect_Pragma_Name (Prag);
 347
 348                --  A pragma that applies to a Ghost construct or specifies an
 349                --  aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
 350
 351                if Is_Ghost_Pragma (Prag) then
 352                   return True;
 353
 354                --  An assertion expression pragma is Ghost when it contains a
 355                --  reference to a Ghost entity (SPARK RM 6.9(10)), except for
 356                --  predicate pragmas (SPARK RM 6.9(11)).
 357
 358                elsif Assertion_Expression_Pragma (Prag_Id)
 359                  and then Prag_Id /= Pragma_Predicate
 360                then
 361                   --  Ensure that the assertion policy and the Ghost policy are
 362                   --  compatible (SPARK RM 6.9(18)).
 363
 364                   Check_Policies (Prag_Nam);
 365                   return True;
 366
 367                --  Several pragmas that may apply to a non-Ghost entity are
 368                --  treated as Ghost when they contain a reference to a Ghost
 369                --  entity (SPARK RM 6.9(11)).
 370
 371                elsif Nam_In (Prag_Nam, Name_Global,
 372                                        Name_Depends,
 373                                        Name_Initializes,
 374                                        Name_Refined_Global,
 375                                        Name_Refined_Depends,
 376                                        Name_Refined_State)
 377                then
 378                   return True;
 379                end if;
 380             end if;
 381
 382             return False;
 383          end Is_OK_Pragma;
 384
 385          ---------------------
 386          -- Is_OK_Statement --
 387          ---------------------
 388
 389          function Is_OK_Statement (Stmt : Node_Id) return Boolean is
 390          begin
 391             --  An assignment statement is Ghost when the target is a Ghost
 392             --  entity.
 393
 394             if Nkind (Stmt) = N_Assignment_Statement then
 395                return Is_Ghost_Assignment (Stmt);
 396
 397             --  A procedure call is Ghost when it calls a Ghost procedure
 398
 399             elsif Nkind (Stmt) = N_Procedure_Call_Statement then
 400                return Is_Ghost_Procedure_Call (Stmt);
 401
 402             --  Special cases
 403
 404             --  An if statement is a suitable context for a Ghost entity if it
 405             --  is the byproduct of assertion expression expansion. Note that
 406             --  the assertion expression may not be related to a Ghost entity,
 407             --  but it may still contain references to Ghost entities.
 408
 409             elsif Nkind (Stmt) = N_If_Statement
 410               and then Nkind (Original_Node (Stmt)) = N_Pragma
 411               and then Assertion_Expression_Pragma
 412                          (Get_Pragma_Id (Original_Node (Stmt)))
 413             then
 414                return True;
 415             end if;
 416
 417             return False;
 418          end Is_OK_Statement;
 419
 420          --  Local variables
 421
 422          Par : Node_Id;
 423
 424       --  Start of processing for Is_OK_Ghost_Context
 425
 426       begin
 427          --  The context is Ghost when it appears within a Ghost package or
 428          --  subprogram.
 429
 430          if Ghost_Mode > None then
 431             return True;
 432
 433          --  A Ghost type may be referenced in a use_type clause
 434          --  (SPARK RM 6.9.10).
 435
 436          elsif Present (Parent (Context))
 437            and then Nkind (Parent (Context)) = N_Use_Type_Clause
 438          then
 439             return True;
 440
 441          --  Routine Expand_Record_Extension creates a parent subtype without
 442          --  inserting it into the tree. There is no good way of recognizing
 443          --  this special case as there is no parent. Try to approximate the
 444          --  context.
 445
 446          elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
 447             return True;
 448
 449          --  Otherwise climb the parent chain looking for a suitable Ghost
 450          --  context.
 451
 452          else
 453             Par := Context;
 454             while Present (Par) loop
 455                if Is_Ignored_Ghost_Node (Par) then
 456                   return True;
 457
 458                --  A reference to a Ghost entity can appear within an aspect
 459                --  specification (SPARK RM 6.9(10)). The precise checking will
 460                --  occur when analyzing the corresponding pragma. We make an
 461                --  exception for predicate aspects that only allow referencing
 462                --  a Ghost entity when the corresponding type declaration is
 463                --  Ghost (SPARK RM 6.9(11)).
 464
 465                elsif Nkind (Par) = N_Aspect_Specification
 466                  and then not Same_Aspect
 467                                 (Get_Aspect_Id (Par), Aspect_Predicate)
 468                then
 469                   return True;
 470
 471                elsif Is_OK_Declaration (Par) then
 472                   return True;
 473
 474                elsif Is_OK_Pragma (Par) then
 475                   return True;
 476
 477                elsif Is_OK_Statement (Par) then
 478                   return True;
 479
 480                --  Prevent the search from going too far
 481
 482                elsif Is_Body_Or_Package_Declaration (Par) then
 483                   exit;
 484                end if;
 485
 486                Par := Parent (Par);
 487             end loop;
 488
 489             --  The expansion of assertion expression pragmas and attribute Old
 490             --  may cause a legal Ghost entity reference to become illegal due
 491             --  to node relocation. Check the In_Assertion_Expr counter as last
 492             --  resort to try and infer the original legal context.
 493
 494             if In_Assertion_Expr > 0 then
 495                return True;
 496
 497             --  Otherwise the context is not suitable for a reference to a
 498             --  Ghost entity.
 499
 500             else
 501                return False;
 502             end if;
 503          end if;
 504       end Is_OK_Ghost_Context;
 505
 506       ------------------------
 507       -- Check_Ghost_Policy --
 508       ------------------------
 509
 510       procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is
 511          Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
 512
 513       begin
 514          --  The Ghost policy in effect a the point of declaration and at the
 515          --  point of use must match (SPARK RM 6.9(13)).
 516
 517          if Is_Checked_Ghost_Entity (Id)
 518            and then Policy = Name_Ignore
 519            and then May_Be_Lvalue (Ref)
 520          then
 521             Error_Msg_Sloc := Sloc (Ref);
 522
 523             Error_Msg_N  ("incompatible ghost policies in effect", Ref);
 524             Error_Msg_NE ("\& declared with ghost policy `Check`", Ref, Id);
 525             Error_Msg_NE ("\& used # with ghost policy `Ignore`",  Ref, Id);
 526
 527          elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
 528             Error_Msg_Sloc := Sloc (Ref);
 529
 530             Error_Msg_N  ("incompatible ghost policies in effect",  Ref);
 531             Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id);
 532             Error_Msg_NE ("\& used # with ghost policy `Check`",    Ref, Id);
 533          end if;
 534       end Check_Ghost_Policy;
 535
 536    --  Start of processing for Check_Ghost_Context
 537
 538    begin
 539       --  Once it has been established that the reference to the Ghost entity
 540       --  is within a suitable context, ensure that the policy at the point of
 541       --  declaration and at the point of use match.
 542
 543       if Is_OK_Ghost_Context (Ghost_Ref) then
 544          Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
 545
 546       --  Otherwise the Ghost entity appears in a non-Ghost context and affects
 547       --  its behavior or value (SPARK RM 6.9(10,11)).
 548
 549       else
 550          Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
 551       end if;
 552    end Check_Ghost_Context;
 553
 554    ----------------------------
 555    -- Check_Ghost_Overriding --
 556    ----------------------------
 557
 558    procedure Check_Ghost_Overriding
 559      (Subp            : Entity_Id;
 560       Overridden_Subp : Entity_Id)
 561    is
 562       Deriv_Typ : Entity_Id;
 563       Over_Subp : Entity_Id;
 564
 565    begin
 566       if Present (Subp) and then Present (Overridden_Subp) then
 567          Over_Subp := Ultimate_Alias (Overridden_Subp);
 568          Deriv_Typ := Find_Dispatching_Type (Subp);
 569
 570          --  A Ghost primitive of a non-Ghost type extension cannot override an
 571          --  inherited non-Ghost primitive (SPARK RM 6.9(8)).
 572
 573          if Is_Ghost_Entity (Subp)
 574            and then Present (Deriv_Typ)
 575            and then not Is_Ghost_Entity (Deriv_Typ)
 576            and then not Is_Ghost_Entity (Over_Subp)
 577            and then not Is_Abstract_Subprogram (Over_Subp)
 578          then
 579             Error_Msg_N ("incompatible overriding in effect", Subp);
 580
 581             Error_Msg_Sloc := Sloc (Over_Subp);
 582             Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
 583
 584             Error_Msg_Sloc := Sloc (Subp);
 585             Error_Msg_N ("\overridden # with ghost subprogram", Subp);
 586          end if;
 587
 588          --  A non-Ghost primitive of a type extension cannot override an
 589          --  inherited Ghost primitive (SPARK RM 6.9(8)).
 590
 591          if Is_Ghost_Entity (Over_Subp)
 592            and then not Is_Ghost_Entity (Subp)
 593            and then not Is_Abstract_Subprogram (Subp)
 594          then
 595             Error_Msg_N ("incompatible overriding in effect", Subp);
 596
 597             Error_Msg_Sloc := Sloc (Over_Subp);
 598             Error_Msg_N ("\& declared # as ghost subprogram", Subp);
 599
 600             Error_Msg_Sloc := Sloc (Subp);
 601             Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
 602          end if;
 603
 604          if Present (Deriv_Typ)
 605            and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
 606          then
 607             --  When a tagged type is either non-Ghost or checked Ghost and
 608             --  one of its primitives overrides an inherited operation, the
 609             --  overridden operation of the ancestor type must be ignored Ghost
 610             --  if the primitive is ignored Ghost (SPARK RM 6.9(17)).
 611
 612             if Is_Ignored_Ghost_Entity (Subp) then
 613
 614                --  Both the parent subprogram and overriding subprogram are
 615                --  ignored Ghost.
 616
 617                if Is_Ignored_Ghost_Entity (Over_Subp) then
 618                   null;
 619
 620                --  The parent subprogram carries policy Check
 621
 622                elsif Is_Checked_Ghost_Entity (Over_Subp) then
 623                   Error_Msg_N
 624                     ("incompatible ghost policies in effect", Subp);
 625
 626                   Error_Msg_Sloc := Sloc (Over_Subp);
 627                   Error_Msg_N
 628                     ("\& declared # with ghost policy `Check`", Subp);
 629
 630                   Error_Msg_Sloc := Sloc (Subp);
 631                   Error_Msg_N
 632                     ("\overridden # with ghost policy `Ignore`", Subp);
 633
 634                --  The parent subprogram is non-Ghost
 635
 636                else
 637                   Error_Msg_N
 638                     ("incompatible ghost policies in effect", Subp);
 639
 640                   Error_Msg_Sloc := Sloc (Over_Subp);
 641                   Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
 642
 643                   Error_Msg_Sloc := Sloc (Subp);
 644                   Error_Msg_N
 645                     ("\overridden # with ghost policy `Ignore`", Subp);
 646                end if;
 647
 648             --  When a tagged type is either non-Ghost or checked Ghost and
 649             --  one of its primitives overrides an inherited operation, the
 650             --  the primitive of the tagged type must be ignored Ghost if the
 651             --  overridden operation is ignored Ghost (SPARK RM 6.9(17)).
 652
 653             elsif Is_Ignored_Ghost_Entity (Over_Subp) then
 654
 655                --  Both the parent subprogram and the overriding subprogram are
 656                --  ignored Ghost.
 657
 658                if Is_Ignored_Ghost_Entity (Subp) then
 659                   null;
 660
 661                --  The overriding subprogram carries policy Check
 662
 663                elsif Is_Checked_Ghost_Entity (Subp) then
 664                   Error_Msg_N
 665                     ("incompatible ghost policies in effect", Subp);
 666
 667                   Error_Msg_Sloc := Sloc (Over_Subp);
 668                   Error_Msg_N
 669                     ("\& declared # with ghost policy `Ignore`", Subp);
 670
 671                   Error_Msg_Sloc := Sloc (Subp);
 672                   Error_Msg_N
 673                     ("\overridden # with Ghost policy `Check`", Subp);
 674
 675                --  The overriding subprogram is non-Ghost
 676
 677                else
 678                   Error_Msg_N
 679                     ("incompatible ghost policies in effect", Subp);
 680
 681                   Error_Msg_Sloc := Sloc (Over_Subp);
 682                   Error_Msg_N
 683                     ("\& declared # with ghost policy `Ignore`", Subp);
 684
 685                   Error_Msg_Sloc := Sloc (Subp);
 686                   Error_Msg_N
 687                     ("\overridden # with non-ghost subprogram", Subp);
 688                end if;
 689             end if;
 690          end if;
 691       end if;
 692    end Check_Ghost_Overriding;
 693
 694    ---------------------------
 695    -- Check_Ghost_Primitive --
 696    ---------------------------
 697
 698    procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
 699    begin
 700       --  The Ghost policy in effect at the point of declaration of a primitive
 701       --  operation and a tagged type must match (SPARK RM 6.9(16)).
 702
 703       if Is_Tagged_Type (Typ) then
 704          if Is_Checked_Ghost_Entity (Prim)
 705            and then Is_Ignored_Ghost_Entity (Typ)
 706          then
 707             Error_Msg_N ("incompatible ghost policies in effect", Prim);
 708
 709             Error_Msg_Sloc := Sloc (Typ);
 710             Error_Msg_NE
 711               ("\tagged type & declared # with ghost policy `Ignore`",
 712                Prim, Typ);
 713
 714             Error_Msg_Sloc := Sloc (Prim);
 715             Error_Msg_N
 716               ("\primitive subprogram & declared # with ghost policy `Check`",
 717                Prim);
 718
 719          elsif Is_Ignored_Ghost_Entity (Prim)
 720            and then Is_Checked_Ghost_Entity (Typ)
 721          then
 722             Error_Msg_N ("incompatible ghost policies in effect", Prim);
 723
 724             Error_Msg_Sloc := Sloc (Typ);
 725             Error_Msg_NE
 726               ("\tagged type & declared # with ghost policy `Check`",
 727                Prim, Typ);
 728
 729             Error_Msg_Sloc := Sloc (Prim);
 730             Error_Msg_N
 731               ("\primitive subprogram & declared # with ghost policy `Ignore`",
 732                Prim);
 733          end if;
 734       end if;
 735    end Check_Ghost_Primitive;
 736
 737    ----------------------------
 738    -- Check_Ghost_Refinement --
 739    ----------------------------
 740
 741    procedure Check_Ghost_Refinement
 742      (State      : Node_Id;
 743       State_Id   : Entity_Id;
 744       Constit    : Node_Id;
 745       Constit_Id : Entity_Id)
 746    is
 747    begin
 748       if Is_Ghost_Entity (State_Id) then
 749          if Is_Ghost_Entity (Constit_Id) then
 750
 751             --  The Ghost policy in effect at the point of abstract state
 752             --  declaration and constituent must match (SPARK RM 6.9(15)).
 753
 754             if Is_Checked_Ghost_Entity (State_Id)
 755               and then Is_Ignored_Ghost_Entity (Constit_Id)
 756             then
 757                Error_Msg_Sloc := Sloc (Constit);
 758                SPARK_Msg_N ("incompatible ghost policies in effect", State);
 759
 760                SPARK_Msg_NE
 761                  ("\abstract state & declared with ghost policy `Check`",
 762                   State, State_Id);
 763                SPARK_Msg_NE
 764                  ("\constituent & declared # with ghost policy `Ignore`",
 765                   State, Constit_Id);
 766
 767             elsif Is_Ignored_Ghost_Entity (State_Id)
 768               and then Is_Checked_Ghost_Entity (Constit_Id)
 769             then
 770                Error_Msg_Sloc := Sloc (Constit);
 771                SPARK_Msg_N ("incompatible ghost policies in effect", State);
 772
 773                SPARK_Msg_NE
 774                  ("\abstract state & declared with ghost policy `Ignore`",
 775                   State, State_Id);
 776                SPARK_Msg_NE
 777                  ("\constituent & declared # with ghost policy `Check`",
 778                   State, Constit_Id);
 779             end if;
 780
 781             --  A constituent of a Ghost abstract state must be a Ghost entity
 782             --  (SPARK RM 7.2.2(12)).
 783
 784          else
 785             SPARK_Msg_NE
 786               ("constituent of ghost state & must be ghost",
 787                Constit, State_Id);
 788          end if;
 789       end if;
 790    end Check_Ghost_Refinement;
 791
 792    ----------------------
 793    -- Check_Ghost_Type --
 794    ----------------------
 795
 796    procedure Check_Ghost_Type (Typ : Entity_Id) is
 797       Conc_Typ : Entity_Id;
 798       Full_Typ : Entity_Id;
 799
 800    begin
 801       if Is_Ghost_Entity (Typ) then
 802          Conc_Typ := Empty;
 803          Full_Typ := Typ;
 804
 805          if Is_Single_Concurrent_Type (Typ) then
 806             Conc_Typ := Anonymous_Object (Typ);
 807             Full_Typ := Conc_Typ;
 808
 809          elsif Is_Concurrent_Type (Typ) then
 810             Conc_Typ := Typ;
 811          end if;
 812
 813          --  A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
 814          --  legality rule first to give a finer-grained diagnostic.
 815
 816          if Present (Conc_Typ) then
 817             Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ);
 818          end if;
 819
 820          --  A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
 821
 822          if Is_Effectively_Volatile (Full_Typ) then
 823             Error_Msg_N ("ghost type & cannot be volatile", Full_Typ);
 824          end if;
 825       end if;
 826    end Check_Ghost_Type;
 827
 828    ------------------
 829    -- Ghost_Entity --
 830    ------------------
 831
 832    function Ghost_Entity (N : Node_Id) return Entity_Id is
 833       Ref : Node_Id;
 834
 835    begin
 836       --  When the reference denotes a subcomponent, recover the related
 837       --  object (SPARK RM 6.9(1)).
 838
 839       Ref := N;
 840       while Nkind_In (Ref, N_Explicit_Dereference,
 841                            N_Indexed_Component,
 842                            N_Selected_Component,
 843                            N_Slice)
 844       loop
 845          Ref := Prefix (Ref);
 846       end loop;
 847
 848       if Is_Entity_Name (Ref) then
 849          return Entity (Ref);
 850       else
 851          return Empty;
 852       end if;
 853    end Ghost_Entity;
 854
 855    --------------------------------
 856    -- Implements_Ghost_Interface --
 857    --------------------------------
 858
 859    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
 860       Iface_Elmt : Elmt_Id;
 861
 862    begin
 863       --  Traverse the list of interfaces looking for a Ghost interface
 864
 865       if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
 866          Iface_Elmt := First_Elmt (Interfaces (Typ));
 867          while Present (Iface_Elmt) loop
 868             if Is_Ghost_Entity (Node (Iface_Elmt)) then
 869                return True;
 870             end if;
 871
 872             Next_Elmt (Iface_Elmt);
 873          end loop;
 874       end if;
 875
 876       return False;
 877    end Implements_Ghost_Interface;
 878
 879    ----------------
 880    -- Initialize --
 881    ----------------
 882
 883    procedure Initialize is
 884    begin
 885       Ignored_Ghost_Nodes.Init;
 886
 887       --  Set the soft link which enables Atree.Mark_New_Ghost_Node to record
 888       --  an ignored Ghost node or entity.
 889
 890       Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access);
 891    end Initialize;
 892
 893    ------------------------
 894    -- Install_Ghost_Mode --
 895    ------------------------
 896
 897    procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is
 898    begin
 899       Install_Ghost_Region (Mode, Empty);
 900    end Install_Ghost_Mode;
 901
 902    --------------------------
 903    -- Install_Ghost_Region --
 904    --------------------------
 905
 906    procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
 907    begin
 908       --  The context is already within an ignored Ghost region. Maintain the
 909       --  start of the outermost ignored Ghost region.
 910
 911       if Present (Ignored_Ghost_Region) then
 912          null;
 913
 914       --  The current region is the outermost ignored Ghost region. Save its
 915       --  starting node.
 916
 917       elsif Present (N) and then Mode = Ignore then
 918          Ignored_Ghost_Region := N;
 919
 920       --  Otherwise the current region is not ignored, nothing to save
 921
 922       else
 923          Ignored_Ghost_Region := Empty;
 924       end if;
 925
 926       Ghost_Mode := Mode;
 927    end Install_Ghost_Region;
 928
 929    procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is
 930    begin
 931       Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N);
 932    end Install_Ghost_Region;
 933
 934    -------------------------
 935    -- Is_Ghost_Assignment --
 936    -------------------------
 937
 938    function Is_Ghost_Assignment (N : Node_Id) return Boolean is
 939       Id : Entity_Id;
 940
 941    begin
 942       --  An assignment statement is Ghost when its target denotes a Ghost
 943       --  entity.
 944
 945       if Nkind (N) = N_Assignment_Statement then
 946          Id := Ghost_Entity (Name (N));
 947
 948          return Present (Id) and then Is_Ghost_Entity (Id);
 949       end if;
 950
 951       return False;
 952    end Is_Ghost_Assignment;
 953
 954    --------------------------
 955    -- Is_Ghost_Declaration --
 956    --------------------------
 957
 958    function Is_Ghost_Declaration (N : Node_Id) return Boolean is
 959       Id : Entity_Id;
 960
 961    begin
 962       --  A declaration is Ghost when it elaborates a Ghost entity or is
 963       --  subject to pragma Ghost.
 964
 965       if Is_Declaration (N) then
 966          Id := Defining_Entity (N);
 967
 968          return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N);
 969       end if;
 970
 971       return False;
 972    end Is_Ghost_Declaration;
 973
 974    ---------------------
 975    -- Is_Ghost_Pragma --
 976    ---------------------
 977
 978    function Is_Ghost_Pragma (N : Node_Id) return Boolean is
 979    begin
 980       return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N);
 981    end Is_Ghost_Pragma;
 982
 983    -----------------------------
 984    -- Is_Ghost_Procedure_Call --
 985    -----------------------------
 986
 987    function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is
 988       Id : Entity_Id;
 989
 990    begin
 991       --  A procedure call is Ghost when it invokes a Ghost procedure
 992
 993       if Nkind (N) = N_Procedure_Call_Statement then
 994          Id := Ghost_Entity (Name (N));
 995
 996          return Present (Id) and then Is_Ghost_Entity (Id);
 997       end if;
 998
 999       return False;
1000    end Is_Ghost_Procedure_Call;
1001
1002    ---------------------------
1003    -- Is_Ignored_Ghost_Unit --
1004    ---------------------------
1005
1006    function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean is
1007       function Ultimate_Original_Node (Nod : Node_Id) return Node_Id;
1008       --  Obtain the original node of arbitrary node Nod following a potential
1009       --  chain of rewritings.
1010
1011       ----------------------------
1012       -- Ultimate_Original_Node --
1013       ----------------------------
1014
1015       function Ultimate_Original_Node (Nod : Node_Id) return Node_Id is
1016          Res : Node_Id;
1017
1018       begin
1019          Res := Nod;
1020          while Original_Node (Res) /= Res loop
1021             Res := Original_Node (Res);
1022          end loop;
1023
1024          return Res;
1025       end Ultimate_Original_Node;
1026
1027    --  Start of processing for Is_Ignored_Ghost_Unit
1028
1029    begin
1030       --  Inspect the original node of the unit in case removal of ignored
1031       --  Ghost code has already taken place.
1032
1033       return
1034         Nkind (N) = N_Compilation_Unit
1035           and then Is_Ignored_Ghost_Entity
1036                      (Defining_Entity (Ultimate_Original_Node (Unit (N))));
1037    end Is_Ignored_Ghost_Unit;
1038
1039    -------------------------
1040    -- Is_Subject_To_Ghost --
1041    -------------------------
1042
1043    function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
1044       function Enables_Ghostness (Arg : Node_Id) return Boolean;
1045       --  Determine whether aspect or pragma argument Arg enables "ghostness"
1046
1047       -----------------------
1048       -- Enables_Ghostness --
1049       -----------------------
1050
1051       function Enables_Ghostness (Arg : Node_Id) return Boolean is
1052          Expr : Node_Id;
1053
1054       begin
1055          Expr := Arg;
1056
1057          if Nkind (Expr) = N_Pragma_Argument_Association then
1058             Expr := Get_Pragma_Arg (Expr);
1059          end if;
1060
1061          --  Determine whether the expression of the aspect or pragma is static
1062          --  and denotes True.
1063
1064          if Present (Expr) then
1065             Preanalyze_And_Resolve (Expr);
1066
1067             return
1068               Is_OK_Static_Expression (Expr)
1069                 and then Is_True (Expr_Value (Expr));
1070
1071          --  Otherwise Ghost defaults to True
1072
1073          else
1074             return True;
1075          end if;
1076       end Enables_Ghostness;
1077
1078       --  Local variables
1079
1080       Id      : constant Entity_Id := Defining_Entity (N);
1081       Asp     : Node_Id;
1082       Decl    : Node_Id;
1083       Prev_Id : Entity_Id;
1084
1085    --  Start of processing for Is_Subject_To_Ghost
1086
1087    begin
1088       --  The related entity of the declaration has not been analyzed yet, do
1089       --  not inspect its attributes.
1090
1091       if Ekind (Id) = E_Void then
1092          null;
1093
1094       elsif Is_Ghost_Entity (Id) then
1095          return True;
1096
1097       --  The completion of a type or a constant is not fully analyzed when the
1098       --  reference to the Ghost entity is resolved. Because the completion is
1099       --  not marked as Ghost yet, inspect the partial view.
1100
1101       elsif Is_Record_Type (Id)
1102         or else Ekind (Id) = E_Constant
1103         or else (Nkind (N) = N_Object_Declaration
1104                   and then Constant_Present (N))
1105       then
1106          Prev_Id := Incomplete_Or_Partial_View (Id);
1107
1108          if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
1109             return True;
1110          end if;
1111       end if;
1112
1113       --  Examine the aspect specifications (if any) looking for aspect Ghost
1114
1115       if Permits_Aspect_Specifications (N) then
1116          Asp := First (Aspect_Specifications (N));
1117          while Present (Asp) loop
1118             if Chars (Identifier (Asp)) = Name_Ghost then
1119                return Enables_Ghostness (Expression (Asp));
1120             end if;
1121
1122             Next (Asp);
1123          end loop;
1124       end if;
1125
1126       Decl := Empty;
1127
1128       --  When the context is a [generic] package declaration, pragma Ghost
1129       --  resides in the visible declarations.
1130
1131       if Nkind_In (N, N_Generic_Package_Declaration,
1132                       N_Package_Declaration)
1133       then
1134          Decl := First (Visible_Declarations (Specification (N)));
1135
1136       --  When the context is a package or a subprogram body, pragma Ghost
1137       --  resides in the declarative part.
1138
1139       elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
1140          Decl := First (Declarations (N));
1141
1142       --  Otherwise pragma Ghost appears in the declarations following N
1143
1144       elsif Is_List_Member (N) then
1145          Decl := Next (N);
1146       end if;
1147
1148       while Present (Decl) loop
1149          if Nkind (Decl) = N_Pragma
1150            and then Pragma_Name (Decl) = Name_Ghost
1151          then
1152             return
1153               Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
1154
1155          --  A source construct ends the region where pragma Ghost may appear,
1156          --  stop the traversal. Check the original node as source constructs
1157          --  may be rewritten into something else by expansion.
1158
1159          elsif Comes_From_Source (Original_Node (Decl)) then
1160             exit;
1161          end if;
1162
1163          Next (Decl);
1164       end loop;
1165
1166       return False;
1167    end Is_Subject_To_Ghost;
1168
1169    ----------
1170    -- Lock --
1171    ----------
1172
1173    procedure Lock is
1174    begin
1175       Ignored_Ghost_Nodes.Release;
1176       Ignored_Ghost_Nodes.Locked := True;
1177    end Lock;
1178
1179    -----------------------------------
1180    -- Mark_And_Set_Ghost_Assignment --
1181    -----------------------------------
1182
1183    procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is
1184       Id : Entity_Id;
1185
1186    begin
1187       --  An assignment statement becomes Ghost when its target denotes a Ghost
1188       --  object. Install the Ghost mode of the target.
1189
1190       Id := Ghost_Entity (Name (N));
1191
1192       if Present (Id) then
1193          if Is_Checked_Ghost_Entity (Id) then
1194             Install_Ghost_Region (Check, N);
1195
1196          elsif Is_Ignored_Ghost_Entity (Id) then
1197             Install_Ghost_Region (Ignore, N);
1198
1199             Set_Is_Ignored_Ghost_Node (N);
1200             Record_Ignored_Ghost_Node (N);
1201          end if;
1202       end if;
1203    end Mark_And_Set_Ghost_Assignment;
1204
1205    -----------------------------
1206    -- Mark_And_Set_Ghost_Body --
1207    -----------------------------
1208
1209    procedure Mark_And_Set_Ghost_Body
1210      (N       : Node_Id;
1211       Spec_Id : Entity_Id)
1212    is
1213       Body_Id : constant Entity_Id := Defining_Entity (N);
1214       Policy  : Name_Id := No_Name;
1215
1216    begin
1217       --  A body becomes Ghost when it is subject to aspect or pragma Ghost
1218
1219       if Is_Subject_To_Ghost (N) then
1220          Policy := Policy_In_Effect (Name_Ghost);
1221
1222       --  A body declared within a Ghost region is automatically Ghost
1223       --  (SPARK RM 6.9(2)).
1224
1225       elsif Ghost_Mode = Check then
1226          Policy := Name_Check;
1227
1228       elsif Ghost_Mode = Ignore then
1229          Policy := Name_Ignore;
1230
1231       --  Inherit the "ghostness" of the previous declaration when the body
1232       --  acts as a completion.
1233
1234       elsif Present (Spec_Id) then
1235          if Is_Checked_Ghost_Entity (Spec_Id) then
1236             Policy := Name_Check;
1237
1238          elsif Is_Ignored_Ghost_Entity (Spec_Id) then
1239             Policy := Name_Ignore;
1240          end if;
1241       end if;
1242
1243       --  The Ghost policy in effect at the point of declaration and at the
1244       --  point of completion must match (SPARK RM 6.9(14)).
1245
1246       Check_Ghost_Completion
1247         (Prev_Id  => Spec_Id,
1248          Compl_Id => Body_Id);
1249
1250       --  Mark the body as its formals as Ghost
1251
1252       Mark_Ghost_Declaration_Or_Body (N, Policy);
1253
1254       --  Install the appropriate Ghost region
1255
1256       Install_Ghost_Region (Policy, N);
1257    end Mark_And_Set_Ghost_Body;
1258
1259    -----------------------------------
1260    -- Mark_And_Set_Ghost_Completion --
1261    -----------------------------------
1262
1263    procedure Mark_And_Set_Ghost_Completion
1264      (N       : Node_Id;
1265       Prev_Id : Entity_Id)
1266    is
1267       Compl_Id : constant Entity_Id := Defining_Entity (N);
1268       Policy   : Name_Id := No_Name;
1269
1270    begin
1271       --  A completion elaborated in a Ghost region is automatically Ghost
1272       --  (SPARK RM 6.9(2)).
1273
1274       if Ghost_Mode = Check then
1275          Policy := Name_Check;
1276
1277       elsif Ghost_Mode = Ignore then
1278          Policy := Name_Ignore;
1279
1280       --  The completion becomes Ghost when its initial declaration is also
1281       --  Ghost.
1282
1283       elsif Is_Checked_Ghost_Entity (Prev_Id) then
1284          Policy := Name_Check;
1285
1286       elsif Is_Ignored_Ghost_Entity (Prev_Id) then
1287          Policy := Name_Ignore;
1288       end if;
1289
1290       --  The Ghost policy in effect at the point of declaration and at the
1291       --  point of completion must match (SPARK RM 6.9(14)).
1292
1293       Check_Ghost_Completion
1294         (Prev_Id  => Prev_Id,
1295          Compl_Id => Compl_Id);
1296
1297       --  Mark the completion as Ghost
1298
1299       Mark_Ghost_Declaration_Or_Body (N, Policy);
1300
1301       --  Install the appropriate Ghost region
1302
1303       Install_Ghost_Region (Policy, N);
1304    end Mark_And_Set_Ghost_Completion;
1305
1306    ------------------------------------
1307    -- Mark_And_Set_Ghost_Declaration --
1308    ------------------------------------
1309
1310    procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is
1311       Par_Id : Entity_Id;
1312       Policy : Name_Id := No_Name;
1313
1314    begin
1315       --  A declaration becomes Ghost when it is subject to aspect or pragma
1316       --  Ghost.
1317
1318       if Is_Subject_To_Ghost (N) then
1319          Policy := Policy_In_Effect (Name_Ghost);
1320
1321       --  A declaration elaborated in a Ghost region is automatically Ghost
1322       --  (SPARK RM 6.9(2)).
1323
1324       elsif Ghost_Mode = Check then
1325          Policy := Name_Check;
1326
1327       elsif Ghost_Mode = Ignore then
1328          Policy := Name_Ignore;
1329
1330       --  A child package or subprogram declaration becomes Ghost when its
1331       --  parent is Ghost (SPARK RM 6.9(2)).
1332
1333       elsif Nkind_In (N, N_Generic_Function_Renaming_Declaration,
1334                          N_Generic_Package_Declaration,
1335                          N_Generic_Package_Renaming_Declaration,
1336                          N_Generic_Procedure_Renaming_Declaration,
1337                          N_Generic_Subprogram_Declaration,
1338                          N_Package_Declaration,
1339                          N_Package_Renaming_Declaration,
1340                          N_Subprogram_Declaration,
1341                          N_Subprogram_Renaming_Declaration)
1342         and then Present (Parent_Spec (N))
1343       then
1344          Par_Id := Defining_Entity (Unit (Parent_Spec (N)));
1345
1346          if Is_Checked_Ghost_Entity (Par_Id) then
1347             Policy := Name_Check;
1348
1349          elsif Is_Ignored_Ghost_Entity (Par_Id) then
1350             Policy := Name_Ignore;
1351          end if;
1352       end if;
1353
1354       --  Mark the declaration and its formals as Ghost
1355
1356       Mark_Ghost_Declaration_Or_Body (N, Policy);
1357
1358       --  Install the appropriate Ghost region
1359
1360       Install_Ghost_Region (Policy, N);
1361    end Mark_And_Set_Ghost_Declaration;
1362
1363    --------------------------------------
1364    -- Mark_And_Set_Ghost_Instantiation --
1365    --------------------------------------
1366
1367    procedure Mark_And_Set_Ghost_Instantiation
1368      (N      : Node_Id;
1369       Gen_Id : Entity_Id)
1370    is
1371       procedure Check_Ghost_Actuals;
1372       --  Check the context of ghost actuals
1373
1374       -------------------------
1375       -- Check_Ghost_Actuals --
1376       -------------------------
1377
1378       procedure Check_Ghost_Actuals is
1379          Assoc : Node_Id := First (Generic_Associations (N));
1380          Act   : Node_Id;
1381
1382       begin
1383          while Present (Assoc) loop
1384             if Nkind (Assoc) /= N_Others_Choice then
1385                Act := Explicit_Generic_Actual_Parameter (Assoc);
1386
1387                --  Within a nested instantiation, a defaulted actual is an
1388                --  empty association, so nothing to check.
1389
1390                if No (Act) then
1391                   null;
1392
1393                elsif Comes_From_Source (Act)
1394                   and then Nkind (Act) in N_Has_Etype
1395                   and then Present (Etype (Act))
1396                   and then Is_Ghost_Entity (Etype (Act))
1397                then
1398                   Check_Ghost_Context (Etype (Act), Act);
1399                end if;
1400             end if;
1401
1402             Next (Assoc);
1403          end loop;
1404       end Check_Ghost_Actuals;
1405
1406       --  Local variables
1407
1408       Policy : Name_Id := No_Name;
1409
1410    begin
1411       --  An instantiation becomes Ghost when it is subject to pragma Ghost
1412
1413       if Is_Subject_To_Ghost (N) then
1414          Policy := Policy_In_Effect (Name_Ghost);
1415
1416       --  An instantiation declaration within a Ghost region is automatically
1417       --  Ghost (SPARK RM 6.9(2)).
1418
1419       elsif Ghost_Mode = Check then
1420          Policy := Name_Check;
1421
1422       elsif Ghost_Mode = Ignore then
1423          Policy := Name_Ignore;
1424
1425       --  Inherit the "ghostness" of the generic unit
1426
1427       elsif Is_Checked_Ghost_Entity (Gen_Id) then
1428          Policy := Name_Check;
1429
1430       elsif Is_Ignored_Ghost_Entity (Gen_Id) then
1431          Policy := Name_Ignore;
1432       end if;
1433
1434       --  Mark the instantiation as Ghost
1435
1436       Mark_Ghost_Declaration_Or_Body (N, Policy);
1437
1438       --  Install the appropriate Ghost region
1439
1440       Install_Ghost_Region (Policy, N);
1441
1442       --  Check Ghost actuals. Given that this routine is unconditionally
1443       --  invoked with subprogram and package instantiations, this check
1444       --  verifies the context of all the ghost entities passed in generic
1445       --  instantiations.
1446
1447       Check_Ghost_Actuals;
1448    end Mark_And_Set_Ghost_Instantiation;
1449
1450    ---------------------------------------
1451    -- Mark_And_Set_Ghost_Procedure_Call --
1452    ---------------------------------------
1453
1454    procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is
1455       Id : Entity_Id;
1456
1457    begin
1458       --  A procedure call becomes Ghost when the procedure being invoked is
1459       --  Ghost. Install the Ghost mode of the procedure.
1460
1461       Id := Ghost_Entity (Name (N));
1462
1463       if Present (Id) then
1464          if Is_Checked_Ghost_Entity (Id) then
1465             Install_Ghost_Region (Check, N);
1466
1467          elsif Is_Ignored_Ghost_Entity (Id) then
1468             Install_Ghost_Region (Ignore, N);
1469
1470             Set_Is_Ignored_Ghost_Node (N);
1471             Record_Ignored_Ghost_Node (N);
1472          end if;
1473       end if;
1474    end Mark_And_Set_Ghost_Procedure_Call;
1475
1476    -----------------------
1477    -- Mark_Ghost_Clause --
1478    -----------------------
1479
1480    procedure Mark_Ghost_Clause (N : Node_Id) is
1481       Nam : Node_Id := Empty;
1482
1483    begin
1484       if Nkind (N) = N_Use_Package_Clause then
1485          Nam := Name (N);
1486
1487       elsif Nkind (N) = N_Use_Type_Clause then
1488          Nam := Subtype_Mark (N);
1489
1490       elsif Nkind (N) = N_With_Clause then
1491          Nam := Name (N);
1492       end if;
1493
1494       if Present (Nam)
1495         and then Is_Entity_Name (Nam)
1496         and then Present (Entity (Nam))
1497         and then Is_Ignored_Ghost_Entity (Entity (Nam))
1498       then
1499          Set_Is_Ignored_Ghost_Node (N);
1500          Record_Ignored_Ghost_Node (N);
1501       end if;
1502    end Mark_Ghost_Clause;
1503
1504    ------------------------------------
1505    -- Mark_Ghost_Declaration_Or_Body --
1506    ------------------------------------
1507
1508    procedure Mark_Ghost_Declaration_Or_Body
1509      (N    : Node_Id;
1510       Mode : Name_Id)
1511    is
1512       Id : constant Entity_Id := Defining_Entity (N);
1513
1514       Mark_Formals : Boolean := False;
1515       Param        : Node_Id;
1516       Param_Id     : Entity_Id;
1517
1518    begin
1519       --  Mark the related node and its entity
1520
1521       if Mode = Name_Check then
1522          Mark_Formals := True;
1523          Set_Is_Checked_Ghost_Entity (Id);
1524
1525       elsif Mode = Name_Ignore then
1526          Mark_Formals := True;
1527          Set_Is_Ignored_Ghost_Entity (Id);
1528          Set_Is_Ignored_Ghost_Node (N);
1529          Record_Ignored_Ghost_Node (N);
1530       end if;
1531
1532       --  Mark all formal parameters when the related node denotes a subprogram
1533       --  or a body. The traversal is performed via the specification because
1534       --  the related subprogram or body may be unanalyzed.
1535
1536       --  ??? could extra formal parameters cause a Ghost leak?
1537
1538       if Mark_Formals
1539         and then Nkind_In (N, N_Abstract_Subprogram_Declaration,
1540                               N_Formal_Abstract_Subprogram_Declaration,
1541                               N_Formal_Concrete_Subprogram_Declaration,
1542                               N_Generic_Subprogram_Declaration,
1543                               N_Subprogram_Body,
1544                               N_Subprogram_Body_Stub,
1545                               N_Subprogram_Declaration,
1546                               N_Subprogram_Renaming_Declaration)
1547       then
1548          Param := First (Parameter_Specifications (Specification (N)));
1549          while Present (Param) loop
1550             Param_Id := Defining_Entity (Param);
1551
1552             if Mode = Name_Check then
1553                Set_Is_Checked_Ghost_Entity (Param_Id);
1554
1555             elsif Mode = Name_Ignore then
1556                Set_Is_Ignored_Ghost_Entity (Param_Id);
1557             end if;
1558
1559             Next (Param);
1560          end loop;
1561       end if;
1562    end Mark_Ghost_Declaration_Or_Body;
1563
1564    -----------------------
1565    -- Mark_Ghost_Pragma --
1566    -----------------------
1567
1568    procedure Mark_Ghost_Pragma
1569      (N  : Node_Id;
1570       Id : Entity_Id)
1571    is
1572    begin
1573       --  A pragma becomes Ghost when it encloses a Ghost entity or relates to
1574       --  a Ghost entity.
1575
1576       if Is_Checked_Ghost_Entity (Id) then
1577          Set_Is_Checked_Ghost_Pragma (N);
1578
1579       elsif Is_Ignored_Ghost_Entity (Id) then
1580          Set_Is_Ignored_Ghost_Pragma (N);
1581          Set_Is_Ignored_Ghost_Node (N);
1582          Record_Ignored_Ghost_Node (N);
1583       end if;
1584    end Mark_Ghost_Pragma;
1585
1586    -------------------------
1587    -- Mark_Ghost_Renaming --
1588    -------------------------
1589
1590    procedure Mark_Ghost_Renaming
1591      (N  : Node_Id;
1592       Id : Entity_Id)
1593    is
1594       Policy : Name_Id := No_Name;
1595
1596    begin
1597       --  A renaming becomes Ghost when it renames a Ghost entity
1598
1599       if Is_Checked_Ghost_Entity (Id) then
1600          Policy := Name_Check;
1601
1602       elsif Is_Ignored_Ghost_Entity (Id) then
1603          Policy := Name_Ignore;
1604       end if;
1605
1606       Mark_Ghost_Declaration_Or_Body (N, Policy);
1607    end Mark_Ghost_Renaming;
1608
1609    ------------------------
1610    -- Name_To_Ghost_Mode --
1611    ------------------------
1612
1613    function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is
1614    begin
1615       if Mode = Name_Check then
1616          return Check;
1617
1618       elsif Mode = Name_Ignore then
1619          return Ignore;
1620
1621       --  Otherwise the mode must denote one of the following:
1622       --
1623       --    * Disable indicates that the Ghost policy in effect is Disable
1624       --
1625       --    * None or No_Name indicates that the associated construct is not
1626       --      subject to any Ghost annotation.
1627
1628       else
1629          pragma Assert (Nam_In (Mode, Name_Disable, Name_None, No_Name));
1630          return None;
1631       end if;
1632    end Name_To_Ghost_Mode;
1633
1634    -------------------------------
1635    -- Record_Ignored_Ghost_Node --
1636    -------------------------------
1637
1638    procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id) is
1639    begin
1640       --  Save all "top level" ignored Ghost nodes which can be safely replaced
1641       --  with a null statement. Note that there is need to save other kinds of
1642       --  nodes because those will always be enclosed by some top level ignored
1643       --  Ghost node.
1644
1645       if Is_Body (N)
1646         or else Is_Declaration (N)
1647         or else Nkind (N) in N_Generic_Instantiation
1648         or else Nkind (N) in N_Push_Pop_xxx_Label
1649         or else Nkind (N) in N_Raise_xxx_Error
1650         or else Nkind (N) in N_Representation_Clause
1651         or else Nkind_In (N, N_Assignment_Statement,
1652                              N_Call_Marker,
1653                              N_Freeze_Entity,
1654                              N_Freeze_Generic_Entity,
1655                              N_Itype_Reference,
1656                              N_Pragma,
1657                              N_Procedure_Call_Statement,
1658                              N_Use_Package_Clause,
1659                              N_Use_Type_Clause,
1660                              N_Variable_Reference_Marker,
1661                              N_With_Clause)
1662       then
1663          --  Only ignored Ghost nodes must be recorded in the table
1664
1665          pragma Assert (Is_Ignored_Ghost_Node (N));
1666          Ignored_Ghost_Nodes.Append (N);
1667       end if;
1668    end Record_Ignored_Ghost_Node;
1669
1670    -------------------------------
1671    -- Remove_Ignored_Ghost_Code --
1672    -------------------------------
1673
1674    procedure Remove_Ignored_Ghost_Code is
1675       procedure Remove_Ignored_Ghost_Node (N : Node_Id);
1676       --  Eliminate ignored Ghost node N from the tree
1677
1678       -------------------------------
1679       -- Remove_Ignored_Ghost_Node --
1680       -------------------------------
1681
1682       procedure Remove_Ignored_Ghost_Node (N : Node_Id) is
1683       begin
1684          --  The generation and processing of ignored Ghost nodes may cause the
1685          --  same node to be saved multiple times. Reducing the number of saves
1686          --  to one involves costly solutions such as a hash table or the use
1687          --  of a flag shared by all nodes. To solve this problem, the removal
1688          --  machinery allows for multiple saves, but does not eliminate a node
1689          --  which has already been eliminated.
1690
1691          if Nkind (N) = N_Null_Statement then
1692             null;
1693
1694          --  Otherwise the ignored Ghost node must be eliminated
1695
1696          else
1697             --  Only ignored Ghost nodes must be eliminated from the tree
1698
1699             pragma Assert (Is_Ignored_Ghost_Node (N));
1700
1701             --  Eliminate the node by rewriting it into null. Another option
1702             --  is to remove it from the tree, however multiple corner cases
1703             --  emerge which have be dealt individually.
1704
1705             Rewrite (N, Make_Null_Statement (Sloc (N)));
1706
1707             --  Eliminate any aspects hanging off the ignored Ghost node
1708
1709             Remove_Aspects (N);
1710          end if;
1711       end Remove_Ignored_Ghost_Node;
1712
1713    --  Start of processing for Remove_Ignored_Ghost_Code
1714
1715    begin
1716       for Index in Ignored_Ghost_Nodes.First .. Ignored_Ghost_Nodes.Last loop
1717          Remove_Ignored_Ghost_Node (Ignored_Ghost_Nodes.Table (Index));
1718       end loop;
1719    end Remove_Ignored_Ghost_Code;
1720
1721    --------------------------
1722    -- Restore_Ghost_Region --
1723    --------------------------
1724
1725    procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
1726    begin
1727       Ghost_Mode           := Mode;
1728       Ignored_Ghost_Region := N;
1729    end Restore_Ghost_Region;
1730
1731    --------------------
1732    -- Set_Ghost_Mode --
1733    --------------------
1734
1735    procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is
1736       procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
1737       --  Install the Ghost mode of entity Id
1738
1739       --------------------------------
1740       -- Set_Ghost_Mode_From_Entity --
1741       --------------------------------
1742
1743       procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
1744       begin
1745          if Is_Checked_Ghost_Entity (Id) then
1746             Install_Ghost_Mode (Check);
1747          elsif Is_Ignored_Ghost_Entity (Id) then
1748             Install_Ghost_Mode (Ignore);
1749          else
1750             Install_Ghost_Mode (None);
1751          end if;
1752       end Set_Ghost_Mode_From_Entity;
1753
1754       --  Local variables
1755
1756       Id : Entity_Id;
1757
1758    --  Start of processing for Set_Ghost_Mode
1759
1760    begin
1761       --  The Ghost mode of an assignment statement depends on the Ghost mode
1762       --  of the target.
1763
1764       if Nkind (N) = N_Assignment_Statement then
1765          Id := Ghost_Entity (Name (N));
1766
1767          if Present (Id) then
1768             Set_Ghost_Mode_From_Entity (Id);
1769          end if;
1770
1771       --  The Ghost mode of a body or a declaration depends on the Ghost mode
1772       --  of its defining entity.
1773
1774       elsif Is_Body (N) or else Is_Declaration (N) then
1775          Set_Ghost_Mode_From_Entity (Defining_Entity (N));
1776
1777       --  The Ghost mode of an entity depends on the entity itself
1778
1779       elsif Nkind (N) in N_Entity then
1780          Set_Ghost_Mode_From_Entity (N);
1781
1782       --  The Ghost mode of a [generic] freeze node depends on the Ghost mode
1783       --  of the entity being frozen.
1784
1785       elsif Nkind_In (N, N_Freeze_Entity, N_Freeze_Generic_Entity) then
1786          Set_Ghost_Mode_From_Entity (Entity (N));
1787
1788       --  The Ghost mode of a pragma depends on the associated entity. The
1789       --  property is encoded in the pragma itself.
1790
1791       elsif Nkind (N) = N_Pragma then
1792          if Is_Checked_Ghost_Pragma (N) then
1793             Install_Ghost_Mode (Check);
1794          elsif Is_Ignored_Ghost_Pragma (N) then
1795             Install_Ghost_Mode (Ignore);
1796          else
1797             Install_Ghost_Mode (None);
1798          end if;
1799
1800       --  The Ghost mode of a procedure call depends on the Ghost mode of the
1801       --  procedure being invoked.
1802
1803       elsif Nkind (N) = N_Procedure_Call_Statement then
1804          Id := Ghost_Entity (Name (N));
1805
1806          if Present (Id) then
1807             Set_Ghost_Mode_From_Entity (Id);
1808          end if;
1809       end if;
1810    end Set_Ghost_Mode;
1811
1812    -------------------------
1813    -- Set_Is_Ghost_Entity --
1814    -------------------------
1815
1816    procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
1817       Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
1818    begin
1819       if Policy = Name_Check then
1820          Set_Is_Checked_Ghost_Entity (Id);
1821       elsif Policy = Name_Ignore then
1822          Set_Is_Ignored_Ghost_Entity (Id);
1823       end if;
1824    end Set_Is_Ghost_Entity;
1825
1826 end Ghost;