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