gcc/ada/exp_spark.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                            E X P _ S P A R K                             --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2020, 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 Atree;    use Atree;
  27 with Checks;   use Checks;
  28 with Einfo;    use Einfo;
  29 with Exp_Attr;
  30 with Exp_Ch4;
  31 with Exp_Ch5;  use Exp_Ch5;
  32 with Exp_Dbug; use Exp_Dbug;
  33 with Exp_Util; use Exp_Util;
  34 with Namet;    use Namet;
  35 with Nlists;   use Nlists;
  36 with Nmake;    use Nmake;
  37 with Rtsfind;  use Rtsfind;
  38 with Sem;      use Sem;
  39 with Sem_Ch8;  use Sem_Ch8;
  40 with Sem_Prag; use Sem_Prag;
  41 with Sem_Res;  use Sem_Res;
  42 with Sem_Util; use Sem_Util;
  43 with Sinfo;    use Sinfo;
  44 with Snames;   use Snames;
  45 with Stand;    use Stand;
  46 with Tbuild;   use Tbuild;
  47 with Uintp;    use Uintp;
  48
  49 package body Exp_SPARK is
  50
  51    -----------------------
  52    -- Local Subprograms --
  53    -----------------------
  54
  55    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
  56    --  Perform attribute-reference-specific expansion
  57
  58    procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
  59    --  Perform delta-aggregate-specific expansion
  60
  61    procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
  62    --  Build the DIC procedure of a type when needed, if not already done
  63
  64    procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
  65    --  Perform loop-statement-specific expansion
  66
  67    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
  68    --  Perform object-declaration-specific expansion
  69
  70    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  71    --  Perform name evaluation for a renamed object
  72
  73    procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
  74    --  Rewrite operator /= based on operator = when defined explicitly
  75
  76    procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
  77    --  Common expansion for attribute Update and delta aggregates
  78
  79    ------------------
  80    -- Expand_SPARK --
  81    ------------------
  82
  83    procedure Expand_SPARK (N : Node_Id) is
  84    begin
  85       case Nkind (N) is
  86
  87          --  Qualification of entity names in formal verification mode
  88          --  is limited to the addition of a suffix for homonyms (see
  89          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  90          --  as full expansion does, but this was removed as this prevents the
  91          --  verification back-end from using a short name for debugging and
  92          --  user interaction. The verification back-end already takes care
  93          --  of qualifying names when needed.
  94
  95          when N_Block_Statement
  96             | N_Entry_Declaration
  97             | N_Package_Body
  98             | N_Package_Declaration
  99             | N_Protected_Type_Declaration
 100             | N_Subprogram_Body
 101             | N_Task_Type_Declaration
 102          =>
 103             Qualify_Entity_Names (N);
 104
 105          --  Replace occurrences of System'To_Address by calls to
 106          --  System.Storage_Elements.To_Address.
 107
 108          when N_Attribute_Reference =>
 109             Expand_SPARK_N_Attribute_Reference (N);
 110
 111          when N_Delta_Aggregate =>
 112             Expand_SPARK_N_Delta_Aggregate (N);
 113
 114          when N_Expanded_Name
 115             | N_Identifier
 116          =>
 117             Expand_SPARK_Potential_Renaming (N);
 118
 119          --  Loop iterations over arrays need to be expanded, to avoid getting
 120          --  two names referring to the same object in memory (the array and
 121          --  the iterator) in GNATprove, especially since both can be written
 122          --  (thus possibly leading to interferences due to aliasing). No such
 123          --  problem arises with quantified expressions over arrays, which are
 124          --  dealt with specially in GNATprove.
 125
 126          when N_Loop_Statement =>
 127             Expand_SPARK_N_Loop_Statement (N);
 128
 129          when N_Object_Declaration =>
 130             Expand_SPARK_N_Object_Declaration (N);
 131
 132          when N_Object_Renaming_Declaration =>
 133             Expand_SPARK_N_Object_Renaming_Declaration (N);
 134
 135          when N_Op_Ne =>
 136             Expand_SPARK_N_Op_Ne (N);
 137
 138          when N_Freeze_Entity =>
 139             if Is_Type (Entity (N)) then
 140                Expand_SPARK_N_Freeze_Type (Entity (N));
 141             end if;
 142
 143          --  In SPARK mode, no other constructs require expansion
 144
 145          when others =>
 146             null;
 147       end case;
 148    end Expand_SPARK;
 149
 150    ----------------------------------
 151    -- Expand_SPARK_Delta_Or_Update --
 152    ----------------------------------
 153
 154    procedure Expand_SPARK_Delta_Or_Update
 155      (Typ  : Entity_Id;
 156       Aggr : Node_Id)
 157    is
 158       Assoc     : Node_Id;
 159       Comp      : Node_Id;
 160       Comp_Id   : Entity_Id;
 161       Comp_Type : Entity_Id;
 162       Expr      : Node_Id;
 163       Index     : Node_Id;
 164       Index_Typ : Entity_Id;
 165       New_Assoc : Node_Id;
 166
 167    begin
 168       --  Apply scalar range checks on the updated components, if needed
 169
 170       if Is_Array_Type (Typ) then
 171
 172          --  Multidimensional arrays
 173
 174          if Present (Next_Index (First_Index (Typ))) then
 175             Assoc := First (Component_Associations (Aggr));
 176
 177             while Present (Assoc) loop
 178                Expr      := Expression (Assoc);
 179                Comp_Type := Component_Type (Typ);
 180
 181                if Is_Scalar_Type (Comp_Type) then
 182                   Apply_Scalar_Range_Check (Expr, Comp_Type);
 183                end if;
 184
 185                --  The current association contains a sequence of indexes
 186                --  denoting an element of a multidimensional array:
 187                --
 188                --    (Index_1, ..., Index_N)
 189
 190                Expr := First (Choices (Assoc));
 191
 192                pragma Assert (Nkind (Aggr) = N_Aggregate);
 193
 194                while Present (Expr) loop
 195                   Index     := First (Expressions (Expr));
 196                   Index_Typ := First_Index (Typ);
 197
 198                   while Present (Index_Typ) loop
 199                      Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
 200                      Next (Index);
 201                      Next_Index (Index_Typ);
 202                   end loop;
 203
 204                   Next (Expr);
 205                end loop;
 206
 207                Next (Assoc);
 208             end loop;
 209
 210          --  One-dimensional arrays
 211
 212          else
 213             Assoc := First (Component_Associations (Aggr));
 214
 215             while Present (Assoc) loop
 216                Expr      := Expression (Assoc);
 217                Comp_Type := Component_Type (Typ);
 218
 219                --  Analyze expression of the iterated_component_association
 220                --  with its index parameter in scope.
 221
 222                if Nkind (Assoc) = N_Iterated_Component_Association then
 223                   Push_Scope (Scope (Defining_Identifier (Assoc)));
 224                   Enter_Name (Defining_Identifier (Assoc));
 225                   Analyze_And_Resolve (Expr, Comp_Type);
 226                end if;
 227
 228                if Is_Scalar_Type (Comp_Type) then
 229                   Apply_Scalar_Range_Check (Expr, Comp_Type);
 230                end if;
 231
 232                --  Restore scope of the iterated_component_association
 233
 234                if Nkind (Assoc) = N_Iterated_Component_Association then
 235                   End_Scope;
 236                end if;
 237
 238                Index     := First (Choice_List (Assoc));
 239                Index_Typ := First_Index (Typ);
 240
 241                while Present (Index) loop
 242                   --  If the index denotes a range of elements or a constrained
 243                   --  subtype indication, then their low and high bounds
 244                   --  already have range checks applied.
 245
 246                   if Nkind (Index) in N_Range | N_Subtype_Indication then
 247                      null;
 248
 249                   --  Otherwise the index denotes a single expression where
 250                   --  range checks need to be applied or a subtype name
 251                   --  (without range constraints) where applying checks is
 252                   --  harmless.
 253                   --
 254                   --  In delta_aggregate and Update attribute on array the
 255                   --  others_choice is not allowed.
 256
 257                   else pragma Assert (Nkind (Index) in N_Subexpr);
 258                      Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
 259                   end if;
 260
 261                   Next (Index);
 262                end loop;
 263
 264                Next (Assoc);
 265             end loop;
 266          end if;
 267
 268       else pragma Assert (Is_Record_Type (Typ));
 269
 270          --  If the aggregate has multiple component choices, e.g.:
 271          --
 272          --    X'Update (A | B | C => 123)
 273          --
 274          --  then each component might be of a different type and might or
 275          --  might not require a range check. We first rewrite associations
 276          --  into single-component choices, e.g.:
 277          --
 278          --    X'Update (A => 123, B => 123, C => 123)
 279          --
 280          --  and then apply range checks to individual copies of the
 281          --  expressions. We do the same for delta aggregates, accordingly.
 282
 283          --  Iterate over associations of the original aggregate
 284
 285          Assoc := First (Component_Associations (Aggr));
 286
 287          --  Rewrite into a new aggregate and decorate
 288
 289          case Nkind (Aggr) is
 290             when N_Aggregate =>
 291                Rewrite
 292                  (Aggr,
 293                   Make_Aggregate
 294                     (Sloc                   => Sloc (Aggr),
 295                      Component_Associations => New_List));
 296
 297             when N_Delta_Aggregate =>
 298                Rewrite
 299                  (Aggr,
 300                   Make_Delta_Aggregate
 301                     (Sloc                   => Sloc (Aggr),
 302                      Expression             => Expression (Aggr),
 303                      Component_Associations => New_List));
 304
 305             when others =>
 306                raise Program_Error;
 307          end case;
 308
 309          Set_Etype (Aggr, Typ);
 310
 311          --  Populate the new aggregate with component associations
 312
 313          while Present (Assoc) loop
 314             Expr := Expression (Assoc);
 315             Comp := First (Choices (Assoc));
 316
 317             while Present (Comp) loop
 318                Comp_Id   := Entity (Comp);
 319                Comp_Type := Etype (Comp_Id);
 320
 321                New_Assoc :=
 322                  Make_Component_Association
 323                    (Sloc       => Sloc (Assoc),
 324                     Choices    =>
 325                       New_List
 326                         (New_Occurrence_Of (Comp_Id, Sloc (Comp))),
 327                     Expression => New_Copy_Tree (Expr));
 328
 329                --  New association must be attached to the aggregate before we
 330                --  analyze it.
 331
 332                Append (New_Assoc, Component_Associations (Aggr));
 333
 334                Analyze_And_Resolve (Expression (New_Assoc), Comp_Type);
 335
 336                if Is_Scalar_Type (Comp_Type) then
 337                   Apply_Scalar_Range_Check
 338                     (Expression (New_Assoc), Comp_Type);
 339                end if;
 340
 341                Next (Comp);
 342             end loop;
 343
 344             Next (Assoc);
 345          end loop;
 346       end if;
 347    end Expand_SPARK_Delta_Or_Update;
 348
 349    --------------------------------
 350    -- Expand_SPARK_N_Freeze_Type --
 351    --------------------------------
 352
 353    procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is
 354    begin
 355       --  When a DIC is inherited by a tagged type, it may need to be
 356       --  specialized to the descendant type, hence build a separate DIC
 357       --  procedure for it as done during regular expansion for compilation.
 358
 359       if Has_DIC (E) and then Is_Tagged_Type (E) then
 360          Build_DIC_Procedure_Body (E, For_Freeze => True);
 361       end if;
 362    end Expand_SPARK_N_Freeze_Type;
 363
 364    ----------------------------------------
 365    -- Expand_SPARK_N_Attribute_Reference --
 366    ----------------------------------------
 367
 368    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
 369       Aname   : constant Name_Id      := Attribute_Name (N);
 370       Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
 371       Loc     : constant Source_Ptr   := Sloc (N);
 372       Pref    : constant Node_Id      := Prefix (N);
 373       Typ     : constant Entity_Id    := Etype (N);
 374       Expr    : Node_Id;
 375
 376    begin
 377       if Attr_Id = Attribute_To_Address then
 378
 379          --  Extract and convert argument to expected type for call
 380
 381          Expr :=
 382            Make_Type_Conversion (Loc,
 383              Subtype_Mark =>
 384                New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
 385              Expression   => Relocate_Node (First (Expressions (N))));
 386
 387          --  Replace attribute reference with call
 388
 389          Rewrite (N,
 390            Make_Function_Call (Loc,
 391              Name                   =>
 392                New_Occurrence_Of (RTE (RE_To_Address), Loc),
 393              Parameter_Associations => New_List (Expr)));
 394          Analyze_And_Resolve (N, Typ);
 395
 396       elsif Attr_Id = Attribute_Object_Size
 397         or else Attr_Id = Attribute_Size
 398         or else Attr_Id = Attribute_Value_Size
 399         or else Attr_Id = Attribute_VADS_Size
 400       then
 401          Exp_Attr.Expand_Size_Attribute (N);
 402
 403       --  For attributes which return Universal_Integer, introduce a conversion
 404       --  to the expected type with the appropriate check flags set.
 405
 406       elsif Attr_Id = Attribute_Alignment
 407         or else Attr_Id = Attribute_Bit
 408         or else Attr_Id = Attribute_Bit_Position
 409         or else Attr_Id = Attribute_Descriptor_Size
 410         or else Attr_Id = Attribute_First_Bit
 411         or else Attr_Id = Attribute_Last_Bit
 412         or else Attr_Id = Attribute_Length
 413         or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
 414         or else Attr_Id = Attribute_Pos
 415         or else Attr_Id = Attribute_Position
 416         or else Attr_Id = Attribute_Range_Length
 417         or else Attr_Id = Attribute_Aft
 418         or else Attr_Id = Attribute_Max_Alignment_For_Allocation
 419       then
 420          --  If the expected type is Long_Long_Integer, there will be no check
 421          --  flag as the compiler assumes attributes always fit in this type.
 422          --  Since in SPARK_Mode we do not take Storage_Error into account, we
 423          --  cannot make this assumption and need to produce a check.
 424          --  ??? It should be enough to add this check for attributes
 425          --  'Length, 'Range_Length and 'Pos when the type is as big
 426          --  as Long_Long_Integer.
 427
 428          declare
 429             Typ : Entity_Id;
 430          begin
 431             if Attr_Id = Attribute_Range_Length
 432               or else Attr_Id = Attribute_Pos
 433             then
 434                Typ := Etype (Prefix (N));
 435
 436             elsif Attr_Id = Attribute_Length then
 437                Typ := Get_Index_Subtype (N);
 438
 439             else
 440                Typ := Empty;
 441             end if;
 442
 443             Apply_Universal_Integer_Attribute_Checks (N);
 444
 445             if Present (Typ)
 446               and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
 447             then
 448                --  ??? This should rather be a range check, but this would
 449                --  crash GNATprove which somehow recovers the proper kind
 450                --  of check anyway.
 451                Set_Do_Overflow_Check (N);
 452             end if;
 453          end;
 454
 455       elsif Attr_Id = Attribute_Constrained then
 456
 457          --  If the prefix is an access to object, the attribute applies to
 458          --  the designated object, so rewrite with an explicit dereference.
 459
 460          if Is_Access_Type (Etype (Pref))
 461            and then
 462              (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
 463          then
 464             Rewrite (Pref,
 465                      Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
 466             Analyze_And_Resolve (N, Standard_Boolean);
 467          end if;
 468
 469       elsif Attr_Id = Attribute_Update then
 470          Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
 471       end if;
 472    end Expand_SPARK_N_Attribute_Reference;
 473
 474    ------------------------------------
 475    -- Expand_SPARK_N_Delta_Aggregate --
 476    ------------------------------------
 477
 478    procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is
 479    begin
 480       Expand_SPARK_Delta_Or_Update (Etype (N), N);
 481    end Expand_SPARK_N_Delta_Aggregate;
 482
 483    -----------------------------------
 484    -- Expand_SPARK_N_Loop_Statement --
 485    -----------------------------------
 486
 487    procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is
 488       Scheme : constant Node_Id := Iteration_Scheme (N);
 489
 490    begin
 491       --  Loop iterations over arrays need to be expanded, to avoid getting
 492       --  two names referring to the same object in memory (the array and the
 493       --  iterator) in GNATprove, especially since both can be written (thus
 494       --  possibly leading to interferences due to aliasing). No such problem
 495       --  arises with quantified expressions over arrays, which are dealt with
 496       --  specially in GNATprove.
 497
 498       if Present (Scheme)
 499         and then Present (Iterator_Specification (Scheme))
 500         and then Is_Iterator_Over_Array (Iterator_Specification (Scheme))
 501       then
 502          Expand_Iterator_Loop_Over_Array (N);
 503       end if;
 504    end Expand_SPARK_N_Loop_Statement;
 505
 506    ---------------------------------------
 507    -- Expand_SPARK_N_Object_Declaration --
 508    ---------------------------------------
 509
 510    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
 511       Loc    : constant Source_Ptr := Sloc (N);
 512       Obj_Id : constant Entity_Id  := Defining_Identifier (N);
 513       Typ    : constant Entity_Id  := Etype (Obj_Id);
 514
 515       Call : Node_Id;
 516
 517    begin
 518       --  If the object declaration denotes a variable without initialization
 519       --  whose type is subject to pragma Default_Initial_Condition, create
 520       --  and analyze a dummy call to the DIC procedure of the type in order
 521       --  to detect potential elaboration issues.
 522
 523       if Comes_From_Source (Obj_Id)
 524         and then Ekind (Obj_Id) = E_Variable
 525         and then Has_DIC (Typ)
 526         and then Present (DIC_Procedure (Typ))
 527         and then not Has_Init_Expression (N)
 528       then
 529          Call := Build_DIC_Call (Loc, Obj_Id, Typ);
 530
 531          --  Partially insert the call into the tree by setting its parent
 532          --  pointer.
 533
 534          Set_Parent (Call, N);
 535          Analyze (Call);
 536       end if;
 537    end Expand_SPARK_N_Object_Declaration;
 538
 539    ------------------------------------------------
 540    -- Expand_SPARK_N_Object_Renaming_Declaration --
 541    ------------------------------------------------
 542
 543    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 544       CFS    : constant Boolean    := Comes_From_Source (N);
 545       Loc    : constant Source_Ptr := Sloc (N);
 546       Obj_Id : constant Entity_Id  := Defining_Entity (N);
 547       Nam    : constant Node_Id    := Name (N);
 548       Typ    : constant Entity_Id  := Etype (Obj_Id);
 549
 550    begin
 551       --  Transform a renaming of the form
 552
 553       --    Obj_Id : <subtype mark> renames <function call>;
 554
 555       --  into
 556
 557       --    Obj_Id : constant <subtype mark> := <function call>;
 558
 559       --  Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
 560       --  a temporary to capture the function result. Once potential renamings
 561       --  are rewritten for SPARK, the temporary may be leaked out into source
 562       --  constructs and lead to confusing error diagnostics. Using an object
 563       --  declaration prevents this unwanted side effect.
 564
 565       if Nkind (Nam) = N_Function_Call then
 566          Rewrite (N,
 567            Make_Object_Declaration (Loc,
 568              Defining_Identifier => Obj_Id,
 569              Constant_Present    => True,
 570              Object_Definition   => New_Occurrence_Of (Typ, Loc),
 571              Expression          => Nam));
 572
 573          --  Inherit the original Comes_From_Source status of the renaming
 574
 575          Set_Comes_From_Source (N, CFS);
 576
 577          --  Sever the link to the renamed function result because the entity
 578          --  will no longer alias anything.
 579
 580          Set_Renamed_Object (Obj_Id, Empty);
 581
 582          --  Remove the entity of the renaming declaration from visibility as
 583          --  the analysis of the object declaration will reintroduce it again.
 584
 585          Remove_Entity_And_Homonym (Obj_Id);
 586          Analyze (N);
 587
 588       --  Otherwise unconditionally remove all side effects from the name
 589
 590       else
 591          Evaluate_Name (Nam);
 592       end if;
 593    end Expand_SPARK_N_Object_Renaming_Declaration;
 594
 595    --------------------------
 596    -- Expand_SPARK_N_Op_Ne --
 597    --------------------------
 598
 599    procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is
 600       Typ : constant Entity_Id := Etype (Left_Opnd (N));
 601
 602    begin
 603       --  Case of elementary type with standard operator
 604
 605       if Is_Elementary_Type (Typ)
 606         and then Sloc (Entity (N)) = Standard_Location
 607       then
 608          null;
 609
 610       else
 611          Exp_Ch4.Expand_N_Op_Ne (N);
 612       end if;
 613    end Expand_SPARK_N_Op_Ne;
 614
 615    -------------------------------------
 616    -- Expand_SPARK_Potential_Renaming --
 617    -------------------------------------
 618
 619    procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
 620       function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
 621       --  Determine whether arbitrary node Nod appears within a significant
 622       --  pragma for SPARK.
 623
 624       -----------------------------
 625       -- In_Insignificant_Pragma --
 626       -----------------------------
 627
 628       function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
 629          Par : Node_Id;
 630
 631       begin
 632          --  Climb the parent chain looking for an enclosing pragma
 633
 634          Par := Nod;
 635          while Present (Par) loop
 636             if Nkind (Par) = N_Pragma then
 637                return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
 638
 639             --  Prevent the search from going too far
 640
 641             elsif Is_Body_Or_Package_Declaration (Par) then
 642                exit;
 643             end if;
 644
 645             Par := Parent (Par);
 646          end loop;
 647
 648          return False;
 649       end In_Insignificant_Pragma;
 650
 651       --  Local variables
 652
 653       Loc    : constant Source_Ptr := Sloc (N);
 654       Obj_Id : constant Entity_Id  := Entity (N);
 655       Typ    : constant Entity_Id  := Etype (N);
 656       Ren    : Node_Id;
 657
 658    --  Start of processing for Expand_SPARK_Potential_Renaming
 659
 660    begin
 661       --  Replace a reference to a renaming with the actual renamed object
 662
 663       if Is_Object (Obj_Id) then
 664          Ren := Renamed_Object (Obj_Id);
 665
 666          if Present (Ren) then
 667
 668             --  Do not process a reference when it appears within a pragma of
 669             --  no significance to SPARK. It is assumed that the replacement
 670             --  will violate the semantics of the pragma and cause a spurious
 671             --  error.
 672
 673             if In_Insignificant_Pragma (N) then
 674                return;
 675
 676             --  Instantiations and inlining of subprograms employ "prologues"
 677             --  which map actual to formal parameters by means of renamings.
 678             --  Replace a reference to a formal by the corresponding actual
 679             --  parameter.
 680
 681             elsif Nkind (Ren) in N_Entity then
 682                Rewrite (N, New_Occurrence_Of (Ren, Loc));
 683
 684             --  Otherwise the renamed object denotes a name
 685
 686             else
 687                Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
 688                Reset_Analyzed_Flags (N);
 689             end if;
 690
 691             Analyze_And_Resolve (N, Typ);
 692          end if;
 693       end if;
 694    end Expand_SPARK_Potential_Renaming;
 695
 696 end Exp_SPARK;