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