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