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 26with Atree; use Atree; 27with Checks; use Checks; 28with Einfo; use Einfo; 29with Einfo.Entities; use Einfo.Entities; 30with Einfo.Utils; use Einfo.Utils; 31with Exp_Attr; 32with Exp_Ch3; 33with Exp_Ch4; 34with Exp_Ch5; use Exp_Ch5; 35with Exp_Dbug; use Exp_Dbug; 36with Exp_Util; use Exp_Util; 37with Ghost; use Ghost; 38with Namet; use Namet; 39with Nlists; use Nlists; 40with Nmake; use Nmake; 41with Opt; use Opt; 42with Restrict; use Restrict; 43with Rident; use Rident; 44with Rtsfind; use Rtsfind; 45with Sem; use Sem; 46with Sem_Aux; use Sem_Aux; 47with Sem_Ch7; use Sem_Ch7; 48with Sem_Ch8; use Sem_Ch8; 49with Sem_Prag; use Sem_Prag; 50with Sem_Res; use Sem_Res; 51with Sem_Util; use Sem_Util; 52with Sinfo; use Sinfo; 53with Sinfo.Nodes; use Sinfo.Nodes; 54with Sinfo.Utils; use Sinfo.Utils; 55with Snames; use Snames; 56with Stand; use Stand; 57with Tbuild; use Tbuild; 58with Uintp; use Uintp; 59 60package body Exp_SPARK is 61 62 ----------------------- 63 -- Local Subprograms -- 64 ----------------------- 65 66 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id); 67 -- Perform attribute-reference-specific expansion 68 69 procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id); 70 -- Perform delta-aggregate-specific expansion 71 72 procedure Expand_SPARK_N_Freeze_Entity (N : Node_Id); 73 -- Do a minimal expansion of freeze entities required by GNATprove. It is 74 -- a subset of what is done for GNAT in Exp_Ch13.Expand_N_Freeze_Entity. 75 -- Those two routines should be kept in sync. 76 77 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id); 78 -- Perform loop-statement-specific expansion 79 80 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); 81 -- Perform object-declaration-specific expansion 82 83 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id); 84 -- Perform name evaluation for a renamed object 85 86 procedure Expand_SPARK_N_Op_Ne (N : Node_Id); 87 -- Rewrite operator /= based on operator = when defined explicitly 88 89 procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id); 90 -- Common expansion for attribute Update and delta aggregates 91 92 procedure SPARK_Freeze_Type (N : Node_Id); 93 -- Do a minimal type freezing required by GNATprove. It is a subset of what 94 -- is done for GNAT in Exp_Ch3.Freeze_Type. Those two routines should be 95 -- kept in sync. 96 -- 97 -- Currently in freezing we build the spec of dispatching equality. This 98 -- spec is needed to properly resolve references to the equality operator. 99 -- The body is not needed, because proof knows how to directly synthesize a 100 -- logical meaning for it. Also, for tagged types with extension the 101 -- expanded body would compare the _parent component, which is 102 -- intentionally not generated in the GNATprove mode. 103 -- 104 -- We build the DIC procedure body here as well. 105 106 ------------------ 107 -- Expand_SPARK -- 108 ------------------ 109 110 procedure Expand_SPARK (N : Node_Id) is 111 begin 112 case Nkind (N) is 113 114 -- Qualification of entity names in formal verification mode 115 -- is limited to the addition of a suffix for homonyms (see 116 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names 117 -- as full expansion does, but this was removed as this prevents the 118 -- verification back-end from using a short name for debugging and 119 -- user interaction. The verification back-end already takes care 120 -- of qualifying names when needed. 121 122 when N_Block_Statement 123 | N_Entry_Declaration 124 | N_Package_Body 125 | N_Package_Declaration 126 | N_Protected_Type_Declaration 127 | N_Subprogram_Body 128 | N_Task_Type_Declaration 129 => 130 Qualify_Entity_Names (N); 131 132 -- Replace occurrences of System'To_Address by calls to 133 -- System.Storage_Elements.To_Address. 134 135 when N_Attribute_Reference => 136 Expand_SPARK_N_Attribute_Reference (N); 137 138 when N_Delta_Aggregate => 139 Expand_SPARK_N_Delta_Aggregate (N); 140 141 when N_Expanded_Name 142 | N_Identifier 143 => 144 Expand_SPARK_Potential_Renaming (N); 145 146 -- Loop iterations over arrays need to be expanded, to avoid getting 147 -- two names referring to the same object in memory (the array and 148 -- the iterator) in GNATprove, especially since both can be written 149 -- (thus possibly leading to interferences due to aliasing). No such 150 -- problem arises with quantified expressions over arrays, which are 151 -- dealt with specially in GNATprove. 152 153 when N_Loop_Statement => 154 Expand_SPARK_N_Loop_Statement (N); 155 156 when N_Object_Declaration => 157 Expand_SPARK_N_Object_Declaration (N); 158 159 when N_Object_Renaming_Declaration => 160 Expand_SPARK_N_Object_Renaming_Declaration (N); 161 162 when N_Op_Ne => 163 Expand_SPARK_N_Op_Ne (N); 164 165 when N_Freeze_Entity => 166 -- Currently we only expand type freeze entities, so ignore other 167 -- freeze entites, because it is expensive to create a suitable 168 -- freezing environment. 169 170 if Is_Type (Entity (N)) then 171 Expand_SPARK_N_Freeze_Entity (N); 172 end if; 173 174 -- In SPARK mode, no other constructs require expansion 175 176 when others => 177 null; 178 end case; 179 end Expand_SPARK; 180 181 ---------------------------------- 182 -- Expand_SPARK_Delta_Or_Update -- 183 ---------------------------------- 184 185 procedure Expand_SPARK_Delta_Or_Update 186 (Typ : Entity_Id; 187 Aggr : Node_Id) 188 is 189 Assoc : Node_Id; 190 Comp : Node_Id; 191 Comp_Id : Entity_Id; 192 Comp_Type : Entity_Id; 193 Expr : Node_Id; 194 Index : Node_Id; 195 Index_Typ : Entity_Id; 196 New_Assoc : Node_Id; 197 198 begin 199 -- Apply scalar range checks on the updated components, if needed 200 201 if Is_Array_Type (Typ) then 202 203 -- Multidimensional arrays 204 205 if Present (Next_Index (First_Index (Typ))) then 206 Assoc := First (Component_Associations (Aggr)); 207 208 while Present (Assoc) loop 209 Expr := Expression (Assoc); 210 Comp_Type := Component_Type (Typ); 211 212 if Is_Scalar_Type (Comp_Type) then 213 Apply_Scalar_Range_Check (Expr, Comp_Type); 214 end if; 215 216 -- The current association contains a sequence of indexes 217 -- denoting an element of a multidimensional array: 218 -- 219 -- (Index_1, ..., Index_N) 220 221 Expr := First (Choices (Assoc)); 222 223 pragma Assert (Nkind (Aggr) = N_Aggregate); 224 225 while Present (Expr) loop 226 Index := First (Expressions (Expr)); 227 Index_Typ := First_Index (Typ); 228 229 while Present (Index_Typ) loop 230 Apply_Scalar_Range_Check (Index, Etype (Index_Typ)); 231 Next (Index); 232 Next_Index (Index_Typ); 233 end loop; 234 235 Next (Expr); 236 end loop; 237 238 Next (Assoc); 239 end loop; 240 241 -- One-dimensional arrays 242 243 else 244 Assoc := First (Component_Associations (Aggr)); 245 246 while Present (Assoc) loop 247 Expr := Expression (Assoc); 248 Comp_Type := Component_Type (Typ); 249 250 -- Analyze expression of the iterated_component_association 251 -- with its index parameter in scope. 252 253 if Nkind (Assoc) = N_Iterated_Component_Association then 254 Push_Scope (Scope (Defining_Identifier (Assoc))); 255 Enter_Name (Defining_Identifier (Assoc)); 256 Analyze_And_Resolve (Expr, Comp_Type); 257 end if; 258 259 if Is_Scalar_Type (Comp_Type) then 260 Apply_Scalar_Range_Check (Expr, Comp_Type); 261 end if; 262 263 -- Restore scope of the iterated_component_association 264 265 if Nkind (Assoc) = N_Iterated_Component_Association then 266 End_Scope; 267 end if; 268 269 Index := First (Choice_List (Assoc)); 270 Index_Typ := First_Index (Typ); 271 272 while Present (Index) loop 273 -- If the index denotes a range of elements or a constrained 274 -- subtype indication, then their low and high bounds 275 -- already have range checks applied. 276 277 if Nkind (Index) in N_Range | N_Subtype_Indication then 278 null; 279 280 -- Otherwise the index denotes a single expression where 281 -- range checks need to be applied or a subtype name 282 -- (without range constraints) where applying checks is 283 -- harmless. 284 -- 285 -- In delta_aggregate and Update attribute on array the 286 -- others_choice is not allowed. 287 288 else pragma Assert (Nkind (Index) in N_Subexpr); 289 Apply_Scalar_Range_Check (Index, Etype (Index_Typ)); 290 end if; 291 292 Next (Index); 293 end loop; 294 295 Next (Assoc); 296 end loop; 297 end if; 298 299 else pragma Assert (Is_Record_Type (Typ)); 300 301 -- If the aggregate has multiple component choices, e.g.: 302 -- 303 -- X'Update (A | B | C => 123) 304 -- 305 -- then each component might be of a different type and might or 306 -- might not require a range check. We first rewrite associations 307 -- into single-component choices, e.g.: 308 -- 309 -- X'Update (A => 123, B => 123, C => 123) 310 -- 311 -- and then apply range checks to individual copies of the 312 -- expressions. We do the same for delta aggregates, accordingly. 313 314 -- Iterate over associations of the original aggregate 315 316 Assoc := First (Component_Associations (Aggr)); 317 318 -- Rewrite into a new aggregate and decorate 319 320 case Nkind (Aggr) is 321 when N_Aggregate => 322 Rewrite 323 (Aggr, 324 Make_Aggregate 325 (Sloc => Sloc (Aggr), 326 Component_Associations => New_List)); 327 328 when N_Delta_Aggregate => 329 Rewrite 330 (Aggr, 331 Make_Delta_Aggregate 332 (Sloc => Sloc (Aggr), 333 Expression => Expression (Aggr), 334 Component_Associations => New_List)); 335 336 when others => 337 raise Program_Error; 338 end case; 339 340 Set_Etype (Aggr, Typ); 341 342 -- Populate the new aggregate with component associations 343 344 while Present (Assoc) loop 345 Expr := Expression (Assoc); 346 Comp := First (Choices (Assoc)); 347 348 while Present (Comp) loop 349 Comp_Id := Entity (Comp); 350 Comp_Type := Etype (Comp_Id); 351 352 New_Assoc := 353 Make_Component_Association 354 (Sloc => Sloc (Assoc), 355 Choices => 356 New_List 357 (New_Occurrence_Of (Comp_Id, Sloc (Comp))), 358 Expression => New_Copy_Tree (Expr)); 359 360 -- New association must be attached to the aggregate before we 361 -- analyze it. 362 363 Append (New_Assoc, Component_Associations (Aggr)); 364 365 Analyze_And_Resolve (Expression (New_Assoc), Comp_Type); 366 367 if Is_Scalar_Type (Comp_Type) then 368 Apply_Scalar_Range_Check 369 (Expression (New_Assoc), Comp_Type); 370 end if; 371 372 Next (Comp); 373 end loop; 374 375 Next (Assoc); 376 end loop; 377 end if; 378 end Expand_SPARK_Delta_Or_Update; 379 380 ---------------------------------- 381 -- Expand_SPARK_N_Freeze_Entity -- 382 ---------------------------------- 383 384 procedure Expand_SPARK_N_Freeze_Entity (N : Entity_Id) is 385 E : constant Entity_Id := Entity (N); 386 387 Action : Node_Id; 388 E_Scope : Entity_Id; 389 In_Other_Scope : Boolean; 390 In_Outer_Scope : Boolean; 391 392 begin 393 -- Here E is a type or a subprogram 394 395 E_Scope := Scope (E); 396 397 -- This is an error protection against previous errors 398 399 if No (E_Scope) then 400 Check_Error_Detected; 401 return; 402 end if; 403 404 -- The entity may be a subtype declared for a constrained record 405 -- component, in which case the relevant scope is the scope of 406 -- the record. This happens for class-wide subtypes created for 407 -- a constrained type extension with inherited discriminants. 408 409 if Is_Type (E_Scope) 410 and then not Is_Concurrent_Type (E_Scope) 411 then 412 E_Scope := Scope (E_Scope); 413 414 -- The entity may be a subtype declared for an iterator 415 416 elsif Ekind (E_Scope) = E_Loop then 417 E_Scope := Scope (E_Scope); 418 end if; 419 420 -- If we are freezing entities defined in protected types, they belong 421 -- in the enclosing scope, given that the original type has been 422 -- expanded away. The same is true for entities in task types, in 423 -- particular the parameter records of entries (Entities in bodies are 424 -- all frozen within the body). If we are in the task body, this is a 425 -- proper scope. If we are within a subprogram body, the proper scope 426 -- is the corresponding spec. This may happen for itypes generated in 427 -- the bodies of protected operations. 428 429 if Ekind (E_Scope) = E_Protected_Type 430 or else (Ekind (E_Scope) = E_Task_Type 431 and then not Has_Completion (E_Scope)) 432 then 433 E_Scope := Scope (E_Scope); 434 435 elsif Ekind (E_Scope) = E_Subprogram_Body then 436 E_Scope := Corresponding_Spec (Unit_Declaration_Node (E_Scope)); 437 end if; 438 439 -- If the scope of the entity is in open scopes, it is the current one 440 -- or an enclosing one, including a loop, a block, or a subprogram. 441 442 if In_Open_Scopes (E_Scope) then 443 In_Other_Scope := False; 444 In_Outer_Scope := E_Scope /= Current_Scope; 445 446 -- Otherwise it is a local package or a different compilation unit 447 448 else 449 In_Other_Scope := True; 450 In_Outer_Scope := False; 451 end if; 452 453 -- If the entity being frozen is defined in a scope that is not 454 -- currently on the scope stack, we must establish the proper 455 -- visibility before freezing the entity and related subprograms. 456 457 if In_Other_Scope then 458 Push_Scope (E_Scope); 459 460 -- Finalizers are little odd in terms of freezing. The spec of the 461 -- procedure appears in the declarations while the body appears in 462 -- the statement part of a single construct. Since the finalizer must 463 -- be called by the At_End handler of the construct, the spec is 464 -- manually frozen right after its declaration. The only side effect 465 -- of this action appears in contexts where the construct is not in 466 -- its final resting place. These contexts are: 467 468 -- * Entry bodies - The declarations and statements are moved to 469 -- the procedure equivalen of the entry. 470 -- * Protected subprograms - The declarations and statements are 471 -- moved to the non-protected version of the subprogram. 472 -- * Task bodies - The declarations and statements are moved to the 473 -- task body procedure. 474 -- * Blocks that will be rewritten as subprograms when unnesting 475 -- is in effect. 476 477 -- Visible declarations do not need to be installed in these three 478 -- cases since it does not make semantic sense to do so. All entities 479 -- referenced by a finalizer are visible and already resolved, plus 480 -- the enclosing scope may not have visible declarations at all. 481 482 if Ekind (E) = E_Procedure 483 and then Is_Finalizer (E) 484 and then 485 (Is_Entry (E_Scope) 486 or else (Is_Subprogram (E_Scope) 487 and then Is_Protected_Type (Scope (E_Scope))) 488 or else Is_Task_Type (E_Scope) 489 or else Ekind (E_Scope) = E_Block) 490 then 491 null; 492 else 493 Install_Visible_Declarations (E_Scope); 494 end if; 495 496 if Is_Concurrent_Type (E_Scope) 497 or else Is_Package_Or_Generic_Package (E_Scope) 498 then 499 Install_Private_Declarations (E_Scope); 500 end if; 501 502 -- If the entity is in an outer scope, then that scope needs to 503 -- temporarily become the current scope so that operations created 504 -- during type freezing will be declared in the right scope and 505 -- can properly override any corresponding inherited operations. 506 507 elsif In_Outer_Scope then 508 Push_Scope (E_Scope); 509 end if; 510 511 -- Remember that we are processing a freezing entity and its freezing 512 -- nodes. This flag (non-zero = set) is used to avoid the need of 513 -- climbing through the tree while processing the freezing actions (ie. 514 -- to avoid generating spurious warnings or to avoid killing constant 515 -- indications while processing the code associated with freezing 516 -- actions). We use a counter to deal with nesting. 517 518 Inside_Freezing_Actions := Inside_Freezing_Actions + 1; 519 520 -- Currently only types require freezing in SPARK 521 522 SPARK_Freeze_Type (N); 523 524 -- Analyze actions in freeze node, if any 525 526 Action := First (Actions (N)); 527 while Present (Action) loop 528 Analyze (Action); 529 Next (Action); 530 end loop; 531 532 -- Pop scope if we installed one for the analysis 533 534 if In_Other_Scope then 535 if Ekind (Current_Scope) = E_Package then 536 End_Package_Scope (E_Scope); 537 else 538 End_Scope; 539 end if; 540 541 elsif In_Outer_Scope then 542 Pop_Scope; 543 end if; 544 545 -- Restore previous value of the nesting-level counter that records 546 -- whether we are inside a (possibly nested) call to this procedure. 547 548 Inside_Freezing_Actions := Inside_Freezing_Actions - 1; 549 end Expand_SPARK_N_Freeze_Entity; 550 551 ---------------------------------------- 552 -- Expand_SPARK_N_Attribute_Reference -- 553 ---------------------------------------- 554 555 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is 556 Aname : constant Name_Id := Attribute_Name (N); 557 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname); 558 Loc : constant Source_Ptr := Sloc (N); 559 Pref : constant Node_Id := Prefix (N); 560 Typ : constant Entity_Id := Etype (N); 561 Expr : Node_Id; 562 563 begin 564 case Attr_Id is 565 when Attribute_To_Address => 566 567 -- Extract and convert argument to expected type for call 568 569 Expr := 570 Make_Type_Conversion (Loc, 571 Subtype_Mark => 572 New_Occurrence_Of (RTE (RE_Integer_Address), Loc), 573 Expression => Relocate_Node (First (Expressions (N)))); 574 575 -- Replace attribute reference with call 576 577 Rewrite 578 (N, 579 Make_Function_Call (Loc, 580 Name => 581 New_Occurrence_Of (RTE (RE_To_Address), Loc), 582 Parameter_Associations => New_List (Expr))); 583 Analyze_And_Resolve (N, Typ); 584 585 when Attribute_Object_Size 586 | Attribute_Size 587 | Attribute_Value_Size 588 | Attribute_VADS_Size 589 => 590 Exp_Attr.Expand_Size_Attribute (N); 591 592 -- For attributes which return Universal_Integer, introduce a 593 -- conversion to the expected type with the appropriate check flags 594 -- set. 595 596 when Attribute_Aft 597 | Attribute_Alignment 598 | Attribute_Bit 599 | Attribute_Bit_Position 600 | Attribute_Descriptor_Size 601 | Attribute_First_Bit 602 | Attribute_Last_Bit 603 | Attribute_Length 604 | Attribute_Max_Alignment_For_Allocation 605 | Attribute_Max_Size_In_Storage_Elements 606 | Attribute_Pos 607 | Attribute_Position 608 | Attribute_Range_Length 609 => 610 -- If the expected type is Long_Long_Integer, there will be no 611 -- check flag as the compiler assumes attributes always fit in 612 -- this type. Since in SPARK_Mode we do not take Storage_Error 613 -- into account, we cannot make this assumption and need to 614 -- produce a check. ??? It should be enough to add this check for 615 -- attributes 'Length, 'Range_Length and 'Pos when the type is as 616 -- big as Long_Long_Integer. 617 618 declare 619 Typ : Entity_Id; 620 begin 621 if Attr_Id in Attribute_Pos | Attribute_Range_Length then 622 Typ := Etype (Prefix (N)); 623 624 elsif Attr_Id = Attribute_Length then 625 Typ := Get_Index_Subtype (N); 626 627 else 628 Typ := Empty; 629 end if; 630 631 Apply_Universal_Integer_Attribute_Checks (N); 632 633 if Present (Typ) 634 and then Known_RM_Size (Typ) 635 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer) 636 then 637 -- ??? This should rather be a range check, but this would 638 -- crash GNATprove which somehow recovers the proper kind 639 -- of check anyway. 640 Set_Do_Overflow_Check (N); 641 end if; 642 end; 643 644 when Attribute_Constrained => 645 646 -- If the prefix is an access to object, the attribute applies to 647 -- the designated object, so rewrite with an explicit dereference. 648 649 if Is_Access_Type (Etype (Pref)) 650 and then 651 (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref))) 652 then 653 Rewrite (Pref, 654 Make_Explicit_Dereference (Loc, Relocate_Node (Pref))); 655 Analyze_And_Resolve (N, Standard_Boolean); 656 end if; 657 658 when Attribute_Update => 659 Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N))); 660 661 when others => 662 null; 663 end case; 664 end Expand_SPARK_N_Attribute_Reference; 665 666 ------------------------------------ 667 -- Expand_SPARK_N_Delta_Aggregate -- 668 ------------------------------------ 669 670 procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is 671 begin 672 Expand_SPARK_Delta_Or_Update (Etype (N), N); 673 end Expand_SPARK_N_Delta_Aggregate; 674 675 ----------------------------------- 676 -- Expand_SPARK_N_Loop_Statement -- 677 ----------------------------------- 678 679 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is 680 Scheme : constant Node_Id := Iteration_Scheme (N); 681 682 begin 683 -- Loop iterations over arrays need to be expanded, to avoid getting 684 -- two names referring to the same object in memory (the array and the 685 -- iterator) in GNATprove, especially since both can be written (thus 686 -- possibly leading to interferences due to aliasing). No such problem 687 -- arises with quantified expressions over arrays, which are dealt with 688 -- specially in GNATprove. 689 690 if Present (Scheme) 691 and then Present (Iterator_Specification (Scheme)) 692 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme)) 693 then 694 Expand_Iterator_Loop_Over_Array (N); 695 end if; 696 end Expand_SPARK_N_Loop_Statement; 697 698 --------------------------------------- 699 -- Expand_SPARK_N_Object_Declaration -- 700 --------------------------------------- 701 702 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is 703 Loc : constant Source_Ptr := Sloc (N); 704 Obj_Id : constant Entity_Id := Defining_Identifier (N); 705 Typ : constant Entity_Id := Etype (Obj_Id); 706 707 Call : Node_Id; 708 709 begin 710 -- If the object declaration denotes a variable without initialization 711 -- whose type is subject to pragma Default_Initial_Condition, create 712 -- and analyze a dummy call to the DIC procedure of the type in order 713 -- to detect potential elaboration issues. 714 715 if Comes_From_Source (Obj_Id) 716 and then Ekind (Obj_Id) = E_Variable 717 and then Has_DIC (Typ) 718 and then Present (DIC_Procedure (Typ)) 719 and then not Has_Init_Expression (N) 720 then 721 Call := Build_DIC_Call (Loc, New_Occurrence_Of (Obj_Id, Loc), Typ); 722 723 -- Partially insert the call into the tree by setting its parent 724 -- pointer. 725 726 Set_Parent (Call, N); 727 Analyze (Call); 728 end if; 729 end Expand_SPARK_N_Object_Declaration; 730 731 ------------------------------------------------ 732 -- Expand_SPARK_N_Object_Renaming_Declaration -- 733 ------------------------------------------------ 734 735 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is 736 CFS : constant Boolean := Comes_From_Source (N); 737 Loc : constant Source_Ptr := Sloc (N); 738 Obj_Id : constant Entity_Id := Defining_Entity (N); 739 Nam : constant Node_Id := Name (N); 740 Typ : constant Entity_Id := Etype (Obj_Id); 741 742 begin 743 -- Transform a renaming of the form 744 745 -- Obj_Id : <subtype mark> renames <function call>; 746 747 -- into 748 749 -- Obj_Id : constant <subtype mark> := <function call>; 750 751 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces 752 -- a temporary to capture the function result. Once potential renamings 753 -- are rewritten for SPARK, the temporary may be leaked out into source 754 -- constructs and lead to confusing error diagnostics. Using an object 755 -- declaration prevents this unwanted side effect. 756 757 if Nkind (Nam) = N_Function_Call then 758 Rewrite (N, 759 Make_Object_Declaration (Loc, 760 Defining_Identifier => Obj_Id, 761 Constant_Present => True, 762 Object_Definition => New_Occurrence_Of (Typ, Loc), 763 Expression => Nam)); 764 765 -- Inherit the original Comes_From_Source status of the renaming 766 767 Set_Comes_From_Source (N, CFS); 768 769 -- Sever the link to the renamed function result because the entity 770 -- will no longer alias anything. 771 772 Set_Renamed_Object (Obj_Id, Empty); 773 774 -- Remove the entity of the renaming declaration from visibility as 775 -- the analysis of the object declaration will reintroduce it again. 776 777 Remove_Entity_And_Homonym (Obj_Id); 778 Analyze (N); 779 780 -- Otherwise unconditionally remove all side effects from the name 781 782 else 783 Evaluate_Name (Nam); 784 end if; 785 end Expand_SPARK_N_Object_Renaming_Declaration; 786 787 -------------------------- 788 -- Expand_SPARK_N_Op_Ne -- 789 -------------------------- 790 791 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is 792 Typ : constant Entity_Id := Etype (Left_Opnd (N)); 793 794 begin 795 -- Case of elementary type with standard operator 796 797 if Is_Elementary_Type (Typ) 798 and then Sloc (Entity (N)) = Standard_Location 799 then 800 null; 801 802 else 803 Exp_Ch4.Expand_N_Op_Ne (N); 804 end if; 805 end Expand_SPARK_N_Op_Ne; 806 807 ------------------------------------- 808 -- Expand_SPARK_Potential_Renaming -- 809 ------------------------------------- 810 811 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is 812 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean; 813 -- Determine whether arbitrary node Nod appears within a significant 814 -- pragma for SPARK. 815 816 ----------------------------- 817 -- In_Insignificant_Pragma -- 818 ----------------------------- 819 820 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is 821 Par : Node_Id; 822 823 begin 824 -- Climb the parent chain looking for an enclosing pragma 825 826 Par := Nod; 827 while Present (Par) loop 828 if Nkind (Par) = N_Pragma then 829 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par)); 830 831 -- Prevent the search from going too far 832 833 elsif Is_Body_Or_Package_Declaration (Par) then 834 exit; 835 end if; 836 837 Par := Parent (Par); 838 end loop; 839 840 return False; 841 end In_Insignificant_Pragma; 842 843 -- Local variables 844 845 Loc : constant Source_Ptr := Sloc (N); 846 Obj_Id : constant Entity_Id := Entity (N); 847 Typ : constant Entity_Id := Etype (N); 848 Ren : Node_Id; 849 850 -- Start of processing for Expand_SPARK_Potential_Renaming 851 852 begin 853 -- Replace a reference to a renaming with the actual renamed object 854 855 if Is_Object (Obj_Id) then 856 Ren := Renamed_Object (Obj_Id); 857 858 if Present (Ren) then 859 860 -- Do not process a reference when it appears within a pragma of 861 -- no significance to SPARK. It is assumed that the replacement 862 -- will violate the semantics of the pragma and cause a spurious 863 -- error. 864 865 if In_Insignificant_Pragma (N) then 866 return; 867 868 -- Instantiations and inlining of subprograms employ "prologues" 869 -- which map actual to formal parameters by means of renamings. 870 -- Replace a reference to a formal by the corresponding actual 871 -- parameter. 872 873 elsif Nkind (Ren) in N_Entity then 874 Rewrite (N, New_Occurrence_Of (Ren, Loc)); 875 876 -- Otherwise the renamed object denotes a name 877 878 else 879 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc)); 880 Reset_Analyzed_Flags (N); 881 end if; 882 883 Analyze_And_Resolve (N, Typ); 884 end if; 885 end if; 886 end Expand_SPARK_Potential_Renaming; 887 888 ----------------------- 889 -- SPARK_Freeze_Type -- 890 ----------------------- 891 892 procedure SPARK_Freeze_Type (N : Entity_Id) is 893 Typ : constant Entity_Id := Entity (N); 894 895 Renamed_Eq : Node_Id; 896 -- Defining unit name for the predefined equality function in the case 897 -- where the type has a primitive operation that is a renaming of 898 -- predefined equality (but only if there is also an overriding 899 -- user-defined equality function). Used to pass this entity from 900 -- Make_Predefined_Primitive_Specs to Predefined_Primitive_Bodies. 901 902 Decl : Node_Id; 903 Eq_Spec : Node_Id := Empty; 904 Predef_List : List_Id; 905 906 Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; 907 Saved_IGR : constant Node_Id := Ignored_Ghost_Region; 908 -- Save the Ghost-related attributes to restore on exit 909 910 begin 911 -- The type being frozen may be subject to pragma Ghost. Set the mode 912 -- now to ensure that any nodes generated during freezing are properly 913 -- marked as Ghost. 914 915 Set_Ghost_Mode (Typ); 916 917 -- When a DIC is inherited by a tagged type, it may need to be 918 -- specialized to the descendant type, hence build a separate DIC 919 -- procedure for it as done during regular expansion for compilation. 920 921 if Has_DIC (Typ) and then Is_Tagged_Type (Typ) then 922 -- Why is this needed for DIC, but not for other aspects (such as 923 -- Type_Invariant)??? 924 925 Build_DIC_Procedure_Body (Typ); 926 end if; 927 928 if Ekind (Typ) = E_Record_Type 929 and then Is_Tagged_Type (Typ) 930 and then not Is_Interface (Typ) 931 and then not Is_Limited_Type (Typ) 932 then 933 if Is_CPP_Class (Root_Type (Typ)) 934 and then Convention (Typ) = Convention_CPP 935 then 936 null; 937 938 -- Do not add the spec of the predefined primitives if we are 939 -- compiling under restriction No_Dispatching_Calls. 940 941 elsif not Restriction_Active (No_Dispatching_Calls) then 942 Set_Is_Frozen (Typ, False); 943 944 Predef_List := New_List; 945 Exp_Ch3.Make_Predefined_Primitive_Eq_Spec 946 (Typ, Predef_List, Renamed_Eq); 947 Eq_Spec := First (Predef_List); 948 Insert_List_Before_And_Analyze (N, Predef_List); 949 950 Set_Is_Frozen (Typ); 951 952 -- Remove link from the parent list to the spec and body of 953 -- the dispatching equality, but keep the link in the opposite 954 -- direction, to allow up-traversal of the AST. 955 956 if Present (Eq_Spec) then 957 Decl := Parent (Eq_Spec); 958 Remove (Eq_Spec); 959 Set_Parent (Eq_Spec, Decl); 960 end if; 961 end if; 962 end if; 963 964 Restore_Ghost_Region (Saved_GM, Saved_IGR); 965 end SPARK_Freeze_Type; 966 967end Exp_SPARK; 968