Mercurial > hg > CbC > CbC_gcc
diff gcc/ada/sem_elab.adb @ 111:04ced10e8804
gcc 7
| author | kono |
|---|---|
| date | Fri, 27 Oct 2017 22:46:09 +0900 |
| parents | |
| children | 84e7813d76e9 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gcc/ada/sem_elab.adb Fri Oct 27 22:46:09 2017 +0900 @@ -0,0 +1,8489 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S E M _ E L A B -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 1997-2017, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- +-- for more details. You should have received a copy of the GNU General -- +-- Public License distributed with GNAT; see file COPYING3. If not, go to -- +-- http://www.gnu.org/licenses for a complete copy of the license. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +with Atree; use Atree; +with Debug; use Debug; +with Einfo; use Einfo; +with Errout; use Errout; +with Exp_Ch11; use Exp_Ch11; +with Exp_Tss; use Exp_Tss; +with Exp_Util; use Exp_Util; +with Lib; use Lib; +with Lib.Load; use Lib.Load; +with Namet; use Namet; +with Nlists; use Nlists; +with Nmake; use Nmake; +with Opt; use Opt; +with Restrict; use Restrict; +with Rident; use Rident; +with Rtsfind; use Rtsfind; +with Sem; use Sem; +with Sem_Aux; use Sem_Aux; +with Sem_Ch7; use Sem_Ch7; +with Sem_Ch8; use Sem_Ch8; +with Sem_Prag; use Sem_Prag; +with Sem_Util; use Sem_Util; +with Sinfo; use Sinfo; +with Snames; use Snames; +with Stand; use Stand; +with Table; +with Tbuild; use Tbuild; +with Uintp; use Uintp; +with Uname; use Uname; + +with GNAT.HTable; use GNAT.HTable; + +package body Sem_Elab is + + ----------------------------------------- + -- Access-before-elaboration mechanism -- + ----------------------------------------- + + -- The access-before-elaboration (ABE) mechanism implemented in this unit + -- has the following objectives: + -- + -- * Diagnose at compile-time or install run-time checks to prevent ABE + -- access to data and behaviour. + -- + -- The high level idea is to accurately diagnose ABE issues within a + -- single unit because the ABE mechanism can inspect the whole unit. + -- As soon as the elaboration graph extends to an external unit, the + -- diagnostics stop because the body of the unit may not be available. + -- Due to control and data flow, the ABE mechanism cannot accurately + -- determine whether a particular scenario will be elaborated or not. + -- Conditional ABE checks are therefore used to verify the elaboration + -- status of a local and external target at run time. + -- + -- * Supply elaboration dependencies for a unit to binde + -- + -- The ABE mechanism registers each outgoing elaboration edge for the + -- main unit in its ALI file. GNATbind and binde can then reconstruct + -- the full elaboration graph and determine the proper elaboration + -- order for all units in the compilation. + -- + -- The ABE mechanism supports three models of elaboration: + -- + -- * Dynamic model - This is the most permissive of the three models. + -- When the dynamic model is in effect, the mechanism performs very + -- little diagnostics and generates run-time checks to detect ABE + -- issues. The behaviour of this model is identical to that specified + -- by the Ada RM. This model is enabled with switch -gnatE. + -- + -- * Static model - This is the middle ground of the three models. When + -- the static model is in effect, the mechanism diagnoses and installs + -- run-time checks to detect ABE issues in the main unit. In addition, + -- the mechanism generates implicit Elaborate or Elaborate_All pragmas + -- to ensure the prior elaboration of withed units. The model employs + -- textual order, with clause context, and elaboration-related source + -- pragmas. This is the default model. + -- + -- * SPARK model - This is the most conservative of the three models and + -- impelements the semantics defined in SPARK RM 7.7. The SPARK model + -- is in effect only when a context resides in a SPARK_Mode On region, + -- otherwise the mechanism falls back to one of the previous models. + -- + -- The ABE mechanism consists of a "recording" phase and a "processing" + -- phase. + + ----------------- + -- Terminology -- + ----------------- + + -- * Bridge target - A type of target. A bridge target is a link between + -- scenarios. It is usually a byproduct of expansion and does not have + -- any direct ABE ramifications. + -- + -- * Call marker - A special node used to indicate the presence of a call + -- in the tree in case expansion transforms or eliminates the original + -- call. N_Call_Marker nodes do not have static and run-time semantics. + -- + -- * Conditional ABE - A type of ABE. A conditional ABE occurs when the + -- elaboration or invocation of a target by a scenario within the main + -- unit causes an ABE, but does not cause an ABE for another scenarios + -- within the main unit. + -- + -- * Declaration level - A type of enclosing level. A scenario or target is + -- at the declaration level when it appears within the declarations of a + -- block statement, entry body, subprogram body, or task body, ignoring + -- enclosing packges. + -- + -- * Generic library level - A type of enclosing level. A scenario or + -- target is at the generic library level if it appears in a generic + -- package library unit, ignoring enclosing packages. + -- + -- * Guaranteed ABE - A type of ABE. A guaranteed ABE occurs when the + -- elaboration or invocation of a target by all scenarios within the + -- main unit causes an ABE. + -- + -- * Instantiation library level - A type of enclosing level. A scenario + -- or target is at the instantiation library level if it appears in an + -- instantiation library unit, ignoring enclosing packages. + -- + -- * Library level - A type of enclosing level. A scenario or target is at + -- the library level if it appears in a package library unit, ignoring + -- enclosng packages. + -- + -- * Non-library level encapsulator - A construct that cannot be elaborated + -- on its own and requires elaboration by a top level scenario. + -- + -- * Scenario - A construct or context which may be elaborated or executed + -- by elaboration code. The scenarios recognized by the ABE mechanism are + -- as follows: + -- + -- - '[Unrestricted_]Access of entries, operators, and subprograms + -- + -- - Assignments to variables + -- + -- - Calls to entries, operators, and subprograms + -- + -- - Instantiations + -- + -- - Reads of variables + -- + -- - Task activation + -- + -- * Target - A construct referenced by a scenario. The targets recognized + -- by the ABE mechanism are as follows: + -- + -- - For '[Unrestricted_]Access of entries, operators, and subprograms, + -- the target is the entry, operator, or subprogram. + -- + -- - For assignments to variables, the target is the variable + -- + -- - For calls, the target is the entry, operator, or subprogram + -- + -- - For instantiations, the target is the generic template + -- + -- - For reads of variables, the target is the variable + -- + -- - For task activation, the target is the task body + -- + -- * Top level scenario - A scenario which appears in a non-generic main + -- unit. Depending on the elaboration model is in effect, the following + -- addotional restrictions apply: + -- + -- - Dynamic model - No restrictions + -- + -- - SPARK model - Falls back to either the dynamic or static model + -- + -- - Static model - The scenario must be at the library level + + --------------------- + -- Recording phase -- + --------------------- + + -- The Recording phase coincides with the analysis/resolution phase of the + -- compiler. It has the following objectives: + -- + -- * Record all top level scenarios for examination by the Processing + -- phase. + -- + -- Saving only a certain number of nodes improves the performance of + -- the ABE mechanism. This eliminates the need to examine the whole + -- tree in a separate pass. + -- + -- * Detect and diagnose calls in preelaborable or pure units, including + -- generic bodies. + -- + -- This diagnostic is carried out during the Recording phase because it + -- does not need the heavy recursive traversal done by the Processing + -- phase. + -- + -- * Detect and diagnose guaranteed ABEs caused by instantiations, + -- calls, and task activation. + -- + -- The issues detected by the ABE mechanism are reported as warnings + -- because they do not violate Ada semantics. Forward instantiations + -- may thus reach gigi, however gigi cannot handle certain kinds of + -- premature instantiations and may crash. To avoid this limitation, + -- the ABE mechanism must identify forward instantiations as early as + -- possible and suppress their bodies. Calls and task activations are + -- included in this category for completeness. + + ---------------------- + -- Processing phase -- + ---------------------- + + -- The Processing phase is a separate pass which starts after instantiating + -- and/or inlining of bodies, but before the removal of Ghost code. It has + -- the following objectives: + -- + -- * Examine all top level scenarios saved during the Recording phase + -- + -- The top level scenarios act as roots for depth-first traversal of + -- the call/instantiation/task activation graph. The traversal stops + -- when an outgoing edge leaves the main unit. + -- + -- * Depending on the elaboration model in effect, perform the following + -- actions: + -- + -- - Dynamic model - Diagnose guaranteed ABEs and install run-time + -- conditional ABE checks. + -- + -- - SPARK model - Enforce the SPARK elaboration rules + -- + -- - Static model - Diagnose conditional/guaranteed ABEs, install + -- run-time conditional ABE checks, and guarantee the elaboration + -- of external units. + -- + -- * Examine nested scenarios + -- + -- Nested scenarios discovered during the depth-first traversal are + -- in turn subjected to the same actions outlined above and examined + -- for the next level of nested scenarios. + + ------------------ + -- Architecture -- + ------------------ + + -- +------------------------ Recording phase ---------------------------+ + -- | | + -- | Record_Elaboration_Scenario | + -- | | | + -- | +--> Check_Preelaborated_Call | + -- | | | + -- | +--> Process_Guaranteed_ABE | + -- | | | + -- +------------------------- | --------------------------------------+ + -- | + -- | + -- v + -- Top_Level_Scenarios + -- +-----------+-----------+ .. +-----------+ + -- | Scenario1 | Scenario2 | .. | ScenarioN | + -- +-----------+-----------+ .. +-----------+ + -- | + -- | + -- +------------------------- | --------------------------------------+ + -- | | | + -- | Check_Elaboration_Scenarios | + -- | | | + -- | v | + -- | +----------- Process_Scenario <-----------+ | + -- | | | | + -- | +--> Process_Access Is_Suitable_Scenario | + -- | | ^ | + -- | +--> Process_Activation_Call --+ | | + -- | | +---> Traverse_Body | + -- | +--> Process_Call -------------+ | + -- | | | + -- | +--> Process_Instantiation | + -- | | | + -- | +--> Process_Variable_Assignment | + -- | | | + -- | +--> Process_Variable_Read | + -- | | + -- +------------------------- Processing phase -------------------------+ + + ---------------------- + -- Important points -- + ---------------------- + + -- The Processing phase starts after the analysis, resolution, expansion + -- phase has completed. As a result, no current semantic information is + -- available. The scope stack is empty, global flags such as In_Instance + -- or Inside_A_Generic become useless. To remedy this, the ABE mechanism + -- must either save or recompute semantic information. + + -- Expansion heavily transforms calls and to some extent instantiations. To + -- remedy this, the ABE mechanism generates N_Call_Marker nodes in order to + -- capture the target and relevant attributes of the original call. + + -- The diagnostics of the ABE mechanism depend on accurate source locations + -- to determine the spacial relation of nodes. + + -------------- + -- Switches -- + -------------- + + -- The following switches may be used to control the behavior of the ABE + -- mechanism. + -- + -- -gnatdE elaboration checks on predefined units + -- + -- The ABE mechanism considers scenarios which appear in internal + -- units (Ada, GNAT, Interfaces, System). + -- + -- -gnatd.G ignore calls through generic formal parameters for elaboration + -- + -- The ABE mechanism does not generate N_Call_Marker nodes for + -- calls which occur in expanded instances, and invoke generic + -- actual subprograms through generic formal subprograms. As a + -- result, the calls are not recorded or processed. + -- + -- If switches -gnatd.G and -gnatdL are used together, then the + -- ABE mechanism effectively ignores all calls which cause the + -- elaboration flow to "leave" the instance. + -- + -- -gnatdL ignore external calls from instances for elaboration + -- + -- The ABE mechanism does not generate N_Call_Marker nodes for + -- calls which occur in expanded instances, do not invoke generic + -- actual subprograms through formal subprograms, and the target + -- is external to the instance. As a result, the calls are not + -- recorded or processed. + -- + -- If switches -gnatd.G and -gnatdL are used together, then the + -- ABE mechanism effectively ignores all calls which cause the + -- elaboration flow to "leave" the instance. + -- + -- -gnatd.o conservative elaboration order for indirect calls + -- + -- The ABE mechanism treats '[Unrestricted_]Access of an entry, + -- operator, or subprogram as an immediate invocation of the + -- target. As a result, it performs ABE checks and diagnostics on + -- the immediate call. + -- + -- -gnatd.U ignore indirect calls for static elaboration + -- + -- The ABE mechanism does not consider '[Unrestricted_]Access of + -- entries, operators, and subprograms. As a result, the scenarios + -- are not recorder or processed. + -- + -- -gnatd.v enforce SPARK elaboration rules in SPARK code + -- + -- The ABE mechanism applies some of the SPARK elaboration rules + -- defined in the SPARK reference manual, chapter 7.7. Note that + -- certain rules are always enforced, regardless of whether the + -- switch is active. + -- + -- -gnatd.y disable implicit pragma Elaborate_All on task bodies + -- + -- The ABE mechanism does not generate implicit Elaborate_All when + -- the need for the pragma came from a task body. + -- + -- -gnatE dynamic elaboration checking mode enabled + -- + -- The ABE mechanism assumes that any scenario is elaborated or + -- invoked by elaboration code. The ABE mechanism performs very + -- little diagnostics and generates condintional ABE checks to + -- detect ABE issues at run-time. + -- + -- -gnatel turn on info messages on generated Elaborate[_All] pragmas + -- + -- The ABE mechanism produces information messages on generated + -- implicit Elabote[_All] pragmas along with traceback showing + -- why the pragma was generated. In addition, the ABE mechanism + -- produces information messages for each scenario elaborated or + -- invoked by elaboration code. + -- + -- -gnateL turn off info messages on generated Elaborate[_All] pragmas + -- + -- The complimentary switch for -gnatel. + -- + -- -gnatwl turn on warnings for elaboration problems + -- + -- The ABE mechanism produces warnings on detected ABEs along with + -- traceback showing the graph of the ABE. + -- + -- -gnatwL turn off warnings for elaboration problems + -- + -- The complimentary switch for -gnatwl. + -- + -- -gnatw.f turn on warnings for suspicious Subp'Access + -- + -- The ABE mechanism treats '[Unrestricted_]Access of an entry, + -- operator, or subprogram as a pseudo invocation of the target. + -- As a result, it performs ABE diagnostics on the pseudo call. + -- + -- -gnatw.F turn off warnings for suspicious Subp'Access + -- + -- The complimentary switch for -gnatw.f. + + --------------------------- + -- Adding a new scenario -- + --------------------------- + + -- The following steps describe how to add a new elaboration scenario and + -- preserve the existing architecture. + -- + -- 1) If necessary, update predicates Is_Check_Emitting_Scenario and + -- Is_Scenario. + -- + -- 2) Add predicate Is_Suitable_xxx. Include a call to it in predicate + -- Is_Suitable_Scenario. + -- + -- 3) Update routine Record_Elaboration_Scenario + -- + -- 4) Add routine Process_xxx. Include a call to it in Process_Scenario. + -- + -- 5) Add routine Info_xxx. Include a call to it in Process_xxx. + -- + -- 6) Add routine Output_xxx. Include a call to it in routine + -- Output_Active_Scenarios. + -- + -- 7) If necessary, add a new Extract_xxx_Attributes routine + -- + -- 8) If necessary, update routine Is_Potential_Scenario + + ------------------------- + -- Adding a new target -- + ------------------------- + + -- The following steps describe how to add a new elaboration target and + -- preserve the existing architecture. + -- + -- 1) Add predicate Is_xxx. + -- + -- 2) Update predicates Is_Ada_Semantic_Target, Is_Bridge_Target, or + -- Is_SPARK_Semantic_Target. If necessary, create a new category. + -- + -- 3) Update the appropriate Info_xxx routine. + -- + -- 4) Update the appropriate Output_xxx routine. + -- + -- 5) Update routine Extract_Target_Attributes. If necessary, create a + -- new Extract_xxx routine. + + -------------------------- + -- Debugging ABE issues -- + -------------------------- + + -- * If the issue involves a call, ensure that the call is eligible for ABE + -- processing and receives a corresponding call marker. The routines of + -- interest are + -- + -- Build_Call_Marker + -- Record_Elaboration_Scenario + + -- * If the issue involves an arbitrary scenario, ensure that the scenario + -- is either recorded, or is successfully recognized while traversing a + -- body. The routines of interest are + -- + -- Record_Elaboration_Scenario + -- Process_Scenario + -- Traverse_Body + + -- * If the issue involves a circularity in the elaboration order, examine + -- the ALI files and look for the following encodings next to units: + -- + -- E indicates a source Elaborate + -- + -- EA indicates a source Elaborate_All + -- + -- AD indicates an implicit Elaborate_All + -- + -- ED indicates an implicit Elaborate + -- + -- If possible, compare these encodings with those generated by the old + -- ABE mechanism. The routines of interest are + -- + -- Ensure_Prior_Elaboration + + ---------------- + -- Attributes -- + ---------------- + + -- The following type captures relevant attributes which pertain to a call + + type Call_Attributes is record + Elab_Checks_OK : Boolean; + -- This flag is set when the call has elaboration checks enabled + + From_Source : Boolean; + -- This flag is set when the call comes from source + + Ghost_Mode_Ignore : Boolean; + -- This flag is set when the call appears in a region subject to pragma + -- Ghost with policy Ignore. + + In_Declarations : Boolean; + -- This flag is set when the call appears at the declaration level + + Is_Dispatching : Boolean; + -- This flag is set when the call is dispatching + + SPARK_Mode_On : Boolean; + -- This flag is set when the call appears in a region subject to pragma + -- SPARK_Mode with value On. + end record; + + -- The following type captures relevant attributes which pertain to the + -- prior elaboration of a unit. This type is coupled together with a unit + -- to form a key -> value relationship. + + type Elaboration_Attributes is record + Source_Pragma : Node_Id; + -- This attribute denotes a source Elaborate or Elaborate_All pragma + -- which guarantees the prior elaboration of some unit with respect + -- to the main unit. The pragma may come from the following contexts: + + -- * The main unit + -- * The spec of the main unit (if applicable) + -- * Any parent spec of the main unit (if applicable) + -- * Any parent subunit of the main unit (if applicable) + + -- The attribute remains Empty if no such pragma is available. Source + -- pragmas play a role in satisfying SPARK elaboration requirements. + + With_Clause : Node_Id; + -- This attribute denotes an internally generated or source with clause + -- for some unit withed by the main unit. With clauses carry flags which + -- represent implicit Elaborate or Elaborate_All pragmas. These clauses + -- play a role in supplying the elaboration dependencies to binde. + end record; + + No_Elaboration_Attributes : constant Elaboration_Attributes := + (Source_Pragma => Empty, + With_Clause => Empty); + + -- The following type captures relevant attributes which pertain to an + -- instantiation. + + type Instantiation_Attributes is record + Elab_Checks_OK : Boolean; + -- This flag is set when the instantiation has elaboration checks + -- enabled. + + Ghost_Mode_Ignore : Boolean; + -- This flag is set when the instantiation appears in a region subject + -- to pragma Ghost with policy ignore, or starts one such region. + + In_Declarations : Boolean; + -- This flag is set when the instantiation appears at the declaration + -- level. + + SPARK_Mode_On : Boolean; + -- This flag is set when the instantiation appears in a region subject + -- to pragma SPARK_Mode with value On, or starts one such region. + end record; + + -- The following type captures relevant attributes which pertain to a + -- target. + + type Target_Attributes is record + Elab_Checks_OK : Boolean; + -- This flag is set when the target has elaboration checks enabled + + From_Source : Boolean; + -- This flag is set when the target comes from source + + Ghost_Mode_Ignore : Boolean; + -- This flag is set when the target appears in a region subject to + -- pragma Ghost with policy ignore, or starts one such region. + + SPARK_Mode_On : Boolean; + -- This flag is set when the target appears in a region subject to + -- pragma SPARK_Mode with value On, or starts one such region. + + Spec_Decl : Node_Id; + -- This attribute denotes the declaration of Spec_Id + + Unit_Id : Entity_Id; + -- This attribute denotes the top unit where Spec_Id resides + + -- The semantics of the following attributes depend on the target + + Body_Barf : Node_Id; + Body_Decl : Node_Id; + Spec_Id : Entity_Id; + + -- The target is a generic package or a subprogram + -- + -- * Body_Barf - Empty + -- + -- * Body_Decl - This attribute denotes the generic or subprogram + -- body. + -- + -- * Spec_Id - This attribute denotes the entity of the generic + -- package or subprogram. + + -- The target is a protected entry + -- + -- * Body_Barf - This attribute denotes the body of the barrier + -- function if expansion took place, otherwise it is Empty. + -- + -- * Body_Decl - This attribute denotes the body of the procedure + -- which emulates the entry if expansion took place, otherwise it + -- denotes the body of the protected entry. + -- + -- * Spec_Id - This attribute denotes the entity of the procedure + -- which emulates the entry if expansion took place, otherwise it + -- denotes the protected entry. + + -- The target is a protected subprogram + -- + -- * Body_Barf - Empty + -- + -- * Body_Decl - This attribute denotes the body of the protected or + -- unprotected version of the protected subprogram if expansion took + -- place, otherwise it denotes the body of the protected subprogram. + -- + -- * Spec_Id - This attribute denotes the entity of the protected or + -- unprotected version of the protected subprogram if expansion took + -- place, otherwise it is the entity of the protected subprogram. + + -- The target is a task entry + -- + -- * Body_Barf - Empty + -- + -- * Body_Decl - This attribute denotes the body of the procedure + -- which emulates the task body if expansion took place, otherwise + -- it denotes the body of the task type. + -- + -- * Spec_Id - This attribute denotes the entity of the procedure + -- which emulates the task body if expansion took place, otherwise + -- it denotes the entity of the task type. + end record; + + -- The following type captures relevant attributes which pertain to a task + -- type. + + type Task_Attributes is record + Body_Decl : Node_Id; + -- This attribute denotes the declaration of the procedure body which + -- emulates the behaviour of the task body. + + Elab_Checks_OK : Boolean; + -- This flag is set when the task type has elaboration checks enabled + + Ghost_Mode_Ignore : Boolean; + -- This flag is set when the task type appears in a region subject to + -- pragma Ghost with policy ignore, or starts one such region. + + SPARK_Mode_On : Boolean; + -- This flag is set when the task type appears in a region subject to + -- pragma SPARK_Mode with value On, or starts one such region. + + Spec_Id : Entity_Id; + -- This attribute denotes the entity of the initial declaration of the + -- procedure body which emulates the behaviour of the task body. + + Task_Decl : Node_Id; + -- This attribute denotes the declaration of the task type + + Unit_Id : Entity_Id; + -- This attribute denotes the entity of the compilation unit where the + -- task type resides. + end record; + + -- The following type captures relevant attributes which pertain to a + -- variable. + + type Variable_Attributes is record + SPARK_Mode_On : Boolean; + -- This flag is set when the variable appears in a region subject to + -- pragma SPARK_Mode with value On, or starts one such region. + + Unit_Id : Entity_Id; + -- This attribute denotes the entity of the compilation unit where the + -- variable resides. + end record; + + --------------------- + -- Data structures -- + --------------------- + + -- The following table stores the elaboration status of all units withed by + -- the main unit. + + Elaboration_Context_Max : constant := 1009; + + type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1; + + function Elaboration_Context_Hash + (Key : Entity_Id) return Elaboration_Context_Index; + -- Obtain the hash value of entity Key + + package Elaboration_Context is new Simple_HTable + (Header_Num => Elaboration_Context_Index, + Element => Elaboration_Attributes, + No_Element => No_Elaboration_Attributes, + Key => Entity_Id, + Hash => Elaboration_Context_Hash, + Equal => "="); + + -- The following table stores all active scenarios in a recursive traversal + -- starting from a top level scenario. This table must be maintained in a + -- FIFO fashion. + + package Scenario_Stack is new Table.Table + (Table_Component_Type => Node_Id, + Table_Index_Type => Int, + Table_Low_Bound => 1, + Table_Initial => 50, + Table_Increment => 100, + Table_Name => "Scenario_Stack"); + + -- The following table stores all top level scenario saved during the + -- Recording phase. The contents of this table act as traversal roots + -- later in the Processing phase. This table must be maintained in a + -- LIFO fashion. + + package Top_Level_Scenarios is new Table.Table + (Table_Component_Type => Node_Id, + Table_Index_Type => Int, + Table_Low_Bound => 1, + Table_Initial => 1000, + Table_Increment => 100, + Table_Name => "Top_Level_Scenarios"); + + -- The following table stores the bodies of all eligible scenarios visited + -- during a traversal starting from a top level scenario. The contents of + -- this table must be reset upon each new traversal. + + Visited_Bodies_Max : constant := 511; + + type Visited_Bodies_Index is range 0 .. Visited_Bodies_Max - 1; + + function Visited_Bodies_Hash (Key : Node_Id) return Visited_Bodies_Index; + -- Obtain the hash value of node Key + + package Visited_Bodies is new Simple_HTable + (Header_Num => Visited_Bodies_Index, + Element => Boolean, + No_Element => False, + Key => Node_Id, + Hash => Visited_Bodies_Hash, + Equal => "="); + + ----------------------- + -- Local subprograms -- + ----------------------- + + procedure Check_Preelaborated_Call (Call : Node_Id); + -- Determine whether entry, operator, or subprogram call Call appears at + -- the library level of a preelaborated unit. Emit an error if this is the + -- case. + + function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id; + pragma Inline (Compilation_Unit); + -- Return the N_Compilation_Unit node of unit Unit_Id + + procedure Elab_Msg_NE + (Msg : String; + N : Node_Id; + Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean); + pragma Inline (Elab_Msg_NE); + -- Wrapper around Error_Msg_NE. Emit message Msg concerning arbitrary node + -- N and entity. If flag Info_Msg is set, the routine emits an information + -- message, otherwise it emits an error. If flag In_SPARK is set, then + -- string " in SPARK" is added to the end of the message. + + procedure Ensure_Prior_Elaboration + (N : Node_Id; + Unit_Id : Entity_Id; + In_Task_Body : Boolean); + -- Guarantee the elaboration of unit Unit_Id with respect to the main unit. + -- N denotes the related scenario. Flag In_Task_Body should be set when the + -- need for elaboration is initiated from a task body. + + procedure Ensure_Prior_Elaboration_Dynamic + (N : Node_Id; + Unit_Id : Entity_Id; + Prag_Nam : Name_Id); + -- Guarantee the elaboration of unit Unit_Id with respect to the main unit + -- by suggesting the use of Elaborate[_All] with name Prag_Nam. N denotes + -- the related scenario. + + procedure Ensure_Prior_Elaboration_Static + (N : Node_Id; + Unit_Id : Entity_Id; + Prag_Nam : Name_Id); + -- Guarantee the elaboration of unit Unit_Id with respect to the main unit + -- by installing an implicit Elaborate[_All] pragma with name Prag_Nam. N + -- denotes the related scenario. + + function Extract_Assignment_Name (Asmt : Node_Id) return Node_Id; + pragma Inline (Extract_Assignment_Name); + -- Obtain the Name attribute of assignment statement Asmt + + procedure Extract_Call_Attributes + (Call : Node_Id; + Target_Id : out Entity_Id; + Attrs : out Call_Attributes); + pragma Inline (Extract_Call_Attributes); + -- Obtain attributes Attrs associated with call Call. Target_Id is the + -- entity of the call target. + + function Extract_Call_Name (Call : Node_Id) return Node_Id; + pragma Inline (Extract_Call_Name); + -- Obtain the Name attribute of entry or subprogram call Call + + procedure Extract_Instance_Attributes + (Exp_Inst : Node_Id; + Inst_Body : out Node_Id; + Inst_Decl : out Node_Id); + pragma Inline (Extract_Instance_Attributes); + -- Obtain body Inst_Body and spec Inst_Decl of expanded instance Exp_Inst + + procedure Extract_Instantiation_Attributes + (Exp_Inst : Node_Id; + Inst : out Node_Id; + Inst_Id : out Entity_Id; + Gen_Id : out Entity_Id; + Attrs : out Instantiation_Attributes); + pragma Inline (Extract_Instantiation_Attributes); + -- Obtain attributes Attrs associated with expanded instantiation Exp_Inst. + -- Inst is the instantiation. Inst_Id is the entity of the instance. Gen_Id + -- is the entity of the generic unit being instantiated. + + procedure Extract_Target_Attributes + (Target_Id : Entity_Id; + Attrs : out Target_Attributes); + -- Obtain attributes Attrs associated with an entry, package, or subprogram + -- denoted by Target_Id. + + procedure Extract_Task_Attributes + (Typ : Entity_Id; + Attrs : out Task_Attributes); + pragma Inline (Extract_Task_Attributes); + -- Obtain attributes Attrs associated with task type Typ + + procedure Extract_Variable_Reference_Attributes + (Ref : Node_Id; + Var_Id : out Entity_Id; + Attrs : out Variable_Attributes); + pragma Inline (Extract_Variable_Reference_Attributes); + -- Obtain attributes Attrs associated with reference Ref that mentions + -- variable Var_Id. + + function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id; + pragma Inline (Find_Code_Unit); + -- Return the code unit which contains arbitrary node or entity N. This + -- is the unit of the file which physically contains the related construct + -- denoted by N except when N is within an instantiation. In that case the + -- unit is that of the top level instantiation. + + procedure Find_Elaborated_Units; + -- Populate table Elaboration_Context with all units which have prior + -- elaboration with respect to the main unit. + + function Find_Enclosing_Instance (N : Node_Id) return Node_Id; + pragma Inline (Find_Enclosing_Instance); + -- Find the declaration or body of the nearest expanded instance which + -- encloses arbitrary node N. Return Empty if no such instance exists. + + function Find_Top_Unit (N : Node_Or_Entity_Id) return Entity_Id; + pragma Inline (Find_Top_Unit); + -- Return the top unit which contains arbitrary node or entity N. The unit + -- is obtained by logically unwinding instantiations and subunits when N + -- resides within one. + + function Find_Unit_Entity (N : Node_Id) return Entity_Id; + pragma Inline (Find_Unit_Entity); + -- Return the entity of unit N + + function First_Formal_Type (Subp_Id : Entity_Id) return Entity_Id; + pragma Inline (First_Formal_Type); + -- Return the type of subprogram Subp_Id's first formal parameter. If the + -- subprogram lacks formal parameters, return Empty. + + function Has_Body (Pack_Decl : Node_Id) return Boolean; + -- Determine whether package declaration Pack_Decl has a corresponding body + -- or would eventually have one. + + function Has_Prior_Elaboration + (Unit_Id : Entity_Id; + Context_OK : Boolean := False; + Elab_Body_OK : Boolean := False; + Same_Unit_OK : Boolean := False) return Boolean; + pragma Inline (Has_Prior_Elaboration); + -- Determine whether unit Unit_Id is elaborated prior to the main unit. + -- If flag Context_OK is set, the routine considers the following case + -- as valid prior elaboration: + -- + -- * Unit_Id is in the elaboration context of the main unit + -- + -- If flag Elab_Body_OK is set, the routine considers the following case + -- as valid prior elaboration: + -- + -- * Unit_Id has pragma Elaborate_Body and is not the main unit + -- + -- If flag Same_Unit_OK is set, the routine considers the following cases + -- as valid prior elaboration: + -- + -- * Unit_Id is the main unit + -- + -- * Unit_Id denotes the spec of the main unit body + + function In_External_Instance + (N : Node_Id; + Target_Decl : Node_Id) return Boolean; + pragma Inline (In_External_Instance); + -- Determine whether a target desctibed by its declaration Target_Decl + -- resides in a package instance which is external to scenario N. + + function In_Main_Context (N : Node_Id) return Boolean; + pragma Inline (In_Main_Context); + -- Determine whether arbitrary node N appears within the main compilation + -- unit. + + function In_Same_Context + (N1 : Node_Id; + N2 : Node_Id; + Nested_OK : Boolean := False) return Boolean; + -- Determine whether two arbitrary nodes N1 and N2 appear within the same + -- context ignoring enclosing library levels. Nested_OK should be set when + -- the context of N1 can enclose that of N2. + + procedure Info_Call + (Call : Node_Id; + Target_Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean); + -- Output information concerning call Call which invokes target Target_Id. + -- If flag Info_Msg is set, the routine emits an information message, + -- otherwise it emits an error. If flag In_SPARK is set, then the string + -- " in SPARK" is added to the end of the message. + + procedure Info_Instantiation + (Inst : Node_Id; + Gen_Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean); + pragma Inline (Info_Instantiation); + -- Output information concerning instantiation Inst which instantiates + -- generic unit Gen_Id. If flag Info_Msg is set, the routine emits an + -- information message, otherwise it emits an error. If flag In_SPARK + -- is set, then string " in SPARK" is added to the end of the message. + + procedure Info_Variable_Read + (Ref : Node_Id; + Var_Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean); + pragma Inline (Info_Variable_Read); + -- Output information concerning reference Ref which reads variable Var_Id. + -- If flag Info_Msg is set, the routine emits an information message, + -- otherwise it emits an error. If flag In_SPARK is set, then string " in + -- SPARK" is added to the end of the message. + + function Insertion_Node (N : Node_Id; Ins_Nod : Node_Id) return Node_Id; + pragma Inline (Insertion_Node); + -- Obtain the proper insertion node of an ABE check or failure for scenario + -- N and candidate insertion node Ins_Nod. + + procedure Install_ABE_Check + (N : Node_Id; + Id : Entity_Id; + Ins_Nod : Node_Id); + -- Insert a run-time ABE check for elaboration scenario N which verifies + -- whether arbitrary entity Id is elaborated. The check in inserted prior + -- to node Ins_Nod. + + procedure Install_ABE_Check + (N : Node_Id; + Target_Id : Entity_Id; + Target_Decl : Node_Id; + Target_Body : Node_Id; + Ins_Nod : Node_Id); + -- Insert a run-time ABE check for elaboration scenario N which verifies + -- whether target Target_Id with initial declaration Target_Decl and body + -- Target_Body is elaborated. The check is inserted prior to node Ins_Nod. + + procedure Install_ABE_Failure (N : Node_Id; Ins_Nod : Node_Id); + -- Insert a Program_Error concerning a guaranteed ABE for elaboration + -- scenario N. The failure is inserted prior to node Node_Id. + + function Is_Accept_Alternative_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Accept_Alternative_Proc); + -- Determine whether arbitrary entity Id denotes an internally generated + -- procedure which encapsulates the statements of an accept alternative. + + function Is_Activation_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Activation_Proc); + -- Determine whether arbitrary entity Id denotes a runtime procedure in + -- charge with activating tasks. + + function Is_Ada_Semantic_Target (Id : Entity_Id) return Boolean; + pragma Inline (Is_Ada_Semantic_Target); + -- Determine whether arbitrary entity Id nodes a source or internally + -- generated subprogram which emulates Ada semantics. + + function Is_Bodiless_Subprogram (Subp_Id : Entity_Id) return Boolean; + pragma Inline (Is_Bodiless_Subprogram); + -- Determine whether subprogram Subp_Id will never have a body + + function Is_Check_Emitting_Scenario (N : Node_Id) return Boolean; + pragma Inline (Is_Check_Emitting_Scenario); + -- Determine whether arbitrary node N denotes a scenario which may emit a + -- conditional ABE check. + + function Is_Controlled_Proc + (Subp_Id : Entity_Id; + Subp_Nam : Name_Id) return Boolean; + pragma Inline (Is_Controlled_Proc); + -- Determine whether subprogram Subp_Id denotes controlled type primitives + -- Adjust, Finalize, or Initialize as denoted by name Subp_Nam. + + function Is_Default_Initial_Condition_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Default_Initial_Condition_Proc); + -- Determine whether arbitrary entity Id denotes internally generated + -- routine Default_Initial_Condition. + + function Is_Finalizer_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Finalizer_Proc); + -- Determine whether arbitrary entity Id denotes internally generated + -- routine _Finalizer. + + function Is_Guaranteed_ABE + (N : Node_Id; + Target_Decl : Node_Id; + Target_Body : Node_Id) return Boolean; + pragma Inline (Is_Guaranteed_ABE); + -- Determine whether scenario N with a target described by its initial + -- declaration Target_Decl and body Target_Decl results in a guaranteed + -- ABE. + + function Is_Initial_Condition_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Initial_Condition_Proc); + -- Determine whether arbitrary entity Id denotes internally generated + -- routine Initial_Condition. + + function Is_Initialized (Obj_Decl : Node_Id) return Boolean; + pragma Inline (Is_Initialized); + -- Determine whether object declaration Obj_Decl is initialized + + function Is_Invariant_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Invariant_Proc); + -- Determine whether arbitrary entity Id denotes an invariant procedure + + function Is_Non_Library_Level_Encapsulator (N : Node_Id) return Boolean; + pragma Inline (Is_Non_Library_Level_Encapsulator); + -- Determine whether arbitrary node N is a non-library encapsulator + + function Is_Partial_Invariant_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Partial_Invariant_Proc); + -- Determine whether arbitrary entity Id denotes a partial invariant + -- procedure. + + function Is_Postconditions_Proc (Id : Entity_Id) return Boolean; + pragma Inline (Is_Postconditions_Proc); + -- Determine whether arbitrary entity Id denotes internally generated + -- routine _Postconditions. + + function Is_Preelaborated_Unit (Id : Entity_Id) return Boolean; + pragma Inline (Is_Preelaborated_Unit); + -- Determine whether arbitrary entity Id denotes a unit which is subject to + -- one of the following pragmas: + -- + -- * Preelaborable + -- * Pure + -- * Remote_Call_Interface + -- * Remote_Types + -- * Shared_Passive + + function Is_Protected_Entry (Id : Entity_Id) return Boolean; + pragma Inline (Is_Protected_Entry); + -- Determine whether arbitrary entity Id denotes a protected entry + + function Is_Protected_Subp (Id : Entity_Id) return Boolean; + pragma Inline (Is_Protected_Subp); + -- Determine whether entity Id denotes a protected subprogram + + function Is_Protected_Body_Subp (Id : Entity_Id) return Boolean; + pragma Inline (Is_Protected_Body_Subp); + -- Determine whether entity Id denotes the protected or unprotected version + -- of a protected subprogram. + + function Is_Safe_Activation + (Call : Node_Id; + Task_Decl : Node_Id) return Boolean; + pragma Inline (Is_Safe_Activation); + -- Determine whether call Call which activates a task object described by + -- declaration Task_Decl is always ABE-safe. + + function Is_Safe_Call + (Call : Node_Id; + Target_Attrs : Target_Attributes) return Boolean; + pragma Inline (Is_Safe_Call); + -- Determine whether call Call which invokes a target described by + -- attributes Target_Attrs is always ABE-safe. + + function Is_Safe_Instantiation + (Inst : Node_Id; + Gen_Attrs : Target_Attributes) return Boolean; + pragma Inline (Is_Safe_Instantiation); + -- Determine whether instance Inst which instantiates a generic unit + -- described by attributes Gen_Attrs is always ABE-safe. + + function Is_Same_Unit + (Unit_1 : Entity_Id; + Unit_2 : Entity_Id) return Boolean; + pragma Inline (Is_Same_Unit); + -- Determine whether entities Unit_1 and Unit_2 denote the same unit + + function Is_Scenario (N : Node_Id) return Boolean; + pragma Inline (Is_Scenario); + -- Determine whether attribute node N denotes a scenario. The scenario may + -- not necessarily be eligible for ABE processing. + + function Is_SPARK_Semantic_Target (Id : Entity_Id) return Boolean; + pragma Inline (Is_SPARK_Semantic_Target); + -- Determine whether arbitrary entity Id nodes a source or internally + -- generated subprogram which emulates SPARK semantics. + + function Is_Suitable_Access (N : Node_Id) return Boolean; + pragma Inline (Is_Suitable_Access); + -- Determine whether arbitrary node N denotes a suitable attribute for ABE + -- processing. + + function Is_Suitable_Call (N : Node_Id) return Boolean; + pragma Inline (Is_Suitable_Call); + -- Determine whether arbitrary node N denotes a suitable call for ABE + -- processing. + + function Is_Suitable_Instantiation (N : Node_Id) return Boolean; + pragma Inline (Is_Suitable_Instantiation); + -- Determine whether arbitrary node N is a suitable instantiation for ABE + -- processing. + + function Is_Suitable_Scenario (N : Node_Id) return Boolean; + pragma Inline (Is_Suitable_Scenario); + -- Determine whether arbitrary node N is a suitable scenario for ABE + -- processing. + + function Is_Suitable_Variable_Assignment (N : Node_Id) return Boolean; + pragma Inline (Is_Suitable_Variable_Assignment); + -- Determine whether arbitrary node N denotes a suitable assignment for ABE + -- processing. + + function Is_Suitable_Variable_Read (N : Node_Id) return Boolean; + pragma Inline (Is_Suitable_Variable_Read); + -- Determine whether arbitrary node N is a suitable variable read for ABE + -- processing. + + function Is_Task_Entry (Id : Entity_Id) return Boolean; + pragma Inline (Is_Task_Entry); + -- Determine whether arbitrary entity Id denotes a task entry + + function Is_Up_Level_Target (Target_Decl : Node_Id) return Boolean; + pragma Inline (Is_Up_Level_Target); + -- Determine whether the current root resides at the declaration level. If + -- this is the case, determine whether a target described by declaration + -- Target_Decl is within a context which encloses the current root or is in + -- a different unit. + + procedure Meet_Elaboration_Requirement + (N : Node_Id; + Target_Id : Entity_Id; + Req_Nam : Name_Id); + -- Determine whether elaboration requirement Req_Nam for scenario N with + -- target Target_Id is met by the context of the main unit using the SPARK + -- rules. Req_Nam must denote either Elaborate or Elaborate_All. Emit an + -- error if this is not the case. + + function Non_Private_View (Typ : Entity_Id) return Entity_Id; + pragma Inline (Non_Private_View); + -- Return the full view of private type Typ if available, otherwise return + -- type Typ. + + procedure Output_Active_Scenarios (Error_Nod : Node_Id); + -- Output the contents of the active scenario stack from earliest to latest + -- to supplement an earlier error emitted for node Error_Nod. + + procedure Pop_Active_Scenario (N : Node_Id); + pragma Inline (Pop_Active_Scenario); + -- Pop the top of the scenario stack. A check is made to ensure that the + -- scenario being removed is the same as N. + + procedure Process_Access (Attr : Node_Id; In_Task_Body : Boolean); + -- Perform ABE checks and diagnostics for 'Access to entry, operator, or + -- subprogram denoted by Attr. Flag In_Task_Body should be set when the + -- processing is initiated from a task body. + + generic + with procedure Process_Single_Activation + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Obj_Id : Entity_Id; + Task_Attrs : Task_Attributes; + In_Task_Body : Boolean); + -- Perform ABE checks and diagnostics for task activation call Call + -- which activates task Obj_Id. Call_Attrs are the attributes of the + -- activation call. Task_Attrs are the attributes of the task type. + -- Flag In_Task_Body should be set when the processing is initiated + -- from a task body. + + procedure Process_Activation_Call + (Call : Node_Id; + Call_Attrs : Call_Attributes; + In_Task_Body : Boolean); + -- Perform ABE checks and diagnostics for activation call Call by invoking + -- routine Process_Single_Activation on each task object being activated. + -- Call_Attrs are the attributes of the activation call. Flag In_Task_Body + -- should be set when the processing is initiated from a task body. + + procedure Process_Activation_Conditional_ABE_Impl + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Obj_Id : Entity_Id; + Task_Attrs : Task_Attributes; + In_Task_Body : Boolean); + -- Perform common conditional ABE checks and diagnostics for call Call + -- which activates task Obj_Id ignoring the Ada or SPARK rules. CAll_Attrs + -- are the attributes of the activation call. Task_Attrs are the attributes + -- of the task type. Flag In_Task_Body should be set when the processing is + -- initiated from a task body. + + procedure Process_Activation_Guaranteed_ABE_Impl + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Obj_Id : Entity_Id; + Task_Attrs : Task_Attributes; + In_Task_Body : Boolean); + -- Perform common guaranteed ABE checks and diagnostics for call Call + -- which activates task Obj_Id ignoring the Ada or SPARK rules. CAll_Attrs + -- are the attributes of the activation call. Task_Attrs are the attributes + -- of the task type. Flag In_Task_Body should be set when the processing is + -- initiated from a task body. + + procedure Process_Call + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + In_Task_Body : Boolean); + -- Top-level dispatcher for processing of calls. Perform ABE checks and + -- diagnostics for call Call which invokes target Target_Id. Call_Attrs + -- are the attributes of the call. Flag In_Task_Body should be set when + -- the processing is initiated from a task body. + + procedure Process_Call_Ada + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + Target_Attrs : Target_Attributes; + In_Task_Body : Boolean); + -- Perform ABE checks and diagnostics for call Call which invokes target + -- Target_Id using the Ada rules. Call_Attrs are the attributes of the + -- call. Target_Attrs are attributes of the target. Flag In_Task_Body + -- should be set when the processing is initiated from a task body. + + procedure Process_Call_Conditional_ABE + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + Target_Attrs : Target_Attributes); + -- Perform common conditional ABE checks and diagnostics for call Call that + -- invokes target Target_Id ignoring the Ada or SPARK rules. Call_Attrs are + -- the attributes of the call. Target_Attrs are attributes of the target. + + procedure Process_Call_Guaranteed_ABE + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id); + -- Perform common guaranteed ABE checks and diagnostics for call Call which + -- invokes target Target_Id ignoring the Ada or SPARK rules. Call_Attrs are + -- the attributes of the call. + + procedure Process_Call_SPARK + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + Target_Attrs : Target_Attributes); + -- Perform ABE checks and diagnostics for call Call which invokes target + -- Target_Id using the SPARK rules. Call_Attrs are the attributes of the + -- call. Target_Attrs are attributes of the target. + + procedure Process_Guaranteed_ABE (N : Node_Id); + -- Top level dispatcher for processing of scenarios which result in a + -- guaranteed ABE. + + procedure Process_Instantiation + (Exp_Inst : Node_Id; + In_Task_Body : Boolean); + -- Top level dispatcher for processing of instantiations. Perform ABE + -- checks and diagnostics for expanded instantiation Exp_Inst. Flag + -- In_Task_Body should be set when the processing is initiated from a + -- task body. + + procedure Process_Instantiation_Ada + (Exp_Inst : Node_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Gen_Id : Entity_Id; + Gen_Attrs : Target_Attributes; + In_Task_Body : Boolean); + -- Perform ABE checks and diagnostics for expanded instantiation Exp_Inst + -- of generic Gen_Id using the Ada rules. Inst is the instantiation node. + -- Inst_Attrs are the attributes of the instance. Gen_Attrs are the + -- attributes of the generic. Flag In_Task_Body should be set when the + -- processing is initiated from a task body. + + procedure Process_Instantiation_Conditional_ABE + (Exp_Inst : Node_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Gen_Id : Entity_Id; + Gen_Attrs : Target_Attributes); + -- Perform common conditional ABE checks and diagnostics for expanded + -- instantiation Exp_Inst of generic Gen_Id ignoring the Ada or SPARK + -- rules. Inst is the instantiation node. Inst_Attrs are the attributes + -- of the instance. Gen_Attrs are the attributes of the generic. + + procedure Process_Instantiation_Guaranteed_ABE (Exp_Inst : Node_Id); + -- Perform common guaranteed ABE checks and diagnostics for expanded + -- instantiation Exp_Inst of generic Gen_Id ignoring the Ada or SPARK + -- rules. + + procedure Process_Instantiation_SPARK + (Exp_Inst : Node_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Gen_Id : Entity_Id; + Gen_Attrs : Target_Attributes); + -- Perform ABE checks and diagnostics for expanded instantiation Exp_Inst + -- of generic Gen_Id using the SPARK rules. Inst is the instantiation node. + -- Inst_Attrs are the attributes of the instance. Gen_Attrs are the + -- attributes of the generic. + + procedure Process_Scenario (N : Node_Id; In_Task_Body : Boolean := False); + -- Top level dispatcher for processing of various elaboration scenarios. + -- Perform ABE checks and diagnostics for scenario N. Flag In_Task_Body + -- should be set when the processing is initiated from a task body. + + procedure Process_Variable_Assignment (Asmt : Node_Id); + -- Top level dispatcher for processing of variable assignments. Perform ABE + -- checks and diagnostics for assignment statement Asmt. + + procedure Process_Variable_Assignment_Ada + (Asmt : Node_Id; + Var_Id : Entity_Id); + -- Perform ABE checks and diagnostics for assignment statement Asmt that + -- updates the value of variable Var_Id using the Ada rules. + + procedure Process_Variable_Assignment_SPARK + (Asmt : Node_Id; + Var_Id : Entity_Id); + -- Perform ABE checks and diagnostics for assignment statement Asmt that + -- updates the value of variable Var_Id using the SPARK rules. + + procedure Process_Variable_Read (Ref : Node_Id); + -- Perform ABE checks and diagnostics for reference Ref that reads a + -- variable. + + procedure Push_Active_Scenario (N : Node_Id); + pragma Inline (Push_Active_Scenario); + -- Push scenario N on top of the scenario stack + + function Root_Scenario return Node_Id; + pragma Inline (Root_Scenario); + -- Return the top level scenario which started a recursive search for other + -- scenarios. It is assumed that there is a valid top level scenario on the + -- active scenario stack. + + function Static_Elaboration_Checks return Boolean; + pragma Inline (Static_Elaboration_Checks); + -- Determine whether the static model is in effect + + procedure Traverse_Body (N : Node_Id; In_Task_Body : Boolean); + -- Inspect the declarations and statements of subprogram body N for + -- suitable elaboration scenarios and process them. Flag In_Task_Body + -- should be set when the traversal is initiated from a task body. + + procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id); + pragma Inline (Update_Elaboration_Scenario); + -- Update all relevant internal data structures when scenario Old_N is + -- transformed into scenario New_N by Atree.Rewrite. + + ----------------------- + -- Build_Call_Marker -- + ----------------------- + + procedure Build_Call_Marker (N : Node_Id) is + function In_External_Context + (Call : Node_Id; + Target_Id : Entity_Id) return Boolean; + pragma Inline (In_External_Context); + -- Determine whether target Target_Id is external to call N which must + -- reside within an instance. + + function In_Premature_Context (Call : Node_Id) return Boolean; + -- Determine whether call Call appears within a premature context + + function Is_Bridge_Target (Id : Entity_Id) return Boolean; + pragma Inline (Is_Bridge_Target); + -- Determine whether arbitrary entity Id denotes a bridge target + + function Is_Default_Expression (Call : Node_Id) return Boolean; + pragma Inline (Is_Default_Expression); + -- Determine whether call Call acts as the expression of a defaulted + -- parameter within a source call. + + function Is_Generic_Formal_Subp (Subp_Id : Entity_Id) return Boolean; + pragma Inline (Is_Generic_Formal_Subp); + -- Determine whether subprogram Subp_Id denotes a generic formal + -- subprogram which appears in the "prologue" of an instantiation. + + ------------------------- + -- In_External_Context -- + ------------------------- + + function In_External_Context + (Call : Node_Id; + Target_Id : Entity_Id) return Boolean + is + Target_Decl : constant Node_Id := Unit_Declaration_Node (Target_Id); + + Inst : Node_Id; + Inst_Body : Node_Id; + Inst_Decl : Node_Id; + + begin + -- Performance note: parent traversal + + Inst := Find_Enclosing_Instance (Call); + + -- The call appears within an instance + + if Present (Inst) then + + -- The call comes from the main unit and the target does not + + if In_Extended_Main_Code_Unit (Call) + and then not In_Extended_Main_Code_Unit (Target_Decl) + then + return True; + + -- Otherwise the target declaration must not appear within the + -- instance spec or body. + + else + Extract_Instance_Attributes + (Exp_Inst => Inst, + Inst_Decl => Inst_Decl, + Inst_Body => Inst_Body); + + -- Performance note: parent traversal + + return not In_Subtree + (N => Target_Decl, + Root1 => Inst_Decl, + Root2 => Inst_Body); + end if; + end if; + + return False; + end In_External_Context; + + -------------------------- + -- In_Premature_Context -- + -------------------------- + + function In_Premature_Context (Call : Node_Id) return Boolean is + Par : Node_Id; + + begin + -- Climb the parent chain looking for premature contexts + + Par := Parent (Call); + while Present (Par) loop + + -- Aspect specifications and generic associations are premature + -- contexts because nested calls has not been relocated to their + -- final context. + + if Nkind_In (Par, N_Aspect_Specification, + N_Generic_Association) + then + return True; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Par := Parent (Par); + end loop; + + return False; + end In_Premature_Context; + + ---------------------- + -- Is_Bridge_Target -- + ---------------------- + + function Is_Bridge_Target (Id : Entity_Id) return Boolean is + begin + return + Is_Accept_Alternative_Proc (Id) + or else Is_Finalizer_Proc (Id) + or else Is_Partial_Invariant_Proc (Id) + or else Is_Postconditions_Proc (Id) + or else Is_TSS (Id, TSS_Deep_Adjust) + or else Is_TSS (Id, TSS_Deep_Finalize) + or else Is_TSS (Id, TSS_Deep_Initialize); + end Is_Bridge_Target; + + --------------------------- + -- Is_Default_Expression -- + --------------------------- + + function Is_Default_Expression (Call : Node_Id) return Boolean is + Outer_Call : constant Node_Id := Parent (Call); + Outer_Nam : Node_Id; + + begin + -- To qualify, the node must appear immediately within a source call + -- which invokes a source target. + + if Nkind_In (Outer_Call, N_Entry_Call_Statement, + N_Function_Call, + N_Procedure_Call_Statement) + and then Comes_From_Source (Outer_Call) + then + Outer_Nam := Extract_Call_Name (Outer_Call); + + return + Is_Entity_Name (Outer_Nam) + and then Present (Entity (Outer_Nam)) + and then Is_Subprogram_Or_Entry (Entity (Outer_Nam)) + and then Comes_From_Source (Entity (Outer_Nam)); + end if; + + return False; + end Is_Default_Expression; + + ---------------------------- + -- Is_Generic_Formal_Subp -- + ---------------------------- + + function Is_Generic_Formal_Subp (Subp_Id : Entity_Id) return Boolean is + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Context : constant Node_Id := Parent (Subp_Decl); + + begin + -- To qualify, the subprogram must rename a generic actual subprogram + -- where the enclosing context is an instantiation. + + return + Nkind (Subp_Decl) = N_Subprogram_Renaming_Declaration + and then not Comes_From_Source (Subp_Decl) + and then Nkind_In (Context, N_Function_Specification, + N_Package_Specification, + N_Procedure_Specification) + and then Present (Generic_Parent (Context)); + end Is_Generic_Formal_Subp; + + -- Local variables + + Call_Attrs : Call_Attributes; + Call_Nam : Node_Id; + Marker : Node_Id; + Target_Id : Entity_Id; + + -- Start of processing for Build_Call_Marker + + begin + -- Nothing to do for ASIS. As a result, ABE checks and diagnostics are + -- not performed in this mode. + + if ASIS_Mode then + return; + + -- Nothing to do when the input does not denote a call or a requeue + + elsif not Nkind_In (N, N_Entry_Call_Statement, + N_Function_Call, + N_Procedure_Call_Statement, + N_Requeue_Statement) + then + return; + + -- Nothing to do when the call is being preanalyzed as the marker will + -- be inserted in the wrong place. + + elsif Preanalysis_Active then + return; + + -- Nothing to do when the call is analyzed/resolved too early within an + -- intermediate context. + + -- Performance note: parent traversal + + elsif In_Premature_Context (N) then + return; + end if; + + Call_Nam := Extract_Call_Name (N); + + -- Nothing to do when the call is erroneous or left in a bad state + + if not (Is_Entity_Name (Call_Nam) + and then Present (Entity (Call_Nam)) + and then Is_Subprogram_Or_Entry (Entity (Call_Nam))) + then + return; + + -- Nothing to do when the call invokes a generic formal subprogram and + -- switch -gnatd.G (ignore calls through generic formal parameters for + -- elaboration) is in effect. This check must be performed with the + -- direct target of the call to avoid the side effects of mapping + -- actuals to formals using renamings. + + elsif Debug_Flag_Dot_GG + and then Is_Generic_Formal_Subp (Entity (Call_Nam)) + then + return; + end if; + + Extract_Call_Attributes + (Call => N, + Target_Id => Target_Id, + Attrs => Call_Attrs); + + -- Nothing to do when the call appears within the expanded spec or + -- body of an instantiated generic, the call does not invoke a generic + -- formal subprogram, the target is external to the instance, and switch + -- -gnatdL (ignore external calls from instances for elaboration) is in + -- effect. This behaviour approximates that of the old ABE mechanism. + + if Debug_Flag_LL + and then not Is_Generic_Formal_Subp (Entity (Call_Nam)) + + -- Performance note: parent traversal + + and then In_External_Context + (Call => N, + Target_Id => Target_Id) + then + return; + + -- Source calls to source targets are always considered because they + -- reflect the original call graph. + + elsif Comes_From_Source (Target_Id) and then Call_Attrs.From_Source then + null; + + -- A call to a source function which acts as the default expression in + -- another call requires special detection. + + elsif Comes_From_Source (Target_Id) + and then Nkind (N) = N_Function_Call + and then Is_Default_Expression (N) + then + null; + + -- The target emulates Ada semantics + + elsif Is_Ada_Semantic_Target (Target_Id) then + null; + + -- The target acts as a link between scenarios + + elsif Is_Bridge_Target (Target_Id) then + null; + + -- The target emulates SPARK semantics + + elsif Is_SPARK_Semantic_Target (Target_Id) then + null; + + -- Otherwise the call is not suitable for ABE processing. This prevents + -- the generation of call markers which will never play a role in ABE + -- diagnostics. + + else + return; + end if; + + -- At this point it is known that the call will play some role in ABE + -- checks and diagnostics. Create a corresponding call marker in case + -- the original call is heavily transformed by expansion later on. + + Marker := Make_Call_Marker (Sloc (N)); + + -- Inherit the attributes of the original call + + Set_Target (Marker, Target_Id); + Set_Is_Elaboration_Checks_OK_Node (Marker, Call_Attrs.Elab_Checks_OK); + Set_Is_Declaration_Level_Node (Marker, Call_Attrs.In_Declarations); + Set_Is_Dispatching_Call (Marker, Call_Attrs.Is_Dispatching); + Set_Is_Ignored_Ghost_Node (Marker, Call_Attrs.Ghost_Mode_Ignore); + Set_Is_Source_Call (Marker, Call_Attrs.From_Source); + Set_Is_SPARK_Mode_On_Node (Marker, Call_Attrs.SPARK_Mode_On); + + -- The marker is inserted prior to the original call. This placement has + -- several desirable effects: + + -- 1) The marker appears in the same context, in close proximity to + -- the call. + + -- <marker> + -- <call> + + -- 2) Inserting the marker prior to the call ensures that an ABE check + -- will take effect prior to the call. + + -- <ABE check> + -- <marker> + -- <call> + + -- 3) The above two properties are preserved even when the call is a + -- function which is subsequently relocated in order to capture its + -- result. Note that if the call is relocated to a new context, the + -- relocated call will receive a marker of its own. + + -- <ABE check> + -- <maker> + -- Temp : ... := Func_Call ...; + -- ... Temp ... + + -- The insertion must take place even when the call does not occur in + -- the main unit to keep the tree symmetric. This ensures that internal + -- name serialization is consistent in case the call marker causes the + -- tree to transform in some way. + + Insert_Action (N, Marker); + + -- The marker becomes the "corresponding" scenario for the call. Save + -- the marker for later processing by the ABE phase. + + Record_Elaboration_Scenario (Marker); + end Build_Call_Marker; + + --------------------------------- + -- Check_Elaboration_Scenarios -- + --------------------------------- + + procedure Check_Elaboration_Scenarios is + begin + -- Nothing to do for ASIS. As a result, no ABE checks and diagnostics + -- are performed in this mode. + + if ASIS_Mode then + return; + end if; + + -- Examine the context of the main unit and record all units with prior + -- elaboration with respect to it. + + Find_Elaborated_Units; + + -- Examine each top level scenario saved during the Recording phase and + -- perform various actions depending on the elaboration model in effect. + + for Index in Top_Level_Scenarios.First .. Top_Level_Scenarios.Last loop + + -- Clear the table of visited scenario bodies for each new top level + -- scenario. + + Visited_Bodies.Reset; + + Process_Scenario (Top_Level_Scenarios.Table (Index)); + end loop; + end Check_Elaboration_Scenarios; + + ------------------------------ + -- Check_Preelaborated_Call -- + ------------------------------ + + procedure Check_Preelaborated_Call (Call : Node_Id) is + function In_Preelaborated_Context (N : Node_Id) return Boolean; + -- Determine whether arbitrary node appears in a preelaborated context + + ------------------------------ + -- In_Preelaborated_Context -- + ------------------------------ + + function In_Preelaborated_Context (N : Node_Id) return Boolean is + Body_Id : constant Entity_Id := Find_Code_Unit (N); + Spec_Id : constant Entity_Id := Unique_Entity (Body_Id); + + begin + -- The node appears within a package body whose corresponding spec is + -- subject to pragma Remote_Call_Interface or Remote_Types. This does + -- not result in a preelaborated context because the package body may + -- be on another machine. + + if Ekind (Body_Id) = E_Package_Body + and then Ekind_In (Spec_Id, E_Generic_Package, E_Package) + and then (Is_Remote_Call_Interface (Spec_Id) + or else Is_Remote_Types (Spec_Id)) + then + return False; + + -- Otherwise the node appears within a preelaborated context when the + -- associated unit is preelaborated. + + else + return Is_Preelaborated_Unit (Spec_Id); + end if; + end In_Preelaborated_Context; + + -- Local variables + + Call_Attrs : Call_Attributes; + Level : Enclosing_Level_Kind; + Target_Id : Entity_Id; + + -- Start of processing for Check_Preelaborated_Call + + begin + Extract_Call_Attributes + (Call => Call, + Target_Id => Target_Id, + Attrs => Call_Attrs); + + -- Nothing to do when the call is internally generated because it is + -- assumed that it will never violate preelaboration. + + if not Call_Attrs.From_Source then + return; + end if; + + -- Performance note: parent traversal + + Level := Find_Enclosing_Level (Call); + + -- Library level calls are always considered because they are part of + -- the associated unit's elaboration actions. + + if Level in Library_Level then + null; + + -- Calls at the library level of a generic package body must be checked + -- because they would render an instantiation illegal if the template is + -- marked as preelaborated. Note that this does not apply to calls at + -- the library level of a generic package spec. + + elsif Level = Generic_Package_Body then + null; + + -- Otherwise the call does not appear at the proper level and must not + -- be considered for this check. + + else + return; + end if; + + -- The call appears within a preelaborated unit. Emit a warning only for + -- internal uses, otherwise this is an error. + + if In_Preelaborated_Context (Call) then + Error_Msg_Warn := GNAT_Mode; + Error_Msg_N + ("<<non-static call not allowed in preelaborated unit", Call); + end if; + end Check_Preelaborated_Call; + + ---------------------- + -- Compilation_Unit -- + ---------------------- + + function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id is + Comp_Unit : Node_Id; + + begin + Comp_Unit := Parent (Unit_Id); + + -- Handle the case where a concurrent subunit is rewritten as a null + -- statement due to expansion activities. + + if Nkind (Comp_Unit) = N_Null_Statement + and then Nkind_In (Original_Node (Comp_Unit), N_Protected_Body, + N_Task_Body) + then + Comp_Unit := Parent (Comp_Unit); + pragma Assert (Nkind (Comp_Unit) = N_Subunit); + + -- Otherwise use the declaration node of the unit + + else + Comp_Unit := Parent (Unit_Declaration_Node (Unit_Id)); + end if; + + -- Handle the case where a subprogram instantiation which acts as a + -- compilation unit is expanded into an anonymous package that wraps + -- the instantiated subprogram. + + if Nkind (Comp_Unit) = N_Package_Specification + and then Nkind_In (Original_Node (Parent (Comp_Unit)), + N_Function_Instantiation, + N_Procedure_Instantiation) + then + Comp_Unit := Parent (Parent (Comp_Unit)); + + -- Handle the case where the compilation unit is a subunit + + elsif Nkind (Comp_Unit) = N_Subunit then + Comp_Unit := Parent (Comp_Unit); + end if; + + pragma Assert (Nkind (Comp_Unit) = N_Compilation_Unit); + + return Comp_Unit; + end Compilation_Unit; + + ----------------- + -- Elab_Msg_NE -- + ----------------- + + procedure Elab_Msg_NE + (Msg : String; + N : Node_Id; + Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean) + is + function Prefix return String; + -- Obtain the prefix of the message + + function Suffix return String; + -- Obtain the suffix of the message + + ------------ + -- Prefix -- + ------------ + + function Prefix return String is + begin + if Info_Msg then + return "info: "; + else + return ""; + end if; + end Prefix; + + ------------ + -- Suffix -- + ------------ + + function Suffix return String is + begin + if In_SPARK then + return " in SPARK"; + else + return ""; + end if; + end Suffix; + + -- Start of processing for Elab_Msg_NE + + begin + Error_Msg_NE (Prefix & Msg & Suffix, N, Id); + end Elab_Msg_NE; + + ------------------------------ + -- Elaboration_Context_Hash -- + ------------------------------ + + function Elaboration_Context_Hash + (Key : Entity_Id) return Elaboration_Context_Index + is + begin + return Elaboration_Context_Index (Key mod Elaboration_Context_Max); + end Elaboration_Context_Hash; + + ------------------------------ + -- Ensure_Prior_Elaboration -- + ------------------------------ + + procedure Ensure_Prior_Elaboration + (N : Node_Id; + Unit_Id : Entity_Id; + In_Task_Body : Boolean) + is + Prag_Nam : Name_Id; + + begin + -- Instantiating an external generic unit requires an implicit Elaborate + -- because Elaborate_All is too strong and could introduce non-existent + -- elaboration cycles. + + -- package External is + -- function Func ...; + -- end External; + + -- with External; + -- generic + -- package Gen is + -- X : ... := External.Func; + -- end Gen; + + -- [with External;] -- implicit with for External + -- [pragma Elaborate_All (External);] -- Elaborate_All for External + -- with Gen; + -- [pragma Elaborate (Gen);] -- Elaborate for generic + -- procedure Main is + -- package Inst is new Gen; -- calls External.Func + -- ... + -- end Main; + + if Nkind (N) in N_Generic_Instantiation then + Prag_Nam := Name_Elaborate; + + -- Otherwise generate an implicit Elaborate_All + + else + Prag_Nam := Name_Elaborate_All; + end if; + + -- Nothing to do when the need for prior elaboration came from a task + -- body and switch -gnatd.y (disable implicit pragma Elaborate_All on + -- task bodies) is in effect. + + if Debug_Flag_Dot_Y and then In_Task_Body then + return; + + -- Nothing to do when the unit is elaborated prior to the main unit. + -- This check must also consider the following cases: + + -- * No check is made against the context of the main unit because this + -- is specific to the elaboration model in effect and requires custom + -- handling (see Ensure_xxx_Prior_Elaboration). + + -- * Unit_Id is subject to pragma Elaborate_Body. An implicit pragma + -- Elaborate[_All] MUST be generated even though Unit_Id is always + -- elaborated prior to the main unit. This is a conservative strategy + -- which ensures that other units withed by Unit_Id will not lead to + -- an ABE. + + -- package A is package body A is + -- procedure ABE; procedure ABE is ... end ABE; + -- end A; end A; + + -- with A; + -- package B is package body B is + -- pragma Elaborate_Body; procedure Proc is + -- begin + -- procedure Proc; A.ABE; + -- package B; end Proc; + -- end B; + + -- with B; + -- package C is package body C is + -- ... ... + -- end C; begin + -- B.Proc; + -- end C; + + -- In the example above, the elaboration of C invokes B.Proc. B is + -- subject to pragma Elaborate_Body. If no pragma Elaborate[_All] is + -- generated for B in C, then the following elaboratio order will lead + -- to an ABE: + + -- spec of A elaborated + -- spec of B elaborated + -- body of B elaborated + -- spec of C elaborated + -- body of C elaborated <-- calls B.Proc which calls A.ABE + -- body of A elaborated <-- problem + + -- The generation of an implicit pragma Elaborate_All (B) ensures that + -- the elaboration order mechanism will not pick the above order. + + -- An implicit Elaborate is NOT generated when the unit is subject to + -- Elaborate_Body because both pragmas have the exact same effect. + + -- * Unit_Id is the main unit. An implicit pragma Elaborate[_All] MUST + -- NOT be generated in this case because a unit cannot depend on its + -- own elaboration. This case is therefore treated as valid prior + -- elaboration. + + elsif Has_Prior_Elaboration + (Unit_Id => Unit_Id, + Same_Unit_OK => True, + Elab_Body_OK => Prag_Nam = Name_Elaborate) + then + return; + + -- Suggest the use of pragma Prag_Nam when the dynamic model is in + -- effect. + + elsif Dynamic_Elaboration_Checks then + Ensure_Prior_Elaboration_Dynamic + (N => N, + Unit_Id => Unit_Id, + Prag_Nam => Prag_Nam); + + -- Install an implicit pragma Prag_Nam when the static model is in + -- effect. + + else + pragma Assert (Static_Elaboration_Checks); + + Ensure_Prior_Elaboration_Static + (N => N, + Unit_Id => Unit_Id, + Prag_Nam => Prag_Nam); + end if; + end Ensure_Prior_Elaboration; + + -------------------------------------- + -- Ensure_Prior_Elaboration_Dynamic -- + -------------------------------------- + + procedure Ensure_Prior_Elaboration_Dynamic + (N : Node_Id; + Unit_Id : Entity_Id; + Prag_Nam : Name_Id) + is + procedure Info_Missing_Pragma; + pragma Inline (Info_Missing_Pragma); + -- Output information concerning missing Elaborate or Elaborate_All + -- pragma with name Prag_Nam for scenario N, which would ensure the + -- prior elaboration of Unit_Id. + + ------------------------- + -- Info_Missing_Pragma -- + ------------------------- + + procedure Info_Missing_Pragma is + begin + -- Internal units are ignored as they cause unnecessary noise + + if not In_Internal_Unit (Unit_Id) then + + -- The name of the unit subjected to the elaboration pragma is + -- fully qualified to improve the clarity of the info message. + + Error_Msg_Name_1 := Prag_Nam; + Error_Msg_Qual_Level := Nat'Last; + + Error_Msg_NE ("info: missing pragma % for unit &", N, Unit_Id); + Error_Msg_Qual_Level := 0; + end if; + end Info_Missing_Pragma; + + -- Local variables + + Elab_Attrs : Elaboration_Attributes; + Level : Enclosing_Level_Kind; + + -- Start of processing for Ensure_Prior_Elaboration_Dynamic + + begin + Elab_Attrs := Elaboration_Context.Get (Unit_Id); + + -- Nothing to do when the unit is guaranteed prior elaboration by means + -- of a source Elaborate[_All] pragma. + + if Present (Elab_Attrs.Source_Pragma) then + return; + end if; + + -- Output extra information on a missing Elaborate[_All] pragma when + -- switch -gnatel (info messages on implicit Elaborate[_All] pragmas + -- is in effect. + + if Elab_Info_Messages then + + -- Performance note: parent traversal + + Level := Find_Enclosing_Level (N); + + -- Declaration-level scenario + + if (Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N)) + and then Level = Declaration_Level + then + null; + + -- Library-level scenario + + elsif Level in Library_Level then + null; + + -- Instantiation library-level scenario + + elsif Level = Instantiation then + null; + + -- Otherwise the scenario does not appear at the proper level and + -- cannot possibly act as a top-level scenario. + + else + return; + end if; + + Info_Missing_Pragma; + end if; + end Ensure_Prior_Elaboration_Dynamic; + + ------------------------------------- + -- Ensure_Prior_Elaboration_Static -- + ------------------------------------- + + procedure Ensure_Prior_Elaboration_Static + (N : Node_Id; + Unit_Id : Entity_Id; + Prag_Nam : Name_Id) + is + function Find_With_Clause + (Items : List_Id; + Withed_Id : Entity_Id) return Node_Id; + pragma Inline (Find_With_Clause); + -- Find a nonlimited with clause in the list of context items Items + -- that withs unit Withed_Id. Return Empty if no such clause is found. + + procedure Info_Implicit_Pragma; + pragma Inline (Info_Implicit_Pragma); + -- Output information concerning an implicitly generated Elaborate or + -- Elaborate_All pragma with name Prag_Nam for scenario N which ensures + -- the prior elaboration of unit Unit_Id. + + ---------------------- + -- Find_With_Clause -- + ---------------------- + + function Find_With_Clause + (Items : List_Id; + Withed_Id : Entity_Id) return Node_Id + is + Item : Node_Id; + + begin + -- Examine the context clauses looking for a suitable with. Note that + -- limited clauses do not affect the elaboration order. + + Item := First (Items); + while Present (Item) loop + if Nkind (Item) = N_With_Clause + and then not Error_Posted (Item) + and then not Limited_Present (Item) + and then Entity (Name (Item)) = Withed_Id + then + return Item; + end if; + + Next (Item); + end loop; + + return Empty; + end Find_With_Clause; + + -------------------------- + -- Info_Implicit_Pragma -- + -------------------------- + + procedure Info_Implicit_Pragma is + begin + -- Internal units are ignored as they cause unnecessary noise + + if not In_Internal_Unit (Unit_Id) then + + -- The name of the unit subjected to the elaboration pragma is + -- fully qualified to improve the clarity of the info message. + + Error_Msg_Name_1 := Prag_Nam; + Error_Msg_Qual_Level := Nat'Last; + + Error_Msg_NE + ("info: implicit pragma % generated for unit &", N, Unit_Id); + + Error_Msg_Qual_Level := 0; + Output_Active_Scenarios (N); + end if; + end Info_Implicit_Pragma; + + -- Local variables + + Main_Cunit : constant Node_Id := Cunit (Main_Unit); + Loc : constant Source_Ptr := Sloc (Main_Cunit); + Unit_Cunit : constant Node_Id := Compilation_Unit (Unit_Id); + + Is_Instantiation : constant Boolean := + Nkind (N) in N_Generic_Instantiation; + + Clause : Node_Id; + Elab_Attrs : Elaboration_Attributes; + Items : List_Id; + + -- Start of processing for Ensure_Prior_Elaboration_Static + + begin + Elab_Attrs := Elaboration_Context.Get (Unit_Id); + + -- Nothing to do when the unit is guaranteed prior elaboration by means + -- of a source Elaborate[_All] pragma. + + if Present (Elab_Attrs.Source_Pragma) then + return; + + -- Nothing to do when the unit has an existing implicit Elaborate[_All] + -- pragma installed by a previous scenario. + + elsif Present (Elab_Attrs.With_Clause) then + + -- The unit is already guaranteed prior elaboration by means of an + -- implicit Elaborate pragma, however the current scenario imposes + -- a stronger requirement of Elaborate_All. "Upgrade" the existing + -- pragma to match this new requirement. + + if Elaborate_Desirable (Elab_Attrs.With_Clause) + and then Prag_Nam = Name_Elaborate_All + then + Set_Elaborate_All_Desirable (Elab_Attrs.With_Clause); + Set_Elaborate_Desirable (Elab_Attrs.With_Clause, False); + end if; + + return; + end if; + + -- At this point it is known that the unit has no prior elaboration + -- according to pragmas and hierarchical relationships. + + Items := Context_Items (Main_Cunit); + + if No (Items) then + Items := New_List; + Set_Context_Items (Main_Cunit, Items); + end if; + + -- Locate the with clause for the unit. Note that there may not be a + -- clause if the unit is visible through a subunit-body, body-spec, or + -- spec-parent relationship. + + Clause := + Find_With_Clause + (Items => Items, + Withed_Id => Unit_Id); + + -- Generate: + -- with Id; + + -- Note that adding implicit with clauses is safe because analysis, + -- resolution, and expansion have already taken place and it is not + -- possible to interfere with visibility. + + if No (Clause) then + Clause := + Make_With_Clause (Loc, + Name => New_Occurrence_Of (Unit_Id, Loc)); + + Set_Implicit_With (Clause); + Set_Library_Unit (Clause, Unit_Cunit); + + Append_To (Items, Clause); + end if; + + -- Instantiations require an implicit Elaborate because Elaborate_All is + -- too conservative and may introduce non-existent elaboration cycles. + + if Is_Instantiation then + Set_Elaborate_Desirable (Clause); + + -- Otherwise generate an implicit Elaborate_All + + else + Set_Elaborate_All_Desirable (Clause); + end if; + + -- The implicit Elaborate[_All] ensures the prior elaboration of the + -- unit. Include the unit in the elaboration context of the main unit. + + Elaboration_Context.Set (Unit_Id, + Elaboration_Attributes'(Source_Pragma => Empty, + With_Clause => Clause)); + + -- Output extra information on an implicit Elaborate[_All] pragma when + -- switch -gnatel (info messages on implicit Elaborate[_All] pragmas is + -- in effect. + + if Elab_Info_Messages then + Info_Implicit_Pragma; + end if; + end Ensure_Prior_Elaboration_Static; + + ----------------------------- + -- Extract_Assignment_Name -- + ----------------------------- + + function Extract_Assignment_Name (Asmt : Node_Id) return Node_Id is + Nam : Node_Id; + + begin + Nam := Name (Asmt); + + -- When the name denotes an array or record component, find the whole + -- object. + + while Nkind_In (Nam, N_Explicit_Dereference, + N_Indexed_Component, + N_Selected_Component, + N_Slice) + loop + Nam := Prefix (Nam); + end loop; + + return Nam; + end Extract_Assignment_Name; + + ----------------------------- + -- Extract_Call_Attributes -- + ----------------------------- + + procedure Extract_Call_Attributes + (Call : Node_Id; + Target_Id : out Entity_Id; + Attrs : out Call_Attributes) + is + From_Source : Boolean; + In_Declarations : Boolean; + Is_Dispatching : Boolean; + + begin + -- Extraction for call markers + + if Nkind (Call) = N_Call_Marker then + Target_Id := Target (Call); + From_Source := Is_Source_Call (Call); + In_Declarations := Is_Declaration_Level_Node (Call); + Is_Dispatching := Is_Dispatching_Call (Call); + + -- Extraction for entry calls, requeue, and subprogram calls + + else + pragma Assert (Nkind_In (Call, N_Entry_Call_Statement, + N_Function_Call, + N_Procedure_Call_Statement, + N_Requeue_Statement)); + + Target_Id := Entity (Extract_Call_Name (Call)); + From_Source := Comes_From_Source (Call); + + -- Performance note: parent traversal + + In_Declarations := Find_Enclosing_Level (Call) = Declaration_Level; + Is_Dispatching := + Nkind_In (Call, N_Function_Call, N_Procedure_Call_Statement) + and then Present (Controlling_Argument (Call)); + end if; + + -- Obtain the original entry or subprogram which the target may rename + -- except when the target is an instantiation. In this case the alias + -- is the internally generated subprogram which appears within the the + -- anonymous package created for the instantiation. Such an alias is not + -- a suitable target. + + if not (Is_Subprogram (Target_Id) + and then Is_Generic_Instance (Target_Id)) + then + Target_Id := Get_Renamed_Entity (Target_Id); + end if; + + -- Set all attributes + + Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Node (Call); + Attrs.From_Source := From_Source; + Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Node (Call); + Attrs.In_Declarations := In_Declarations; + Attrs.Is_Dispatching := Is_Dispatching; + Attrs.SPARK_Mode_On := Is_SPARK_Mode_On_Node (Call); + end Extract_Call_Attributes; + + ----------------------- + -- Extract_Call_Name -- + ----------------------- + + function Extract_Call_Name (Call : Node_Id) return Node_Id is + Nam : Node_Id; + + begin + Nam := Name (Call); + + -- When the call invokes an entry family, the name appears as an indexed + -- component. + + if Nkind (Nam) = N_Indexed_Component then + Nam := Prefix (Nam); + end if; + + -- When the call employs the object.operation form, the name appears as + -- a selected component. + + if Nkind (Nam) = N_Selected_Component then + Nam := Selector_Name (Nam); + end if; + + return Nam; + end Extract_Call_Name; + + --------------------------------- + -- Extract_Instance_Attributes -- + --------------------------------- + + procedure Extract_Instance_Attributes + (Exp_Inst : Node_Id; + Inst_Body : out Node_Id; + Inst_Decl : out Node_Id) + is + Body_Id : Entity_Id; + + begin + -- Assume that the attributes are unavailable + + Inst_Body := Empty; + Inst_Decl := Empty; + + -- Generic package or subprogram spec + + if Nkind_In (Exp_Inst, N_Package_Declaration, + N_Subprogram_Declaration) + then + Inst_Decl := Exp_Inst; + Body_Id := Corresponding_Body (Inst_Decl); + + if Present (Body_Id) then + Inst_Body := Unit_Declaration_Node (Body_Id); + end if; + + -- Generic package or subprogram body + + else + pragma Assert + (Nkind_In (Exp_Inst, N_Package_Body, N_Subprogram_Body)); + + Inst_Body := Exp_Inst; + Inst_Decl := Unit_Declaration_Node (Corresponding_Spec (Inst_Body)); + end if; + end Extract_Instance_Attributes; + + -------------------------------------- + -- Extract_Instantiation_Attributes -- + -------------------------------------- + + procedure Extract_Instantiation_Attributes + (Exp_Inst : Node_Id; + Inst : out Node_Id; + Inst_Id : out Entity_Id; + Gen_Id : out Entity_Id; + Attrs : out Instantiation_Attributes) + is + begin + Inst := Original_Node (Exp_Inst); + Inst_Id := Defining_Entity (Inst); + + -- Traverse a possible chain of renamings to obtain the original generic + -- being instantiatied. + + Gen_Id := Get_Renamed_Entity (Entity (Name (Inst))); + + -- Set all attributes + + Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Node (Inst); + Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Node (Inst); + Attrs.In_Declarations := Is_Declaration_Level_Node (Inst); + Attrs.SPARK_Mode_On := Is_SPARK_Mode_On_Node (Inst); + end Extract_Instantiation_Attributes; + + ------------------------------- + -- Extract_Target_Attributes -- + ------------------------------- + + procedure Extract_Target_Attributes + (Target_Id : Entity_Id; + Attrs : out Target_Attributes) + is + procedure Extract_Package_Or_Subprogram_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id); + -- Obtain the attributes associated with a package or a subprogram. + -- Spec_Id is the package or subprogram. Body_Decl is the declaration + -- of the corresponding package or subprogram body. + + procedure Extract_Protected_Entry_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id; + Body_Barf : out Node_Id); + -- Obtain the attributes associated with a protected entry [family]. + -- Spec_Id is the entity of the protected body subprogram. Body_Decl + -- is the declaration of Spec_Id's corresponding body. Body_Barf is + -- the declaration of the barrier function body. + + procedure Extract_Protected_Subprogram_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id); + -- Obtain the attributes associated with a protected subprogram. Formal + -- Spec_Id is the entity of the protected body subprogram. Body_Decl is + -- the declaration of Spec_Id's corresponding body. + + procedure Extract_Task_Entry_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id); + -- Obtain the attributes associated with a task entry [family]. Formal + -- Spec_Id is the entity of the task body procedure. Body_Decl is the + -- declaration of Spec_Id's corresponding body. + + ---------------------------------------------- + -- Extract_Package_Or_Subprogram_Attributes -- + ---------------------------------------------- + + procedure Extract_Package_Or_Subprogram_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id) + is + Body_Id : Entity_Id; + Init_Id : Entity_Id; + Spec_Decl : Node_Id; + + begin + -- Assume that the body is not available + + Body_Decl := Empty; + Spec_Id := Target_Id; + + -- For body retrieval purposes, the entity of the initial declaration + -- is that of the spec. + + Init_Id := Spec_Id; + + -- The only exception to the above is a function which returns a + -- constrained array type in a SPARK-to-C compilation. In this case + -- the function receives a corresponding procedure which has an out + -- parameter. The proper body for ABE checks and diagnostics is that + -- of the procedure. + + if Ekind (Init_Id) = E_Function + and then Rewritten_For_C (Init_Id) + then + Init_Id := Corresponding_Procedure (Init_Id); + end if; + + -- Extract the attributes of the body + + Spec_Decl := Unit_Declaration_Node (Init_Id); + + -- The initial declaration is a stand alone subprogram body + + if Nkind (Spec_Decl) = N_Subprogram_Body then + Body_Decl := Spec_Decl; + + -- Otherwise the package or subprogram has a spec and a completing + -- body. + + elsif Nkind_In (Spec_Decl, N_Generic_Package_Declaration, + N_Generic_Subprogram_Declaration, + N_Package_Declaration, + N_Subprogram_Body_Stub, + N_Subprogram_Declaration) + then + Body_Id := Corresponding_Body (Spec_Decl); + + if Present (Body_Id) then + Body_Decl := Unit_Declaration_Node (Body_Id); + end if; + end if; + end Extract_Package_Or_Subprogram_Attributes; + + ---------------------------------------- + -- Extract_Protected_Entry_Attributes -- + ---------------------------------------- + + procedure Extract_Protected_Entry_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id; + Body_Barf : out Node_Id) + is + Barf_Id : Entity_Id; + Body_Id : Entity_Id; + + begin + -- Assume that the bodies are not available + + Body_Barf := Empty; + Body_Decl := Empty; + + -- When the entry [family] has already been expanded, it carries both + -- the procedure which emulates the behavior of the entry [family] as + -- well as the barrier function. + + if Present (Protected_Body_Subprogram (Target_Id)) then + Spec_Id := Protected_Body_Subprogram (Target_Id); + + -- Extract the attributes of the barrier function + + Barf_Id := + Corresponding_Body + (Unit_Declaration_Node (Barrier_Function (Target_Id))); + + if Present (Barf_Id) then + Body_Barf := Unit_Declaration_Node (Barf_Id); + end if; + + -- Otherwise no expansion took place + + else + Spec_Id := Target_Id; + end if; + + -- Extract the attributes of the entry body + + Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id)); + + if Present (Body_Id) then + Body_Decl := Unit_Declaration_Node (Body_Id); + end if; + end Extract_Protected_Entry_Attributes; + + --------------------------------------------- + -- Extract_Protected_Subprogram_Attributes -- + --------------------------------------------- + + procedure Extract_Protected_Subprogram_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id) + is + Body_Id : Entity_Id; + + begin + -- Assume that the body is not available + + Body_Decl := Empty; + + -- When the protected subprogram has already been expanded, it + -- carries the subprogram which seizes the lock and invokes the + -- original statements. + + if Present (Protected_Subprogram (Target_Id)) then + Spec_Id := + Protected_Body_Subprogram (Protected_Subprogram (Target_Id)); + + -- Otherwise no expansion took place + + else + Spec_Id := Target_Id; + end if; + + -- Extract the attributes of the body + + Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id)); + + if Present (Body_Id) then + Body_Decl := Unit_Declaration_Node (Body_Id); + end if; + end Extract_Protected_Subprogram_Attributes; + + ----------------------------------- + -- Extract_Task_Entry_Attributes -- + ----------------------------------- + + procedure Extract_Task_Entry_Attributes + (Spec_Id : out Entity_Id; + Body_Decl : out Node_Id) + is + Task_Typ : constant Entity_Id := Non_Private_View (Scope (Target_Id)); + Body_Id : Entity_Id; + + begin + -- Assume that the body is not available + + Body_Decl := Empty; + + -- The the task type has already been expanded, it carries the + -- procedure which emulates the behavior of the task body. + + if Present (Task_Body_Procedure (Task_Typ)) then + Spec_Id := Task_Body_Procedure (Task_Typ); + + -- Otherwise no expansion took place + + else + Spec_Id := Task_Typ; + end if; + + -- Extract the attributes of the body + + Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id)); + + if Present (Body_Id) then + Body_Decl := Unit_Declaration_Node (Body_Id); + end if; + end Extract_Task_Entry_Attributes; + + -- Local variables + + Prag : constant Node_Id := SPARK_Pragma (Target_Id); + Body_Barf : Node_Id; + Body_Decl : Node_Id; + Spec_Id : Entity_Id; + + -- Start of processing for Extract_Target_Attributes + + begin + -- Assume that the body of the barrier function is not available + + Body_Barf := Empty; + + -- The target is a protected entry [family] + + if Is_Protected_Entry (Target_Id) then + Extract_Protected_Entry_Attributes + (Spec_Id => Spec_Id, + Body_Decl => Body_Decl, + Body_Barf => Body_Barf); + + -- The target is a protected subprogram + + elsif Is_Protected_Subp (Target_Id) + or else Is_Protected_Body_Subp (Target_Id) + then + Extract_Protected_Subprogram_Attributes + (Spec_Id => Spec_Id, + Body_Decl => Body_Decl); + + -- The target is a task entry [family] + + elsif Is_Task_Entry (Target_Id) then + Extract_Task_Entry_Attributes + (Spec_Id => Spec_Id, + Body_Decl => Body_Decl); + + -- Otherwise the target is a package or a subprogram + + else + Extract_Package_Or_Subprogram_Attributes + (Spec_Id => Spec_Id, + Body_Decl => Body_Decl); + end if; + + -- Set all attributes + + Attrs.Body_Barf := Body_Barf; + Attrs.Body_Decl := Body_Decl; + Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Id (Target_Id); + Attrs.From_Source := Comes_From_Source (Target_Id); + Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Entity (Target_Id); + Attrs.SPARK_Mode_On := + Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = On; + Attrs.Spec_Decl := Unit_Declaration_Node (Spec_Id); + Attrs.Spec_Id := Spec_Id; + Attrs.Unit_Id := Find_Top_Unit (Target_Id); + + -- At this point certain attributes should always be available + + pragma Assert (Present (Attrs.Spec_Decl)); + pragma Assert (Present (Attrs.Spec_Id)); + pragma Assert (Present (Attrs.Unit_Id)); + end Extract_Target_Attributes; + + ----------------------------- + -- Extract_Task_Attributes -- + ----------------------------- + + procedure Extract_Task_Attributes + (Typ : Entity_Id; + Attrs : out Task_Attributes) + is + Task_Typ : constant Entity_Id := Non_Private_View (Typ); + + Body_Decl : Node_Id; + Body_Id : Entity_Id; + Prag : Node_Id; + Spec_Id : Entity_Id; + + begin + -- Assume that the body of the task procedure is not available + + Body_Decl := Empty; + + -- The initial declaration is that of the task body procedure + + Spec_Id := Get_Task_Body_Procedure (Task_Typ); + Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id)); + + if Present (Body_Id) then + Body_Decl := Unit_Declaration_Node (Body_Id); + end if; + + Prag := SPARK_Pragma (Task_Typ); + + -- Set all attributes + + Attrs.Body_Decl := Body_Decl; + Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Id (Task_Typ); + Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Entity (Task_Typ); + Attrs.SPARK_Mode_On := + Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = On; + Attrs.Spec_Id := Spec_Id; + Attrs.Task_Decl := Declaration_Node (Task_Typ); + Attrs.Unit_Id := Find_Top_Unit (Task_Typ); + + -- At this point certain attributes should always be available + + pragma Assert (Present (Attrs.Spec_Id)); + pragma Assert (Present (Attrs.Task_Decl)); + pragma Assert (Present (Attrs.Unit_Id)); + end Extract_Task_Attributes; + + ------------------------------------------- + -- Extract_Variable_Reference_Attributes -- + ------------------------------------------- + + procedure Extract_Variable_Reference_Attributes + (Ref : Node_Id; + Var_Id : out Entity_Id; + Attrs : out Variable_Attributes) + is + begin + -- Traverse a possible chain of renamings to obtain the original + -- variable being referenced. + + Var_Id := Get_Renamed_Entity (Entity (Ref)); + + Attrs.SPARK_Mode_On := Is_SPARK_Mode_On_Node (Ref); + Attrs.Unit_Id := Find_Top_Unit (Var_Id); + + -- At this point certain attributes should always be available + + pragma Assert (Present (Attrs.Unit_Id)); + end Extract_Variable_Reference_Attributes; + + -------------------- + -- Find_Code_Unit -- + -------------------- + + function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id is + begin + return Find_Unit_Entity (Unit (Cunit (Get_Code_Unit (N)))); + end Find_Code_Unit; + + --------------------------- + -- Find_Elaborated_Units -- + --------------------------- + + procedure Find_Elaborated_Units is + procedure Add_Pragma (Prag : Node_Id); + -- Determine whether pragma Prag denotes a legal Elaborate[_All] pragma. + -- If this is the case, add the related unit to the elaboration context. + -- For pragma Elaborate_All, include recursively all units withed by the + -- related unit. + + procedure Add_Unit + (Unit_Id : Entity_Id; + Prag : Node_Id; + Full_Context : Boolean); + -- Add unit Unit_Id to the elaboration context. Prag denotes the pragma + -- which prompted the inclusion of the unit to the elaboration context. + -- If flag Full_Context is set, examine the nonlimited clauses of unit + -- Unit_Id and add each withed unit to the context. + + procedure Find_Elaboration_Context (Comp_Unit : Node_Id); + -- Examine the context items of compilation unit Comp_Unit for suitable + -- elaboration-related pragmas and add all related units to the context. + + ---------------- + -- Add_Pragma -- + ---------------- + + procedure Add_Pragma (Prag : Node_Id) is + Prag_Args : constant List_Id := Pragma_Argument_Associations (Prag); + Prag_Nam : constant Name_Id := Pragma_Name (Prag); + Unit_Arg : Node_Id; + + begin + -- Nothing to do if the pragma is not related to elaboration + + if not Nam_In (Prag_Nam, Name_Elaborate, Name_Elaborate_All) then + return; + + -- Nothing to do when the pragma is illegal + + elsif Error_Posted (Prag) then + return; + end if; + + Unit_Arg := Get_Pragma_Arg (First (Prag_Args)); + + -- The argument of the pragma may appear in package.package form + + if Nkind (Unit_Arg) = N_Selected_Component then + Unit_Arg := Selector_Name (Unit_Arg); + end if; + + Add_Unit + (Unit_Id => Entity (Unit_Arg), + Prag => Prag, + Full_Context => Prag_Nam = Name_Elaborate_All); + end Add_Pragma; + + -------------- + -- Add_Unit -- + -------------- + + procedure Add_Unit + (Unit_Id : Entity_Id; + Prag : Node_Id; + Full_Context : Boolean) + is + Clause : Node_Id; + Elab_Attrs : Elaboration_Attributes; + + begin + -- Nothing to do when some previous error left a with clause or a + -- pragma in a bad state. + + if No (Unit_Id) then + return; + end if; + + Elab_Attrs := Elaboration_Context.Get (Unit_Id); + + -- The current unit is not part of the context. Prepare a new set of + -- attributes. + + if Elab_Attrs = No_Elaboration_Attributes then + Elab_Attrs := + Elaboration_Attributes'(Source_Pragma => Prag, + With_Clause => Empty); + + -- The unit is already included in the context by means of pragma + -- Elaborate. "Upgrage" the existing attributes when the unit is + -- subject to Elaborate_All because the new pragma covers a larger + -- set of units. All other properties remain the same. + + elsif Pragma_Name (Elab_Attrs.Source_Pragma) = Name_Elaborate + and then Pragma_Name (Prag) = Name_Elaborate_All + then + Elab_Attrs.Source_Pragma := Prag; + + -- Otherwise the unit is already included in the context + + else + return; + end if; + + -- Add or update the attributes of the unit + + Elaboration_Context.Set (Unit_Id, Elab_Attrs); + + -- Includes all units withed by the current one when computing the + -- full context. + + if Full_Context then + + -- Process all nonlimited with clauses found in the context of + -- the current unit. Note that limited clauses do not impose an + -- elaboration order. + + Clause := First (Context_Items (Compilation_Unit (Unit_Id))); + while Present (Clause) loop + if Nkind (Clause) = N_With_Clause + and then not Error_Posted (Clause) + and then not Limited_Present (Clause) + then + Add_Unit + (Unit_Id => Entity (Name (Clause)), + Prag => Prag, + Full_Context => Full_Context); + end if; + + Next (Clause); + end loop; + end if; + end Add_Unit; + + ------------------------------ + -- Find_Elaboration_Context -- + ------------------------------ + + procedure Find_Elaboration_Context (Comp_Unit : Node_Id) is + Prag : Node_Id; + + begin + pragma Assert (Nkind (Comp_Unit) = N_Compilation_Unit); + + -- Process all elaboration-related pragmas found in the context of + -- the compilation unit. + + Prag := First (Context_Items (Comp_Unit)); + while Present (Prag) loop + if Nkind (Prag) = N_Pragma then + Add_Pragma (Prag); + end if; + + Next (Prag); + end loop; + end Find_Elaboration_Context; + + -- Local variables + + Par_Id : Entity_Id; + Unt : Node_Id; + + -- Start of processing for Find_Elaborated_Units + + begin + -- Perform a traversal which examines the context of the main unit and + -- populates the Elaboration_Context table with all units elaborated + -- prior to the main unit. The traversal performs the following jumps: + + -- subunit -> parent subunit + -- parent subunit -> body + -- body -> spec + -- spec -> parent spec + -- parent spec -> grandparent spec and so on + + -- The traversal relies on units rather than scopes because the scope of + -- a subunit is some spec, while this traversal must process the body as + -- well. Given that protected and task bodies can also be subunits, this + -- complicates the scope approach even further. + + Unt := Unit (Cunit (Main_Unit)); + + -- Perform the following traversals when the main unit is a subunit + + -- subunit -> parent subunit + -- parent subunit -> body + + while Present (Unt) and then Nkind (Unt) = N_Subunit loop + Find_Elaboration_Context (Parent (Unt)); + + -- Continue the traversal by going to the unit which contains the + -- corresponding stub. + + if Present (Corresponding_Stub (Unt)) then + Unt := Unit (Cunit (Get_Source_Unit (Corresponding_Stub (Unt)))); + + -- Otherwise the subunit may be erroneous or left in a bad state + + else + exit; + end if; + end loop; + + -- Perform the following traversal now that subunits have been taken + -- care of, or the main unit is a body. + + -- body -> spec + + if Present (Unt) + and then Nkind_In (Unt, N_Package_Body, N_Subprogram_Body) + then + Find_Elaboration_Context (Parent (Unt)); + + -- Continue the traversal by going to the unit which contains the + -- corresponding spec. + + if Present (Corresponding_Spec (Unt)) then + Unt := Unit (Cunit (Get_Source_Unit (Corresponding_Spec (Unt)))); + end if; + end if; + + -- Perform the following traversals now that the body has been taken + -- care of, or the main unit is a spec. + + -- spec -> parent spec + -- parent spec -> grandparent spec and so on + + if Present (Unt) + and then Nkind_In (Unt, N_Generic_Package_Declaration, + N_Generic_Subprogram_Declaration, + N_Package_Declaration, + N_Subprogram_Declaration) + then + Find_Elaboration_Context (Parent (Unt)); + + -- Process a potential chain of parent units which ends with the + -- main unit spec. The traversal can now safely rely on the scope + -- chain. + + Par_Id := Scope (Defining_Entity (Unt)); + while Present (Par_Id) and then Par_Id /= Standard_Standard loop + Find_Elaboration_Context (Compilation_Unit (Par_Id)); + + Par_Id := Scope (Par_Id); + end loop; + end if; + end Find_Elaborated_Units; + + ----------------------------- + -- Find_Enclosing_Instance -- + ----------------------------- + + function Find_Enclosing_Instance (N : Node_Id) return Node_Id is + Par : Node_Id; + Spec_Id : Entity_Id; + + begin + -- Climb the parent chain looking for an enclosing instance spec or body + + Par := N; + while Present (Par) loop + + -- Generic package or subprogram spec + + if Nkind_In (Par, N_Package_Declaration, + N_Subprogram_Declaration) + and then Is_Generic_Instance (Defining_Entity (Par)) + then + return Par; + + -- Generic package or subprogram body + + elsif Nkind_In (Par, N_Package_Body, N_Subprogram_Body) then + Spec_Id := Corresponding_Spec (Par); + + if Present (Spec_Id) and then Is_Generic_Instance (Spec_Id) then + return Par; + end if; + end if; + + Par := Parent (Par); + end loop; + + return Empty; + end Find_Enclosing_Instance; + + -------------------------- + -- Find_Enclosing_Level -- + -------------------------- + + function Find_Enclosing_Level (N : Node_Id) return Enclosing_Level_Kind is + function Level_Of (Unit : Node_Id) return Enclosing_Level_Kind; + -- Obtain the corresponding level of unit Unit + + -------------- + -- Level_Of -- + -------------- + + function Level_Of (Unit : Node_Id) return Enclosing_Level_Kind is + Spec_Id : Entity_Id; + + begin + if Nkind (Unit) in N_Generic_Instantiation then + return Instantiation; + + elsif Nkind (Unit) = N_Generic_Package_Declaration then + return Generic_Package_Spec; + + elsif Nkind (Unit) = N_Package_Declaration then + return Package_Spec; + + elsif Nkind (Unit) = N_Package_Body then + Spec_Id := Corresponding_Spec (Unit); + + -- The body belongs to a generic package + + if Present (Spec_Id) + and then Ekind (Spec_Id) = E_Generic_Package + then + return Generic_Package_Body; + + -- Otherwise the body belongs to a non-generic package. This also + -- treats an illegal package body without a corresponding spec as + -- a non-generic package body. + + else + return Package_Body; + end if; + end if; + + return No_Level; + end Level_Of; + + -- Local variables + + Context : Node_Id; + Curr : Node_Id; + Prev : Node_Id; + + -- Start of processing for Find_Enclosing_Level + + begin + -- Call markers and instantiations which appear at the declaration level + -- but are later relocated in a different context retain their original + -- declaration level. + + if Nkind_In (N, N_Call_Marker, + N_Function_Instantiation, + N_Package_Instantiation, + N_Procedure_Instantiation) + and then Is_Declaration_Level_Node (N) + then + return Declaration_Level; + end if; + + -- Climb the parent chain looking at the enclosing levels + + Prev := N; + Curr := Parent (Prev); + while Present (Curr) loop + + -- A traversal from a subunit continues via the corresponding stub + + if Nkind (Curr) = N_Subunit then + Curr := Corresponding_Stub (Curr); + + -- The current construct is a package. Packages are ignored because + -- they are always elaborated when the enclosing context is invoked + -- or elaborated. + + elsif Nkind_In (Curr, N_Package_Body, N_Package_Declaration) then + null; + + -- The current construct is a block statement + + elsif Nkind (Curr) = N_Block_Statement then + + -- Ignore internally generated blocks created by the expander for + -- various purposes such as abort defer/undefer. + + if not Comes_From_Source (Curr) then + null; + + -- If the traversal came from the handled sequence of statments, + -- then the node appears at the level of the enclosing construct. + -- This is a more reliable test because transients scopes within + -- the declarative region of the encapsulator are hard to detect. + + elsif Nkind (Prev) = N_Handled_Sequence_Of_Statements + and then Handled_Statement_Sequence (Curr) = Prev + then + return Find_Enclosing_Level (Parent (Curr)); + + -- Otherwise the traversal came from the declarations, the node is + -- at the declaration level. + + else + return Declaration_Level; + end if; + + -- The current construct is a declaration level encapsulator + + elsif Nkind_In (Curr, N_Entry_Body, + N_Subprogram_Body, + N_Task_Body) + then + -- If the traversal came from the handled sequence of statments, + -- then the node cannot possibly appear at any level. This is + -- a more reliable test because transients scopes within the + -- declarative region of the encapsulator are hard to detect. + + if Nkind (Prev) = N_Handled_Sequence_Of_Statements + and then Handled_Statement_Sequence (Curr) = Prev + then + return No_Level; + + -- Otherwise the traversal came from the declarations, the node is + -- at the declaration level. + + else + return Declaration_Level; + end if; + + -- The current construct is a non-library level encapsulator which + -- indicates that the node cannot possibly appear at any level. + -- Note that this check must come after the declaration level check + -- because both predicates share certain nodes. + + elsif Is_Non_Library_Level_Encapsulator (Curr) then + Context := Parent (Curr); + + -- The sole exception is when the encapsulator is the compilation + -- utit itself because the compilation unit node requires special + -- processing (see below). + + if Present (Context) + and then Nkind (Context) = N_Compilation_Unit + then + null; + + -- Otherwise the node is not at any level + + else + return No_Level; + end if; + + -- The current construct is a compilation unit. The node appears at + -- the [generic] library level when the unit is a [generic] package. + + elsif Nkind (Curr) = N_Compilation_Unit then + return Level_Of (Unit (Curr)); + end if; + + Prev := Curr; + Curr := Parent (Prev); + end loop; + + return No_Level; + end Find_Enclosing_Level; + + ------------------- + -- Find_Top_Unit -- + ------------------- + + function Find_Top_Unit (N : Node_Or_Entity_Id) return Entity_Id is + begin + return Find_Unit_Entity (Unit (Cunit (Get_Top_Level_Code_Unit (N)))); + end Find_Top_Unit; + + ---------------------- + -- Find_Unit_Entity -- + ---------------------- + + function Find_Unit_Entity (N : Node_Id) return Entity_Id is + Context : constant Node_Id := Parent (N); + Orig_N : constant Node_Id := Original_Node (N); + + begin + -- The unit denotes a package body of an instantiation which acts as + -- a compilation unit. The proper entity is that of the package spec. + + if Nkind (N) = N_Package_Body + and then Nkind (Orig_N) = N_Package_Instantiation + and then Nkind (Context) = N_Compilation_Unit + then + return Corresponding_Spec (N); + + -- The unit denotes an anonymous package created to wrap a subprogram + -- instantiation which acts as a compilation unit. The proper entity is + -- that of the "related instance". + + elsif Nkind (N) = N_Package_Declaration + and then Nkind_In (Orig_N, N_Function_Instantiation, + N_Procedure_Instantiation) + and then Nkind (Context) = N_Compilation_Unit + then + return + Related_Instance (Defining_Entity (N, Concurrent_Subunit => True)); + + -- Otherwise the proper entity is the defining entity + + else + return Defining_Entity (N, Concurrent_Subunit => True); + end if; + end Find_Unit_Entity; + + ----------------------- + -- First_Formal_Type -- + ----------------------- + + function First_Formal_Type (Subp_Id : Entity_Id) return Entity_Id is + Formal_Id : constant Entity_Id := First_Formal (Subp_Id); + Typ : Entity_Id; + + begin + if Present (Formal_Id) then + Typ := Etype (Formal_Id); + + -- Handle various combinations of concurrent and private types + + loop + if Ekind_In (Typ, E_Protected_Type, E_Task_Type) + and then Present (Anonymous_Object (Typ)) + then + Typ := Anonymous_Object (Typ); + + elsif Is_Concurrent_Record_Type (Typ) then + Typ := Corresponding_Concurrent_Type (Typ); + + elsif Is_Private_Type (Typ) and then Present (Full_View (Typ)) then + Typ := Full_View (Typ); + + else + exit; + end if; + end loop; + + return Typ; + end if; + + return Empty; + end First_Formal_Type; + + -------------- + -- Has_Body -- + -------------- + + function Has_Body (Pack_Decl : Node_Id) return Boolean is + function Find_Corresponding_Body (Spec_Id : Entity_Id) return Node_Id; + -- Try to locate the corresponding body of spec Spec_Id. If no body is + -- found, return Empty. + + function Find_Body + (Spec_Id : Entity_Id; + From : Node_Id) return Node_Id; + -- Try to locate the corresponding body of spec Spec_Id in the node list + -- which follows arbitrary node From. If no body is found, return Empty. + + function Load_Package_Body (Unit_Nam : Unit_Name_Type) return Node_Id; + -- Attempt to load the body of unit Unit_Nam. If the load failed, return + -- Empty. If the compilation will not generate code, return Empty. + + ----------------------------- + -- Find_Corresponding_Body -- + ----------------------------- + + function Find_Corresponding_Body (Spec_Id : Entity_Id) return Node_Id is + Context : constant Entity_Id := Scope (Spec_Id); + Spec_Decl : constant Node_Id := Unit_Declaration_Node (Spec_Id); + Body_Decl : Node_Id; + Body_Id : Entity_Id; + + begin + if Is_Compilation_Unit (Spec_Id) then + Body_Id := Corresponding_Body (Spec_Decl); + + if Present (Body_Id) then + return Unit_Declaration_Node (Body_Id); + + -- The package is at the library and requires a body. Load the + -- corresponding body because the optional body may be declared + -- there. + + elsif Unit_Requires_Body (Spec_Id) then + return + Load_Package_Body + (Get_Body_Name (Unit_Name (Get_Source_Unit (Spec_Decl)))); + + -- Otherwise there is no optional body + + else + return Empty; + end if; + + -- The immediate context is a package. The optional body may be + -- within the body of that package. + + -- procedure Proc is + -- package Nested_1 is + -- package Nested_2 is + -- generic + -- package Pack is + -- end Pack; + -- end Nested_2; + -- end Nested_1; + + -- package body Nested_1 is + -- package body Nested_2 is separate; + -- end Nested_1; + + -- separate (Proc.Nested_1.Nested_2) + -- package body Nested_2 is + -- package body Pack is -- optional body + -- ... + -- end Pack; + -- end Nested_2; + + elsif Is_Package_Or_Generic_Package (Context) then + Body_Decl := Find_Corresponding_Body (Context); + + -- The optional body is within the body of the enclosing package + + if Present (Body_Decl) then + return + Find_Body + (Spec_Id => Spec_Id, + From => First (Declarations (Body_Decl))); + + -- Otherwise the enclosing package does not have a body. This may + -- be the result of an error or a genuine lack of a body. + + else + return Empty; + end if; + + -- Otherwise the immediate context is a body. The optional body may + -- be within the same list as the spec. + + -- procedure Proc is + -- generic + -- package Pack is + -- end Pack; + + -- package body Pack is -- optional body + -- ... + -- end Pack; + + else + return + Find_Body + (Spec_Id => Spec_Id, + From => Next (Spec_Decl)); + end if; + end Find_Corresponding_Body; + + --------------- + -- Find_Body -- + --------------- + + function Find_Body + (Spec_Id : Entity_Id; + From : Node_Id) return Node_Id + is + Spec_Nam : constant Name_Id := Chars (Spec_Id); + Item : Node_Id; + Lib_Unit : Node_Id; + + begin + Item := From; + while Present (Item) loop + + -- The current item denotes the optional body + + if Nkind (Item) = N_Package_Body + and then Chars (Defining_Entity (Item)) = Spec_Nam + then + return Item; + + -- The current item denotes a stub, the optional body may be in + -- the subunit. + + elsif Nkind (Item) = N_Package_Body_Stub + and then Chars (Defining_Entity (Item)) = Spec_Nam + then + Lib_Unit := Library_Unit (Item); + + -- The corresponding subunit was previously loaded + + if Present (Lib_Unit) then + return Lib_Unit; + + -- Otherwise attempt to load the corresponding subunit + + else + return Load_Package_Body (Get_Unit_Name (Item)); + end if; + end if; + + Next (Item); + end loop; + + return Empty; + end Find_Body; + + ----------------------- + -- Load_Package_Body -- + ----------------------- + + function Load_Package_Body (Unit_Nam : Unit_Name_Type) return Node_Id is + Body_Decl : Node_Id; + Unit_Num : Unit_Number_Type; + + begin + -- The load is performed only when the compilation will generate code + + if Operating_Mode = Generate_Code then + Unit_Num := + Load_Unit + (Load_Name => Unit_Nam, + Required => False, + Subunit => False, + Error_Node => Pack_Decl); + + -- The load failed most likely because the physical file is + -- missing. + + if Unit_Num = No_Unit then + return Empty; + + -- Otherwise the load was successful, return the body of the unit + + else + Body_Decl := Unit (Cunit (Unit_Num)); + + -- If the unit is a subunit with an available proper body, + -- return the proper body. + + if Nkind (Body_Decl) = N_Subunit + and then Present (Proper_Body (Body_Decl)) + then + Body_Decl := Proper_Body (Body_Decl); + end if; + + return Body_Decl; + end if; + end if; + + return Empty; + end Load_Package_Body; + + -- Local variables + + Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl); + + -- Start of processing for Has_Body + + begin + -- The body is available + + if Present (Corresponding_Body (Pack_Decl)) then + return True; + + -- The body is required if the package spec contains a construct which + -- requires a completion in a body. + + elsif Unit_Requires_Body (Pack_Id) then + return True; + + -- The body may be optional + + else + return Present (Find_Corresponding_Body (Pack_Id)); + end if; + end Has_Body; + + --------------------------- + -- Has_Prior_Elaboration -- + --------------------------- + + function Has_Prior_Elaboration + (Unit_Id : Entity_Id; + Context_OK : Boolean := False; + Elab_Body_OK : Boolean := False; + Same_Unit_OK : Boolean := False) return Boolean + is + Main_Id : constant Entity_Id := Cunit_Entity (Main_Unit); + + begin + -- A preelaborated unit is always elaborated prior to the main unit + + if Is_Preelaborated_Unit (Unit_Id) then + return True; + + -- An internal unit is always elaborated prior to a non-internal main + -- unit. + + elsif In_Internal_Unit (Unit_Id) + and then not In_Internal_Unit (Main_Id) + then + return True; + + -- A unit has prior elaboration if it appears within the context of the + -- main unit. Consider this case only when requested by the caller. + + elsif Context_OK + and then Elaboration_Context.Get (Unit_Id) /= No_Elaboration_Attributes + then + return True; + + -- A unit whose body is elaborated together with its spec has prior + -- elaboration except with respect to itself. Consider this case only + -- when requested by the caller. + + elsif Elab_Body_OK + and then Has_Pragma_Elaborate_Body (Unit_Id) + and then not Is_Same_Unit (Unit_Id, Main_Id) + then + return True; + + -- A unit has no prior elaboration with respect to itself, but does not + -- require any means of ensuring its own elaboration either. Treat this + -- case as valid prior elaboration only when requested by the caller. + + elsif Same_Unit_OK and then Is_Same_Unit (Unit_Id, Main_Id) then + return True; + end if; + + return False; + end Has_Prior_Elaboration; + + -------------------------- + -- In_External_Instance -- + -------------------------- + + function In_External_Instance + (N : Node_Id; + Target_Decl : Node_Id) return Boolean + is + Dummy : Node_Id; + Inst_Body : Node_Id; + Inst_Decl : Node_Id; + + begin + -- Performance note: parent traversal + + Inst_Decl := Find_Enclosing_Instance (Target_Decl); + + -- The target declaration appears within an instance spec. Visibility is + -- ignored because internally generated primitives for private types may + -- reside in the private declarations and still be invoked from outside. + + if Present (Inst_Decl) + and then Nkind (Inst_Decl) = N_Package_Declaration + then + -- The scenario comes from the main unit and the instance does not + + if In_Extended_Main_Code_Unit (N) + and then not In_Extended_Main_Code_Unit (Inst_Decl) + then + return True; + + -- Otherwise the scenario must not appear within the instance spec or + -- body. + + else + Extract_Instance_Attributes + (Exp_Inst => Inst_Decl, + Inst_Body => Inst_Body, + Inst_Decl => Dummy); + + -- Performance note: parent traversal + + return not In_Subtree + (N => N, + Root1 => Inst_Decl, + Root2 => Inst_Body); + end if; + end if; + + return False; + end In_External_Instance; + + --------------------- + -- In_Main_Context -- + --------------------- + + function In_Main_Context (N : Node_Id) return Boolean is + begin + -- Scenarios outside the main unit are not considered because the ALI + -- information supplied to binde is for the main unit only. + + if not In_Extended_Main_Code_Unit (N) then + return False; + + -- Scenarios within internal units are not considered unless switch + -- -gnatdE (elaboration checks on predefined units) is in effect. + + elsif not Debug_Flag_EE and then In_Internal_Unit (N) then + return False; + end if; + + return True; + end In_Main_Context; + + --------------------- + -- In_Same_Context -- + --------------------- + + function In_Same_Context + (N1 : Node_Id; + N2 : Node_Id; + Nested_OK : Boolean := False) return Boolean + is + function Find_Enclosing_Context (N : Node_Id) return Node_Id; + -- Return the nearest enclosing non-library level or compilation unit + -- node which which encapsulates arbitrary node N. Return Empty is no + -- such context is available. + + function In_Nested_Context + (Outer : Node_Id; + Inner : Node_Id) return Boolean; + -- Determine whether arbitrary node Outer encapsulates arbitrary node + -- Inner. + + ---------------------------- + -- Find_Enclosing_Context -- + ---------------------------- + + function Find_Enclosing_Context (N : Node_Id) return Node_Id is + Context : Node_Id; + Par : Node_Id; + + begin + Par := Parent (N); + while Present (Par) loop + + -- A traversal from a subunit continues via the corresponding stub + + if Nkind (Par) = N_Subunit then + Par := Corresponding_Stub (Par); + + -- Stop the traversal when the nearest enclosing non-library level + -- encapsulator has been reached. + + elsif Is_Non_Library_Level_Encapsulator (Par) then + Context := Parent (Par); + + -- The sole exception is when the encapsulator is the unit of + -- compilation because this case requires special processing + -- (see below). + + if Present (Context) + and then Nkind (Context) = N_Compilation_Unit + then + null; + + else + return Par; + end if; + + -- Reaching a compilation unit node without hitting a non-library + -- level encapsulator indicates that N is at the library level in + -- which case the compilation unit is the context. + + elsif Nkind (Par) = N_Compilation_Unit then + return Par; + end if; + + Par := Parent (Par); + end loop; + + return Empty; + end Find_Enclosing_Context; + + ----------------------- + -- In_Nested_Context -- + ----------------------- + + function In_Nested_Context + (Outer : Node_Id; + Inner : Node_Id) return Boolean + is + Par : Node_Id; + + begin + Par := Inner; + while Present (Par) loop + + -- A traversal from a subunit continues via the corresponding stub + + if Nkind (Par) = N_Subunit then + Par := Corresponding_Stub (Par); + + elsif Par = Outer then + return True; + end if; + + Par := Parent (Par); + end loop; + + return False; + end In_Nested_Context; + + -- Local variables + + Context_1 : constant Node_Id := Find_Enclosing_Context (N1); + Context_2 : constant Node_Id := Find_Enclosing_Context (N2); + + -- Start of processing for In_Same_Context + + begin + -- Both nodes appear within the same context + + if Context_1 = Context_2 then + return True; + + -- Both nodes appear in compilation units. Determine whether one unit + -- is the body of the other. + + elsif Nkind (Context_1) = N_Compilation_Unit + and then Nkind (Context_2) = N_Compilation_Unit + then + return + Is_Same_Unit + (Unit_1 => Defining_Entity (Unit (Context_1)), + Unit_2 => Defining_Entity (Unit (Context_2))); + + -- The context of N1 encloses the context of N2 + + elsif Nested_OK and then In_Nested_Context (Context_1, Context_2) then + return True; + end if; + + return False; + end In_Same_Context; + + ---------------- + -- Initialize -- + ---------------- + + procedure Initialize is + begin + -- Set the soft link which enables Atree.Rewrite to update a top level + -- scenario each time it is transformed into another node. + + Set_Rewriting_Proc (Update_Elaboration_Scenario'Access); + end Initialize; + + --------------- + -- Info_Call -- + --------------- + + procedure Info_Call + (Call : Node_Id; + Target_Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean) + is + procedure Info_Accept_Alternative; + pragma Inline (Info_Accept_Alternative); + -- Output information concerning an accept alternative + + procedure Info_Simple_Call; + pragma Inline (Info_Simple_Call); + -- Output information concerning the call + + procedure Info_Type_Actions (Action : String); + pragma Inline (Info_Type_Actions); + -- Output information concerning action Action of a type + + procedure Info_Verification_Call + (Pred : String; + Id : Entity_Id; + Id_Kind : String); + pragma Inline (Info_Verification_Call); + -- Output information concerning the verification of predicate Pred + -- applied to related entity Id with kind Id_Kind. + + ----------------------------- + -- Info_Accept_Alternative -- + ----------------------------- + + procedure Info_Accept_Alternative is + Entry_Id : constant Entity_Id := Receiving_Entry (Target_Id); + + begin + pragma Assert (Present (Entry_Id)); + + Elab_Msg_NE + (Msg => "accept for entry & during elaboration", + N => Call, + Id => Entry_Id, + Info_Msg => Info_Msg, + In_SPARK => In_SPARK); + end Info_Accept_Alternative; + + ---------------------- + -- Info_Simple_Call -- + ---------------------- + + procedure Info_Simple_Call is + begin + Elab_Msg_NE + (Msg => "call to & during elaboration", + N => Call, + Id => Target_Id, + Info_Msg => Info_Msg, + In_SPARK => In_SPARK); + end Info_Simple_Call; + + ----------------------- + -- Info_Type_Actions -- + ----------------------- + + procedure Info_Type_Actions (Action : String) is + Typ : constant Entity_Id := First_Formal_Type (Target_Id); + + begin + pragma Assert (Present (Typ)); + + Elab_Msg_NE + (Msg => Action & " actions for type & during elaboration", + N => Call, + Id => Typ, + Info_Msg => Info_Msg, + In_SPARK => In_SPARK); + end Info_Type_Actions; + + ---------------------------- + -- Info_Verification_Call -- + ---------------------------- + + procedure Info_Verification_Call + (Pred : String; + Id : Entity_Id; + Id_Kind : String) + is + begin + pragma Assert (Present (Id)); + + Elab_Msg_NE + (Msg => + "verification of " & Pred & " of " & Id_Kind & " & during " + & "elaboration", + N => Call, + Id => Id, + Info_Msg => Info_Msg, + In_SPARK => In_SPARK); + end Info_Verification_Call; + + -- Start of processing for Info_Call + + begin + -- Do not output anything for targets defined in internal units because + -- this creates noise. + + if not In_Internal_Unit (Target_Id) then + + -- Accept alternative + + if Is_Accept_Alternative_Proc (Target_Id) then + Info_Accept_Alternative; + + -- Adjustment + + elsif Is_TSS (Target_Id, TSS_Deep_Adjust) then + Info_Type_Actions ("adjustment"); + + -- Default_Initial_Condition + + elsif Is_Default_Initial_Condition_Proc (Target_Id) then + Info_Verification_Call + (Pred => "Default_Initial_Condition", + Id => First_Formal_Type (Target_Id), + Id_Kind => "type"); + + -- Entries + + elsif Is_Protected_Entry (Target_Id) then + Info_Simple_Call; + + -- Task entry calls are never processed because the entry being + -- invoked does not have a corresponding "body", it has a select. + + elsif Is_Task_Entry (Target_Id) then + null; + + -- Finalization + + elsif Is_TSS (Target_Id, TSS_Deep_Finalize) then + Info_Type_Actions ("finalization"); + + -- Calls to _Finalizer procedures must not appear in the output + -- because this creates confusing noise. + + elsif Is_Finalizer_Proc (Target_Id) then + null; + + -- Initial_Condition + + elsif Is_Initial_Condition_Proc (Target_Id) then + Info_Verification_Call + (Pred => "Initial_Condition", + Id => Find_Enclosing_Scope (Call), + Id_Kind => "package"); + + -- Initialization + + elsif Is_Init_Proc (Target_Id) + or else Is_TSS (Target_Id, TSS_Deep_Initialize) + then + Info_Type_Actions ("initialization"); + + -- Invariant + + elsif Is_Invariant_Proc (Target_Id) then + Info_Verification_Call + (Pred => "invariants", + Id => First_Formal_Type (Target_Id), + Id_Kind => "type"); + + -- Partial invariant calls must not appear in the output because this + -- creates confusing noise. + + elsif Is_Partial_Invariant_Proc (Target_Id) then + null; + + -- _Postconditions + + elsif Is_Postconditions_Proc (Target_Id) then + Info_Verification_Call + (Pred => "postconditions", + Id => Find_Enclosing_Scope (Call), + Id_Kind => "subprogram"); + + -- Subprograms must come last because some of the previous cases fall + -- under this category. + + elsif Ekind (Target_Id) = E_Function then + Info_Simple_Call; + + elsif Ekind (Target_Id) = E_Procedure then + Info_Simple_Call; + + else + pragma Assert (False); + null; + end if; + end if; + end Info_Call; + + ------------------------ + -- Info_Instantiation -- + ------------------------ + + procedure Info_Instantiation + (Inst : Node_Id; + Gen_Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean) + is + begin + Elab_Msg_NE + (Msg => "instantiation of & during elaboration", + N => Inst, + Id => Gen_Id, + Info_Msg => Info_Msg, + In_SPARK => In_SPARK); + end Info_Instantiation; + + ------------------------ + -- Info_Variable_Read -- + ------------------------ + + procedure Info_Variable_Read + (Ref : Node_Id; + Var_Id : Entity_Id; + Info_Msg : Boolean; + In_SPARK : Boolean) + is + begin + Elab_Msg_NE + (Msg => "read of variable & during elaboration", + N => Ref, + Id => Var_Id, + Info_Msg => Info_Msg, + In_SPARK => In_SPARK); + end Info_Variable_Read; + + -------------------- + -- Insertion_Node -- + -------------------- + + function Insertion_Node (N : Node_Id; Ins_Nod : Node_Id) return Node_Id is + begin + -- When the scenario denotes an instantiation, the proper insertion node + -- is the instance spec. This ensures that the generic actuals will not + -- be evaluated prior to a potential ABE. + + if Nkind (N) in N_Generic_Instantiation + and then Present (Instance_Spec (N)) + then + return Instance_Spec (N); + + -- Otherwise the proper insertion node is the candidate insertion node + + else + return Ins_Nod; + end if; + end Insertion_Node; + + ----------------------- + -- Install_ABE_Check -- + ----------------------- + + procedure Install_ABE_Check + (N : Node_Id; + Id : Entity_Id; + Ins_Nod : Node_Id) + is + Check_Ins_Nod : constant Node_Id := Insertion_Node (N, Ins_Nod); + -- Insert the check prior to this node + + Loc : constant Source_Ptr := Sloc (N); + Spec_Id : constant Entity_Id := Unique_Entity (Id); + Unit_Id : constant Entity_Id := Find_Top_Unit (Id); + Scop_Id : Entity_Id; + + begin + -- Nothing to do when compiling for GNATprove because raise statements + -- are not supported. + + if GNATprove_Mode then + return; + + -- Nothing to do when the compilation will not produce an executable + + elsif Serious_Errors_Detected > 0 then + return; + + -- Nothing to do for a compilation unit because there is no executable + -- environment at that level. + + elsif Nkind (Parent (Check_Ins_Nod)) = N_Compilation_Unit then + return; + + -- Nothing to do when the unit is elaborated prior to the main unit. + -- This check must also consider the following cases: + + -- * Id's unit appears in the context of the main unit + + -- * Id's unit is subject to pragma Elaborate_Body. An ABE check MUST + -- NOT be generated because Id's unit is always elaborated prior to + -- the main unit. + + -- * Id's unit is the main unit. An ABE check MUST be generated in this + -- case because a conditional ABE may be raised depending on the flow + -- of execution within the main unit (flag Same_Unit_OK is False). + + elsif Has_Prior_Elaboration + (Unit_Id => Unit_Id, + Context_OK => True, + Elab_Body_OK => True) + then + return; + end if; + + -- Prevent multiple scenarios from installing the same ABE check + + Set_Is_Elaboration_Checks_OK_Node (N, False); + + -- Install the nearest enclosing scope of the scenario as there must be + -- something on the scope stack. + + -- Performance note: parent traversal + + Scop_Id := Find_Enclosing_Scope (Check_Ins_Nod); + pragma Assert (Present (Scop_Id)); + + Push_Scope (Scop_Id); + + -- Generate: + -- if not Spec_Id'Elaborated then + -- raise Program_Error with "access before elaboration"; + -- end if; + + Insert_Action (Check_Ins_Nod, + Make_Raise_Program_Error (Loc, + Condition => + Make_Op_Not (Loc, + Right_Opnd => + Make_Attribute_Reference (Loc, + Prefix => New_Occurrence_Of (Spec_Id, Loc), + Attribute_Name => Name_Elaborated)), + Reason => PE_Access_Before_Elaboration)); + + Pop_Scope; + end Install_ABE_Check; + + ----------------------- + -- Install_ABE_Check -- + ----------------------- + + procedure Install_ABE_Check + (N : Node_Id; + Target_Id : Entity_Id; + Target_Decl : Node_Id; + Target_Body : Node_Id; + Ins_Nod : Node_Id) + is + procedure Build_Elaboration_Entity; + pragma Inline (Build_Elaboration_Entity); + -- Create a new elaboration flag for Target_Id, insert it prior to + -- Target_Decl, and set it after Body_Decl. + + ------------------------------ + -- Build_Elaboration_Entity -- + ------------------------------ + + procedure Build_Elaboration_Entity is + Loc : constant Source_Ptr := Sloc (Target_Id); + Flag_Id : Entity_Id; + + begin + -- Create the declaration of the elaboration flag. The name carries a + -- unique counter in case of name overloading. + + Flag_Id := + Make_Defining_Identifier (Loc, + Chars => New_External_Name (Chars (Target_Id), 'E', -1)); + + Set_Elaboration_Entity (Target_Id, Flag_Id); + Set_Elaboration_Entity_Required (Target_Id); + + Push_Scope (Scope (Target_Id)); + + -- Generate: + -- Enn : Short_Integer := 0; + + Insert_Action (Target_Decl, + Make_Object_Declaration (Loc, + Defining_Identifier => Flag_Id, + Object_Definition => + New_Occurrence_Of (Standard_Short_Integer, Loc), + Expression => Make_Integer_Literal (Loc, Uint_0))); + + -- Generate: + -- Enn := 1; + + Set_Elaboration_Flag (Target_Body, Target_Id); + + Pop_Scope; + end Build_Elaboration_Entity; + + -- Local variables + + Target_Unit_Id : constant Entity_Id := Find_Top_Unit (Target_Id); + + -- Start for processing for Install_ABE_Check + + begin + -- Nothing to do when compiling for GNATprove because raise statements + -- are not supported. + + if GNATprove_Mode then + return; + + -- Nothing to do when the compilation will not produce an executable + + elsif Serious_Errors_Detected > 0 then + return; + + -- Nothing to do when the target is a protected subprogram because the + -- check is associated with the protected body subprogram. + + elsif Is_Protected_Subp (Target_Id) then + return; + + -- Nothing to do when the target is elaborated prior to the main unit. + -- This check must also consider the following cases: + + -- * The unit of the target appears in the context of the main unit + + -- * The unit of the target is subject to pragma Elaborate_Body. An ABE + -- check MUST NOT be generated because the unit is always elaborated + -- prior to the main unit. + + -- * The unit of the target is the main unit. An ABE check MUST be added + -- in this case because a conditional ABE may be raised depending on + -- the flow of execution within the main unit (flag Same_Unit_OK is + -- False). + + elsif Has_Prior_Elaboration + (Unit_Id => Target_Unit_Id, + Context_OK => True, + Elab_Body_OK => True) + then + return; + + -- Create an elaboration flag for the target when it does not have one + + elsif No (Elaboration_Entity (Target_Id)) then + Build_Elaboration_Entity; + end if; + + Install_ABE_Check + (N => N, + Ins_Nod => Ins_Nod, + Id => Target_Id); + end Install_ABE_Check; + + ------------------------- + -- Install_ABE_Failure -- + ------------------------- + + procedure Install_ABE_Failure (N : Node_Id; Ins_Nod : Node_Id) is + Fail_Ins_Nod : constant Node_Id := Insertion_Node (N, Ins_Nod); + -- Insert the failure prior to this node + + Loc : constant Source_Ptr := Sloc (N); + Scop_Id : Entity_Id; + + begin + -- Nothing to do when compiling for GNATprove because raise statements + -- are not supported. + + if GNATprove_Mode then + return; + + -- Nothing to do when the compilation will not produce an executable + + elsif Serious_Errors_Detected > 0 then + return; + + -- Do not install an ABE check for a compilation unit because there is + -- no executable environment at that level. + + elsif Nkind (Parent (Fail_Ins_Nod)) = N_Compilation_Unit then + return; + end if; + + -- Prevent multiple scenarios from installing the same ABE failure + + Set_Is_Elaboration_Checks_OK_Node (N, False); + + -- Install the nearest enclosing scope of the scenario as there must be + -- something on the scope stack. + + -- Performance note: parent traversal + + Scop_Id := Find_Enclosing_Scope (Fail_Ins_Nod); + pragma Assert (Present (Scop_Id)); + + Push_Scope (Scop_Id); + + -- Generate: + -- raise Program_Error with "access before elaboration"; + + Insert_Action (Fail_Ins_Nod, + Make_Raise_Program_Error (Loc, + Reason => PE_Access_Before_Elaboration)); + + Pop_Scope; + end Install_ABE_Failure; + + -------------------------------- + -- Is_Accept_Alternative_Proc -- + -------------------------------- + + function Is_Accept_Alternative_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote a procedure with a receiving entry + + return Ekind (Id) = E_Procedure and then Present (Receiving_Entry (Id)); + end Is_Accept_Alternative_Proc; + + ------------------------ + -- Is_Activation_Proc -- + ------------------------ + + function Is_Activation_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote one of the runtime procedures in + -- charge of task activation. + + if Ekind (Id) = E_Procedure then + if Restricted_Profile then + return Is_RTE (Id, RE_Activate_Restricted_Tasks); + else + return Is_RTE (Id, RE_Activate_Tasks); + end if; + end if; + + return False; + end Is_Activation_Proc; + + ---------------------------- + -- Is_Ada_Semantic_Target -- + ---------------------------- + + function Is_Ada_Semantic_Target (Id : Entity_Id) return Boolean is + begin + return + Is_Activation_Proc (Id) + or else Is_Controlled_Proc (Id, Name_Adjust) + or else Is_Controlled_Proc (Id, Name_Finalize) + or else Is_Controlled_Proc (Id, Name_Initialize) + or else Is_Init_Proc (Id) + or else Is_Invariant_Proc (Id) + or else Is_Protected_Entry (Id) + or else Is_Protected_Subp (Id) + or else Is_Protected_Body_Subp (Id) + or else Is_Task_Entry (Id); + end Is_Ada_Semantic_Target; + + ---------------------------- + -- Is_Bodiless_Subprogram -- + ---------------------------- + + function Is_Bodiless_Subprogram (Subp_Id : Entity_Id) return Boolean is + begin + -- An abstract subprogram does not have a body + + if Ekind_In (Subp_Id, E_Function, + E_Operator, + E_Procedure) + and then Is_Abstract_Subprogram (Subp_Id) + then + return True; + + -- A formal subprogram does not have a body + + elsif Is_Formal_Subprogram (Subp_Id) then + return True; + + -- An imported subprogram may have a body, however it is not known at + -- compile or bind time where the body resides and whether it will be + -- elaborated on time. + + elsif Is_Imported (Subp_Id) then + return True; + end if; + + return False; + end Is_Bodiless_Subprogram; + + -------------------------------- + -- Is_Check_Emitting_Scenario -- + -------------------------------- + + function Is_Check_Emitting_Scenario (N : Node_Id) return Boolean is + begin + return + Nkind_In (N, N_Call_Marker, + N_Function_Instantiation, + N_Package_Instantiation, + N_Procedure_Instantiation); + end Is_Check_Emitting_Scenario; + + ------------------------ + -- Is_Controlled_Proc -- + ------------------------ + + function Is_Controlled_Proc + (Subp_Id : Entity_Id; + Subp_Nam : Name_Id) return Boolean + is + Formal_Id : Entity_Id; + + begin + pragma Assert (Nam_In (Subp_Nam, Name_Adjust, + Name_Finalize, + Name_Initialize)); + + -- To qualify, the subprogram must denote a source procedure with name + -- Adjust, Finalize, or Initialize where the sole formal is controlled. + + if Comes_From_Source (Subp_Id) + and then Ekind (Subp_Id) = E_Procedure + and then Chars (Subp_Id) = Subp_Nam + then + Formal_Id := First_Formal (Subp_Id); + + return + Present (Formal_Id) + and then Is_Controlled (Etype (Formal_Id)) + and then No (Next_Formal (Formal_Id)); + end if; + + return False; + end Is_Controlled_Proc; + + --------------------------------------- + -- Is_Default_Initial_Condition_Proc -- + --------------------------------------- + + function Is_Default_Initial_Condition_Proc + (Id : Entity_Id) return Boolean + is + begin + -- To qualify, the entity must denote a Default_Initial_Condition + -- procedure. + + return Ekind (Id) = E_Procedure and then Is_DIC_Procedure (Id); + end Is_Default_Initial_Condition_Proc; + + ----------------------- + -- Is_Finalizer_Proc -- + ----------------------- + + function Is_Finalizer_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote a _Finalizer procedure + + return Ekind (Id) = E_Procedure and then Chars (Id) = Name_uFinalizer; + end Is_Finalizer_Proc; + + ----------------------- + -- Is_Guaranteed_ABE -- + ----------------------- + + function Is_Guaranteed_ABE + (N : Node_Id; + Target_Decl : Node_Id; + Target_Body : Node_Id) return Boolean + is + begin + -- Avoid cascaded errors if there were previous serious infractions. + -- As a result the scenario will not be treated as a guaranteed ABE. + -- This behaviour parallels that of the old ABE mechanism. + + if Serious_Errors_Detected > 0 then + return False; + + -- The scenario and the target appear within the same context ignoring + -- enclosing library levels. + + -- Performance note: parent traversal + + elsif In_Same_Context (N, Target_Decl) then + + -- The target body has already been encountered. The scenario results + -- in a guaranteed ABE if it appears prior to the body. + + if Present (Target_Body) then + return Earlier_In_Extended_Unit (N, Target_Body); + + -- Otherwise the body has not been encountered yet. The scenario is + -- a guaranteed ABE since the body will appear later. It is assumed + -- that the caller has already checked whether the scenario is ABE- + -- safe as optional bodies are not considered here. + + else + return True; + end if; + end if; + + return False; + end Is_Guaranteed_ABE; + + ------------------------------- + -- Is_Initial_Condition_Proc -- + ------------------------------- + + function Is_Initial_Condition_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote an Initial_Condition procedure + + return + Ekind (Id) = E_Procedure and then Is_Initial_Condition_Procedure (Id); + end Is_Initial_Condition_Proc; + + -------------------- + -- Is_Initialized -- + -------------------- + + function Is_Initialized (Obj_Decl : Node_Id) return Boolean is + begin + -- To qualify, the object declaration must have an expression + + return + Present (Expression (Obj_Decl)) or else Has_Init_Expression (Obj_Decl); + end Is_Initialized; + + ----------------------- + -- Is_Invariant_Proc -- + ----------------------- + + function Is_Invariant_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote the "full" invariant procedure + + return Ekind (Id) = E_Procedure and then Is_Invariant_Procedure (Id); + end Is_Invariant_Proc; + + --------------------------------------- + -- Is_Non_Library_Level_Encapsulator -- + --------------------------------------- + + function Is_Non_Library_Level_Encapsulator (N : Node_Id) return Boolean is + begin + case Nkind (N) is + when N_Abstract_Subprogram_Declaration + | N_Aspect_Specification + | N_Component_Declaration + | N_Entry_Body + | N_Entry_Declaration + | N_Expression_Function + | N_Formal_Abstract_Subprogram_Declaration + | N_Formal_Concrete_Subprogram_Declaration + | N_Formal_Object_Declaration + | N_Formal_Package_Declaration + | N_Formal_Type_Declaration + | N_Generic_Association + | N_Implicit_Label_Declaration + | N_Incomplete_Type_Declaration + | N_Private_Extension_Declaration + | N_Private_Type_Declaration + | N_Protected_Body + | N_Protected_Type_Declaration + | N_Single_Protected_Declaration + | N_Single_Task_Declaration + | N_Subprogram_Body + | N_Subprogram_Declaration + | N_Task_Body + | N_Task_Type_Declaration + => + return True; + + when others => + return Is_Generic_Declaration_Or_Body (N); + end case; + end Is_Non_Library_Level_Encapsulator; + + ------------------------------- + -- Is_Partial_Invariant_Proc -- + ------------------------------- + + function Is_Partial_Invariant_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote the "partial" invariant procedure + + return + Ekind (Id) = E_Procedure and then Is_Partial_Invariant_Procedure (Id); + end Is_Partial_Invariant_Proc; + + ---------------------------- + -- Is_Postconditions_Proc -- + ---------------------------- + + function Is_Postconditions_Proc (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote a _Postconditions procedure + + return + Ekind (Id) = E_Procedure and then Chars (Id) = Name_uPostconditions; + end Is_Postconditions_Proc; + + --------------------------- + -- Is_Preelaborated_Unit -- + --------------------------- + + function Is_Preelaborated_Unit (Id : Entity_Id) return Boolean is + begin + return + Is_Preelaborated (Id) + or else Is_Pure (Id) + or else Is_Remote_Call_Interface (Id) + or else Is_Remote_Types (Id) + or else Is_Shared_Passive (Id); + end Is_Preelaborated_Unit; + + ------------------------ + -- Is_Protected_Entry -- + ------------------------ + + function Is_Protected_Entry (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote an entry defined in a protected + -- type. + + return + Is_Entry (Id) + and then Is_Protected_Type (Non_Private_View (Scope (Id))); + end Is_Protected_Entry; + + ----------------------- + -- Is_Protected_Subp -- + ----------------------- + + function Is_Protected_Subp (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote a subprogram defined within a + -- protected type. + + return + Ekind_In (Id, E_Function, E_Procedure) + and then Is_Protected_Type (Non_Private_View (Scope (Id))); + end Is_Protected_Subp; + + ---------------------------- + -- Is_Protected_Body_Subp -- + ---------------------------- + + function Is_Protected_Body_Subp (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote a subprogram with attribute + -- Protected_Subprogram set. + + return + Ekind_In (Id, E_Function, E_Procedure) + and then Present (Protected_Subprogram (Id)); + end Is_Protected_Body_Subp; + + ------------------------ + -- Is_Safe_Activation -- + ------------------------ + + function Is_Safe_Activation + (Call : Node_Id; + Task_Decl : Node_Id) return Boolean + is + begin + -- The activation of a task coming from an external instance cannot + -- cause an ABE because the generic was already instantiated. Note + -- that the instantiation itself may lead to an ABE. + + return + In_External_Instance + (N => Call, + Target_Decl => Task_Decl); + end Is_Safe_Activation; + + ------------------ + -- Is_Safe_Call -- + ------------------ + + function Is_Safe_Call + (Call : Node_Id; + Target_Attrs : Target_Attributes) return Boolean + is + begin + -- The target is either an abstract subprogram, formal subprogram, or + -- imported, in which case it does not have a body at compile or bind + -- time. Assume that the call is ABE-safe. + + if Is_Bodiless_Subprogram (Target_Attrs.Spec_Id) then + return True; + + -- The target is an instantiation of a generic subprogram. The call + -- cannot cause an ABE because the generic was already instantiated. + -- Note that the instantiation itself may lead to an ABE. + + elsif Is_Generic_Instance (Target_Attrs.Spec_Id) then + return True; + + -- The invocation of a target coming from an external instance cannot + -- cause an ABE because the generic was already instantiated. Note that + -- the instantiation itself may lead to an ABE. + + elsif In_External_Instance + (N => Call, + Target_Decl => Target_Attrs.Spec_Decl) + then + return True; + + -- The target is a subprogram body without a previous declaration. The + -- call cannot cause an ABE because the body has already been seen. + + elsif Nkind (Target_Attrs.Spec_Decl) = N_Subprogram_Body + and then No (Corresponding_Spec (Target_Attrs.Spec_Decl)) + then + return True; + + -- The target is a subprogram body stub without a prior declaration. + -- The call cannot cause an ABE because the proper body substitutes + -- the stub. + + elsif Nkind (Target_Attrs.Spec_Decl) = N_Subprogram_Body_Stub + and then No (Corresponding_Spec_Of_Stub (Target_Attrs.Spec_Decl)) + then + return True; + + -- Subprogram bodies which wrap attribute references used as actuals + -- in instantiations are always ABE-safe. These bodies are artifacts + -- of expansion. + + elsif Present (Target_Attrs.Body_Decl) + and then Nkind (Target_Attrs.Body_Decl) = N_Subprogram_Body + and then Was_Attribute_Reference (Target_Attrs.Body_Decl) + then + return True; + end if; + + return False; + end Is_Safe_Call; + + --------------------------- + -- Is_Safe_Instantiation -- + --------------------------- + + function Is_Safe_Instantiation + (Inst : Node_Id; + Gen_Attrs : Target_Attributes) return Boolean + is + begin + -- The generic is an intrinsic subprogram in which case it does not + -- have a body at compile or bind time. Assume that the instantiation + -- is ABE-safe. + + if Is_Bodiless_Subprogram (Gen_Attrs.Spec_Id) then + return True; + + -- The instantiation of an external nested generic cannot cause an ABE + -- if the outer generic was already instantiated. Note that the instance + -- of the outer generic may lead to an ABE. + + elsif In_External_Instance + (N => Inst, + Target_Decl => Gen_Attrs.Spec_Decl) + then + return True; + + -- The generic is a package. The instantiation cannot cause an ABE when + -- the package has no body. + + elsif Ekind (Gen_Attrs.Spec_Id) = E_Generic_Package + and then not Has_Body (Gen_Attrs.Spec_Decl) + then + return True; + end if; + + return False; + end Is_Safe_Instantiation; + + ------------------ + -- Is_Same_Unit -- + ------------------ + + function Is_Same_Unit + (Unit_1 : Entity_Id; + Unit_2 : Entity_Id) return Boolean + is + function Is_Subunit (Unit_Id : Entity_Id) return Boolean; + pragma Inline (Is_Subunit); + -- Determine whether unit Unit_Id is a subunit + + function Normalize_Unit (Unit_Id : Entity_Id) return Entity_Id; + -- Strip a potential subunit chain ending with unit Unit_Id and return + -- the corresponding spec. + + ---------------- + -- Is_Subunit -- + ---------------- + + function Is_Subunit (Unit_Id : Entity_Id) return Boolean is + begin + return Nkind (Parent (Unit_Declaration_Node (Unit_Id))) = N_Subunit; + end Is_Subunit; + + -------------------- + -- Normalize_Unit -- + -------------------- + + function Normalize_Unit (Unit_Id : Entity_Id) return Entity_Id is + Result : Entity_Id; + + begin + -- Eliminate a potential chain of subunits to reach to proper body + + Result := Unit_Id; + while Present (Result) + and then Result /= Standard_Standard + and then Is_Subunit (Result) + loop + Result := Scope (Result); + end loop; + + -- Obtain the entity of the corresponding spec (if any) + + return Unique_Entity (Result); + end Normalize_Unit; + + -- Start of processing for Is_Same_Unit + + begin + return Normalize_Unit (Unit_1) = Normalize_Unit (Unit_2); + end Is_Same_Unit; + + ----------------- + -- Is_Scenario -- + ----------------- + + function Is_Scenario (N : Node_Id) return Boolean is + begin + case Nkind (N) is + when N_Assignment_Statement + | N_Attribute_Reference + | N_Call_Marker + | N_Entry_Call_Statement + | N_Expanded_Name + | N_Function_Call + | N_Function_Instantiation + | N_Identifier + | N_Package_Instantiation + | N_Procedure_Call_Statement + | N_Procedure_Instantiation + | N_Requeue_Statement + => + return True; + + when others => + return False; + end case; + end Is_Scenario; + + ------------------------------ + -- Is_SPARK_Semantic_Target -- + ------------------------------ + + function Is_SPARK_Semantic_Target (Id : Entity_Id) return Boolean is + begin + return + Is_Default_Initial_Condition_Proc (Id) + or else Is_Initial_Condition_Proc (Id); + end Is_SPARK_Semantic_Target; + + ------------------------ + -- Is_Suitable_Access -- + ------------------------ + + function Is_Suitable_Access (N : Node_Id) return Boolean is + Nam : Name_Id; + Pref : Node_Id; + Subp_Id : Entity_Id; + + begin + -- This scenario is relevant only when the static model is in effect + -- because it is graph-dependent and does not involve any run-time + -- checks. Allowing it in the dynamic model would create confusing + -- noise. + + if not Static_Elaboration_Checks then + return False; + + -- Nothing to do when switch -gnatd.U (ignore 'Access) is in effect + + elsif Debug_Flag_Dot_UU then + return False; + + -- Nothing to do when the scenario is not an attribute reference + + elsif Nkind (N) /= N_Attribute_Reference then + return False; + + -- Nothing to do for internally-generated attributes because they are + -- assumed to be ABE safe. + + elsif not Comes_From_Source (N) then + return False; + end if; + + Nam := Attribute_Name (N); + Pref := Prefix (N); + + -- Sanitize the prefix of the attribute + + if not Is_Entity_Name (Pref) then + return False; + + elsif No (Entity (Pref)) then + return False; + end if; + + Subp_Id := Entity (Pref); + + if not Is_Subprogram_Or_Entry (Subp_Id) then + return False; + end if; + + -- Traverse a possible chain of renamings to obtain the original entry + -- or subprogram which the prefix may rename. + + Subp_Id := Get_Renamed_Entity (Subp_Id); + + -- To qualify, the attribute must meet the following prerequisites: + + return + + -- The prefix must denote a source entry, operator, or subprogram + -- which is not imported. + + Comes_From_Source (Subp_Id) + and then Is_Subprogram_Or_Entry (Subp_Id) + and then not Is_Bodiless_Subprogram (Subp_Id) + + -- The attribute name must be one of the 'Access forms. Note that + -- 'Unchecked_Access cannot apply to a subprogram. + + and then Nam_In (Nam, Name_Access, Name_Unrestricted_Access); + end Is_Suitable_Access; + + ---------------------- + -- Is_Suitable_Call -- + ---------------------- + + function Is_Suitable_Call (N : Node_Id) return Boolean is + begin + -- Entry and subprogram calls are intentionally ignored because they + -- may undergo expansion depending on the compilation mode, previous + -- errors, generic context, etc. Call markers play the role of calls + -- and provide a uniform foundation for ABE processing. + + return Nkind (N) = N_Call_Marker; + end Is_Suitable_Call; + + ------------------------------- + -- Is_Suitable_Instantiation -- + ------------------------------- + + function Is_Suitable_Instantiation (N : Node_Id) return Boolean is + Orig_N : constant Node_Id := Original_Node (N); + -- Use the original node in case an instantiation library unit is + -- rewritten as a package or subprogram. + + begin + -- To qualify, the instantiation must come from source + + return + Comes_From_Source (Orig_N) + and then Nkind (Orig_N) in N_Generic_Instantiation; + end Is_Suitable_Instantiation; + + -------------------------- + -- Is_Suitable_Scenario -- + -------------------------- + + function Is_Suitable_Scenario (N : Node_Id) return Boolean is + begin + return + Is_Suitable_Access (N) + or else Is_Suitable_Call (N) + or else Is_Suitable_Instantiation (N) + or else Is_Suitable_Variable_Assignment (N) + or else Is_Suitable_Variable_Read (N); + end Is_Suitable_Scenario; + + ------------------------------------- + -- Is_Suitable_Variable_Assignment -- + ------------------------------------- + + function Is_Suitable_Variable_Assignment (N : Node_Id) return Boolean is + N_Unit : Node_Id; + N_Unit_Id : Entity_Id; + Nam : Node_Id; + Var_Decl : Node_Id; + Var_Id : Entity_Id; + Var_Unit : Node_Id; + Var_Unit_Id : Entity_Id; + + begin + -- This scenario is relevant only when the static model is in effect + -- because it is graph-dependent and does not involve any run-time + -- checks. Allowing it in the dynamic model would create confusing + -- noise. + + if not Static_Elaboration_Checks then + return False; + + -- Nothing to do when the scenario is not an assignment + + elsif Nkind (N) /= N_Assignment_Statement then + return False; + + -- Nothing to do for internally-generated assignments because they are + -- assumed to be ABE safe. + + elsif not Comes_From_Source (N) then + return False; + + -- Assignments are ignored in GNAT mode on the assumption that they are + -- ABE-safe. This behaviour parallels that of the old ABE mechanism. + + elsif GNAT_Mode then + return False; + end if; + + Nam := Extract_Assignment_Name (N); + + -- Sanitize the left hand side of the assignment + + if not Is_Entity_Name (Nam) then + return False; + + elsif No (Entity (Nam)) then + return False; + end if; + + Var_Id := Entity (Nam); + + -- Sanitize the variable + + if Var_Id = Any_Id then + return False; + + elsif Ekind (Var_Id) /= E_Variable then + return False; + end if; + + Var_Decl := Declaration_Node (Var_Id); + + if Nkind (Var_Decl) /= N_Object_Declaration then + return False; + end if; + + N_Unit_Id := Find_Top_Unit (N); + N_Unit := Unit_Declaration_Node (N_Unit_Id); + + Var_Unit_Id := Find_Top_Unit (Var_Decl); + Var_Unit := Unit_Declaration_Node (Var_Unit_Id); + + -- To qualify, the assignment must meet the following prerequisites: + + return + Comes_From_Source (Var_Id) + + -- The variable must be declared in the spec of compilation unit U + + and then Nkind (Var_Unit) = N_Package_Declaration + + -- Performance note: parent traversal + + and then Find_Enclosing_Level (Var_Decl) = Package_Spec + + -- The assignment must occur in the body of compilation unit U + + and then Nkind (N_Unit) = N_Package_Body + and then Present (Corresponding_Body (Var_Unit)) + and then Corresponding_Body (Var_Unit) = N_Unit_Id; + end Is_Suitable_Variable_Assignment; + + ------------------------------- + -- Is_Suitable_Variable_Read -- + ------------------------------- + + function Is_Suitable_Variable_Read (N : Node_Id) return Boolean is + function In_Pragma (Nod : Node_Id) return Boolean; + -- Determine whether arbitrary node Nod appears within a pragma + + function Is_Variable_Read (Ref : Node_Id) return Boolean; + -- Determine whether variable reference Ref constitutes a read + + --------------- + -- In_Pragma -- + --------------- + + function In_Pragma (Nod : Node_Id) return Boolean is + Par : Node_Id; + + begin + Par := Nod; + while Present (Par) loop + if Nkind (Par) = N_Pragma then + return True; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Par := Parent (Par); + end loop; + + return False; + end In_Pragma; + + ---------------------- + -- Is_Variable_Read -- + ---------------------- + + function Is_Variable_Read (Ref : Node_Id) return Boolean is + function Is_Out_Actual (Call : Node_Id) return Boolean; + -- Determine whether the corresponding formal of actual Ref which + -- appears in call Call has mode OUT. + + ------------------- + -- Is_Out_Actual -- + ------------------- + + function Is_Out_Actual (Call : Node_Id) return Boolean is + Actual : Node_Id; + Call_Attrs : Call_Attributes; + Formal : Entity_Id; + Target_Id : Entity_Id; + + begin + Extract_Call_Attributes + (Call => Call, + Target_Id => Target_Id, + Attrs => Call_Attrs); + + -- Inspect the actual and formal parameters, trying to find the + -- corresponding formal for Ref. + + Actual := First_Actual (Call); + Formal := First_Formal (Target_Id); + while Present (Actual) and then Present (Formal) loop + if Actual = Ref then + return Ekind (Formal) = E_Out_Parameter; + end if; + + Next_Actual (Actual); + Next_Formal (Formal); + end loop; + + return False; + end Is_Out_Actual; + + -- Local variables + + Context : constant Node_Id := Parent (Ref); + + -- Start of processing for Is_Variable_Read + + begin + -- The majority of variable references are reads, and they can appear + -- in a great number of contexts. To determine whether a reference is + -- a read, it is more practical to find out whether it is a write. + + -- A reference is a write when it appears immediately on the left- + -- hand side of an assignment. + + if Nkind (Context) = N_Assignment_Statement + and then Name (Context) = Ref + then + return False; + + -- A reference is a write when it acts as an actual in a subprogram + -- call and the corresponding formal has mode OUT. + + elsif Nkind_In (Context, N_Function_Call, + N_Procedure_Call_Statement) + and then Is_Out_Actual (Context) + then + return False; + end if; + + -- Any other reference is a read + + return True; + end Is_Variable_Read; + + -- Local variables + + Prag : Node_Id; + Var_Id : Entity_Id; + + -- Start of processing for Is_Suitable_Variable_Read + + begin + -- This scenario is relevant only when the static model is in effect + -- because it is graph-dependent and does not involve any run-time + -- checks. Allowing it in the dynamic model would create confusing + -- noise. + + if not Static_Elaboration_Checks then + return False; + + -- Attributes and operator sumbols are not considered to be suitable + -- references even though they are part of predicate Is_Entity_Name. + + elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then + return False; + + -- Nothing to do for internally-generated references because they are + -- assumed to be ABE safe. + + elsif not Comes_From_Source (N) then + return False; + end if; + + -- Sanitize the reference + + Var_Id := Entity (N); + + if No (Var_Id) then + return False; + + elsif Var_Id = Any_Id then + return False; + + elsif Ekind (Var_Id) /= E_Variable then + return False; + end if; + + Prag := SPARK_Pragma (Var_Id); + + -- To qualify, the reference must meet the following prerequisites: + + return + Comes_From_Source (Var_Id) + + -- Both the variable and the reference must appear in SPARK_Mode On + -- regions because this scenario falls under the SPARK rules. + + and then Present (Prag) + and then Get_SPARK_Mode_From_Annotation (Prag) = On + and then Is_SPARK_Mode_On_Node (N) + + -- The reference must denote a variable read + + and then Is_Variable_Read (N) + + -- The reference must not be considered when it appears in a pragma. + -- If the pragma has run-time semantics, then the reference will be + -- reconsidered once the pragma is expanded. + + -- Performance note: parent traversal + + and then not In_Pragma (N); + end Is_Suitable_Variable_Read; + + ------------------- + -- Is_Task_Entry -- + ------------------- + + function Is_Task_Entry (Id : Entity_Id) return Boolean is + begin + -- To qualify, the entity must denote an entry defined in a task type + + return + Is_Entry (Id) and then Is_Task_Type (Non_Private_View (Scope (Id))); + end Is_Task_Entry; + + ------------------------ + -- Is_Up_Level_Target -- + ------------------------ + + function Is_Up_Level_Target (Target_Decl : Node_Id) return Boolean is + Root : constant Node_Id := Root_Scenario; + + begin + -- The root appears within the declaratons of a block statement, entry + -- body, subprogram body, or task body ignoring enclosing packages. The + -- root is always within the main unit. An up level target is a notion + -- applicable only to the static model because scenarios are reached by + -- means of graph traversal started from a fixed declarative or library + -- level. + + -- Performance note: parent traversal + + if Static_Elaboration_Checks + and then Find_Enclosing_Level (Root) = Declaration_Level + then + -- The target is within the main unit. It acts as an up level target + -- when it appears within a context which encloses the root. + + -- package body Main_Unit is + -- function Func ...; -- target + + -- procedure Proc is + -- X : ... := Func; -- root scenario + + if In_Extended_Main_Code_Unit (Target_Decl) then + + -- Performance note: parent traversal + + return not In_Same_Context (Root, Target_Decl, Nested_OK => True); + + -- Otherwise the target is external to the main unit which makes it + -- an up level target. + + else + return True; + end if; + end if; + + return False; + end Is_Up_Level_Target; + + ------------------------------- + -- Kill_Elaboration_Scenario -- + ------------------------------- + + procedure Kill_Elaboration_Scenario (N : Node_Id) is + begin + -- Eliminate the scenario by suppressing the generation of conditional + -- ABE checks or guaranteed ABE failures. Note that other diagnostics + -- must be carried out ignoring the fact that the scenario is within + -- dead code. + + if Is_Scenario (N) then + Set_Is_Elaboration_Checks_OK_Node (N, False); + end if; + end Kill_Elaboration_Scenario; + + ---------------------------------- + -- Meet_Elaboration_Requirement -- + ---------------------------------- + + procedure Meet_Elaboration_Requirement + (N : Node_Id; + Target_Id : Entity_Id; + Req_Nam : Name_Id) + is + Main_Id : constant Entity_Id := Cunit_Entity (Main_Unit); + Unit_Id : constant Entity_Id := Find_Top_Unit (Target_Id); + + function Find_Preelaboration_Pragma + (Prag_Nam : Name_Id) return Node_Id; + pragma Inline (Find_Preelaboration_Pragma); + -- Traverse the visible declarations of unit Unit_Id and locate a source + -- preelaboration-related pragma with name Prag_Nam. + + procedure Info_Requirement_Met (Prag : Node_Id); + pragma Inline (Info_Requirement_Met); + -- Output information concerning pragma Prag which meets requirement + -- Req_Nam. + + procedure Info_Scenario; + pragma Inline (Info_Scenario); + -- Output information concerning scenario N + + -------------------------------- + -- Find_Preelaboration_Pragma -- + -------------------------------- + + function Find_Preelaboration_Pragma + (Prag_Nam : Name_Id) return Node_Id + is + Spec : constant Node_Id := Parent (Unit_Id); + Decl : Node_Id; + + begin + -- A preelaboration-related pragma comes from source and appears at + -- the top of the visible declarations of a package. + + if Nkind (Spec) = N_Package_Specification then + Decl := First (Visible_Declarations (Spec)); + while Present (Decl) loop + if Comes_From_Source (Decl) then + if Nkind (Decl) = N_Pragma + and then Pragma_Name (Decl) = Prag_Nam + then + return Decl; + + -- Otherwise the construct terminates the region where the + -- preelabortion-related pragma may appear. + + else + exit; + end if; + end if; + + Next (Decl); + end loop; + end if; + + return Empty; + end Find_Preelaboration_Pragma; + + -------------------------- + -- Info_Requirement_Met -- + -------------------------- + + procedure Info_Requirement_Met (Prag : Node_Id) is + begin + pragma Assert (Present (Prag)); + + Error_Msg_Name_1 := Req_Nam; + Error_Msg_Sloc := Sloc (Prag); + Error_Msg_NE + ("\\% requirement for unit & met by pragma #", N, Unit_Id); + end Info_Requirement_Met; + + ------------------- + -- Info_Scenario -- + ------------------- + + procedure Info_Scenario is + begin + if Is_Suitable_Call (N) then + Info_Call + (Call => N, + Target_Id => Target_Id, + Info_Msg => False, + In_SPARK => True); + + elsif Is_Suitable_Instantiation (N) then + Info_Instantiation + (Inst => N, + Gen_Id => Target_Id, + Info_Msg => False, + In_SPARK => True); + + elsif Is_Suitable_Variable_Read (N) then + Info_Variable_Read + (Ref => N, + Var_Id => Target_Id, + Info_Msg => False, + In_SPARK => True); + + -- No other scenario may impose a requirement on the context of the + -- main unit. + + else + pragma Assert (False); + null; + end if; + end Info_Scenario; + + -- Local variables + + Elab_Attrs : Elaboration_Attributes; + Elab_Nam : Name_Id; + Req_Met : Boolean; + + -- Start of processing for Meet_Elaboration_Requirement + + begin + pragma Assert (Nam_In (Req_Nam, Name_Elaborate, Name_Elaborate_All)); + + -- Assume that the requirement has not been met + + Req_Met := False; + + -- Elaboration requirements are verified only when the static model is + -- in effect because this diagnostic is graph-dependent. + + if not Static_Elaboration_Checks then + return; + + -- If the target is within the main unit, either at the source level or + -- through an instantiation, then there is no real requirement to meet + -- because the main unit cannot force its own elaboration by means of an + -- Elaborate[_All] pragma. Treat this case as valid coverage. + + elsif In_Extended_Main_Code_Unit (Target_Id) then + Req_Met := True; + + -- Otherwise the target resides in an external unit + + -- The requirement is met when the target comes from an internal unit + -- because such a unit is elaborated prior to a non-internal unit. + + elsif In_Internal_Unit (Unit_Id) + and then not In_Internal_Unit (Main_Id) + then + Req_Met := True; + + -- The requirement is met when the target comes from a preelaborated + -- unit. This portion must parallel predicate Is_Preelaborated_Unit. + + elsif Is_Preelaborated_Unit (Unit_Id) then + Req_Met := True; + + -- Output extra information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas. + + if Elab_Info_Messages then + if Is_Preelaborated (Unit_Id) then + Elab_Nam := Name_Preelaborate; + + elsif Is_Pure (Unit_Id) then + Elab_Nam := Name_Pure; + + elsif Is_Remote_Call_Interface (Unit_Id) then + Elab_Nam := Name_Remote_Call_Interface; + + elsif Is_Remote_Types (Unit_Id) then + Elab_Nam := Name_Remote_Types; + + else + pragma Assert (Is_Shared_Passive (Unit_Id)); + Elab_Nam := Name_Shared_Passive; + end if; + + Info_Requirement_Met (Find_Preelaboration_Pragma (Elab_Nam)); + end if; + + -- Determine whether the context of the main unit has a pragma strong + -- enough to meet the requirement. + + else + Elab_Attrs := Elaboration_Context.Get (Unit_Id); + + -- The pragma must be either Elaborate_All or be as strong as the + -- requirement. + + if Present (Elab_Attrs.Source_Pragma) + and then Nam_In (Pragma_Name (Elab_Attrs.Source_Pragma), + Name_Elaborate_All, + Req_Nam) + then + Req_Met := True; + + -- Output extra information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas. + + if Elab_Info_Messages then + Info_Requirement_Met (Elab_Attrs.Source_Pragma); + end if; + end if; + end if; + + -- The requirement was not met by the context of the main unit, issue an + -- error. + + if not Req_Met then + Info_Scenario; + + Error_Msg_Name_1 := Req_Nam; + Error_Msg_Node_2 := Unit_Id; + Error_Msg_NE ("\\unit & requires pragma % for &", N, Main_Id); + + Output_Active_Scenarios (N); + end if; + end Meet_Elaboration_Requirement; + + ---------------------- + -- Non_Private_View -- + ---------------------- + + function Non_Private_View (Typ : Entity_Id) return Entity_Id is + Result : Entity_Id; + + begin + Result := Typ; + + if Is_Private_Type (Result) and then Present (Full_View (Result)) then + Result := Full_View (Result); + end if; + + return Result; + end Non_Private_View; + + ----------------------------- + -- Output_Active_Scenarios -- + ----------------------------- + + procedure Output_Active_Scenarios (Error_Nod : Node_Id) is + procedure Output_Access (N : Node_Id); + -- Emit a specific diagnostic message for 'Access denote by N + + procedure Output_Activation_Call (N : Node_Id); + -- Emit a specific diagnostic message for task activation N + + procedure Output_Call (N : Node_Id; Target_Id : Entity_Id); + -- Emit a specific diagnostic message for call N which invokes target + -- Target_Id. + + procedure Output_Header; + -- Emit a specific diagnostic message for the unit of the root scenario + + procedure Output_Instantiation (N : Node_Id); + -- Emit a specific diagnostic message for instantiation N + + procedure Output_Variable_Assignment (N : Node_Id); + -- Emit a specific diagnostic message for assignment statement N + + procedure Output_Variable_Read (N : Node_Id); + -- Emit a specific diagnostic message for reference N which reads a + -- variable. + + ------------------- + -- Output_Access -- + ------------------- + + procedure Output_Access (N : Node_Id) is + Subp_Id : constant Entity_Id := Entity (Prefix (N)); + + begin + Error_Msg_Name_1 := Attribute_Name (N); + Error_Msg_Sloc := Sloc (N); + Error_Msg_NE ("\\ % of & taken #", Error_Nod, Subp_Id); + end Output_Access; + + ---------------------------- + -- Output_Activation_Call -- + ---------------------------- + + procedure Output_Activation_Call (N : Node_Id) is + function Find_Activator (Call : Node_Id) return Entity_Id; + -- Find the nearest enclosing construct which houses call Call + + -------------------- + -- Find_Activator -- + -------------------- + + function Find_Activator (Call : Node_Id) return Entity_Id is + Par : Node_Id; + + begin + -- Climb the parent chain looking for a package [body] or a + -- construct with a statement sequence. + + Par := Parent (Call); + while Present (Par) loop + if Nkind_In (Par, N_Package_Body, N_Package_Declaration) then + return Defining_Entity (Par); + + elsif Nkind (Par) = N_Handled_Sequence_Of_Statements then + return Defining_Entity (Parent (Par)); + end if; + + Par := Parent (Par); + end loop; + + return Empty; + end Find_Activator; + + -- Local variables + + Activator : constant Entity_Id := Find_Activator (N); + + -- Start of processing for Output_Activation_Call + + begin + pragma Assert (Present (Activator)); + + Error_Msg_NE ("\\ local tasks of & activated", Error_Nod, Activator); + end Output_Activation_Call; + + ----------------- + -- Output_Call -- + ----------------- + + procedure Output_Call (N : Node_Id; Target_Id : Entity_Id) is + procedure Output_Accept_Alternative; + pragma Inline (Output_Accept_Alternative); + -- Emit a specific diagnostic message concerning an accept + -- alternative. + + procedure Output_Call (Kind : String); + pragma Inline (Output_Call); + -- Emit a specific diagnostic message concerning a call of kind Kind + + procedure Output_Type_Actions (Action : String); + pragma Inline (Output_Type_Actions); + -- Emit a specific diagnostic message concerning action Action of a + -- type. + + procedure Output_Verification_Call + (Pred : String; + Id : Entity_Id; + Id_Kind : String); + pragma Inline (Output_Verification_Call); + -- Emit a specific diagnostic message concerning the verification of + -- predicate Pred applied to related entity Id with kind Id_Kind. + + ------------------------------- + -- Output_Accept_Alternative -- + ------------------------------- + + procedure Output_Accept_Alternative is + Entry_Id : constant Entity_Id := Receiving_Entry (Target_Id); + + begin + pragma Assert (Present (Entry_Id)); + + Error_Msg_NE ("\\ entry & selected #", Error_Nod, Entry_Id); + end Output_Accept_Alternative; + + ----------------- + -- Output_Call -- + ----------------- + + procedure Output_Call (Kind : String) is + begin + Error_Msg_NE ("\\ " & Kind & " & called #", Error_Nod, Target_Id); + end Output_Call; + + ------------------------- + -- Output_Type_Actions -- + ------------------------- + + procedure Output_Type_Actions (Action : String) is + Typ : constant Entity_Id := First_Formal_Type (Target_Id); + + begin + pragma Assert (Present (Typ)); + + Error_Msg_NE + ("\\ " & Action & " actions for type & #", Error_Nod, Typ); + end Output_Type_Actions; + + ------------------------------ + -- Output_Verification_Call -- + ------------------------------ + + procedure Output_Verification_Call + (Pred : String; + Id : Entity_Id; + Id_Kind : String) + is + begin + pragma Assert (Present (Id)); + + Error_Msg_NE + ("\\ " & Pred & " of " & Id_Kind & " & verified #", + Error_Nod, Id); + end Output_Verification_Call; + + -- Start of processing for Output_Call + + begin + Error_Msg_Sloc := Sloc (N); + + -- Accept alternative + + if Is_Accept_Alternative_Proc (Target_Id) then + Output_Accept_Alternative; + + -- Adjustment + + elsif Is_TSS (Target_Id, TSS_Deep_Adjust) then + Output_Type_Actions ("adjustment"); + + -- Default_Initial_Condition + + elsif Is_Default_Initial_Condition_Proc (Target_Id) then + Output_Verification_Call + (Pred => "Default_Initial_Condition", + Id => First_Formal_Type (Target_Id), + Id_Kind => "type"); + + -- Entries + + elsif Is_Protected_Entry (Target_Id) then + Output_Call ("entry"); + + -- Task entry calls are never processed because the entry being + -- invoked does not have a corresponding "body", it has a select. A + -- task entry call appears in the stack of active scenarios for the + -- sole purpose of checking No_Entry_Calls_In_Elaboration_Code and + -- nothing more. + + elsif Is_Task_Entry (Target_Id) then + null; + + -- Finalization + + elsif Is_TSS (Target_Id, TSS_Deep_Finalize) then + Output_Type_Actions ("finalization"); + + -- Calls to _Finalizer procedures must not appear in the output + -- because this creates confusing noise. + + elsif Is_Finalizer_Proc (Target_Id) then + null; + + -- Initial_Condition + + elsif Is_Initial_Condition_Proc (Target_Id) then + Output_Verification_Call + (Pred => "Initial_Condition", + Id => Find_Enclosing_Scope (N), + Id_Kind => "package"); + + -- Initialization + + elsif Is_Init_Proc (Target_Id) + or else Is_TSS (Target_Id, TSS_Deep_Initialize) + then + Output_Type_Actions ("initialization"); + + -- Invariant + + elsif Is_Invariant_Proc (Target_Id) then + Output_Verification_Call + (Pred => "invariants", + Id => First_Formal_Type (Target_Id), + Id_Kind => "type"); + + -- Partial invariant calls must not appear in the output because this + -- creates confusing noise. Note that a partial invariant is always + -- invoked by the "full" invariant which is already placed on the + -- stack. + + elsif Is_Partial_Invariant_Proc (Target_Id) then + null; + + -- _Postconditions + + elsif Is_Postconditions_Proc (Target_Id) then + Output_Verification_Call + (Pred => "postconditions", + Id => Find_Enclosing_Scope (N), + Id_Kind => "subprogram"); + + -- Subprograms must come last because some of the previous cases fall + -- under this category. + + elsif Ekind (Target_Id) = E_Function then + Output_Call ("function"); + + elsif Ekind (Target_Id) = E_Procedure then + Output_Call ("procedure"); + + else + pragma Assert (False); + null; + end if; + end Output_Call; + + ------------------- + -- Output_Header -- + ------------------- + + procedure Output_Header is + Unit_Id : constant Entity_Id := Find_Top_Unit (Root_Scenario); + + begin + if Ekind (Unit_Id) = E_Package then + Error_Msg_NE ("\\ spec of unit & elaborated", Error_Nod, Unit_Id); + + elsif Ekind (Unit_Id) = E_Package_Body then + Error_Msg_NE ("\\ body of unit & elaborated", Error_Nod, Unit_Id); + + else + Error_Msg_NE ("\\ in body of unit &", Error_Nod, Unit_Id); + end if; + end Output_Header; + + -------------------------- + -- Output_Instantiation -- + -------------------------- + + procedure Output_Instantiation (N : Node_Id) is + procedure Output_Instantiation (Gen_Id : Entity_Id; Kind : String); + pragma Inline (Output_Instantiation); + -- Emit a specific diagnostic message concerning an instantiation of + -- generic unit Gen_Id. Kind denotes the kind of the instantiation. + + -------------------------- + -- Output_Instantiation -- + -------------------------- + + procedure Output_Instantiation (Gen_Id : Entity_Id; Kind : String) is + begin + Error_Msg_NE + ("\\ " & Kind & " & instantiated as & #", Error_Nod, Gen_Id); + end Output_Instantiation; + + -- Local variables + + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Inst_Id : Entity_Id; + Gen_Id : Entity_Id; + + -- Start of processing for Output_Instantiation + + begin + Extract_Instantiation_Attributes + (Exp_Inst => N, + Inst => Inst, + Inst_Id => Inst_Id, + Gen_Id => Gen_Id, + Attrs => Inst_Attrs); + + Error_Msg_Node_2 := Inst_Id; + Error_Msg_Sloc := Sloc (Inst); + + if Nkind (Inst) = N_Function_Instantiation then + Output_Instantiation (Gen_Id, "function"); + + elsif Nkind (Inst) = N_Package_Instantiation then + Output_Instantiation (Gen_Id, "package"); + + elsif Nkind (Inst) = N_Procedure_Instantiation then + Output_Instantiation (Gen_Id, "procedure"); + + else + pragma Assert (False); + null; + end if; + end Output_Instantiation; + + -------------------------------- + -- Output_Variable_Assignment -- + -------------------------------- + + procedure Output_Variable_Assignment (N : Node_Id) is + Var_Id : constant Entity_Id := Entity (Extract_Assignment_Name (N)); + + begin + Error_Msg_Sloc := Sloc (N); + Error_Msg_NE ("\\ variable & assigned #", Error_Nod, Var_Id); + end Output_Variable_Assignment; + + -------------------------- + -- Output_Variable_Read -- + -------------------------- + + procedure Output_Variable_Read (N : Node_Id) is + Dummy : Variable_Attributes; + Var_Id : Entity_Id; + + begin + Extract_Variable_Reference_Attributes + (Ref => N, + Var_Id => Var_Id, + Attrs => Dummy); + + Error_Msg_Sloc := Sloc (N); + Error_Msg_NE ("\\ variable & read #", Error_Nod, Var_Id); + end Output_Variable_Read; + + -- Local variables + + package Stack renames Scenario_Stack; + + Dummy : Call_Attributes; + N : Node_Id; + Posted : Boolean; + Target_Id : Entity_Id; + + -- Start of processing for Output_Active_Scenarios + + begin + -- Active scenarios are emitted only when the static model is in effect + -- because there is an inherent order by which all these scenarios were + -- reached from the declaration or library level. + + if not Static_Elaboration_Checks then + return; + end if; + + Posted := False; + + for Index in Stack.First .. Stack.Last loop + N := Stack.Table (Index); + + if not Posted then + Posted := True; + Output_Header; + end if; + + -- 'Access + + if Nkind (N) = N_Attribute_Reference then + Output_Access (N); + + -- Calls + + elsif Is_Suitable_Call (N) then + Extract_Call_Attributes + (Call => N, + Target_Id => Target_Id, + Attrs => Dummy); + + if Is_Activation_Proc (Target_Id) then + Output_Activation_Call (N); + else + Output_Call (N, Target_Id); + end if; + + -- Instantiations + + elsif Is_Suitable_Instantiation (N) then + Output_Instantiation (N); + + -- Variable assignments + + elsif Nkind (N) = N_Assignment_Statement then + Output_Variable_Assignment (N); + + -- Variable read + + elsif Is_Suitable_Variable_Read (N) then + Output_Variable_Read (N); + + else + pragma Assert (False); + null; + end if; + end loop; + end Output_Active_Scenarios; + + ------------------------- + -- Pop_Active_Scenario -- + ------------------------- + + procedure Pop_Active_Scenario (N : Node_Id) is + Top : Node_Id renames Scenario_Stack.Table (Scenario_Stack.Last); + + begin + pragma Assert (Top = N); + Scenario_Stack.Decrement_Last; + end Pop_Active_Scenario; + + -------------------- + -- Process_Access -- + -------------------- + + procedure Process_Access (Attr : Node_Id; In_Task_Body : Boolean) is + function Build_Access_Marker (Target_Id : Entity_Id) return Node_Id; + pragma Inline (Build_Access_Marker); + -- Create a suitable call marker which invokes target Target_Id + + ------------------------- + -- Build_Access_Marker -- + ------------------------- + + function Build_Access_Marker (Target_Id : Entity_Id) return Node_Id is + Marker : Node_Id; + + begin + Marker := Make_Call_Marker (Sloc (Attr)); + + -- Inherit relevant attributes from the attribute + + -- Performance note: parent traversal + + Set_Target (Marker, Target_Id); + Set_Is_Declaration_Level_Node + (Marker, Find_Enclosing_Level (Attr) = Declaration_Level); + Set_Is_Dispatching_Call + (Marker, False); + Set_Is_Elaboration_Checks_OK_Node + (Marker, Is_Elaboration_Checks_OK_Node (Attr)); + Set_Is_Source_Call + (Marker, Comes_From_Source (Attr)); + Set_Is_SPARK_Mode_On_Node + (Marker, Is_SPARK_Mode_On_Node (Attr)); + + -- Partially insert the call marker into the tree by setting its + -- parent pointer. + + Set_Parent (Marker, Attr); + + return Marker; + end Build_Access_Marker; + + -- Local variables + + Root : constant Node_Id := Root_Scenario; + Target_Id : constant Entity_Id := Entity (Prefix (Attr)); + + Target_Attrs : Target_Attributes; + + -- Start of processing for Process_Access + + begin + -- Output relevant information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas) is in effect. + + if Elab_Info_Messages then + Error_Msg_NE + ("info: access to & during elaboration", Attr, Target_Id); + end if; + + Extract_Target_Attributes + (Target_Id => Target_Id, + Attrs => Target_Attrs); + + -- Both the attribute and the corresponding body are in the same unit. + -- The corresponding body must appear prior to the root scenario which + -- started the recursive search. If this is not the case, then there is + -- a potential ABE if the access value is used to call the subprogram. + -- Emit a warning only when switch -gnatw.f (warnings on suspucious + -- 'Access) is in effect. + + if Warn_On_Elab_Access + and then Present (Target_Attrs.Body_Decl) + and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl) + and then Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl) + then + Error_Msg_Name_1 := Attribute_Name (Attr); + Error_Msg_NE ("??% attribute of & before body seen", Attr, Target_Id); + Error_Msg_N ("\possible Program_Error on later references", Attr); + + Output_Active_Scenarios (Attr); + end if; + + -- Treat the attribute as an immediate invocation of the target when + -- switch -gnatd.o (conservative elaboration order for indirect calls) + -- is in effect. Note that the prior elaboration of the unit containing + -- the target is ensured processing the corresponding call marker. + + if Debug_Flag_Dot_O then + Process_Scenario + (N => Build_Access_Marker (Target_Id), + In_Task_Body => In_Task_Body); + + -- Otherwise ensure that the unit with the corresponding body is + -- elaborated prior to the main unit. + + else + Ensure_Prior_Elaboration + (N => Attr, + Unit_Id => Target_Attrs.Unit_Id, + In_Task_Body => In_Task_Body); + end if; + end Process_Access; + + ----------------------------- + -- Process_Activation_Call -- + ----------------------------- + + procedure Process_Activation_Call + (Call : Node_Id; + Call_Attrs : Call_Attributes; + In_Task_Body : Boolean) + is + procedure Process_Task_Object (Obj_Id : Entity_Id; Typ : Entity_Id); + -- Perform ABE checks and diagnostics for object Obj_Id with type Typ. + -- Typ may be a task type or a composite type with at least one task + -- component. + + procedure Process_Task_Objects (List : List_Id); + -- Perform ABE checks and diagnostics for all task objects found in + -- the list List. + + ------------------------- + -- Process_Task_Object -- + ------------------------- + + procedure Process_Task_Object (Obj_Id : Entity_Id; Typ : Entity_Id) is + Base_Typ : constant Entity_Id := Base_Type (Typ); + + Comp_Id : Entity_Id; + Task_Attrs : Task_Attributes; + + begin + if Is_Task_Type (Typ) then + Extract_Task_Attributes + (Typ => Base_Typ, + Attrs => Task_Attrs); + + Process_Single_Activation + (Call => Call, + Call_Attrs => Call_Attrs, + Obj_Id => Obj_Id, + Task_Attrs => Task_Attrs, + In_Task_Body => In_Task_Body); + + -- Examine the component type when the object is an array + + elsif Is_Array_Type (Typ) and then Has_Task (Base_Typ) then + Process_Task_Object (Obj_Id, Component_Type (Typ)); + + -- Examine individual component types when the object is a record + + elsif Is_Record_Type (Typ) and then Has_Task (Base_Typ) then + Comp_Id := First_Component (Typ); + while Present (Comp_Id) loop + Process_Task_Object (Obj_Id, Etype (Comp_Id)); + Next_Component (Comp_Id); + end loop; + end if; + end Process_Task_Object; + + -------------------------- + -- Process_Task_Objects -- + -------------------------- + + procedure Process_Task_Objects (List : List_Id) is + Item : Node_Id; + Item_Id : Entity_Id; + Item_Typ : Entity_Id; + + begin + -- Examine the contents of the list looking for an object declaration + -- of a task type or one that contains a task within. + + Item := First (List); + while Present (Item) loop + if Nkind (Item) = N_Object_Declaration then + Item_Id := Defining_Entity (Item); + Item_Typ := Etype (Item_Id); + + if Has_Task (Item_Typ) then + Process_Task_Object (Item_Id, Item_Typ); + end if; + end if; + + Next (Item); + end loop; + end Process_Task_Objects; + + -- Local variables + + Context : Node_Id; + Spec : Node_Id; + + -- Start of processing for Process_Activation_Call + + begin + -- Nothing to do when the activation is a guaranteed ABE + + if Is_Known_Guaranteed_ABE (Call) then + return; + end if; + + -- Find the proper context of the activation call where all task objects + -- being activated are declared. This is usually the immediate parent of + -- the call. + + Context := Parent (Call); + + -- In the case of package bodies, the activation call is in the handled + -- sequence of statements, but the task objects are in the declaration + -- list of the body. + + if Nkind (Context) = N_Handled_Sequence_Of_Statements + and then Nkind (Parent (Context)) = N_Package_Body + then + Context := Parent (Context); + end if; + + -- Process all task objects defined in both the spec and body when the + -- activation call precedes the "begin" of a package body. + + if Nkind (Context) = N_Package_Body then + Spec := + Specification + (Unit_Declaration_Node (Corresponding_Spec (Context))); + + Process_Task_Objects (Visible_Declarations (Spec)); + Process_Task_Objects (Private_Declarations (Spec)); + Process_Task_Objects (Declarations (Context)); + + -- Process all task objects defined in the spec when the activation call + -- appears at the end of a package spec. + + elsif Nkind (Context) = N_Package_Specification then + Process_Task_Objects (Visible_Declarations (Context)); + Process_Task_Objects (Private_Declarations (Context)); + + -- Otherwise the context of the activation is some construct with a + -- declarative part. Note that the corresponding record type of a task + -- type is controlled. Because of this, the finalization machinery must + -- relocate the task object to the handled statements of the construct + -- to perform proper finalization in case of an exception. Examine the + -- statements of the construct rather than the declarations. + + else + pragma Assert (Nkind (Context) = N_Handled_Sequence_Of_Statements); + + Process_Task_Objects (Statements (Context)); + end if; + end Process_Activation_Call; + + --------------------------------------------- + -- Process_Activation_Conditional_ABE_Impl -- + --------------------------------------------- + + procedure Process_Activation_Conditional_ABE_Impl + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Obj_Id : Entity_Id; + Task_Attrs : Task_Attributes; + In_Task_Body : Boolean) + is + Check_OK : constant Boolean := + not Is_Ignored_Ghost_Entity (Obj_Id) + and then not Task_Attrs.Ghost_Mode_Ignore + and then Is_Elaboration_Checks_OK_Id (Obj_Id) + and then Task_Attrs.Elab_Checks_OK; + -- A run-time ABE check may be installed only when the object and the + -- task type have active elaboration checks, and both are not ignored + -- Ghost constructs. + + Root : constant Node_Id := Root_Scenario; + + begin + -- Output relevant information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas) is in effect. + + if Elab_Info_Messages then + Error_Msg_NE + ("info: activation of & during elaboration", Call, Obj_Id); + end if; + + -- Nothing to do when the activation is a guaranteed ABE + + if Is_Known_Guaranteed_ABE (Call) then + return; + + -- Nothing to do when the root scenario appears at the declaration + -- level and the task is in the same unit, but outside this context. + + -- task type Task_Typ; -- task declaration + + -- procedure Proc is + -- function A ... is + -- begin + -- if Some_Condition then + -- declare + -- T : Task_Typ; + -- begin + -- <activation call> -- activation site + -- end; + -- ... + -- end A; + + -- X : ... := A; -- root scenario + -- ... + + -- task body Task_Typ is + -- ... + -- end Task_Typ; + + -- In the example above, the context of X is the declarative list of + -- Proc. The "elaboration" of X may reach the activation of T whose body + -- is defined outside of X's context. The task body is relevant only + -- when Proc is invoked, but this happens only in "normal" elaboration, + -- therefore the task body must not be considered if this is not the + -- case. + + -- Performance note: parent traversal + + elsif Is_Up_Level_Target (Task_Attrs.Task_Decl) then + return; + + -- Nothing to do when the activation is ABE-safe + + -- generic + -- package Gen is + -- task type Task_Typ; + -- end Gen; + + -- package body Gen is + -- task body Task_Typ is + -- begin + -- ... + -- end Task_Typ; + -- end Gen; + + -- with Gen; + -- procedure Main is + -- package Nested is + -- ... + -- end Nested; + + -- package body Nested is + -- package Inst is new Gen; + -- T : Inst.Task_Typ; + -- [begin] + -- <activation call> -- safe activation + -- end Nested; + -- ... + + elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then + + -- Note that the task body must still be examined for any nested + -- scenarios. + + null; + + -- The activation call and the task body are both in the main unit + + elsif Present (Task_Attrs.Body_Decl) + and then In_Extended_Main_Code_Unit (Task_Attrs.Body_Decl) + then + -- If the root scenario appears prior to the task body, then this is + -- a possible ABE with respect to the root scenario. + + -- task type Task_Typ; + + -- function A ... is + -- begin + -- if Some_Condition then + -- declare + -- package Pack is + -- ... + -- end Pack; + + -- package body Pack is + -- T : Task_Typ; + -- [begin] + -- <activation call> -- activation of T + -- end Pack; + -- ... + -- end A; + + -- X : ... := A; -- root scenario + + -- task body Task_Typ is -- task body + -- ... + -- end Task_Typ; + + -- Y : ... := A; -- root scenario + + -- IMPORTANT: The activation of T is a possible ABE for X, but + -- not for Y. Intalling an unconditional ABE raise prior to the + -- activation call would be wrong as it will fail for Y as well + -- but in Y's case the activation of T is never an ABE. + + if Earlier_In_Extended_Unit (Root, Task_Attrs.Body_Decl) then + + -- ABE diagnostics are emitted only in the static model because + -- there is a well-defined order to visiting scenarios. Without + -- this order diagnostics appear jumbled and result in unwanted + -- noise. + + if Static_Elaboration_Checks then + Error_Msg_Sloc := Sloc (Call); + Error_Msg_N + ("??task & will be activated # before elaboration of its " + & "body", Obj_Id); + Error_Msg_N + ("\Program_Error may be raised at run time", Obj_Id); + + Output_Active_Scenarios (Obj_Id); + end if; + + -- Install a conditional run-time ABE check to verify that the + -- task body has been elaborated prior to the activation call. + + if Check_OK then + Install_ABE_Check + (N => Call, + Ins_Nod => Call, + Target_Id => Task_Attrs.Spec_Id, + Target_Decl => Task_Attrs.Task_Decl, + Target_Body => Task_Attrs.Body_Decl); + end if; + end if; + + -- Otherwise the task body is not available in this compilation or it + -- resides in an external unit. Install a run-time ABE check to verify + -- that the task body has been elaborated prior to the activation call + -- when the dynamic model is in effect. + + elsif Dynamic_Elaboration_Checks and then Check_OK then + Install_ABE_Check + (N => Call, + Ins_Nod => Call, + Id => Task_Attrs.Unit_Id); + end if; + + -- Both the activation call and task type are subject to SPARK_Mode + -- On, this triggers the SPARK rules for task activation. Compared to + -- calls and instantiations, task activation in SPARK does not require + -- the presence of Elaborate[_All] pragmas in case the task type is + -- defined outside the main unit. This is because SPARK utilizes a + -- special policy which activates all tasks after the main unit has + -- finished its elaboration. + + if Call_Attrs.SPARK_Mode_On and Task_Attrs.SPARK_Mode_On then + null; + + -- Otherwise the Ada rules are in effect. Ensure that the unit with the + -- task body is elaborated prior to the main unit. + + else + Ensure_Prior_Elaboration + (N => Call, + Unit_Id => Task_Attrs.Unit_Id, + In_Task_Body => In_Task_Body); + end if; + + Traverse_Body (Task_Attrs.Body_Decl, In_Task_Body => True); + end Process_Activation_Conditional_ABE_Impl; + + procedure Process_Activation_Conditional_ABE is + new Process_Activation_Call (Process_Activation_Conditional_ABE_Impl); + + -------------------------------------------- + -- Process_Activation_Guaranteed_ABE_Impl -- + -------------------------------------------- + + procedure Process_Activation_Guaranteed_ABE_Impl + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Obj_Id : Entity_Id; + Task_Attrs : Task_Attributes; + In_Task_Body : Boolean) + is + pragma Unreferenced (Call_Attrs); + pragma Unreferenced (In_Task_Body); + + Check_OK : constant Boolean := + not Is_Ignored_Ghost_Entity (Obj_Id) + and then not Task_Attrs.Ghost_Mode_Ignore + and then Is_Elaboration_Checks_OK_Id (Obj_Id) + and then Task_Attrs.Elab_Checks_OK; + -- A run-time ABE check may be installed only when the object and the + -- task type have active elaboration checks, and both are not ignored + -- Ghost constructs. + + begin + -- Nothing to do when the root scenario appears at the declaration + -- level and the task is in the same unit, but outside this context. + + -- task type Task_Typ; -- task declaration + + -- procedure Proc is + -- function A ... is + -- begin + -- if Some_Condition then + -- declare + -- T : Task_Typ; + -- begin + -- <activation call> -- activation site + -- end; + -- ... + -- end A; + + -- X : ... := A; -- root scenario + -- ... + + -- task body Task_Typ is + -- ... + -- end Task_Typ; + + -- In the example above, the context of X is the declarative list of + -- Proc. The "elaboration" of X may reach the activation of T whose body + -- is defined outside of X's context. The task body is relevant only + -- when Proc is invoked, but this happens only in "normal" elaboration, + -- therefore the task body must not be considered if this is not the + -- case. + + -- Performance note: parent traversal + + if Is_Up_Level_Target (Task_Attrs.Task_Decl) then + return; + + -- Nothing to do when the activation is ABE-safe + + -- generic + -- package Gen is + -- task type Task_Typ; + -- end Gen; + + -- package body Gen is + -- task body Task_Typ is + -- begin + -- ... + -- end Task_Typ; + -- end Gen; + + -- with Gen; + -- procedure Main is + -- package Nested is + -- ... + -- end Nested; + + -- package body Nested is + -- package Inst is new Gen; + -- T : Inst.Task_Typ; + -- [begin] + -- <activation call> -- safe activation + -- end Nested; + -- ... + + elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then + return; + + -- An activation call leads to a guaranteed ABE when the activation + -- call and the task appear within the same context ignoring library + -- levels, and the body of the task has not been seen yet or appears + -- after the activation call. + + -- procedure Guaranteed_ABE is + -- task type Task_Typ; + + -- package Nested is + -- ... + -- end Nested; + + -- package body Nested is + -- T : Task_Typ; + -- [begin] + -- <activation call> -- guaranteed ABE + -- end Nested; + + -- task body Task_Typ is + -- ... + -- end Task_Typ; + -- ... + + -- Performance note: parent traversal + + elsif Is_Guaranteed_ABE + (N => Call, + Target_Decl => Task_Attrs.Task_Decl, + Target_Body => Task_Attrs.Body_Decl) + then + Error_Msg_Sloc := Sloc (Call); + Error_Msg_N + ("??task & will be activated # before elaboration of its body", + Obj_Id); + Error_Msg_N ("\Program_Error will be raised at run time", Obj_Id); + + -- Mark the activation call as a guaranteed ABE + + Set_Is_Known_Guaranteed_ABE (Call); + + -- Install a run-time ABE failue because this activation call will + -- always result in an ABE. + + if Check_OK then + Install_ABE_Failure + (N => Call, + Ins_Nod => Call); + end if; + end if; + end Process_Activation_Guaranteed_ABE_Impl; + + procedure Process_Activation_Guaranteed_ABE is + new Process_Activation_Call (Process_Activation_Guaranteed_ABE_Impl); + + ------------------ + -- Process_Call -- + ------------------ + + procedure Process_Call + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + In_Task_Body : Boolean) + is + SPARK_Rules_On : Boolean; + Target_Attrs : Target_Attributes; + + begin + Extract_Target_Attributes + (Target_Id => Target_Id, + Attrs => Target_Attrs); + + -- The SPARK rules are in effect when both the call and target are + -- subject to SPARK_Mode On. + + SPARK_Rules_On := + Call_Attrs.SPARK_Mode_On and Target_Attrs.SPARK_Mode_On; + + -- Output relevant information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas) is in effect. + + if Elab_Info_Messages then + Info_Call + (Call => Call, + Target_Id => Target_Id, + Info_Msg => True, + In_SPARK => SPARK_Rules_On); + end if; + + -- Check whether the invocation of an entry clashes with an existing + -- restriction. + + if Is_Protected_Entry (Target_Id) then + Check_Restriction (No_Entry_Calls_In_Elaboration_Code, Call); + + elsif Is_Task_Entry (Target_Id) then + Check_Restriction (No_Entry_Calls_In_Elaboration_Code, Call); + + -- Task entry calls are never processed because the entry being + -- invoked does not have a corresponding "body", it has a select. + + return; + end if; + + -- Nothing to do when the call is a guaranteed ABE + + if Is_Known_Guaranteed_ABE (Call) then + return; + + -- Nothing to do when the root scenario appears at the declaration level + -- and the target is in the same unit, but outside this context. + + -- function B ...; -- target declaration + + -- procedure Proc is + -- function A ... is + -- begin + -- if Some_Condition then + -- return B; -- call site + -- ... + -- end A; + + -- X : ... := A; -- root scenario + -- ... + + -- function B ... is + -- ... + -- end B; + + -- In the example above, the context of X is the declarative region of + -- Proc. The "elaboration" of X may eventually reach B which is defined + -- outside of X's context. B is relevant only when Proc is invoked, but + -- this happens only by means of "normal" elaboration, therefore B must + -- not be considered if this is not the case. + + -- Performance note: parent traversal + + elsif Is_Up_Level_Target (Target_Attrs.Spec_Decl) then + return; + + -- The SPARK rules are verified only when -gnatd.v (enforce SPARK + -- elaboration rules in SPARK code) is in effect. + + elsif SPARK_Rules_On and Debug_Flag_Dot_V then + Process_Call_SPARK + (Call => Call, + Call_Attrs => Call_Attrs, + Target_Id => Target_Id, + Target_Attrs => Target_Attrs); + + -- Otherwise the Ada rules are in effect, or SPARK code is allowed to + -- violate the SPARK rules. + + else + Process_Call_Ada + (Call => Call, + Call_Attrs => Call_Attrs, + Target_Id => Target_Id, + Target_Attrs => Target_Attrs, + In_Task_Body => In_Task_Body); + end if; + + -- Inspect the target body (and barried function) for other suitable + -- elaboration scenarios. + + Traverse_Body (Target_Attrs.Body_Barf, In_Task_Body); + Traverse_Body (Target_Attrs.Body_Decl, In_Task_Body); + end Process_Call; + + ---------------------- + -- Process_Call_Ada -- + ---------------------- + + procedure Process_Call_Ada + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + Target_Attrs : Target_Attributes; + In_Task_Body : Boolean) + is + function In_Initialization_Context (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N appears within a type init proc or + -- primitive [Deep_]Initialize. + + ------------------------------- + -- In_Initialization_Context -- + ------------------------------- + + function In_Initialization_Context (N : Node_Id) return Boolean is + Par : Node_Id; + Spec_Id : Entity_Id; + + begin + -- Climb the parent chain looking for initialization actions + + Par := Parent (N); + while Present (Par) loop + + -- A block may be part of the initialization actions of a default + -- initialized object. + + if Nkind (Par) = N_Block_Statement + and then Is_Initialization_Block (Par) + then + return True; + + -- A subprogram body may denote an initialization routine + + elsif Nkind (Par) = N_Subprogram_Body then + Spec_Id := Unique_Defining_Entity (Par); + + -- The current subprogram body denotes a type init proc or + -- primitive [Deep_]Initialize. + + if Is_Init_Proc (Spec_Id) + or else Is_Controlled_Proc (Spec_Id, Name_Initialize) + or else Is_TSS (Spec_Id, TSS_Deep_Initialize) + then + return True; + end if; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Par := Parent (Par); + end loop; + + return False; + end In_Initialization_Context; + + -- Local variables + + Check_OK : constant Boolean := + not Call_Attrs.Ghost_Mode_Ignore + and then not Target_Attrs.Ghost_Mode_Ignore + and then Call_Attrs.Elab_Checks_OK + and then Target_Attrs.Elab_Checks_OK; + -- A run-time ABE check may be installed only when both the call and the + -- target have active elaboration checks, and both are not ignored Ghost + -- constructs. + + -- Start of processing for Process_Call_Ada + + begin + -- Nothing to do for an Ada dispatching call because there are no ABE + -- diagnostics for either models. ABE checks for the dynamic model are + -- handled by Install_Primitive_Elaboration_Check. + + if Call_Attrs.Is_Dispatching then + return; + + -- Nothing to do when the call is ABE-safe + + -- generic + -- function Gen ...; + + -- function Gen ... is + -- begin + -- ... + -- end Gen; + + -- with Gen; + -- procedure Main is + -- function Inst is new Gen; + -- X : ... := Inst; -- safe call + -- ... + + elsif Is_Safe_Call (Call, Target_Attrs) then + return; + + -- The call and the target body are both in the main unit + + elsif Present (Target_Attrs.Body_Decl) + and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl) + then + Process_Call_Conditional_ABE + (Call => Call, + Call_Attrs => Call_Attrs, + Target_Id => Target_Id, + Target_Attrs => Target_Attrs); + + -- Otherwise the target body is not available in this compilation or it + -- resides in an external unit. Install a run-time ABE check to verify + -- that the target body has been elaborated prior to the call site when + -- the dynamic model is in effect. + + elsif Dynamic_Elaboration_Checks and then Check_OK then + Install_ABE_Check + (N => Call, + Ins_Nod => Call, + Id => Target_Attrs.Unit_Id); + end if; + + -- No implicit pragma Elaborate[_All] is generated when the call has + -- elaboration checks suppressed. This behaviour parallels that of the + -- old ABE mechanism. + + if not Call_Attrs.Elab_Checks_OK then + null; + + -- No implicit pragma Elaborate[_All] is generated for finalization + -- actions when primitive [Deep_]Finalize is not defined in the main + -- unit and the call appears within some initialization actions. This + -- behaviour parallels that of the old ABE mechanism. + + -- Performance note: parent traversal + + elsif (Is_Controlled_Proc (Target_Id, Name_Finalize) + or else Is_TSS (Target_Id, TSS_Deep_Finalize)) + and then not In_Extended_Main_Code_Unit (Target_Attrs.Spec_Decl) + and then In_Initialization_Context (Call) + then + null; + + -- Otherwise ensure that the unit with the target body is elaborated + -- prior to the main unit. + + else + Ensure_Prior_Elaboration + (N => Call, + Unit_Id => Target_Attrs.Unit_Id, + In_Task_Body => In_Task_Body); + end if; + end Process_Call_Ada; + + ---------------------------------- + -- Process_Call_Conditional_ABE -- + ---------------------------------- + + procedure Process_Call_Conditional_ABE + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + Target_Attrs : Target_Attributes) + is + Check_OK : constant Boolean := + not Call_Attrs.Ghost_Mode_Ignore + and then not Target_Attrs.Ghost_Mode_Ignore + and then Call_Attrs.Elab_Checks_OK + and then Target_Attrs.Elab_Checks_OK; + -- A run-time ABE check may be installed only when both the call and the + -- target have active elaboration checks, and both are not ignored Ghost + -- constructs. + + Root : constant Node_Id := Root_Scenario; + + begin + -- If the root scenario appears prior to the target body, then this is a + -- possible ABE with respect to the root scenario. + + -- function B ...; + + -- function A ... is + -- begin + -- if Some_Condition then + -- return B; -- call site + -- ... + -- end A; + + -- X : ... := A; -- root scenario + + -- function B ... is -- target body + -- ... + -- end B; + + -- Y : ... := A; -- root scenario + + -- IMPORTANT: The call to B from A is a possible ABE for X, but not for + -- Y. Installing an unconditional ABE raise prior to the call to B would + -- be wrong as it will fail for Y as well, but in Y's case the call to B + -- is never an ABE. + + if Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl) then + + -- ABE diagnostics are emitted only in the static model because there + -- is a well-defined order to visiting scenarios. Without this order + -- diagnostics appear jumbled and result in unwanted noise. + + if Static_Elaboration_Checks then + Error_Msg_NE ("??cannot call & before body seen", Call, Target_Id); + Error_Msg_N ("\Program_Error may be raised at run time", Call); + + Output_Active_Scenarios (Call); + end if; + + -- Install a conditional run-time ABE check to verify that the target + -- body has been elaborated prior to the call. + + if Check_OK then + Install_ABE_Check + (N => Call, + Ins_Nod => Call, + Target_Id => Target_Attrs.Spec_Id, + Target_Decl => Target_Attrs.Spec_Decl, + Target_Body => Target_Attrs.Body_Decl); + end if; + end if; + end Process_Call_Conditional_ABE; + + --------------------------------- + -- Process_Call_Guaranteed_ABE -- + --------------------------------- + + procedure Process_Call_Guaranteed_ABE + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id) + is + Target_Attrs : Target_Attributes; + + begin + Extract_Target_Attributes + (Target_Id => Target_Id, + Attrs => Target_Attrs); + + -- Nothing to do when the root scenario appears at the declaration level + -- and the target is in the same unit, but outside this context. + + -- function B ...; -- target declaration + + -- procedure Proc is + -- function A ... is + -- begin + -- if Some_Condition then + -- return B; -- call site + -- ... + -- end A; + + -- X : ... := A; -- root scenario + -- ... + + -- function B ... is + -- ... + -- end B; + + -- In the example above, the context of X is the declarative region of + -- Proc. The "elaboration" of X may eventually reach B which is defined + -- outside of X's context. B is relevant only when Proc is invoked, but + -- this happens only by means of "normal" elaboration, therefore B must + -- not be considered if this is not the case. + + -- Performance note: parent traversal + + if Is_Up_Level_Target (Target_Attrs.Spec_Decl) then + return; + + -- Nothing to do when the call is ABE-safe + + -- generic + -- function Gen ...; + + -- function Gen ... is + -- begin + -- ... + -- end Gen; + + -- with Gen; + -- procedure Main is + -- function Inst is new Gen; + -- X : ... := Inst; -- safe call + -- ... + + elsif Is_Safe_Call (Call, Target_Attrs) then + return; + + -- A call leads to a guaranteed ABE when the call and the target appear + -- within the same context ignoring library levels, and the body of the + -- target has not been seen yet or appears after the call. + + -- procedure Guaranteed_ABE is + -- function Func ...; + + -- package Nested is + -- Obj : ... := Func; -- guaranteed ABE + -- end Nested; + + -- function Func ... is + -- ... + -- end Func; + -- ... + + -- Performance note: parent traversal + + elsif Is_Guaranteed_ABE + (N => Call, + Target_Decl => Target_Attrs.Spec_Decl, + Target_Body => Target_Attrs.Body_Decl) + then + Error_Msg_NE ("??cannot call & before body seen", Call, Target_Id); + Error_Msg_N ("\Program_Error will be raised at run time", Call); + + -- Mark the call as a guarnateed ABE + + Set_Is_Known_Guaranteed_ABE (Call); + + -- Install a run-time ABE failure because the call will always result + -- in an ABE. The failure is installed when both the call and target + -- have enabled elaboration checks, and both are not ignored Ghost + -- constructs. + + if Call_Attrs.Elab_Checks_OK + and then Target_Attrs.Elab_Checks_OK + and then not Call_Attrs.Ghost_Mode_Ignore + and then not Target_Attrs.Ghost_Mode_Ignore + then + Install_ABE_Failure + (N => Call, + Ins_Nod => Call); + end if; + end if; + end Process_Call_Guaranteed_ABE; + + ------------------------ + -- Process_Call_SPARK -- + ------------------------ + + procedure Process_Call_SPARK + (Call : Node_Id; + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + Target_Attrs : Target_Attributes) + is + begin + -- A call to a source target or to a target which emulates Ada or SPARK + -- semantics imposes an Elaborate_All requirement on the context of the + -- main unit. Determine whether the context has a pragma strong enough + -- to meet the requirement. The check is orthogonal to the ABE effects + -- of the call. + + if Target_Attrs.From_Source + or else Is_Ada_Semantic_Target (Target_Id) + or else Is_SPARK_Semantic_Target (Target_Id) + then + Meet_Elaboration_Requirement + (N => Call, + Target_Id => Target_Id, + Req_Nam => Name_Elaborate_All); + end if; + + -- Nothing to do when the call is ABE-safe + + -- generic + -- function Gen ...; + + -- function Gen ... is + -- begin + -- ... + -- end Gen; + + -- with Gen; + -- procedure Main is + -- function Inst is new Gen; + -- X : ... := Inst; -- safe call + -- ... + + if Is_Safe_Call (Call, Target_Attrs) then + return; + + -- The call and the target body are both in the main unit + + elsif Present (Target_Attrs.Body_Decl) + and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl) + then + Process_Call_Conditional_ABE + (Call => Call, + Call_Attrs => Call_Attrs, + Target_Id => Target_Id, + Target_Attrs => Target_Attrs); + + -- Otherwise the target body is not available in this compilation or it + -- resides in an external unit. There is no need to guarantee the prior + -- elaboration of the unit with the target body because either the main + -- unit meets the Elaborate_All requirement imposed by the call, or the + -- program is illegal. + + else + null; + end if; + end Process_Call_SPARK; + + ---------------------------- + -- Process_Guaranteed_ABE -- + ---------------------------- + + procedure Process_Guaranteed_ABE (N : Node_Id) is + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + + begin + -- Add the current scenario to the stack of active scenarios + + Push_Active_Scenario (N); + + -- Only calls, instantiations, and task activations may result in a + -- guaranteed ABE. + + if Is_Suitable_Call (N) then + Extract_Call_Attributes + (Call => N, + Target_Id => Target_Id, + Attrs => Call_Attrs); + + if Is_Activation_Proc (Target_Id) then + Process_Activation_Guaranteed_ABE + (Call => N, + Call_Attrs => Call_Attrs, + In_Task_Body => False); + + else + Process_Call_Guaranteed_ABE + (Call => N, + Call_Attrs => Call_Attrs, + Target_Id => Target_Id); + end if; + + elsif Is_Suitable_Instantiation (N) then + Process_Instantiation_Guaranteed_ABE (N); + end if; + + -- Remove the current scenario from the stack of active scenarios once + -- all ABE diagnostics and checks have been performed. + + Pop_Active_Scenario (N); + end Process_Guaranteed_ABE; + + --------------------------- + -- Process_Instantiation -- + --------------------------- + + procedure Process_Instantiation + (Exp_Inst : Node_Id; + In_Task_Body : Boolean) + is + Gen_Attrs : Target_Attributes; + Gen_Id : Entity_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Inst_Id : Entity_Id; + + SPARK_Rules_On : Boolean; + -- This flag is set when the SPARK rules are in effect + + begin + Extract_Instantiation_Attributes + (Exp_Inst => Exp_Inst, + Inst => Inst, + Inst_Id => Inst_Id, + Gen_Id => Gen_Id, + Attrs => Inst_Attrs); + + Extract_Target_Attributes (Gen_Id, Gen_Attrs); + + -- The SPARK rules are in effect when both the instantiation and generic + -- are subject to SPARK_Mode On. + + SPARK_Rules_On := Inst_Attrs.SPARK_Mode_On and Gen_Attrs.SPARK_Mode_On; + + -- Output relevant information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas) is in effect. + + if Elab_Info_Messages then + Info_Instantiation + (Inst => Inst, + Gen_Id => Gen_Id, + Info_Msg => True, + In_SPARK => SPARK_Rules_On); + end if; + + -- Nothing to do when the instantiation is a guaranteed ABE + + if Is_Known_Guaranteed_ABE (Inst) then + return; + + -- Nothing to do when the root scenario appears at the declaration level + -- and the generic is in the same unit, but outside this context. + + -- generic + -- procedure Gen is ...; -- generic declaration + + -- procedure Proc is + -- function A ... is + -- begin + -- if Some_Condition then + -- declare + -- procedure I is new Gen; -- instantiation site + -- ... + -- ... + -- end A; + + -- X : ... := A; -- root scenario + -- ... + + -- procedure Gen is + -- ... + -- end Gen; + + -- In the example above, the context of X is the declarative region of + -- Proc. The "elaboration" of X may eventually reach Gen which appears + -- outside of X's context. Gen is relevant only when Proc is invoked, + -- but this happens only by means of "normal" elaboration, therefore + -- Gen must not be considered if this is not the case. + + -- Performance note: parent traversal + + elsif Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then + return; + + -- The SPARK rules are verified only when -gnatd.v (enforce SPARK + -- elaboration rules in SPARK code) is in effect. + + elsif SPARK_Rules_On and Debug_Flag_Dot_V then + Process_Instantiation_SPARK + (Exp_Inst => Exp_Inst, + Inst => Inst, + Inst_Attrs => Inst_Attrs, + Gen_Id => Gen_Id, + Gen_Attrs => Gen_Attrs); + + -- Otherwise the Ada rules are in effect, or SPARK code is allowed to + -- violate the SPARK rules. + + else + Process_Instantiation_Ada + (Exp_Inst => Exp_Inst, + Inst => Inst, + Inst_Attrs => Inst_Attrs, + Gen_Id => Gen_Id, + Gen_Attrs => Gen_Attrs, + In_Task_Body => In_Task_Body); + end if; + end Process_Instantiation; + + ------------------------------- + -- Process_Instantiation_Ada -- + ------------------------------- + + procedure Process_Instantiation_Ada + (Exp_Inst : Node_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Gen_Id : Entity_Id; + Gen_Attrs : Target_Attributes; + In_Task_Body : Boolean) + is + Check_OK : constant Boolean := + not Inst_Attrs.Ghost_Mode_Ignore + and then not Gen_Attrs.Ghost_Mode_Ignore + and then Inst_Attrs.Elab_Checks_OK + and then Gen_Attrs.Elab_Checks_OK; + -- A run-time ABE check may be installed only when both the instance and + -- the generic have active elaboration checks and both are not ignored + -- Ghost constructs. + + begin + -- Nothing to do when the instantiation is ABE-safe + + -- generic + -- package Gen is + -- ... + -- end Gen; + + -- package body Gen is + -- ... + -- end Gen; + + -- with Gen; + -- procedure Main is + -- package Inst is new Gen (ABE); -- safe instantiation + -- ... + + if Is_Safe_Instantiation (Inst, Gen_Attrs) then + return; + + -- The instantiation and the generic body are both in the main unit + + elsif Present (Gen_Attrs.Body_Decl) + and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl) + then + Process_Instantiation_Conditional_ABE + (Exp_Inst => Exp_Inst, + Inst => Inst, + Inst_Attrs => Inst_Attrs, + Gen_Id => Gen_Id, + Gen_Attrs => Gen_Attrs); + + -- Otherwise the generic body is not available in this compilation or it + -- resides in an external unit. Install a run-time ABE check to verify + -- that the generic body has been elaborated prior to the instantiation + -- when the dynamic model is in effect. + + elsif Dynamic_Elaboration_Checks and then Check_OK then + Install_ABE_Check + (N => Inst, + Ins_Nod => Exp_Inst, + Id => Gen_Attrs.Unit_Id); + end if; + + -- Ensure that the unit with the generic body is elaborated prior to + -- the main unit. No implicit pragma Elaborate[_All] is generated if + -- the instantiation has elaboration checks suppressed. This behaviour + -- parallels that of the old ABE mechanism. + + if Inst_Attrs.Elab_Checks_OK then + Ensure_Prior_Elaboration + (N => Inst, + Unit_Id => Gen_Attrs.Unit_Id, + In_Task_Body => In_Task_Body); + end if; + end Process_Instantiation_Ada; + + ------------------------------------------- + -- Process_Instantiation_Conditional_ABE -- + ------------------------------------------- + + procedure Process_Instantiation_Conditional_ABE + (Exp_Inst : Node_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Gen_Id : Entity_Id; + Gen_Attrs : Target_Attributes) + is + Check_OK : constant Boolean := + not Inst_Attrs.Ghost_Mode_Ignore + and then not Gen_Attrs.Ghost_Mode_Ignore + and then Inst_Attrs.Elab_Checks_OK + and then Gen_Attrs.Elab_Checks_OK; + -- A run-time ABE check may be installed only when both the instance and + -- the generic have active elaboration checks and both are not ignored + -- Ghost constructs. + + Root : constant Node_Id := Root_Scenario; + + begin + -- If the root scenario appears prior to the generic body, then this is + -- a possible ABE with respect to the root scenario. + + -- generic + -- package Gen is + -- ... + -- end Gen; + + -- function A ... is + -- begin + -- if Some_Condition then + -- declare + -- package Inst is new Gen; -- instantiation site + -- ... + -- end A; + + -- X : ... := A; -- root scenario + + -- package body Gen is -- generic body + -- ... + -- end Gen; + + -- Y : ... := A; -- root scenario + + -- IMPORTANT: The instantiation of Gen is a possible ABE for X, but not + -- for Y. Installing an unconditional ABE raise prior to the instance + -- site would be wrong as it will fail for Y as well, but in Y's case + -- the instantiation of Gen is never an ABE. + + if Earlier_In_Extended_Unit (Root, Gen_Attrs.Body_Decl) then + + -- ABE diagnostics are emitted only in the static model because there + -- is a well-defined order to visiting scenarios. Without this order + -- diagnostics appear jumbled and result in unwanted noise. + + if Static_Elaboration_Checks then + Error_Msg_NE + ("??cannot instantiate & before body seen", Inst, Gen_Id); + Error_Msg_N ("\Program_Error may be raised at run time", Inst); + + Output_Active_Scenarios (Inst); + end if; + + -- Install a conditional run-time ABE check to verify that the + -- generic body has been elaborated prior to the instantiation. + + if Check_OK then + Install_ABE_Check + (N => Inst, + Ins_Nod => Exp_Inst, + Target_Id => Gen_Attrs.Spec_Id, + Target_Decl => Gen_Attrs.Spec_Decl, + Target_Body => Gen_Attrs.Body_Decl); + end if; + end if; + end Process_Instantiation_Conditional_ABE; + + ------------------------------------------ + -- Process_Instantiation_Guaranteed_ABE -- + ------------------------------------------ + + procedure Process_Instantiation_Guaranteed_ABE (Exp_Inst : Node_Id) is + Gen_Attrs : Target_Attributes; + Gen_Id : Entity_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Inst_Id : Entity_Id; + + begin + Extract_Instantiation_Attributes + (Exp_Inst => Exp_Inst, + Inst => Inst, + Inst_Id => Inst_Id, + Gen_Id => Gen_Id, + Attrs => Inst_Attrs); + + Extract_Target_Attributes (Gen_Id, Gen_Attrs); + + -- Nothing to do when the root scenario appears at the declaration level + -- and the generic is in the same unit, but outside this context. + + -- generic + -- procedure Gen is ...; -- generic declaration + + -- procedure Proc is + -- function A ... is + -- begin + -- if Some_Condition then + -- declare + -- procedure I is new Gen; -- instantiation site + -- ... + -- ... + -- end A; + + -- X : ... := A; -- root scenario + -- ... + + -- procedure Gen is + -- ... + -- end Gen; + + -- In the example above, the context of X is the declarative region of + -- Proc. The "elaboration" of X may eventually reach Gen which appears + -- outside of X's context. Gen is relevant only when Proc is invoked, + -- but this happens only by means of "normal" elaboration, therefore + -- Gen must not be considered if this is not the case. + + -- Performance note: parent traversal + + if Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then + return; + + -- Nothing to do when the instantiation is ABE-safe + + -- generic + -- package Gen is + -- ... + -- end Gen; + + -- package body Gen is + -- ... + -- end Gen; + + -- with Gen; + -- procedure Main is + -- package Inst is new Gen (ABE); -- safe instantiation + -- ... + + elsif Is_Safe_Instantiation (Inst, Gen_Attrs) then + return; + + -- An instantiation leads to a guaranteed ABE when the instantiation and + -- the generic appear within the same context ignoring library levels, + -- and the body of the generic has not been seen yet or appears after + -- the instantiation. + + -- procedure Guaranteed_ABE is + -- generic + -- procedure Gen; + + -- package Nested is + -- procedure Inst is new Gen; -- guaranteed ABE + -- end Nested; + + -- procedure Gen is + -- ... + -- end Gen; + -- ... + + -- Performance note: parent traversal + + elsif Is_Guaranteed_ABE + (N => Inst, + Target_Decl => Gen_Attrs.Spec_Decl, + Target_Body => Gen_Attrs.Body_Decl) + then + Error_Msg_NE + ("??cannot instantiate & before body seen", Inst, Gen_Id); + Error_Msg_N ("\Program_Error will be raised at run time", Inst); + + -- Mark the instantiation as a guarantee ABE. This automatically + -- suppresses the instantiation of the generic body. + + Set_Is_Known_Guaranteed_ABE (Inst); + + -- Install a run-time ABE failure because the instantiation will + -- always result in an ABE. The failure is installed when both the + -- instance and the generic have enabled elaboration checks, and both + -- are not ignored Ghost constructs. + + if Inst_Attrs.Elab_Checks_OK + and then Gen_Attrs.Elab_Checks_OK + and then not Inst_Attrs.Ghost_Mode_Ignore + and then not Gen_Attrs.Ghost_Mode_Ignore + then + Install_ABE_Failure + (N => Inst, + Ins_Nod => Exp_Inst); + end if; + end if; + end Process_Instantiation_Guaranteed_ABE; + + --------------------------------- + -- Process_Instantiation_SPARK -- + --------------------------------- + + procedure Process_Instantiation_SPARK + (Exp_Inst : Node_Id; + Inst : Node_Id; + Inst_Attrs : Instantiation_Attributes; + Gen_Id : Entity_Id; + Gen_Attrs : Target_Attributes) + is + Req_Nam : Name_Id; + + begin + -- A source instantiation imposes an Elaborate[_All] requirement on the + -- context of the main unit. Determine whether the context has a pragma + -- strong enough to meet the requirement. The check is orthogonal to the + -- ABE ramifications of the instantiation. + + if Nkind (Inst) = N_Package_Instantiation then + Req_Nam := Name_Elaborate_All; + else + Req_Nam := Name_Elaborate; + end if; + + Meet_Elaboration_Requirement + (N => Inst, + Target_Id => Gen_Id, + Req_Nam => Req_Nam); + + -- Nothing to do when the instantiation is ABE-safe + + -- generic + -- package Gen is + -- ... + -- end Gen; + + -- package body Gen is + -- ... + -- end Gen; + + -- with Gen; + -- procedure Main is + -- package Inst is new Gen (ABE); -- safe instantiation + -- ... + + if Is_Safe_Instantiation (Inst, Gen_Attrs) then + return; + + -- The instantiation and the generic body are both in the main unit + + elsif Present (Gen_Attrs.Body_Decl) + and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl) + then + Process_Instantiation_Conditional_ABE + (Exp_Inst => Exp_Inst, + Inst => Inst, + Inst_Attrs => Inst_Attrs, + Gen_Id => Gen_Id, + Gen_Attrs => Gen_Attrs); + + -- Otherwise the generic body is not available in this compilation or + -- it resides in an external unit. There is no need to guarantee the + -- prior elaboration of the unit with the generic body because either + -- the main unit meets the Elaborate[_All] requirement imposed by the + -- instantiation, or the program is illegal. + + else + null; + end if; + end Process_Instantiation_SPARK; + + --------------------------------- + -- Process_Variable_Assignment -- + --------------------------------- + + procedure Process_Variable_Assignment (Asmt : Node_Id) is + Var_Id : constant Entity_Id := Entity (Extract_Assignment_Name (Asmt)); + Prag : constant Node_Id := SPARK_Pragma (Var_Id); + + SPARK_Rules_On : Boolean; + -- This flag is set when the SPARK rules are in effect + + begin + -- The SPARK rules are in effect when both the assignment and the + -- variable are subject to SPARK_Mode On. + + SPARK_Rules_On := + Present (Prag) + and then Get_SPARK_Mode_From_Annotation (Prag) = On + and then Is_SPARK_Mode_On_Node (Asmt); + + -- Output relevant information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas) is in effect. + + if Elab_Info_Messages then + Elab_Msg_NE + (Msg => "assignment to & during elaboration", + N => Asmt, + Id => Var_Id, + Info_Msg => True, + In_SPARK => SPARK_Rules_On); + end if; + + -- The SPARK rules are in effect. These rules are applied regardless of + -- whether -gnatd.v (enforce SPARK elaboration rules in SPARK code) is + -- in effect because the static model cannot ensure safe assignment of + -- variables. + + if SPARK_Rules_On then + Process_Variable_Assignment_SPARK + (Asmt => Asmt, + Var_Id => Var_Id); + + -- Otherwise the Ada rules are in effect + + else + Process_Variable_Assignment_Ada + (Asmt => Asmt, + Var_Id => Var_Id); + end if; + end Process_Variable_Assignment; + + ------------------------------------- + -- Process_Variable_Assignment_Ada -- + ------------------------------------- + + procedure Process_Variable_Assignment_Ada + (Asmt : Node_Id; + Var_Id : Entity_Id) + is + Var_Decl : constant Node_Id := Declaration_Node (Var_Id); + Spec_Id : constant Entity_Id := Find_Top_Unit (Var_Decl); + + begin + -- Emit a warning when an uninitialized variable declared in a package + -- spec without a pragma Elaborate_Body is initialized by elaboration + -- code within the corresponding body. + + if not Warnings_Off (Var_Id) + and then not Is_Initialized (Var_Decl) + and then not Has_Pragma_Elaborate_Body (Spec_Id) + then + -- Generate an implicit Elaborate_Body in the spec + + Set_Elaborate_Body_Desirable (Spec_Id); + + Error_Msg_NE + ("??variable & can be accessed by clients before this " + & "initialization", Asmt, Var_Id); + + Error_Msg_NE + ("\add pragma ""Elaborate_Body"" to spec & to ensure proper " + & "initialization", Asmt, Spec_Id); + + Output_Active_Scenarios (Asmt); + end if; + end Process_Variable_Assignment_Ada; + + --------------------------------------- + -- Process_Variable_Assignment_SPARK -- + --------------------------------------- + + procedure Process_Variable_Assignment_SPARK + (Asmt : Node_Id; + Var_Id : Entity_Id) + is + Var_Decl : constant Node_Id := Declaration_Node (Var_Id); + Spec_Id : constant Entity_Id := Find_Top_Unit (Var_Decl); + + begin + -- Emit an error when an initialized variable declared in a package spec + -- without pragma Elaborate_Body is further modified by elaboration code + -- within the corresponding body. + + if Is_Initialized (Var_Decl) + and then not Has_Pragma_Elaborate_Body (Spec_Id) + then + Error_Msg_NE + ("variable & modified by elaboration code in package body", + Asmt, Var_Id); + + Error_Msg_NE + ("\add pragma ""Elaborate_Body"" to spec & to ensure full " + & "initialization", Asmt, Spec_Id); + + Output_Active_Scenarios (Asmt); + end if; + end Process_Variable_Assignment_SPARK; + + --------------------------- + -- Process_Variable_Read -- + --------------------------- + + procedure Process_Variable_Read (Ref : Node_Id) is + Var_Attrs : Variable_Attributes; + Var_Id : Entity_Id; + + begin + Extract_Variable_Reference_Attributes + (Ref => Ref, + Var_Id => Var_Id, + Attrs => Var_Attrs); + + -- Output relevant information when switch -gnatel (info messages on + -- implicit Elaborate[_All] pragmas) is in effect. + + if Elab_Info_Messages then + Elab_Msg_NE + (Msg => "read of variable & during elaboration", + N => Ref, + Id => Var_Id, + Info_Msg => True, + In_SPARK => True); + end if; + + -- Nothing to do when the variable appears within the main unit because + -- diagnostics on reads are relevant only for external variables. + + if Is_Same_Unit (Var_Attrs.Unit_Id, Cunit_Entity (Main_Unit)) then + null; + + -- Nothing to do when the variable is already initialized. Note that the + -- variable may be further modified by the external unit. + + elsif Is_Initialized (Declaration_Node (Var_Id)) then + null; + + -- Nothing to do when the external unit guarantees the initialization of + -- the variable by means of pragma Elaborate_Body. + + elsif Has_Pragma_Elaborate_Body (Var_Attrs.Unit_Id) then + null; + + -- A variable read imposes an Elaborate requirement on the context of + -- the main unit. Determine whether the context has a pragma strong + -- enough to meet the requirement. + + else + Meet_Elaboration_Requirement + (N => Ref, + Target_Id => Var_Id, + Req_Nam => Name_Elaborate); + end if; + end Process_Variable_Read; + + -------------------------- + -- Push_Active_Scenario -- + -------------------------- + + procedure Push_Active_Scenario (N : Node_Id) is + begin + Scenario_Stack.Append (N); + end Push_Active_Scenario; + + ---------------------- + -- Process_Scenario -- + ---------------------- + + procedure Process_Scenario (N : Node_Id; In_Task_Body : Boolean := False) is + Call_Attrs : Call_Attributes; + Target_Id : Entity_Id; + + begin + -- Add the current scenario to the stack of active scenarios + + Push_Active_Scenario (N); + + -- 'Access + + if Is_Suitable_Access (N) then + Process_Access (N, In_Task_Body); + + -- Calls + + elsif Is_Suitable_Call (N) then + + -- In general, only calls found within the main unit are processed + -- because the ALI information supplied to binde is for the main + -- unit only. However, to preserve the consistency of the tree and + -- ensure proper serialization of internal names, external calls + -- also receive corresponding call markers (see Build_Call_Marker). + -- Regardless of the reason, external calls must not be processed. + + if In_Main_Context (N) then + Extract_Call_Attributes + (Call => N, + Target_Id => Target_Id, + Attrs => Call_Attrs); + + if Is_Activation_Proc (Target_Id) then + Process_Activation_Conditional_ABE + (Call => N, + Call_Attrs => Call_Attrs, + In_Task_Body => In_Task_Body); + + else + Process_Call + (Call => N, + Call_Attrs => Call_Attrs, + Target_Id => Target_Id, + In_Task_Body => In_Task_Body); + end if; + end if; + + -- Instantiations + + elsif Is_Suitable_Instantiation (N) then + Process_Instantiation (N, In_Task_Body); + + -- Variable assignments + + elsif Is_Suitable_Variable_Assignment (N) then + Process_Variable_Assignment (N); + + -- Variable read + + elsif Is_Suitable_Variable_Read (N) then + Process_Variable_Read (N); + end if; + + -- Remove the current scenario from the stack of active scenarios once + -- all ABE diagnostics and checks have been performed. + + Pop_Active_Scenario (N); + end Process_Scenario; + + --------------------------------- + -- Record_Elaboration_Scenario -- + --------------------------------- + + procedure Record_Elaboration_Scenario (N : Node_Id) is + Level : Enclosing_Level_Kind; + + Declaration_Level_OK : Boolean; + -- This flag is set when a particular scenario is allowed to appear at + -- the declaration level. + + begin + -- Assume that the scenario must not appear at the declaration level + + Declaration_Level_OK := False; + + -- Nothing to do for ASIS. As a result, no ABE checks and diagnostics + -- are performed in this mode. + + if ASIS_Mode then + return; + + -- Nothing to do when the scenario is being preanalyzed + + elsif Preanalysis_Active then + return; + end if; + + -- Ensure that a library level call does not appear in a preelaborated + -- unit. The check must come before ignoring scenarios within external + -- units or inside generics because calls in those context must also be + -- verified. + + if Is_Suitable_Call (N) then + Check_Preelaborated_Call (N); + end if; + + -- Nothing to do when the scenario does not appear within the main unit + + if not In_Main_Context (N) then + return; + + -- Scenarios within a generic unit are never considered because generics + -- cannot be elaborated. + + elsif Inside_A_Generic then + return; + + -- Scenarios which do not fall in one of the elaboration categories + -- listed below are not considered. The categories are: + + -- 'Access for entries, operators, and subprograms + -- Assignments to variables + -- Calls (includes task activation) + -- Instantiations + -- Reads of variables + + elsif Is_Suitable_Access (N) then + + -- Signal any enclosing local exception handlers that the 'Access may + -- raise Program_Error due to a failed ABE check when switch -gnatd.o + -- (conservative elaboration order for indirect calls) is in effect. + -- Marking the exception handlers ensures proper expansion by both + -- the front and back end restriction when No_Exception_Propagation + -- is in effect. + + if Debug_Flag_Dot_O then + Possible_Local_Raise (N, Standard_Program_Error); + end if; + + elsif Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N) then + Declaration_Level_OK := True; + + -- Signal any enclosing local exception handlers that the call or + -- instantiation may raise Program_Error due to a failed ABE check. + -- Marking the exception handlers ensures proper expansion by both + -- the front and back end restriction when No_Exception_Propagation + -- is in effect. + + Possible_Local_Raise (N, Standard_Program_Error); + + elsif Is_Suitable_Variable_Assignment (N) + or else Is_Suitable_Variable_Read (N) + then + null; + + -- Otherwise the input does not denote a suitable scenario + + else + return; + end if; + + -- The static model imposes additional restrictions on the placement of + -- scenarios. In contrast, the dynamic model assumes that every scenario + -- will be elaborated or invoked at some point. + + if Static_Elaboration_Checks then + + -- Performance note: parent traversal + + Level := Find_Enclosing_Level (N); + + -- Declaration level scenario + + if Declaration_Level_OK and then Level = Declaration_Level then + null; + + -- Library level scenario + + elsif Level in Library_Level then + null; + + -- Instantiation library level scenario + + elsif Level = Instantiation then + null; + + -- Otherwise the scenario does not appear at the proper level and + -- cannot possibly act as a top level scenario. + + else + return; + end if; + end if; + + -- Perform early detection of guaranteed ABEs in order to suppress the + -- instantiation of generic bodies as gigi cannot handle certain types + -- of premature instantiations. + + Process_Guaranteed_ABE (N); + + -- At this point all checks have been performed. Record the scenario for + -- later processing by the ABE phase. + + Top_Level_Scenarios.Append (N); + + -- Mark a scenario which may produce run-time conditional ABE checks or + -- guaranteed ABE failures as recorded. The flag ensures that scenario + -- rewriting performed by Atree.Rewrite will be properly reflected in + -- all relevant internal data structures. + + if Is_Check_Emitting_Scenario (N) then + Set_Is_Recorded_Scenario (N); + end if; + end Record_Elaboration_Scenario; + + ------------------- + -- Root_Scenario -- + ------------------- + + function Root_Scenario return Node_Id is + package Stack renames Scenario_Stack; + + begin + -- Ensure that the scenario stack has at least one active scenario in + -- it. The one at the bottom (index First) is the root scenario. + + pragma Assert (Stack.Last >= Stack.First); + return Stack.Table (Stack.First); + end Root_Scenario; + + ------------------------------- + -- Static_Elaboration_Checks -- + ------------------------------- + + function Static_Elaboration_Checks return Boolean is + begin + return not Dynamic_Elaboration_Checks; + end Static_Elaboration_Checks; + + ------------------- + -- Traverse_Body -- + ------------------- + + procedure Traverse_Body (N : Node_Id; In_Task_Body : Boolean) is + function Is_Potential_Scenario (Nod : Node_Id) return Traverse_Result; + -- Determine whether arbitrary node Nod denotes a suitable scenario and + -- if so, process it. + + procedure Traverse_Potential_Scenarios is + new Traverse_Proc (Is_Potential_Scenario); + + procedure Traverse_List (List : List_Id); + -- Inspect list List for suitable elaboration scenarios and process them + + --------------------------- + -- Is_Potential_Scenario -- + --------------------------- + + function Is_Potential_Scenario (Nod : Node_Id) return Traverse_Result is + begin + -- Special cases + + -- Skip constructs which do not have elaboration of their own and + -- need to be elaborated by other means such as invocation, task + -- activation, etc. + + if Is_Non_Library_Level_Encapsulator (Nod) then + return Skip; + + -- Terminate the traversal of a task body with an accept statement + -- when no entry calls in elaboration are allowed because the task + -- will block at run-time and none of the remaining statements will + -- be executed. + + elsif Nkind_In (Original_Node (Nod), N_Accept_Statement, + N_Selective_Accept) + and then Restriction_Active (No_Entry_Calls_In_Elaboration_Code) + then + return Abandon; + + -- Certain nodes carry semantic lists which act as repositories until + -- expansion transforms the node and relocates the contents. Examine + -- these lists in case expansion is disabled. + + elsif Nkind_In (Nod, N_And_Then, N_Or_Else) then + Traverse_List (Actions (Nod)); + + elsif Nkind_In (Nod, N_Elsif_Part, N_Iteration_Scheme) then + Traverse_List (Condition_Actions (Nod)); + + elsif Nkind (Nod) = N_If_Expression then + Traverse_List (Then_Actions (Nod)); + Traverse_List (Else_Actions (Nod)); + + elsif Nkind_In (Nod, N_Component_Association, + N_Iterated_Component_Association) + then + Traverse_List (Loop_Actions (Nod)); + + -- General case + + elsif Is_Suitable_Scenario (Nod) then + Process_Scenario (Nod, In_Task_Body); + end if; + + return OK; + end Is_Potential_Scenario; + + ------------------- + -- Traverse_List -- + ------------------- + + procedure Traverse_List (List : List_Id) is + Item : Node_Id; + + begin + Item := First (List); + while Present (Item) loop + Traverse_Potential_Scenarios (Item); + Next (Item); + end loop; + end Traverse_List; + + -- Start of processing for Traverse_Body + + begin + -- Nothing to do when there is no body + + if No (N) then + return; + + elsif Nkind (N) /= N_Subprogram_Body then + return; + end if; + + -- Nothing to do if the body was already traversed during the processing + -- of the same top level scenario. + + if Visited_Bodies.Get (N) then + return; + + -- Otherwise mark the body as traversed + + else + Visited_Bodies.Set (N, True); + end if; + + -- Examine the declarations for suitable scenarios + + Traverse_List (Declarations (N)); + + -- Examine the handled sequence of statements. This also includes any + -- exceptions handlers. + + Traverse_Potential_Scenarios (Handled_Statement_Sequence (N)); + end Traverse_Body; + + --------------------------------- + -- Update_Elaboration_Scenario -- + --------------------------------- + + procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id) is + package Scenarios renames Top_Level_Scenarios; + + begin + -- A scenario is being transformed by Atree.Rewrite. Update all relevant + -- internal data structures to reflect this change. This ensures that a + -- potential run-time conditional ABE check or a guaranteed ABE failure + -- is inserted at the proper place in the tree. + + if Is_Check_Emitting_Scenario (Old_N) + and then Is_Recorded_Scenario (Old_N) + and then Old_N /= New_N + then + -- Performance note: list traversal + + for Index in Scenarios.First .. Scenarios.Last loop + if Scenarios.Table (Index) = Old_N then + Scenarios.Table (Index) := New_N; + + Set_Is_Recorded_Scenario (Old_N, False); + Set_Is_Recorded_Scenario (New_N); + return; + end if; + end loop; + + -- A recorded scenario must be in the table of recorded scenarios + + pragma Assert (False); + end if; + end Update_Elaboration_Scenario; + + ------------------------- + -- Visited_Bodies_Hash -- + ------------------------- + + function Visited_Bodies_Hash (Key : Node_Id) return Visited_Bodies_Index is + begin + return Visited_Bodies_Index (Key mod Visited_Bodies_Max); + end Visited_Bodies_Hash; + +end Sem_Elab;