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