-- block statement, entry body, subprogram body, or task body, ignoring
-- enclosing packages.
--
+ -- * Early call region - A section of code which ends at a subprogram body
+ -- and starts from the nearest non-preelaborable construct which precedes
+ -- the subprogram body. The early call region extends from a package body
+ -- to a package spec when the spec carries pragma Elaborate_Body.
+ --
-- * 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.
--
-- - '[Unrestricted_]Access of entries, operators, and subprograms
--
- -- - Assignments to variables
+ -- - Assignments to variables
+ --
+ -- - Calls to entries, operators, and subprograms
--
- -- - Calls to entries, operators, and subprograms
+ -- - Derived type declarations
--
- -- - Instantiations
+ -- - Instantiations
--
- -- - Reads of variables
+ -- - Pragma Refined_State
--
- -- - Task activation
+ -- - Reads of variables
+ --
+ -- - Task activation
--
-- * Target - A construct referenced by a scenario. The targets recognized
-- by the ABE mechanism are as follows:
--
-- - For calls, the target is the entry, operator, or subprogram
--
+ -- - For derived type declarations, the target is the derived type
+ --
-- - For instantiations, the target is the generic template
--
+ -- - For pragma Refined_State, the targets are the constituents
+ --
-- - For reads of variables, the target is the variable
--
-- - For task activation, the target is the task body
-- the ABE mechanism. This eliminates the need to examine the whole
-- tree in a separate pass.
--
+ -- * Record certain SPARK scenarios which are not necessarily executable
+ -- during elaboration, but still require elaboration-related checks.
+ --
+ -- 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.
--
-- the call/instantiation/task activation graph. The traversal stops
-- when an outgoing edge leaves the main unit.
--
+ -- * Examine all SPARK scenarios saved during the Recording phase
+ --
-- * Depending on the elaboration model in effect, perform the following
-- actions:
--
-- 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 -------------+ |
+ -- Analysis/Resolution
+ -- |
+ -- +- Build_Call_Marker
+ -- |
+ -- +- Build_Variable_Reference_Marker
+ -- |
+ -- +- | -------------------- Recording phase ---------------------------+
+ -- | v |
+ -- | Record_Elaboration_Scenario |
+ -- | | |
+ -- | +--> Check_Preelaborated_Call |
+ -- | | |
+ -- | +--> Process_Guaranteed_ABE |
+ -- | | | |
+ -- | | +--> Process_Guaranteed_ABE_Activation |
+ -- | | | |
+ -- | | +--> Process_Guaranteed_ABE_Call |
+ -- | | | |
+ -- | | +--> Process_Guaranteed_ABE_Instantiation |
+ -- | | |
+ -- +- | ----------------------------------------------------------------+
+ -- |
+ -- |
+ -- +--> SPARK_Scenarios
+ -- | +-----------+-----------+ .. +-----------+
+ -- | | Scenario1 | Scenario2 | .. | ScenarioN |
+ -- | +-----------+-----------+ .. +-----------+
+ -- |
+ -- +--> Top_Level_Scenarios
+ -- | +-----------+-----------+ .. +-----------+
+ -- | | Scenario1 | Scenario2 | .. | ScenarioN |
+ -- | +-----------+-----------+ .. +-----------+
+ -- |
+ -- End of Compilation
+ -- |
+ -- +- | --------------------- Processing phase -------------------------+
+ -- | v |
+ -- | Check_Elaboration_Scenarios |
+ -- | | |
+ -- | +--> Check_SPARK_Scenario |
+ -- | | | |
+ -- | | +--> Check_SPARK_Derived_Type |
+ -- | | | |
+ -- | | +--> Check_SPARK_Instantiation |
+ -- | | | |
+ -- | | +--> Check_SPARK_Refined_State_Pragma |
+ -- | | |
+ -- | +--> Process_Conditional_ABE <---------------------------+ |
+ -- | | | |
+ -- | +--> Process_Conditional_ABE_Access Is_Suitable_Scenario |
+ -- | | ^ |
+ -- | +--> Process_Conditional_ABE_Activation | |
+ -- | | | | |
+ -- | | +-----------------------------+ | |
+ -- | | | | |
+ -- | +--> Process_Conditional_ABE_Call +--------> Traverse_Body |
+ -- | | | | |
+ -- | | +-----------------------------+ |
-- | | |
- -- | +--> Process_Instantiation |
+ -- | +--> Process_Conditional_ABE_Instantiation |
-- | | |
- -- | +--> Process_Variable_Assignment |
+ -- | +--> Process_Conditional_ABE_Variable_Assignment |
-- | | |
- -- | +--> Process_Variable_Reference |
+ -- | +--> Process_Conditional_ABE_Variable_Reference |
-- | |
- -- +------------------------- Processing phase -------------------------+
+ -- +--------------------------------------------------------------------+
----------------------
-- Important points --
---------------------------
-- The following steps describe how to add a new elaboration scenario and
- -- preserve the existing architecture.
+ -- preserve the existing architecture. Note that not all of the steps may
+ -- need to be carried out.
--
- -- 1) If necessary, update predicate Is_Scenario
+ -- 1) Update predicate 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.
+ -- 4) Add routine Process_Conditional_ABE_xxx. Include a call to it in
+ -- routine Process_Conditional_ABE.
--
- -- 5) Add routine Info_xxx. Include a call to it in Process_xxx.
+ -- 5) Add routine Process_Guaranteed_ABE_xxx. Include a call to it in
+ -- routine Process_Guaranteed_ABE.
--
- -- 6) Add routine Output_xxx. Include a call to it in routine
+ -- 6) Add routine Check_SPARK_xxx. Include a call to it in routine
+ -- Check_SPARK_Scenario.
+ --
+ -- 7) Add routine Info_xxx. Include a call to it in routine
+ -- Process_Conditional_ABE_xxx.
+ --
+ -- 8) Add routine Output_xxx. Include a call to it in routine
-- Output_Active_Scenarios.
--
- -- 7) If necessary, add a new Extract_xxx_Attributes routine
+ -- 9) Add routine Extract_xxx_Attributes
--
- -- 8) If necessary, update routine Is_Potential_Scenario
+ -- 10) 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.
+ -- preserve the existing architecture. Note that not all of the steps may
+ -- need to be carried out.
--
-- 1) Add predicate Is_xxx.
--
-- body. The routines of interest are
--
-- Record_Elaboration_Scenario
- -- Process_Scenario
+ -- Process_Conditional_ABE
+ -- Process_Guaranteed_ABE
-- Traverse_Body
-- * If the issue involves a circularity in the elaboration order, examine
-- Attributes --
----------------
+ -- To minimize the amount of code within routines, the ABE mechanism relies
+ -- on "attribute" records to capture relevant information for a scenario or
+ -- a target.
+
-- The following type captures relevant attributes which pertain to a call
type Call_Attributes is record
-- Data structures --
---------------------
+ -- The ABE mechanism employs lists and hash tables to store information
+ -- pertaining to scenarios and targets, as well as the Processing phase.
+ -- The need for data structures comes partly from the size limitation of
+ -- nodes. Note that the use of hash tables is conservative and operations
+ -- are carried out only when a particular hash table has at least one key
+ -- value pair (see xxx_In_Use flags).
+
+ -- The following table stores the early call regions of subprogram bodies
+
+ Early_Call_Regions_Max : constant := 101;
+
+ type Early_Call_Regions_Index is range 0 .. Early_Call_Regions_Max - 1;
+
+ function Early_Call_Regions_Hash
+ (Key : Entity_Id) return Early_Call_Regions_Index;
+ -- Obtain the hash value of entity Key
+
+ Early_Call_Regions_In_Use : Boolean := False;
+ -- This flag flag determines whether table Early_Call_Regions contains at
+ -- least one key/value pair.
+
+ Early_Call_Regions_No_Element : constant Node_Id := Empty;
+
+ package Early_Call_Regions is new Simple_HTable
+ (Header_Num => Early_Call_Regions_Index,
+ Element => Node_Id,
+ No_Element => Early_Call_Regions_No_Element,
+ Key => Entity_Id,
+ Hash => Early_Call_Regions_Hash,
+ Equal => "=");
+
-- The following table stores the elaboration status of all units withed by
-- the main unit.
- Elaboration_Context_Max : constant := 1009;
+ Elaboration_Statuses_Max : constant := 1009;
- type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
+ type Elaboration_Statuses_Index is range 0 .. Elaboration_Statuses_Max - 1;
- function Elaboration_Context_Hash
- (Key : Entity_Id) return Elaboration_Context_Index;
+ function Elaboration_Statuses_Hash
+ (Key : Entity_Id) return Elaboration_Statuses_Index;
-- Obtain the hash value of entity Key
- package Elaboration_Context is new Simple_HTable
- (Header_Num => Elaboration_Context_Index,
+ Elaboration_Statuses_In_Use : Boolean := False;
+ -- This flag flag determines whether table Elaboration_Statuses contains at
+ -- least one key/value pair.
+
+ Elaboration_Statuses_No_Element : constant Elaboration_Attributes :=
+ No_Elaboration_Attributes;
+
+ package Elaboration_Statuses is new Simple_HTable
+ (Header_Num => Elaboration_Statuses_Index,
Element => Elaboration_Attributes,
- No_Element => No_Elaboration_Attributes,
+ No_Element => Elaboration_Statuses_No_Element,
Key => Entity_Id,
- Hash => Elaboration_Context_Hash,
+ Hash => Elaboration_Statuses_Hash,
+ Equal => "=");
+
+ -- The following table stores a status flag for each SPARK scenario saved
+ -- in table SPARK_Scenarios.
+
+ Recorded_SPARK_Scenarios_Max : constant := 127;
+
+ type Recorded_SPARK_Scenarios_Index is
+ range 0 .. Recorded_SPARK_Scenarios_Max - 1;
+
+ function Recorded_SPARK_Scenarios_Hash
+ (Key : Node_Id) return Recorded_SPARK_Scenarios_Index;
+ -- Obtain the hash value of Key
+
+ Recorded_SPARK_Scenarios_In_Use : Boolean := False;
+ -- This flag flag determines whether table Recorded_SPARK_Scenarios
+ -- contains at least one key/value pair.
+
+ Recorded_SPARK_Scenarios_No_Element : constant Boolean := False;
+
+ package Recorded_SPARK_Scenarios is new Simple_HTable
+ (Header_Num => Recorded_SPARK_Scenarios_Index,
+ Element => Boolean,
+ No_Element => Recorded_SPARK_Scenarios_No_Element,
+ Key => Node_Id,
+ Hash => Recorded_SPARK_Scenarios_Hash,
Equal => "=");
-- The following table stores a status flag for each top-level scenario
(Key : Node_Id) return Recorded_Top_Level_Scenarios_Index;
-- Obtain the hash value of entity Key
+ Recorded_Top_Level_Scenarios_In_Use : Boolean := False;
+ -- This flag flag determines whether table Recorded_Top_Level_Scenarios
+ -- contains at least one key/value pair.
+
+ Recorded_Top_Level_Scenarios_No_Element : constant Boolean := False;
+
package Recorded_Top_Level_Scenarios is new Simple_HTable
(Header_Num => Recorded_Top_Level_Scenarios_Index,
Element => Boolean,
- No_Element => False,
+ No_Element => Recorded_Top_Level_Scenarios_No_Element,
Key => Node_Id,
Hash => Recorded_Top_Level_Scenarios_Hash,
Equal => "=");
Table_Increment => 100,
Table_Name => "Scenario_Stack");
+ -- The following table stores SPARK scenarios which are not necessarily
+ -- executable during elaboration, but still require elaboration-related
+ -- checks.
+
+ package SPARK_Scenarios 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 => "SPARK_Scenarios");
+
-- 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
function Visited_Bodies_Hash (Key : Node_Id) return Visited_Bodies_Index;
-- Obtain the hash value of node Key
+ Visited_Bodies_In_Use : Boolean := False;
+ -- This flag determines whether table Visited_Bodies contains at least one
+ -- key/value pair.
+
+ Visited_Bodies_No_Element : constant Boolean := False;
+
package Visited_Bodies is new Simple_HTable
(Header_Num => Visited_Bodies_Index,
Element => Boolean,
- No_Element => False,
+ No_Element => Visited_Bodies_No_Element,
Key => Node_Id,
Hash => Visited_Bodies_Hash,
Equal => "=");
-- Local subprograms --
-----------------------
+ -- Multiple local subprograms are utilized to lower the semantic complexity
+ -- of the Recording and Processing phase.
+
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.
+ pragma Inline (Check_Preelaborated_Call);
+ -- Verify that entry, operator, or subprogram call Call does not appear at
+ -- the library level of a preelaborated unit.
+
+ procedure Check_SPARK_Derived_Type (Typ_Decl : Node_Id);
+ pragma Inline (Check_SPARK_Derived_Type);
+ -- Verify that the freeze node of a derived type denoted by declaration
+ -- Typ_Decl is within the early call region of each overriding primitive
+ -- body that belongs to the derived type (SPARK RM 7.7(8)).
+
+ procedure Check_SPARK_Instantiation (Exp_Inst : Node_Id);
+ pragma Inline (Check_SPARK_Instantiation);
+ -- Verify that expanded instance Exp_Inst does not precede the generic body
+ -- it instantiates (SPARK RM 7.7(6)).
+
+ procedure Check_SPARK_Scenario (N : Node_Id);
+ pragma Inline (Check_SPARK_Scenario);
+ -- Top level dispatcher for verifying SPARK scenarios which are not always
+ -- executable during elaboration but still need elaboration-related checks.
+
+ procedure Check_SPARK_Refined_State_Pragma (N : Node_Id);
+ pragma Inline (Check_SPARK_Refined_State_Pragma);
+ -- Verify that each constituent of Refined_State pragma N which belongs to
+ -- an abstract state mentioned in pragma Initializes has prior elaboration
+ -- with respect to the main unit (SPARK RM 7.7.1(7)).
function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id;
pragma Inline (Compilation_Unit);
-- Return the N_Compilation_Unit node of unit Unit_Id
+ function Early_Call_Region (Body_Id : Entity_Id) return Node_Id;
+ pragma Inline (Early_Call_Region);
+ -- Return the early call region associated with entry or subprogram body
+ -- Body_Id. IMPORTANT: This routine does not find the early call region.
+ -- To compute it, use routine Find_Early_Call_Region.
+
procedure Elab_Msg_NE
(Msg : String;
N : Node_Id;
-- 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 Elaboration_Status
+ (Unit_Id : Entity_Id) return Elaboration_Attributes;
+ pragma Inline (Elaboration_Status);
+ -- Return the set of elaboration attributes associated with unit Unit_Id
+
procedure Ensure_Prior_Elaboration
(N : Node_Id;
Unit_Id : Entity_Id;
+ Prag_Nam : Name_Id;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean);
- -- Guarantee the elaboration of unit Unit_Id with respect to the main unit.
- -- N denotes the related scenario. Flag In_Partial_Fin should be set when
- -- the need for elaboration is initiated by a partial finalization routine.
- -- Flag In_Task_Body should be set when the need for prior elaboration is
- -- initiated from a task body.
+ -- Guarantee the elaboration of unit Unit_Id with respect to the main unit
+ -- by installing pragma Elaborate or Elaborate_All denoted by Prag_Nam. N
+ -- denotes the related scenario. The flags should be set when the need for
+ -- elaboration was initiated as follows:
+ --
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
procedure Ensure_Prior_Elaboration_Dynamic
(N : Node_Id;
-- denoted by N except when N is within an instantiation. In that case the
-- unit is that of the top-level instantiation.
+ function Find_Early_Call_Region
+ (Body_Decl : Node_Id;
+ Assume_Elab_Body : Boolean := False;
+ Skip_Memoization : Boolean := False) return Node_Id;
+ -- Find the start of the early call region which belongs to subprogram body
+ -- Body_Decl as defined in SPARK RM 7.7. The behavior of the routine is to
+ -- find the early call region, memoize it, and return it, but this behavior
+ -- can be altered. Flag Assume_Elab_Body should be set when a package spec
+ -- may lack pragma Elaborate_Body, but the routine must still examine that
+ -- spec. Flag Skip_Memoization should be set when the routine must avoid
+ -- memoizing the region.
+
procedure Find_Elaborated_Units;
- -- Populate table Elaboration_Context with all units which have prior
+ -- Populate table Elaboration_Statuses with all units which have prior
-- elaboration with respect to the main unit.
function Find_Enclosing_Instance (N : Node_Id) return Node_Id;
-- Determine whether entity Id denotes the protected or unprotected version
-- of a protected subprogram.
+ function Is_Recorded_SPARK_Scenario (N : Node_Id) return Boolean;
+ pragma Inline (Is_Recorded_SPARK_Scenario);
+ -- Determine whether arbitrary node N is a recorded SPARK scenario which
+ -- appears in table SPARK_Scenarios.
+
function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean;
pragma Inline (Is_Recorded_Top_Level_Scenario);
- -- Determine whether arbitrary node is a recorded top-level scenario which
- -- appears in table Top_Level_Scenarios.
+ -- Determine whether arbitrary node N is a recorded top-level scenario
+ -- which appears in table Top_Level_Scenarios.
function Is_Safe_Activation
(Call : Node_Id;
-- Determine whether arbitrary node N is a suitable scenario for ABE
-- processing.
+ function Is_Suitable_SPARK_Derived_Type (N : Node_Id) return Boolean;
+ pragma Inline (Is_Suitable_SPARK_Derived_Type);
+ -- Determine whether arbitrary node N denotes a suitable derived type
+ -- declaration for ABE processing using the SPARK rules.
+
+ function Is_Suitable_SPARK_Instantiation (N : Node_Id) return Boolean;
+ pragma Inline (Is_Suitable_SPARK_Instantiation);
+ -- Determine whether arbitrary node N denotes a suitable instantiation for
+ -- ABE processing using the SPARK rules.
+
+ function Is_Suitable_SPARK_Refined_State_Pragma
+ (N : Node_Id) return Boolean;
+ pragma Inline (Is_Suitable_SPARK_Refined_State_Pragma);
+ -- Determine whether arbitrary node N denotes a suitable Refined_State
+ -- pragma for ABE processing using the SPARK rules.
+
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
-- Target_Decl is within a context which encloses the current root or is in
-- a different unit.
+ function Is_Visited_Body (Body_Decl : Node_Id) return Boolean;
+ pragma Inline (Is_Visited_Body);
+ -- Determine whether subprogram body Body_Decl is already visited during a
+ -- recursive traversal started from a top-level scenario.
+
procedure Meet_Elaboration_Requirement
(N : Node_Id;
Target_Id : Entity_Id;
-- 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_Partial_Fin : Boolean;
- In_Task_Body : Boolean);
- -- Perform ABE checks and diagnostics for 'Access to entry, operator, or
- -- subprogram denoted by Attr. Flag In_Partial_Fin shoud be set when the
- -- processing is initiated by a partial finalization routine. 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_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
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_Partial_Fin shoud be set when the processing is initiated
- -- by a partial finalization routine. Flag In_Task_Body should be set
- -- when the processing is initiated from a task body.
+ -- The flags should be set when the processing was initated as follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Activation_Call
+ procedure Process_Activation_Generic
(Call : Node_Id;
Call_Attrs : Call_Attributes;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
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. In_Partial_Fin
- -- shoud be set when the processing is initiated by a partial finalization
- -- routine. Flag In_Task_Body should be set when the processing is started
- -- from a task body.
+ -- Call_Attrs are the attributes of the activation call. The flags should
+ -- be set when the processing was initiated as follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Activation_Conditional_ABE_Impl
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Obj_Id : Entity_Id;
- Task_Attrs : Task_Attributes;
+ procedure Process_Conditional_ABE
+ (N : Node_Id;
+ In_Init_Cond : Boolean := False;
+ In_Partial_Fin : Boolean := False;
+ In_Task_Body : Boolean := False);
+ -- Top-level dispatcher for processing of various elaboration scenarios.
+ -- Perform conditional ABE checks and diagnostics for scenario N. The flags
+ -- should be set when the processing was initiated as follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
+
+ procedure Process_Conditional_ABE_Access
+ (Attr : Node_Id;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
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_Partial_Fin shoud be set when the processing
- -- is initiated by a partial finalization routine. Flag In_Task_Body should
- -- be set when the processing is initiated from a task body.
+ -- Perform ABE checks and diagnostics for 'Access to entry, operator, or
+ -- subprogram denoted by Attr. The flags should be set when the processing
+ -- was initiated as follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Activation_Guaranteed_ABE_Impl
+ procedure Process_Conditional_ABE_Activation_Impl
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Obj_Id : Entity_Id;
Task_Attrs : Task_Attributes;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
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. Task_Attrs are
- -- the attributes of the task type. The following parameters are provided
- -- for compatibility and are unused.
+ -- 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. The flags should be set when the processing was
+ -- initiated as follows:
--
- -- Call_Attrs
- -- In_Partial_Fin
- -- In_Task_Body
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Call
+ procedure Process_Conditional_ABE_Call
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
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_Partial_Fin shoud be set when
- -- the processing is initiated by a partial finalization routine. Flag
- -- In_Task_Body should be set when the processing is started from a task
- -- body.
+ -- are the attributes of the call. The flags should be set when the
+ -- processing was initiated as follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Call_Ada
+ procedure Process_Conditional_ABE_Call_Ada
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
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_Partial_Fin
- -- shoud be set when the processing is initiated by a partial finalization
- -- routine. Flag In_Task_Body should be set when the processing is started
- -- from a task body.
-
- procedure Process_Call_Conditional_ABE
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Target_Id : Entity_Id;
- Target_Attrs : Target_Attributes;
- In_Partial_Fin : Boolean);
- -- 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.
- -- Flag In_Partial_Fin shoud be set when the processing is initiated by a
- -- partial finalization routine.
-
- 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.
+ -- call. Target_Attrs are attributes of the target. The flags should be
+ -- set when the processing was initiated as follows:
+ --
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Call_SPARK
+ procedure Process_Conditional_ABE_Call_SPARK
(Call : Node_Id;
- Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
Target_Attrs : Target_Attributes;
- In_Partial_Fin : Boolean);
+ In_Init_Cond : Boolean;
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean);
-- 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. Flag In_Partial_Fin
- -- shoud be set when the processing is initiated by a partial finalization
- -- routine.
-
- procedure Process_Guaranteed_ABE (N : Node_Id);
- -- Top-level dispatcher for processing of scenarios which result in a
- -- guaranteed ABE.
+ -- Target_Id using the SPARK rules. Target_Attrs denotes the attributes of
+ -- the target. The flags should be set when the processing was initiated as
+ -- follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Instantiation
+ procedure Process_Conditional_ABE_Instantiation
(Exp_Inst : Node_Id;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean);
-- Top-level dispatcher for processing of instantiations. Perform ABE
- -- checks and diagnostics for expanded instantiation Exp_Inst. Flag
- -- In_Partial_Fin shoud be set when the processing is initiated by a
- -- partial finalization routine. Flag In_Task_Body should be set when
- -- the processing is initiated from a task body.
+ -- checks and diagnostics for expanded instantiation Exp_Inst. The flags
+ -- should be set when the processing was initiated as follows:
+ --
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Instantiation_Ada
+ procedure Process_Conditional_ABE_Instantiation_Ada
(Exp_Inst : Node_Id;
Inst : Node_Id;
Inst_Attrs : Instantiation_Attributes;
-- 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 denotes the
- -- attributes of the generic. Flag In_Partial_Fin shoud be set when the
- -- processing is initiated by a partial finalization routine. 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;
- In_Partial_Fin : Boolean);
- -- 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. Flag
- -- In_Partial_Fin shoud be set when the processing is initiated by a
- -- partial finalization routine.
-
- 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.
+ -- attributes of the generic. The flags should be set when the processing
+ -- was initiated as follows:
+ --
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Instantiation_SPARK
- (Exp_Inst : Node_Id;
- Inst : Node_Id;
- Inst_Attrs : Instantiation_Attributes;
+ procedure Process_Conditional_ABE_Instantiation_SPARK
+ (Inst : Node_Id;
Gen_Id : Entity_Id;
Gen_Attrs : Target_Attributes;
- In_Partial_Fin : Boolean);
- -- 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 denotes the
- -- attributes of the generic. Flag In_Partial_Fin shoud be set when the
- -- processing is initiated by a partial finalization routine.
-
- procedure Process_Scenario
- (N : Node_Id;
- In_Partial_Fin : Boolean := False;
- In_Task_Body : Boolean := False);
- -- Top-level dispatcher for processing of various elaboration scenarios.
- -- Perform ABE checks and diagnostics for scenario N. Flag In_Partial_Fin
- -- shoud be set when the processing is initiated by a partial finalization
- -- routine. Flag In_Task_Body should be set when the processing is started
- -- from a task body.
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean);
+ -- Perform ABE checks and diagnostics for instantiation Inst of generic
+ -- Gen_Id using the SPARK rules. Gen_Attrs denotes the attributes of the
+ -- generic. The flags should be set when the processing was initiated as
+ -- follows:
+ --
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
- procedure Process_Variable_Assignment (Asmt : Node_Id);
+ procedure Process_Conditional_ABE_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
+ procedure Process_Conditional_ABE_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
+ procedure Process_Conditional_ABE_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_Reference (Ref : Node_Id);
+ procedure Process_Conditional_ABE_Variable_Reference (Ref : Node_Id);
-- Top-level dispatcher for processing of variable references. Perform ABE
-- checks and diagnostics for variable reference Ref.
- procedure Process_Variable_Reference_Read
+ procedure Process_Conditional_ABE_Variable_Reference_Read
(Ref : Node_Id;
Var_Id : Entity_Id;
Attrs : Variable_Attributes);
-- Perform ABE checks and diagnostics for reference Ref described by its
-- attributes Attrs, that reads variable Var_Id.
+ procedure Process_Guaranteed_ABE (N : Node_Id);
+ -- Top-level dispatcher for processing of scenarios which result in a
+ -- guaranteed ABE.
+
+ procedure Process_Guaranteed_ABE_Activation_Impl
+ (Call : Node_Id;
+ Call_Attrs : Call_Attributes;
+ Obj_Id : Entity_Id;
+ Task_Attrs : Task_Attributes;
+ In_Init_Cond : Boolean;
+ In_Partial_Fin : Boolean;
+ 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. Task_Attrs are
+ -- the attributes of the task type. The following parameters are provided
+ -- for compatibility and are unused.
+ --
+ -- Call_Attrs
+ -- In_Init_Cond
+ -- In_Partial_Fin
+ -- In_Task_Body
+
+ procedure Process_Guaranteed_ABE_Call
+ (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_Guaranteed_ABE_Instantiation (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 Push_Active_Scenario (N : Node_Id);
pragma Inline (Push_Active_Scenario);
-- Push scenario N on top of the scenario stack
+ procedure Record_SPARK_Elaboration_Scenario (N : Node_Id);
+ pragma Inline (Record_SPARK_Elaboration_Scenario);
+ -- Save SPARK scenario N in table SPARK_Scenarios for later processing
+
+ procedure Reset_Visited_Bodies;
+ pragma Inline (Reset_Visited_Bodies);
+ -- Clear the contents of table Visited_Bodies
+
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.
+ procedure Set_Early_Call_Region (Body_Id : Entity_Id; Start : Node_Id);
+ pragma Inline (Set_Early_Call_Region);
+ -- Associate an early call region with begins at construct Start with entry
+ -- or subprogram body Body_Id.
+
+ procedure Set_Elaboration_Status
+ (Unit_Id : Entity_Id;
+ Val : Elaboration_Attributes);
+ pragma Inline (Set_Elaboration_Status);
+ -- Associate an set of elaboration attributes with unit Unit_Id
+
+ procedure Set_Is_Recorded_SPARK_Scenario
+ (N : Node_Id;
+ Val : Boolean := True);
+ pragma Inline (Set_Is_Recorded_SPARK_Scenario);
+ -- Mark scenario N as being recorded in table SPARK_Scenarios
+
procedure Set_Is_Recorded_Top_Level_Scenario
(N : Node_Id;
Val : Boolean := True);
pragma Inline (Set_Is_Recorded_Top_Level_Scenario);
-- Mark scenario N as being recorded in table Top_Level_Scenarios
+ procedure Set_Is_Visited_Body (Subp_Body : Node_Id);
+ pragma Inline (Set_Is_Visited_Body);
+ -- Mark subprogram body Subp_Body as being visited during a recursive
+ -- traversal started from a top-level scenario.
+
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_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean);
-- Inspect the declarations and statements of subprogram body N for
- -- suitable elaboration scenarios and process them. Flag In_Partial_Fin
- -- shoud be set when the processing is initiated by a partial finalization
- -- routine. Flag In_Task_Body should be set when the traversal is initiated
- -- from a task body.
+ -- suitable elaboration scenarios and process them. The flags should
+ -- be set when the processing was initiated as follows:
+ --
+ -- In_Init_Cond - initial condition procedure
+ -- In_Partial_Fin - partial finalization procedure
+ -- In_Task_Body - task body
procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id);
pragma Inline (Update_Elaboration_Scenario);
Find_Elaborated_Units;
- -- Examine each top-level scenario saved during the Recording phase and
- -- perform various actions depending on the elaboration model in effect.
+ -- Examine each top-level scenario saved during the Recording phase for
+ -- conditional ABEs and perform various actions depending on the model
+ -- in effect. The table of visited bodies is created for each new top-
+ -- level scenario.
for Index in Top_Level_Scenarios.First .. Top_Level_Scenarios.Last loop
+ Reset_Visited_Bodies;
- -- Clear the table of visited scenario bodies for each new top-level
- -- scenario.
+ Process_Conditional_ABE (Top_Level_Scenarios.Table (Index));
+ end loop;
- Visited_Bodies.Reset;
+ -- Examine each SPARK scenario saved during the Recording phase which
+ -- isnot necessarily executable during elaboration, but still requires
+ -- elaboration-related checks.
- Process_Scenario (Top_Level_Scenarios.Table (Index));
+ for Index in SPARK_Scenarios.First .. SPARK_Scenarios.Last loop
+ Check_SPARK_Scenario (SPARK_Scenarios.Table (Index));
end loop;
end Check_Elaboration_Scenarios;
end if;
end Check_Preelaborated_Call;
- ----------------------
- -- Compilation_Unit --
- ----------------------
+ ------------------------------
+ -- Check_SPARK_Derived_Type --
+ ------------------------------
- function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id is
- Comp_Unit : Node_Id;
+ procedure Check_SPARK_Derived_Type (Typ_Decl : Node_Id) is
+ Typ : constant Entity_Id := Defining_Entity (Typ_Decl);
- begin
- Comp_Unit := Parent (Unit_Id);
+ -- NOTE: The routines within Check_SPARK_Derived_Type are intentionally
+ -- unnested to avoid deep indentation of code.
- -- Handle the case where a concurrent subunit is rewritten as a null
- -- statement due to expansion activities.
+ Stop_Check : exception;
+ -- This exception is raised when the freeze node violates the placement
+ -- rules.
- 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);
+ procedure Check_Overriding_Primitive
+ (Prim : Entity_Id;
+ FNode : Node_Id);
+ pragma Inline (Check_Overriding_Primitive);
+ -- Verify that freeze node FNode is within the early call region of
+ -- overriding primitive Prim's body.
- -- Otherwise use the declaration node of the unit
+ function Freeze_Node_Location (FNode : Node_Id) return Source_Ptr;
+ pragma Inline (Freeze_Node_Location);
+ -- Return a more accurate source location associated with freeze node
+ -- FNode.
- else
- Comp_Unit := Parent (Unit_Declaration_Node (Unit_Id));
- end if;
+ function Precedes_Source_Construct (N : Node_Id) return Boolean;
+ pragma Inline (Precedes_Source_Construct);
+ -- Determine whether arbitrary node N appears prior to some source
+ -- construct.
- -- Handle the case where a subprogram instantiation which acts as a
- -- compilation unit is expanded into an anonymous package that wraps
- -- the instantiated subprogram.
+ procedure Suggest_Elaborate_Body
+ (N : Node_Id;
+ Body_Decl : Node_Id;
+ Error_Nod : Node_Id);
+ pragma Inline (Suggest_Elaborate_Body);
+ -- Suggest the use of pragma Elaborate_Body when the pragma will allow
+ -- for node N to appear within the early call region of subprogram body
+ -- Body_Decl. The suggestion is attached to Error_Nod as a continuation
+ -- error.
- 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));
+ --------------------------------
+ -- Check_Overriding_Primitive --
+ --------------------------------
- -- Handle the case where the compilation unit is a subunit
+ procedure Check_Overriding_Primitive
+ (Prim : Entity_Id;
+ FNode : Node_Id)
+ is
+ Prim_Decl : constant Node_Id := Unit_Declaration_Node (Prim);
+ Body_Decl : Node_Id;
+ Body_Id : Entity_Id;
+ Region : Node_Id;
- elsif Nkind (Comp_Unit) = N_Subunit then
- Comp_Unit := Parent (Comp_Unit);
- end if;
+ begin
+ Body_Id := Corresponding_Body (Prim_Decl);
- pragma Assert (Nkind (Comp_Unit) = N_Compilation_Unit);
+ -- Nothing to do when the primitive does not have a corresponding
+ -- body. This can happen when the unit with the bodies is not the
+ -- main unit subjected to ABE checks.
- return Comp_Unit;
- end Compilation_Unit;
+ if No (Body_Id) then
+ return;
- -----------------
- -- Elab_Msg_NE --
- -----------------
+ -- The primitive overrides a parent or progenitor primitive
- 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
+ elsif Present (Overridden_Operation (Prim)) then
- function Suffix return String;
- -- Obtain the suffix of the message
+ -- Nothing to do when overriding an interface primitive happens by
+ -- inheriting a non-interface primitive as the check would be done
+ -- on the parent primitive.
- ------------
- -- Prefix --
- ------------
+ if Present (Alias (Prim)) then
+ return;
+ end if;
+
+ -- Nothing to do when the primitive is not overriding. The body of
+ -- such a primitive cannot be targeted by a dispatching call which
+ -- is executable during elaboration, and cannot cause an ABE.
- function Prefix return String is
- begin
- if Info_Msg then
- return "info: ";
else
- return "";
+ return;
end if;
- end Prefix;
- ------------
- -- Suffix --
- ------------
+ Body_Decl := Unit_Declaration_Node (Body_Id);
+ Region := Find_Early_Call_Region (Body_Decl);
- function Suffix return String is
- begin
- if In_SPARK then
- return " in SPARK";
- else
- return "";
- end if;
- end Suffix;
+ -- The freeze node appears prior to the early call region of the
+ -- primitive body.
- -- Start of processing for Elab_Msg_NE
+ -- IMPORTANT: This check must always be performed even when -gnatd.v
+ -- (enforce SPARK elaboration rules in SPARK code) is not specified
+ -- because the static model cannot guarantee the absence of ABEs in
+ -- in the presence of dispatching calls.
- begin
- Error_Msg_NE (Prefix & Msg & Suffix, N, Id);
- end Elab_Msg_NE;
+ if Earlier_In_Extended_Unit (FNode, Region) then
+ Error_Msg_Node_2 := Prim;
+ Error_Msg_NE
+ ("first freezing point of type & must appear within early call "
+ & "region of primitive body & (SPARK RM 7.7(8))",
+ Typ_Decl, Typ);
- ------------------------------
- -- Elaboration_Context_Hash --
- ------------------------------
+ Error_Msg_Sloc := Sloc (Region);
+ Error_Msg_N ("\region starts #", Typ_Decl);
- 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;
+ Error_Msg_Sloc := Sloc (Body_Decl);
+ Error_Msg_N ("\region ends #", Typ_Decl);
- ------------------------------
- -- Ensure_Prior_Elaboration --
- ------------------------------
+ Error_Msg_Sloc := Freeze_Node_Location (FNode);
+ Error_Msg_N ("\first freezing point #", Typ_Decl);
- procedure Ensure_Prior_Elaboration
- (N : Node_Id;
- Unit_Id : Entity_Id;
- In_Partial_Fin : Boolean;
- In_Task_Body : Boolean)
- is
- Prag_Nam : Name_Id;
+ -- If applicable, suggest the use of pragma Elaborate_Body in the
+ -- associated package spec.
- begin
- -- Instantiating an external generic unit requires an implicit Elaborate
- -- because Elaborate_All is too strong and could introduce non-existent
- -- elaboration cycles.
+ Suggest_Elaborate_Body
+ (N => FNode,
+ Body_Decl => Body_Decl,
+ Error_Nod => Typ_Decl);
- -- package External is
- -- function Func ...;
- -- end External;
+ raise Stop_Check;
+ end if;
+ end Check_Overriding_Primitive;
- -- with External;
- -- generic
- -- package Gen is
- -- X : ... := External.Func;
- -- end Gen;
+ --------------------------
+ -- Freeze_Node_Location --
+ --------------------------
- -- [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;
+ function Freeze_Node_Location (FNode : Node_Id) return Source_Ptr is
+ Context : constant Node_Id := Parent (FNode);
+ Loc : constant Source_Ptr := Sloc (FNode);
- if Nkind (N) in N_Generic_Instantiation then
- Prag_Nam := Name_Elaborate;
+ Prv_Decls : List_Id;
+ Vis_Decls : List_Id;
- -- Otherwise generate an implicit Elaborate_All
+ begin
+ -- In general, the source location of the freeze node is as close as
+ -- possible to the real freeze point, except when the freeze node is
+ -- at the "bottom" of a package spec.
- else
- Prag_Nam := Name_Elaborate_All;
- end if;
+ if Nkind (Context) = N_Package_Specification then
+ Prv_Decls := Private_Declarations (Context);
+ Vis_Decls := Visible_Declarations (Context);
- -- Nothing to do when the need for prior elaboration came from a partial
- -- finalization routine which occurs in an initialization context. This
- -- behaviour parallels that of the old ABE mechanism.
+ -- The freeze node appears in the private declarations of the
+ -- package.
- if In_Partial_Fin then
- return;
+ if Present (Prv_Decls)
+ and then List_Containing (FNode) = Prv_Decls
+ then
+ null;
- -- 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.
+ -- The freeze node appears in the visible declarations of the
+ -- package and there are no private declarations.
- elsif Debug_Flag_Dot_Y and then In_Task_Body then
- return;
+ elsif Present (Vis_Decls)
+ and then List_Containing (FNode) = Vis_Decls
+ and then (No (Prv_Decls) or else Is_Empty_List (Prv_Decls))
+ then
+ null;
- -- Nothing to do when the unit is elaborated prior to the main unit.
- -- This check must also consider the following cases:
+ -- Otherwise the freeze node is not in the "last" declarative list
+ -- of the package. Use the existing source location of the freeze
+ -- node.
- -- * 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).
+ else
+ return Loc;
+ end if;
- -- * 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.
+ -- The freeze node appears at the "bottom" of the package when it
+ -- is in the "last" declarative list and is either the last in the
+ -- list or is followed by internal constructs only. In that case
+ -- the more appropriate source location is that of the package end
+ -- label.
- -- package A is package body A is
- -- procedure ABE; procedure ABE is ... end ABE;
- -- end A; end A;
+ if not Precedes_Source_Construct (FNode) then
+ return Sloc (End_Label (Context));
+ end if;
+ end if;
- -- 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;
+ return Loc;
+ end Freeze_Node_Location;
- -- with B;
- -- package C is package body C is
- -- ... ...
- -- end C; begin
- -- B.Proc;
- -- end C;
+ -------------------------------
+ -- Precedes_Source_Construct --
+ -------------------------------
- -- 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:
+ function Precedes_Source_Construct (N : Node_Id) return Boolean is
+ Decl : Node_Id;
- -- 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
+ begin
+ Decl := Next (N);
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ return True;
- -- The generation of an implicit pragma Elaborate_All (B) ensures that
- -- the elaboration order mechanism will not pick the above order.
+ -- A generated body for a source expression function is treated as
+ -- a source construct.
- -- An implicit Elaborate is NOT generated when the unit is subject to
- -- Elaborate_Body because both pragmas have the exact same effect.
+ elsif Nkind (Decl) = N_Subprogram_Body
+ and then Was_Expression_Function (Decl)
+ and then Comes_From_Source (Original_Node (Decl))
+ then
+ return True;
+ end if;
- -- * 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.
+ Next (Decl);
+ end loop;
- elsif Has_Prior_Elaboration
- (Unit_Id => Unit_Id,
- Same_Unit_OK => True,
- Elab_Body_OK => Prag_Nam = Name_Elaborate)
- then
- return;
+ return False;
+ end Precedes_Source_Construct;
- -- Suggest the use of pragma Prag_Nam when the dynamic model is in
- -- effect.
+ ----------------------------
+ -- Suggest_Elaborate_Body --
+ ----------------------------
- elsif Dynamic_Elaboration_Checks then
- Ensure_Prior_Elaboration_Dynamic
- (N => N,
- Unit_Id => Unit_Id,
- Prag_Nam => Prag_Nam);
+ procedure Suggest_Elaborate_Body
+ (N : Node_Id;
+ Body_Decl : Node_Id;
+ Error_Nod : Node_Id)
+ is
+ Unt : constant Node_Id := Unit (Cunit (Main_Unit));
+ Region : Node_Id;
- -- Install an implicit pragma Prag_Nam when the static model is in
- -- effect.
+ begin
+ -- The suggestion applies only when the subprogram body resides in a
+ -- compilation package body, and a pragma Elaborate_Body would allow
+ -- for the node to appear in the early call region of the subprogram
+ -- body. This implies that all code from the subprogram body upto the
+ -- node is preelaborable.
+
+ if Nkind (Unt) = N_Package_Body then
+
+ -- Find the start of the early call region again assuming that the
+ -- package spec has pragma Elaborate_Body. Note that the internal
+ -- data structures are intentionally not updated because this is a
+ -- speculative search.
+
+ Region :=
+ Find_Early_Call_Region
+ (Body_Decl => Body_Decl,
+ Assume_Elab_Body => True,
+ Skip_Memoization => True);
+
+ -- If the node appears within the early call region assuming that
+ -- the package spec carries pragma Elaborate_Body, then it is safe
+ -- to suggest the pragma.
+
+ if Earlier_In_Extended_Unit (Region, N) then
+ Error_Msg_Name_1 := Name_Elaborate_Body;
+ Error_Msg_NE
+ ("\consider adding pragma % in spec of unit &",
+ Error_Nod, Defining_Entity (Unt));
+ end if;
+ end if;
+ end Suggest_Elaborate_Body;
- else
- pragma Assert (Static_Elaboration_Checks);
+ -- Local variables
- Ensure_Prior_Elaboration_Static
- (N => N,
- Unit_Id => Unit_Id,
- Prag_Nam => Prag_Nam);
+ FNode : constant Node_Id := Freeze_Node (Typ);
+ Prims : constant Elist_Id := Direct_Primitive_Operations (Typ);
+
+ Prim_Elmt : Elmt_Id;
+
+ -- Start of processing for Check_SPARK_Derived_Type
+
+ begin
+ -- A type should have its freeze node set by the time SPARK scenarios
+ -- are being verified.
+
+ pragma Assert (Present (FNode));
+
+ -- Verify that the freeze node of the derived type is within the early
+ -- call region of each overriding primitive body (SPARK RM 7.7(8)).
+
+ if Present (Prims) then
+ Prim_Elmt := First_Elmt (Prims);
+ while Present (Prim_Elmt) loop
+ Check_Overriding_Primitive
+ (Prim => Node (Prim_Elmt),
+ FNode => FNode);
+
+ Next_Elmt (Prim_Elmt);
+ end loop;
end if;
- end Ensure_Prior_Elaboration;
- --------------------------------------
- -- Ensure_Prior_Elaboration_Dynamic --
- --------------------------------------
+ exception
+ when Stop_Check =>
+ null;
+ end Check_SPARK_Derived_Type;
- 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.
+ -------------------------------
+ -- Check_SPARK_Instantiation --
+ -------------------------------
- -------------------------
- -- Info_Missing_Pragma --
- -------------------------
+ procedure Check_SPARK_Instantiation (Exp_Inst : Node_Id) is
+ Gen_Attrs : Target_Attributes;
+ Gen_Id : Entity_Id;
+ Inst : Node_Id;
+ Inst_Attrs : Instantiation_Attributes;
+ Inst_Id : Entity_Id;
- procedure Info_Missing_Pragma is
- begin
- -- Internal units are ignored as they cause unnecessary noise
+ begin
+ Extract_Instantiation_Attributes
+ (Exp_Inst => Exp_Inst,
+ Inst => Inst,
+ Inst_Id => Inst_Id,
+ Gen_Id => Gen_Id,
+ Attrs => Inst_Attrs);
- if not In_Internal_Unit (Unit_Id) then
+ Extract_Target_Attributes (Gen_Id, Gen_Attrs);
- -- The name of the unit subjected to the elaboration pragma is
- -- fully qualified to improve the clarity of the info message.
+ -- The instantiation and the generic body are both in the main unit
- Error_Msg_Name_1 := Prag_Nam;
- Error_Msg_Qual_Level := Nat'Last;
+ if Present (Gen_Attrs.Body_Decl)
+ and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
- Error_Msg_NE ("info: missing pragma % for unit &", N, Unit_Id);
- Error_Msg_Qual_Level := 0;
- end if;
- end Info_Missing_Pragma;
+ -- If the instantiation appears prior to the generic body, then the
+ -- instantiation is illegal (SPARK RM 7.7(6)).
- -- Local variables
+ -- IMPORTANT: This check must always be performed even when -gnatd.v
+ -- (enforce SPARK elaboration rules in SPARK code) is not specified
+ -- because the rule prevents use-before-declaration of objects that
+ -- may precede the generic body.
- Elab_Attrs : Elaboration_Attributes;
- Level : Enclosing_Level_Kind;
+ and then Earlier_In_Extended_Unit (Inst, Gen_Attrs.Body_Decl)
+ then
+ Error_Msg_NE ("cannot instantiate & before body seen", Inst, Gen_Id);
+ end if;
+ end Check_SPARK_Instantiation;
- -- Start of processing for Ensure_Prior_Elaboration_Dynamic
+ --------------------------
+ -- Check_SPARK_Scenario --
+ --------------------------
+ procedure Check_SPARK_Scenario (N : Node_Id) is
begin
- Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+ -- Add the current scenario to the stack of active scenarios
- -- Nothing to do when the unit is guaranteed prior elaboration by means
- -- of a source Elaborate[_All] pragma.
+ Push_Active_Scenario (N);
- if Present (Elab_Attrs.Source_Pragma) then
- return;
+ if Is_Suitable_SPARK_Derived_Type (N) then
+ Check_SPARK_Derived_Type (N);
+
+ elsif Is_Suitable_SPARK_Instantiation (N) then
+ Check_SPARK_Instantiation (N);
+
+ elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+ Check_SPARK_Refined_State_Pragma (N);
end if;
- -- Output extra information on a missing Elaborate[_All] pragma when
- -- switch -gnatel (info messages on implicit Elaborate[_All] pragmas
- -- is in effect.
+ -- Remove the current scenario from the stack of active scenarios once
+ -- all ABE diagnostics and checks have been performed.
- if Elab_Info_Messages then
+ Pop_Active_Scenario (N);
+ end Check_SPARK_Scenario;
- -- Performance note: parent traversal
+ --------------------------------------
+ -- Check_SPARK_Refined_State_Pragma --
+ --------------------------------------
- Level := Find_Enclosing_Level (N);
+ procedure Check_SPARK_Refined_State_Pragma (N : Node_Id) is
- -- Declaration-level scenario
+ -- NOTE: The routines within Check_SPARK_Refined_State_Pragma are
+ -- intentionally unnested to avoid deep indentation of code.
- if (Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N))
- and then Level = Declaration_Level
- then
- null;
+ procedure Check_SPARK_Constituent (Constit_Id : Entity_Id);
+ pragma Inline (Check_SPARK_Constituent);
+ -- Ensure that a single constituent Constit_Id is elaborated prior to
+ -- the main unit.
- -- Library-level scenario
+ procedure Check_SPARK_Constituents (Constits : Elist_Id);
+ pragma Inline (Check_SPARK_Constituents);
+ -- Ensure that all constituents found in list Constits are elaborated
+ -- prior to the main unit.
- elsif Level in Library_Level then
- null;
+ procedure Check_SPARK_Initialized_State (State : Node_Id);
+ pragma Inline (Check_SPARK_Initialized_State);
+ -- Ensure that the constituents of single abstract state State are
+ -- elaborated prior to the main unit.
- -- Instantiation library-level scenario
+ procedure Check_SPARK_Initialized_States (Pack_Id : Entity_Id);
+ pragma Inline (Check_SPARK_Initialized_States);
+ -- Ensure that the constituents of all abstract states which appear in
+ -- the Initializes pragma of package Pack_Id are elaborated prior to the
+ -- main unit.
- elsif Level = Instantiation then
- null;
+ -----------------------------
+ -- Check_SPARK_Constituent --
+ -----------------------------
- -- Otherwise the scenario does not appear at the proper level and
- -- cannot possibly act as a top-level scenario.
+ procedure Check_SPARK_Constituent (Constit_Id : Entity_Id) is
+ Prag : Node_Id;
- else
+ begin
+ -- Nothing to do for "null" constituents
+
+ if Nkind (Constit_Id) = N_Null then
+ return;
+
+ -- Nothing to do for illegal constituents
+
+ elsif Error_Posted (Constit_Id) then
return;
end if;
- Info_Missing_Pragma;
- end if;
- end Ensure_Prior_Elaboration_Dynamic;
+ Prag := SPARK_Pragma (Constit_Id);
- -------------------------------------
- -- 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.
+ -- The check applies only when the constituent is subject to pragma
+ -- SPARK_Mode On.
- 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.
+ if Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On
+ then
+ -- An external constituent of an abstract state which appears in
+ -- the Initializes pragma of a package spec imposes an Elaborate
+ -- requirement on the context of the main unit. Determine whether
+ -- the context has a pragma strong enough to meet the requirement.
- ----------------------
- -- Find_With_Clause --
- ----------------------
+ -- IMPORTANT: This check is performed only when -gnatd.v (enforce
+ -- SPARK elaboration rules in SPARK code) is in effect because the
+ -- static model can ensure the prior elaboration of the unit which
+ -- contains a constituent by installing implicit Elaborate pragma.
- function Find_With_Clause
- (Items : List_Id;
- Withed_Id : Entity_Id) return Node_Id
- is
- Item : Node_Id;
+ if Debug_Flag_Dot_V then
+ Meet_Elaboration_Requirement
+ (N => N,
+ Target_Id => Constit_Id,
+ Req_Nam => Name_Elaborate);
- begin
- -- Examine the context clauses looking for a suitable with. Note that
- -- limited clauses do not affect the elaboration order.
+ -- Otherwise ensure that the unit with the external constituent is
+ -- elaborated prior to the main unit.
- 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;
+ else
+ Ensure_Prior_Elaboration
+ (N => N,
+ Unit_Id => Find_Top_Unit (Constit_Id),
+ Prag_Nam => Name_Elaborate,
+ In_Partial_Fin => False,
+ In_Task_Body => False);
end if;
+ end if;
+ end Check_SPARK_Constituent;
- Next (Item);
- end loop;
-
- return Empty;
- end Find_With_Clause;
+ ------------------------------
+ -- Check_SPARK_Constituents --
+ ------------------------------
- --------------------------
- -- Info_Implicit_Pragma --
- --------------------------
+ procedure Check_SPARK_Constituents (Constits : Elist_Id) is
+ Constit_Elmt : Elmt_Id;
- procedure Info_Implicit_Pragma is
begin
- -- Internal units are ignored as they cause unnecessary noise
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Check_SPARK_Constituent (Node (Constit_Elmt));
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
+ end Check_SPARK_Constituents;
- if not In_Internal_Unit (Unit_Id) then
+ -----------------------------------
+ -- Check_SPARK_Initialized_State --
+ -----------------------------------
- -- The name of the unit subjected to the elaboration pragma is
- -- fully qualified to improve the clarity of the info message.
+ procedure Check_SPARK_Initialized_State (State : Node_Id) is
+ Prag : Node_Id;
+ State_Id : Entity_Id;
- Error_Msg_Name_1 := Prag_Nam;
- Error_Msg_Qual_Level := Nat'Last;
+ begin
+ -- Nothing to do for "null" initialization items
- Error_Msg_NE
- ("info: implicit pragma % generated for unit &", N, Unit_Id);
+ if Nkind (State) = N_Null then
+ return;
- Error_Msg_Qual_Level := 0;
- Output_Active_Scenarios (N);
+ -- Nothing to do for illegal states
+
+ elsif Error_Posted (State) then
+ return;
end if;
- end Info_Implicit_Pragma;
- -- Local variables
+ State_Id := Entity_Of (State);
- Main_Cunit : constant Node_Id := Cunit (Main_Unit);
- Loc : constant Source_Ptr := Sloc (Main_Cunit);
- Unit_Cunit : constant Node_Id := Compilation_Unit (Unit_Id);
+ -- Sanitize the state
- Is_Instantiation : constant Boolean :=
- Nkind (N) in N_Generic_Instantiation;
+ if No (State_Id) then
+ return;
- Clause : Node_Id;
- Elab_Attrs : Elaboration_Attributes;
- Items : List_Id;
+ elsif Error_Posted (State_Id) then
+ return;
- -- Start of processing for Ensure_Prior_Elaboration_Static
+ elsif Ekind (State_Id) /= E_Abstract_State then
+ return;
+ end if;
- begin
- Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+ -- The check is performed only when the abstract state is subject to
+ -- SPARK_Mode On.
- -- Nothing to do when the unit is guaranteed prior elaboration by means
- -- of a source Elaborate[_All] pragma.
+ Prag := SPARK_Pragma (State_Id);
- if Present (Elab_Attrs.Source_Pragma) then
- return;
+ if Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On
+ then
+ Check_SPARK_Constituents (Refinement_Constituents (State_Id));
+ end if;
+ end Check_SPARK_Initialized_State;
- -- Nothing to do when the unit has an existing implicit Elaborate[_All]
- -- pragma installed by a previous scenario.
+ ------------------------------------
+ -- Check_SPARK_Initialized_States --
+ ------------------------------------
- elsif Present (Elab_Attrs.With_Clause) then
+ procedure Check_SPARK_Initialized_States (Pack_Id : Entity_Id) is
+ Prag : constant Node_Id := Get_Pragma (Pack_Id, Pragma_Initializes);
+ Init : Node_Id;
+ Inits : Node_Id;
- -- 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.
+ begin
+ if Present (Prag) then
+ Inits := Expression (Get_Argument (Prag, Pack_Id));
- 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;
+ -- Avoid processing a "null" initialization list. The only other
+ -- alternative is an aggregate.
- return;
- end if;
+ if Nkind (Inits) = N_Aggregate then
- -- At this point it is known that the unit has no prior elaboration
- -- according to pragmas and hierarchical relationships.
+ -- The initialization items appear in list form:
+ --
+ -- (state1, state2)
- Items := Context_Items (Main_Cunit);
+ if Present (Expressions (Inits)) then
+ Init := First (Expressions (Inits));
+ while Present (Init) loop
+ Check_SPARK_Initialized_State (Init);
+ Next (Init);
+ end loop;
+ end if;
- if No (Items) then
- Items := New_List;
- Set_Context_Items (Main_Cunit, Items);
- end if;
+ -- The initialization items appear in associated form:
+ --
+ -- (state1 => item1,
+ -- state2 => (item2, item3))
+
+ if Present (Component_Associations (Inits)) then
+ Init := First (Component_Associations (Inits));
+ while Present (Init) loop
+ Check_SPARK_Initialized_State (Init);
+ Next (Init);
+ end loop;
+ end if;
+ end if;
+ end if;
+ end Check_SPARK_Initialized_States;
- -- 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.
+ -- Local variables
- Clause :=
- Find_With_Clause
- (Items => Items,
- Withed_Id => Unit_Id);
+ Pack_Body : constant Node_Id := Find_Related_Package_Or_Body (N);
- -- Generate:
- -- with Id;
+ -- Start of processing for Check_SPARK_Refined_State_Pragma
- -- 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.
+ begin
+ -- Pragma Refined_State must be associated with a package body
- if No (Clause) then
- Clause :=
- Make_With_Clause (Loc,
- Name => New_Occurrence_Of (Unit_Id, Loc));
+ pragma Assert
+ (Present (Pack_Body) and then Nkind (Pack_Body) = N_Package_Body);
- Set_Implicit_With (Clause);
- Set_Library_Unit (Clause, Unit_Cunit);
+ -- Verify that each external contitunent of an abstract state mentioned
+ -- in pragma Initializes is properly elaborated.
- Append_To (Items, Clause);
- end if;
+ Check_SPARK_Initialized_States (Unique_Defining_Entity (Pack_Body));
+ end Check_SPARK_Refined_State_Pragma;
- -- Instantiations require an implicit Elaborate because Elaborate_All is
- -- too conservative and may introduce non-existent elaboration cycles.
+ ----------------------
+ -- Compilation_Unit --
+ ----------------------
- if Is_Instantiation then
- Set_Elaborate_Desirable (Clause);
+ function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id is
+ Comp_Unit : Node_Id;
- -- Otherwise generate an implicit Elaborate_All
+ 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
- Set_Elaborate_All_Desirable (Clause);
+ Comp_Unit := Parent (Unit_Declaration_Node (Unit_Id));
end if;
- -- The implicit Elaborate[_All] ensures the prior elaboration of the
- -- unit. Include the unit in the elaboration context of the main unit.
+ -- Handle the case where a subprogram instantiation which acts as a
+ -- compilation unit is expanded into an anonymous package that wraps
+ -- the instantiated subprogram.
- Elaboration_Context.Set (Unit_Id,
- Elaboration_Attributes'(Source_Pragma => Empty,
- With_Clause => Clause));
+ 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));
- -- Output extra information on an implicit Elaborate[_All] pragma when
- -- switch -gnatel (info messages on implicit Elaborate[_All] pragmas is
- -- in effect.
+ -- Handle the case where the compilation unit is a subunit
- if Elab_Info_Messages then
- Info_Implicit_Pragma;
+ elsif Nkind (Comp_Unit) = N_Subunit then
+ Comp_Unit := Parent (Comp_Unit);
end if;
- end Ensure_Prior_Elaboration_Static;
-
- -----------------------------
- -- Extract_Assignment_Name --
- -----------------------------
- function Extract_Assignment_Name (Asmt : Node_Id) return Node_Id is
- Nam : Node_Id;
+ pragma Assert (Nkind (Comp_Unit) = N_Compilation_Unit);
- begin
- Nam := Name (Asmt);
+ return Comp_Unit;
+ end Compilation_Unit;
- -- When the name denotes an array or record component, find the whole
- -- object.
+ -----------------------
+ -- Early_Call_Region --
+ -----------------------
- while Nkind_In (Nam, N_Explicit_Dereference,
- N_Indexed_Component,
- N_Selected_Component,
- N_Slice)
- loop
- Nam := Prefix (Nam);
- end loop;
+ function Early_Call_Region (Body_Id : Entity_Id) return Node_Id is
+ begin
+ pragma Assert (Ekind_In (Body_Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Procedure,
+ E_Subprogram_Body));
+
+ if Early_Call_Regions_In_Use then
+ return Early_Call_Regions.Get (Body_Id);
+ end if;
- return Nam;
- end Extract_Assignment_Name;
+ return Early_Call_Regions_No_Element;
+ end Early_Call_Region;
-----------------------------
- -- Extract_Call_Attributes --
+ -- Early_Call_Regions_Hash --
-----------------------------
- procedure Extract_Call_Attributes
- (Call : Node_Id;
- Target_Id : out Entity_Id;
- Attrs : out Call_Attributes)
+ function Early_Call_Regions_Hash
+ (Key : Entity_Id) return Early_Call_Regions_Index
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);
+ return Early_Call_Regions_Index (Key mod Early_Call_Regions_Max);
+ end Early_Call_Regions_Hash;
- -- Extraction for entry calls, requeue, and subprogram calls
+ -----------------
+ -- Elab_Msg_NE --
+ -----------------
- else
- pragma Assert (Nkind_In (Call, N_Entry_Call_Statement,
- N_Function_Call,
- N_Procedure_Call_Statement,
- N_Requeue_Statement));
+ 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
- Target_Id := Entity (Extract_Call_Name (Call));
- From_Source := Comes_From_Source (Call);
+ function Suffix return String;
+ -- Obtain the suffix of the message
- -- Performance note: parent traversal
+ ------------
+ -- Prefix --
+ ------------
- In_Declarations := Find_Enclosing_Level (Call) = Declaration_Level;
+ 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_Status --
+ ------------------------
+
+ function Elaboration_Status
+ (Unit_Id : Entity_Id) return Elaboration_Attributes
+ is
+ begin
+ if Elaboration_Statuses_In_Use then
+ return Elaboration_Statuses.Get (Unit_Id);
+ end if;
+
+ return Elaboration_Statuses_No_Element;
+ end Elaboration_Status;
+
+ -------------------------------
+ -- Elaboration_Statuses_Hash --
+ -------------------------------
+
+ function Elaboration_Statuses_Hash
+ (Key : Entity_Id) return Elaboration_Statuses_Index
+ is
+ begin
+ return Elaboration_Statuses_Index (Key mod Elaboration_Statuses_Max);
+ end Elaboration_Statuses_Hash;
+
+ ------------------------------
+ -- Ensure_Prior_Elaboration --
+ ------------------------------
+
+ procedure Ensure_Prior_Elaboration
+ (N : Node_Id;
+ Unit_Id : Entity_Id;
+ Prag_Nam : Name_Id;
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean)
+ is
+ begin
+ pragma Assert (Nam_In (Prag_Nam, Name_Elaborate, Name_Elaborate_All));
+
+ -- Nothing to do when the need for prior elaboration came from a partial
+ -- finalization routine which occurs in an initialization context. This
+ -- behaviour parallels that of the old ABE mechanism.
+
+ if In_Partial_Fin then
+ return;
+
+ -- 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.
+
+ elsif 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_Status (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_Status (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.
+
+ Set_Elaboration_Status
+ (Unit_Id => Unit_Id,
+ Val => 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));
return Find_Unit_Entity (Unit (Cunit (Get_Code_Unit (N))));
end Find_Code_Unit;
+ ----------------------------
+ -- Find_Early_Call_Region --
+ ----------------------------
+
+ function Find_Early_Call_Region
+ (Body_Decl : Node_Id;
+ Assume_Elab_Body : Boolean := False;
+ Skip_Memoization : Boolean := False) return Node_Id
+ is
+ -- NOTE: The routines within Find_Early_Call_Region are intentionally
+ -- unnested to avoid deep indentation of code.
+
+ ECR_Found : exception;
+ -- This exception is raised when the early call region has been found
+
+ Start : Node_Id := Empty;
+ -- The start of the early call region. This variable is updated by the
+ -- various nested routines. Due to the use of exceptions, the variable
+ -- must be global to the nested routines.
+
+ -- The algorithm implemented in this routine attempts to find the early
+ -- call region of a subprogram body by inspecting constructs in reverse
+ -- declarative order, while navigating the tree. The algorithm consists
+ -- of an Inspection phase and an Advancement phase. The pseudocode is as
+ -- follows:
+ --
+ -- loop
+ -- inspection phase
+ -- advancement phase
+ -- end loop
+ --
+ -- The infinite loop is terminated by raising exception ECR_Found. The
+ -- algorithm utilizes two pointers, Curr and Start, to represent the
+ -- current construct to inspect and the start of the early call region.
+ --
+ -- IMPORTANT: The algorithm must maintain the following invariant at all
+ -- time for it to function properly - a nested construct is entered only
+ -- when it contains suitable constructs. This guarantees that leaving a
+ -- nested or encapsulating construct functions properly.
+ --
+ -- The Inspection phase determines whether the current construct is non-
+ -- preelaborable, and if it is, the algorithm terminates.
+ --
+ -- The Advancement phase walks the tree in reverse declarative order,
+ -- while entering and leaving nested and encapsulating constructs. It
+ -- may also terminate the elaborithm. There are several special cases
+ -- of advancement.
+ --
+ -- 1) General case:
+ --
+ -- <construct 1>
+ -- ...
+ -- <construct N-1> <- Curr
+ -- <construct N> <- Start
+ -- <subprogram body>
+ --
+ -- In the general case, a declarative or statement list is traversed in
+ -- reverse order where Curr is the lead pointer, and Start indicates the
+ -- last preelaborable construct.
+ --
+ -- 2) Entering handled bodies
+ --
+ -- package body Nested is <- Curr (2.3)
+ -- <declarations> <- Curr (2.2)
+ -- begin
+ -- <statements> <- Curr (2.1)
+ -- end Nested;
+ -- <construct> <- Start
+ --
+ -- In this case, the algorithm enters a handled body by starting from
+ -- the last statement (2.1), or the last declaration (2.2), or the body
+ -- is consumed (2.3) because it is empty and thus preelaborable.
+ --
+ -- 3) Entering package declarations
+ --
+ -- package Nested is <- Curr (2.3)
+ -- <visible declarations> <- Curr (2.2)
+ -- private
+ -- <private declarations> <- Curr (2.1)
+ -- end Nested;
+ -- <construct> <- Start
+ --
+ -- In this case, the algorithm enters a package declaration by starting
+ -- from the last private declaration (2.1), the last visible declaration
+ -- (2.2), or the package is consumed (2.3) because it is empty and thus
+ -- preelaborable.
+ --
+ -- 4) Transitioning from list to list of the same construct
+ --
+ -- Certain constructs have two eligible lists. The algorithm must thus
+ -- transition from the second to the first list when the second list is
+ -- exhausted.
+ --
+ -- declare <- Curr (4.2)
+ -- <declarations> <- Curr (4.1)
+ -- begin
+ -- <statements> <- Start
+ -- end;
+ --
+ -- In this case, the algorithm has exhausted the second list (statements
+ -- in the example), and continues with the last declaration (4.1) or the
+ -- construct is consumed (4.2) because it contains only preelaborable
+ -- code.
+ --
+ -- 5) Transitioning from list to construct
+ --
+ -- tack body Task is <- Curr (5.1)
+ -- <- Curr (Empty)
+ -- <construct 1> <- Start
+ --
+ -- In this case, the algorithm has exhausted a list, Curr is Empty, and
+ -- the owner of the list is consumed (5.1).
+ --
+ -- 6) Transitioning from unit to unit
+ --
+ -- A package body with a spec subject to pragma Elaborate_Body extends
+ -- the possible range of the early call region to the package spec.
+ --
+ -- package Pack is <- Curr (6.3)
+ -- pragma Elaborate_Body; <- Curr (6.2)
+ -- <visible declarations> <- Curr (6.2)
+ -- private
+ -- <private declarations> <- Curr (6.1)
+ -- end Pack;
+ --
+ -- package body Pack is <- Curr, Start
+ --
+ -- In this case, the algorithm has reached a package body compilation
+ -- unit whose spec is subject to pragma Elaborate_Body, or the caller
+ -- of the algorithm has specified this behavior. This transition is
+ -- equivalent to 3).
+ --
+ -- 7) Transitioning from unit to termination
+ --
+ -- Reaching a compilation unit always terminates the algorithm as there
+ -- are no more lists to examine. This must take 6) into account.
+ --
+ -- 8) Transitioning from subunit to stub
+ --
+ -- package body Pack is separate; <- Curr (8.1)
+ --
+ -- separate (...)
+ -- package body Pack is <- Curr, Start
+ --
+ -- Reaching a subunit continues the search from the corresponding stub
+ -- (8.1).
+
+ procedure Advance (Curr : in out Node_Id);
+ pragma Inline (Advance);
+ -- Update the Curr and Start pointers depending on their location in the
+ -- tree to the next eligible construct. This routine raises ECR_Found.
+
+ procedure Enter_Handled_Body (Curr : in out Node_Id);
+ pragma Inline (Enter_Handled_Body);
+ -- Update the Curr and Start pointers to enter a nested handled body if
+ -- applicable. This routine raises ECR_Found.
+
+ procedure Enter_Package_Declaration (Curr : in out Node_Id);
+ pragma Inline (Enter_Package_Declaration);
+ -- Update the Curr and Start pointers to enter a nested package spec if
+ -- applicable. This routine raises ECR_Found.
+
+ function Find_ECR (N : Node_Id) return Node_Id;
+ pragma Inline (Find_ECR);
+ -- Find an early call region starting from arbitrary node N
+
+ function Has_Suitable_Construct (List : List_Id) return Boolean;
+ pragma Inline (Has_Suitable_Construct);
+ -- Determine whether list List contains at least one suitable construct
+ -- for inclusion into an early call region.
+
+ procedure Include (N : Node_Id; Curr : in out Node_Id);
+ pragma Inline (Include);
+ -- Update the Curr and Start pointers to include arbitrary construct N
+ -- in the early call region.
+
+ function Is_OK_Preelaborable_Construct (N : Node_Id) return Boolean;
+ pragma Inline (Is_OK_Preelaborable_Construct);
+ -- Determine whether arbitrary node N denotes a preelaboration-safe
+ -- construct.
+
+ function Is_Suitable_Construct (N : Node_Id) return Boolean;
+ pragma Inline (Is_Suitable_Construct);
+ -- Determine whether arbitrary node N denotes a suitable construct for
+ -- inclusion into the early call region.
+
+ procedure Transition_Body_Declarations
+ (Bod : Node_Id;
+ Curr : in out Node_Id);
+ pragma Inline (Transition_Body_Declarations);
+ -- Update the Curr and Start pointers when construct Bod denotes a block
+ -- statement or a suitable body. This routine raises ECR_Found.
+
+ procedure Transition_Handled_Statements
+ (HSS : Node_Id;
+ Curr : in out Node_Id);
+ pragma Inline (Transition_Handled_Statements);
+ -- Update the Curr and Start pointers when node HSS denotes a handled
+ -- sequence of statements. This routine raises ECR_Found.
+
+ procedure Transition_Spec_Declarations
+ (Spec : Node_Id;
+ Curr : in out Node_Id);
+ pragma Inline (Transition_Spec_Declarations);
+ -- Update the Curr and Start pointers when construct Spec denotes
+ -- a concurrent definition or a package spec. This routine raises
+ -- ECR_Found.
+
+ procedure Transition_Unit (Unit : Node_Id; Curr : in out Node_Id);
+ pragma Inline (Transition_Unit);
+ -- Update the Curr and Start pointers when node Unit denotes a potential
+ -- compilation unit. This routine raises ECR_Found.
+
+ -------------
+ -- Advance --
+ -------------
+
+ procedure Advance (Curr : in out Node_Id) is
+ Context : Node_Id;
+
+ begin
+ -- Curr denotes one of the following cases upon entry into this
+ -- routine:
+ --
+ -- * Empty - There is no current construct when a declarative or a
+ -- statement list has been exhausted. This does not necessarily
+ -- indicate that the early call region has been computed as it
+ -- may still be possible to transition to another list.
+ --
+ -- * Encapsulator - The current construct encapsulates declarations
+ -- and/or statements. This indicates that the early call region
+ -- may extend within the nested construct.
+ --
+ -- * Preelaborable - The current construct is always preelaborable
+ -- because Find_ECR would not invoke Advance if this was not the
+ -- case.
+
+ -- The current construct is an encapsulator or is preelaborable
+
+ if Present (Curr) then
+
+ -- Enter encapsulators by inspecting their declarations and/or
+ -- statements.
+
+ if Nkind_In (Curr, N_Block_Statement, N_Package_Body) then
+ Enter_Handled_Body (Curr);
+
+ elsif Nkind (Curr) = N_Package_Declaration then
+ Enter_Package_Declaration (Curr);
+
+ -- Early call regions have a property which can be exploited to
+ -- optimize the algorithm.
+ --
+ -- <preceding subprogram body>
+ -- <preelaborable construct 1>
+ -- ...
+ -- <preelaborable construct N>
+ -- <initiating subprogram body>
+ --
+ -- If a traversal initiated from a subprogram body reaches a
+ -- preceding subprogram body, then both bodies share the same
+ -- early call region.
+ --
+ -- The property results in the following desirable effects:
+ --
+ -- * If the preceding body already has an early call region, then
+ -- the initiating body can reuse it. This minimizes the amount
+ -- of processing performed by the algorithm.
+ --
+ -- * If the preceding body lack an early call region, then the
+ -- algorithm can compute the early call region, and reuse it
+ -- for the initiating body. This processing performs the same
+ -- amount of work, but has the beneficial effect of computing
+ -- the early call regions of all preceding bodies.
+
+ elsif Nkind_In (Curr, N_Entry_Body, N_Subprogram_Body) then
+ Start :=
+ Find_Early_Call_Region
+ (Body_Decl => Curr,
+ Assume_Elab_Body => Assume_Elab_Body,
+ Skip_Memoization => Skip_Memoization);
+
+ raise ECR_Found;
+
+ -- Otherwise current construct is preelaborable. Unpdate the early
+ -- call region to include it.
+
+ else
+ Include (Curr, Curr);
+ end if;
+
+ -- Otherwise the current construct is missing, indicating that the
+ -- current list has been exhausted. Depending on the context of the
+ -- list, several transitions are possible.
+
+ else
+ -- The invariant of the algorithm ensures that Curr and Start are
+ -- at the same level of nesting at the point of a transition. The
+ -- algorithm can determine which list the traversal came from by
+ -- examining Start.
+
+ Context := Parent (Start);
+
+ -- Attempt the following transitions:
+ --
+ -- private declarations -> visible declarations
+ -- private declarations -> upper level
+ -- private declarations -> terminate
+ -- visible declarations -> upper level
+ -- visible declarations -> terminate
+
+ if Nkind_In (Context, N_Package_Specification,
+ N_Protected_Definition,
+ N_Task_Definition)
+ then
+ Transition_Spec_Declarations (Context, Curr);
+
+ -- Attempt the following transitions:
+ --
+ -- statements -> declarations
+ -- statements -> upper level
+ -- statements -> corresponding package spec (Elab_Body)
+ -- statements -> terminate
+
+ elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then
+ Transition_Handled_Statements (Context, Curr);
+
+ -- Attempt the following transitions:
+ --
+ -- declarations -> upper level
+ -- declarations -> corresponding package spec (Elab_Body)
+ -- declarations -> terminate
+
+ elsif Nkind_In (Context, N_Block_Statement,
+ N_Entry_Body,
+ N_Package_Body,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body)
+ then
+ Transition_Body_Declarations (Context, Curr);
+
+ -- Otherwise it is not possible to transition. Stop the search
+ -- because there are no more declarations or statements to check.
+
+ else
+ raise ECR_Found;
+ end if;
+ end if;
+ end Advance;
+
+ --------------------------
+ -- Enter_Handled_Body --
+ --------------------------
+
+ procedure Enter_Handled_Body (Curr : in out Node_Id) is
+ Decls : constant List_Id := Declarations (Curr);
+ HSS : constant Node_Id := Handled_Statement_Sequence (Curr);
+ Stmts : List_Id := No_List;
+
+ begin
+ if Present (HSS) then
+ Stmts := Statements (HSS);
+ end if;
+
+ -- The handled body has a non-empty statement sequence. The construct
+ -- to inspect is the last statement.
+
+ if Has_Suitable_Construct (Stmts) then
+ Curr := Last (Stmts);
+
+ -- The handled body lacks statements, but has non-empty declarations.
+ -- The construct to inspect is the last declaration.
+
+ elsif Has_Suitable_Construct (Decls) then
+ Curr := Last (Decls);
+
+ -- Otherwise the handled body lacks both declarations and statements.
+ -- The construct to inspect is the node which precedes the handled
+ -- body. Update the early call region to include the handled body.
+
+ else
+ Include (Curr, Curr);
+ end if;
+ end Enter_Handled_Body;
+
+ -------------------------------
+ -- Enter_Package_Declaration --
+ -------------------------------
+
+ procedure Enter_Package_Declaration (Curr : in out Node_Id) is
+ Pack_Spec : constant Node_Id := Specification (Curr);
+ Prv_Decls : constant List_Id := Private_Declarations (Pack_Spec);
+ Vis_Decls : constant List_Id := Visible_Declarations (Pack_Spec);
+
+ begin
+ -- The package has a non-empty private declarations. The construct to
+ -- inspect is the last private declaration.
+
+ if Has_Suitable_Construct (Prv_Decls) then
+ Curr := Last (Prv_Decls);
+
+ -- The package lacks private declarations, but has non-empty visible
+ -- declarations. In this case the construct to inspect is the last
+ -- visible declaration.
+
+ elsif Has_Suitable_Construct (Vis_Decls) then
+ Curr := Last (Vis_Decls);
+
+ -- Otherwise the package lacks any declarations. The construct to
+ -- inspect is the node which precedes the package. Update the early
+ -- call region to include the package declaration.
+
+ else
+ Include (Curr, Curr);
+ end if;
+ end Enter_Package_Declaration;
+
+ --------------
+ -- Find_ECR --
+ --------------
+
+ function Find_ECR (N : Node_Id) return Node_Id is
+ Curr : Node_Id;
+
+ begin
+ -- The early call region starts at N
+
+ Curr := Prev (N);
+ Start := N;
+
+ -- Inspect each node in reverse declarative order while going in and
+ -- out of nested and enclosing constructs. Note that the only way to
+ -- terminate this infinite loop is to raise exception ECR_Found.
+
+ loop
+ -- The current construct is not preelaboration-safe. Terminate the
+ -- traversal.
+
+ if Present (Curr)
+ and then not Is_OK_Preelaborable_Construct (Curr)
+ then
+ raise ECR_Found;
+ end if;
+
+ -- Advance to the next suitable construct. This may terminate the
+ -- traversal by raising ECR_Found.
+
+ Advance (Curr);
+ end loop;
+
+ exception
+ when ECR_Found =>
+ return Start;
+ end Find_ECR;
+
+ ----------------------------
+ -- Has_Suitable_Construct --
+ ----------------------------
+
+ function Has_Suitable_Construct (List : List_Id) return Boolean is
+ Item : Node_Id;
+
+ begin
+ -- Examine the list in reverse declarative order, looking for a
+ -- suitable construct.
+
+ if Present (List) then
+ Item := Last (List);
+ while Present (Item) loop
+ if Is_Suitable_Construct (Item) then
+ return True;
+ end if;
+
+ Prev (Item);
+ end loop;
+ end if;
+
+ return False;
+ end Has_Suitable_Construct;
+
+ -------------
+ -- Include --
+ -------------
+
+ procedure Include (N : Node_Id; Curr : in out Node_Id) is
+ begin
+ Start := N;
+ Curr := Prev (Start);
+ end Include;
+
+ -----------------------------------
+ -- Is_OK_Preelaborable_Construct --
+ -----------------------------------
+
+ function Is_OK_Preelaborable_Construct (N : Node_Id) return Boolean is
+ begin
+ -- Assignment statements are acceptable as long as they were produced
+ -- by the ABE mechanism to update elaboration flags.
+
+ if Nkind (N) = N_Assignment_Statement then
+ return Is_Elaboration_Code (N);
+
+ -- Block statements are acceptable even though they directly violate
+ -- preelaborability. The intention is not to penalize the early call
+ -- region when a block contains only preelaborable constructs.
+ --
+ -- declare
+ -- Val : constant Integer := 1;
+ -- begin
+ -- pragma Assert (Val = 1);
+ -- null;
+ -- end;
+ --
+ -- Note that the Advancement phase does enter blocks, and will detect
+ -- any non-preelaborable declarations or statements within.
+
+ elsif Nkind (N) = N_Block_Statement then
+ return True;
+ end if;
+
+ -- Otherwise the construct must be preelaborable. The check must take
+ -- the syntactic and semantic structure of the construct. DO NOT use
+ -- Is_Preelaborable_Construct here.
+
+ return not Is_Non_Preelaborable_Construct (N);
+ end Is_OK_Preelaborable_Construct;
+
+ ---------------------------
+ -- Is_Suitable_Construct --
+ ---------------------------
+
+ function Is_Suitable_Construct (N : Node_Id) return Boolean is
+ Context : constant Node_Id := Parent (N);
+
+ begin
+ -- An internally-generated statement sequence which contains only a
+ -- single null statement is not a suitable construct because it is a
+ -- byproduct of the parser. Such a null statement should be excluded
+ -- from the early call region because it carries the source location
+ -- of the "end" keyword, and may lead to confusing diagnistics.
+
+ if Nkind (N) = N_Null_Statement
+ and then not Comes_From_Source (N)
+ and then Present (Context)
+ and then Nkind (Context) = N_Handled_Sequence_Of_Statements
+ and then not Comes_From_Source (N)
+ then
+ return False;
+ end if;
+
+ -- Otherwise only constructs which correspond to pure Ada constructs
+ -- are considered suitable.
+
+ case Nkind (N) is
+ when N_Call_Marker
+ | N_Freeze_Entity
+ | N_Freeze_Generic_Entity
+ | N_Implicit_Label_Declaration
+ | N_Itype_Reference
+ | N_Pop_Constraint_Error_Label
+ | N_Pop_Program_Error_Label
+ | N_Pop_Storage_Error_Label
+ | N_Push_Constraint_Error_Label
+ | N_Push_Program_Error_Label
+ | N_Push_Storage_Error_Label
+ | N_SCIL_Dispatch_Table_Tag_Init
+ | N_SCIL_Dispatching_Call
+ | N_SCIL_Membership_Test
+ | N_Variable_Reference_Marker
+ =>
+ return False;
+
+ when others =>
+ return True;
+ end case;
+ end Is_Suitable_Construct;
+
+ ----------------------------------
+ -- Transition_Body_Declarations --
+ ----------------------------------
+
+ procedure Transition_Body_Declarations
+ (Bod : Node_Id;
+ Curr : in out Node_Id)
+ is
+ Decls : constant List_Id := Declarations (Bod);
+
+ begin
+ -- The search must come from the declarations of the body
+
+ pragma Assert
+ (Is_Non_Empty_List (Decls)
+ and then List_Containing (Start) = Decls);
+
+ -- The search finished inspecting the declarations. The construct
+ -- to inspect is the node which precedes the handled body, unless
+ -- the body is a compilation unit. The transitions are:
+ --
+ -- declarations -> upper level
+ -- declarations -> corresponding package spec (Elab_Body)
+ -- declarations -> terminate
+
+ Transition_Unit (Bod, Curr);
+ end Transition_Body_Declarations;
+
+ -----------------------------------
+ -- Transition_Handled_Statements --
+ -----------------------------------
+
+ procedure Transition_Handled_Statements
+ (HSS : Node_Id;
+ Curr : in out Node_Id)
+ is
+ Bod : constant Node_Id := Parent (HSS);
+ Decls : constant List_Id := Declarations (Bod);
+ Stmts : constant List_Id := Statements (HSS);
+
+ begin
+ -- The search must come from the statements of certain bodies or
+ -- statements.
+
+ pragma Assert (Nkind_In (Bod, N_Block_Statement,
+ N_Entry_Body,
+ N_Package_Body,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body));
+
+ -- The search must come from the statements of the handled sequence
+
+ pragma Assert
+ (Is_Non_Empty_List (Stmts)
+ and then List_Containing (Start) = Stmts);
+
+ -- The search finished inspecting the statements. The handled body
+ -- has non-empty declarations. The construct to inspect is the last
+ -- declaration. The transitions are:
+ --
+ -- statements -> declarations
+
+ if Has_Suitable_Construct (Decls) then
+ Curr := Last (Decls);
+
+ -- Otherwise the handled body lacks declarations. The construct to
+ -- inspect is the node which precedes the handled body, unless the
+ -- body is a compilation unit. The transitions are:
+ --
+ -- statements -> upper level
+ -- statements -> corresponding package spec (Elab_Body)
+ -- statements -> terminate
+
+ else
+ Transition_Unit (Bod, Curr);
+ end if;
+ end Transition_Handled_Statements;
+
+ ----------------------------------
+ -- Transition_Spec_Declarations --
+ ----------------------------------
+
+ procedure Transition_Spec_Declarations
+ (Spec : Node_Id;
+ Curr : in out Node_Id)
+ is
+ Prv_Decls : constant List_Id := Private_Declarations (Spec);
+ Vis_Decls : constant List_Id := Visible_Declarations (Spec);
+
+ begin
+ pragma Assert (Present (Start) and then Is_List_Member (Start));
+
+ -- The search came from the private declarations and finished their
+ -- inspection.
+
+ if Has_Suitable_Construct (Prv_Decls)
+ and then List_Containing (Start) = Prv_Decls
+ then
+ -- The context has non-empty visible declarations. The node to
+ -- inspect is the last visible declaration. The transitions are:
+ --
+ -- private declarations -> visible declarations
+
+ if Has_Suitable_Construct (Vis_Decls) then
+ Curr := Last (Vis_Decls);
+
+ -- Otherwise the context lacks visible declarations. The construct
+ -- to inspect is the node which precedes the context unless the
+ -- context is a compilation unit. The transitions are:
+ --
+ -- private declarations -> upper level
+ -- private declarations -> terminate
+
+ else
+ Transition_Unit (Parent (Spec), Curr);
+ end if;
+
+ -- The search came from the visible declarations and finished their
+ -- inspections. The construct to inspect is the node which precedes
+ -- the context, unless the context is a compilaton unit. The
+ -- transitions are:
+ --
+ -- visible declarations -> upper level
+ -- visible declarations -> terminate
+
+ elsif Has_Suitable_Construct (Vis_Decls)
+ and then List_Containing (Start) = Vis_Decls
+ then
+ Transition_Unit (Parent (Spec), Curr);
+
+ -- At this point both declarative lists are empty, but the traversal
+ -- still came from within the spec. This indicates that the invariant
+ -- of the algorithm has been violated.
+
+ else
+ pragma Assert (False);
+ raise ECR_Found;
+ end if;
+ end Transition_Spec_Declarations;
+
+ ---------------------
+ -- Transition_Unit --
+ ---------------------
+
+ procedure Transition_Unit
+ (Unit : Node_Id;
+ Curr : in out Node_Id)
+ is
+ Context : constant Node_Id := Parent (Unit);
+
+ begin
+ -- The unit is a compilation unit. This terminates the search because
+ -- there are no more lists to inspect and there are no more enclosing
+ -- constructs to climb up to.
+
+ if Nkind (Context) = N_Compilation_Unit then
+
+ -- A package body with a corresponding spec subject to pragma
+ -- Elaborate_Body is an exception to the above. The annotation
+ -- allows the search to continue into the package declaration.
+ -- The transitions are:
+ --
+ -- statements -> corresponding package spec (Elab_Body)
+ -- declarations -> corresponding package spec (Elab_Body)
+
+ if Nkind (Unit) = N_Package_Body
+ and then (Assume_Elab_Body
+ or else Has_Pragma_Elaborate_Body
+ (Corresponding_Spec (Unit)))
+ then
+ Curr := Unit_Declaration_Node (Corresponding_Spec (Unit));
+ Enter_Package_Declaration (Curr);
+
+ -- Otherwise terminate the search. The transitions are:
+ --
+ -- private declarations -> terminate
+ -- visible declarations -> terminate
+ -- statements -> terminate
+ -- declarations -> terminate
+
+ else
+ raise ECR_Found;
+ end if;
+
+ -- The unit is a subunit. The construct to inspect is the node which
+ -- precedes the corresponding stub. Update the early call region to
+ -- include the unit.
+
+ elsif Nkind (Context) = N_Subunit then
+ Start := Unit;
+ Curr := Corresponding_Stub (Context);
+
+ -- Otherwise the unit is nested. The construct to inspect is the node
+ -- which precedes the unit. Update the early call region to include
+ -- the unit.
+
+ else
+ Include (Unit, Curr);
+ end if;
+ end Transition_Unit;
+
+ -- Local variables
+
+ Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+ Region : Node_Id;
+
+ -- Start of processing for Find_Early_Call_Region
+
+ begin
+ -- The caller demands the start of the early call region without saving
+ -- or retrieving it to/from internal data structures.
+
+ if Skip_Memoization then
+ Region := Find_ECR (Body_Decl);
+
+ -- Default behavior
+
+ else
+ -- Check whether the early call region of the subprogram body is
+ -- available.
+
+ Region := Early_Call_Region (Body_Id);
+
+ if No (Region) then
+
+ -- Traverse the declarations in reverse order, starting from the
+ -- subprogram body, searching for the nearest non-preelaborable
+ -- construct. The early call region starts after this construct
+ -- and ends at the subprogram body.
+
+ Region := Find_ECR (Body_Decl);
+
+ -- Associate the early call region with the subprogram body in
+ -- case other scenarios need it.
+
+ Set_Early_Call_Region (Body_Id, Region);
+ end if;
+ end if;
+
+ -- A subprogram body must always have an early call region
+
+ pragma Assert (Present (Region));
+
+ return Region;
+ end Find_Early_Call_Region;
+
---------------------------
-- Find_Elaborated_Units --
---------------------------
return;
end if;
- Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+ Elab_Attrs := Elaboration_Status (Unit_Id);
- -- The current unit is not part of the context. Prepare a new set of
- -- attributes.
+ -- The unit is already included in the context by means of pragma
+ -- Elaborate[_All].
- if Elab_Attrs = No_Elaboration_Attributes then
- Elab_Attrs :=
- Elaboration_Attributes'(Source_Pragma => Prag,
- With_Clause => Empty);
+ if Present (Elab_Attrs.Source_Pragma) then
- -- 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.
+ -- Upgrade an existing pragma Elaborate when the unit is subject
+ -- to Elaborate_All because the new pragma covers a larger set of
+ -- units.
- elsif Pragma_Name (Elab_Attrs.Source_Pragma) = Name_Elaborate
- and then Pragma_Name (Prag) = Name_Elaborate_All
- then
- Elab_Attrs.Source_Pragma := Prag;
+ if 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 retains its existing pragma and does not
+ -- need to be included in the context again.
+
+ else
+ return;
+ end if;
- -- Otherwise the unit is already included in the context
+ -- The current unit is not part of the context. Prepare a new set of
+ -- attributes.
else
- return;
+ Elab_Attrs :=
+ Elaboration_Attributes'(Source_Pragma => Prag,
+ With_Clause => Empty);
end if;
-- Add or update the attributes of the unit
- Elaboration_Context.Set (Unit_Id, Elab_Attrs);
+ Set_Elaboration_Status (Unit_Id, Elab_Attrs);
-- Includes all units withed by the current one when computing the
-- full context.
-- main unit. Consider this case only when requested by the caller.
elsif Context_OK
- and then Elaboration_Context.Get (Unit_Id) /= No_Elaboration_Attributes
+ and then Elaboration_Status (Unit_Id) /= No_Elaboration_Attributes
then
return True;
if Nkind (Par) = N_Subunit then
Par := Corresponding_Stub (Par);
- -- Stop the traversal when the nearest enclosing non-library level
+ -- Stop the traversal when the nearest enclosing non-library-level
-- encapsulator has been reached.
elsif Is_Non_Library_Level_Encapsulator (Par) then
and then Present (Protected_Subprogram (Id));
end Is_Protected_Body_Subp;
+ --------------------------------
+ -- Is_Recorded_SPARK_Scenario --
+ --------------------------------
+
+ function Is_Recorded_SPARK_Scenario (N : Node_Id) return Boolean is
+ begin
+ if Recorded_SPARK_Scenarios_In_Use then
+ return Recorded_SPARK_Scenarios.Get (N);
+ end if;
+
+ return Recorded_SPARK_Scenarios_No_Element;
+ end Is_Recorded_SPARK_Scenario;
+
------------------------------------
-- Is_Recorded_Top_Level_Scenario --
------------------------------------
function Is_Recorded_Top_Level_Scenario (N : Node_Id) return Boolean is
begin
- return Recorded_Top_Level_Scenarios.Get (N);
+ if Recorded_Top_Level_Scenarios_In_Use then
+ return Recorded_Top_Level_Scenarios.Get (N);
+ end if;
+
+ return Recorded_Top_Level_Scenarios_No_Element;
end Is_Recorded_Top_Level_Scenario;
------------------------
function Is_Suitable_Scenario (N : Node_Id) return Boolean is
begin
+ -- NOTE: Derived types and pragma Refined_State are intentionally left
+ -- out because they are not executable during elaboration.
+
return
Is_Suitable_Access (N)
or else Is_Suitable_Call (N)
or else Is_Suitable_Variable_Reference (N);
end Is_Suitable_Scenario;
+ ------------------------------------
+ -- Is_Suitable_SPARK_Derived_Type --
+ ------------------------------------
+
+ function Is_Suitable_SPARK_Derived_Type (N : Node_Id) return Boolean is
+ Prag : Node_Id;
+ Typ : Entity_Id;
+
+ begin
+ -- To qualify, the type declaration must denote a derived tagged type
+ -- with primitive operations, subject to pragma SPARK_Mode On.
+
+ if Nkind (N) = N_Full_Type_Declaration
+ and then Nkind (Type_Definition (N)) = N_Derived_Type_Definition
+ then
+ Typ := Defining_Entity (N);
+ Prag := SPARK_Pragma (Typ);
+
+ return
+ Is_Tagged_Type (Typ)
+ and then Has_Primitive_Operations (Typ)
+ and then Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On;
+ end if;
+
+ return False;
+ end Is_Suitable_SPARK_Derived_Type;
+
+ -------------------------------------
+ -- Is_Suitable_SPARK_Instantiation --
+ -------------------------------------
+
+ function Is_Suitable_SPARK_Instantiation (N : Node_Id) return Boolean is
+ Gen_Attrs : Target_Attributes;
+ Gen_Id : Entity_Id;
+ Inst : Node_Id;
+ Inst_Attrs : Instantiation_Attributes;
+ Inst_Id : Entity_Id;
+
+ begin
+ -- To qualify, both the instantiation and the generic must be subject to
+ -- SPARK_Mode On.
+
+ if Is_Suitable_Instantiation (N) then
+ Extract_Instantiation_Attributes
+ (Exp_Inst => N,
+ Inst => Inst,
+ Inst_Id => Inst_Id,
+ Gen_Id => Gen_Id,
+ Attrs => Inst_Attrs);
+
+ Extract_Target_Attributes (Gen_Id, Gen_Attrs);
+
+ return Inst_Attrs.SPARK_Mode_On and Gen_Attrs.SPARK_Mode_On;
+ end if;
+
+ return False;
+ end Is_Suitable_SPARK_Instantiation;
+
+ --------------------------------------------
+ -- Is_Suitable_SPARK_Refined_State_Pragma --
+ --------------------------------------------
+
+ function Is_Suitable_SPARK_Refined_State_Pragma
+ (N : Node_Id) return Boolean
+ is
+ begin
+ -- To qualfy, the pragma must denote Refined_State
+
+ return
+ Nkind (N) = N_Pragma
+ and then Pragma_Name (N) = Name_Refined_State;
+ end Is_Suitable_SPARK_Refined_State_Pragma;
+
-------------------------------------
-- Is_Suitable_Variable_Assignment --
-------------------------------------
return False;
end Is_Up_Level_Target;
+ ---------------------
+ -- Is_Visited_Body --
+ ---------------------
+
+ function Is_Visited_Body (Body_Decl : Node_Id) return Boolean is
+ begin
+ if Visited_Bodies_In_Use then
+ return Visited_Bodies.Get (Body_Decl);
+ end if;
+
+ return Visited_Bodies_No_Element;
+ end Is_Visited_Body;
+
-------------------------------
-- Kill_Elaboration_Scenario --
-------------------------------
procedure Kill_Elaboration_Scenario (N : Node_Id) is
- package Scenarios renames Top_Level_Scenarios;
+ procedure Kill_SPARK_Scenario;
+ pragma Inline (Kill_SPARK_Scenario);
+ -- Eliminate scenario N from table SPARK_Scenarios if it is recorded
+ -- there.
- begin
- -- Eliminate a recorded top-level scenario when it appears within dead
- -- code because it will not be executed at elaboration time.
+ procedure Kill_Top_Level_Scenario;
+ pragma Inline (Kill_Top_Level_Scenario);
+ -- Eliminate scenario N from table Top_Level_Scenarios if it is recorded
+ -- there.
- if Is_Scenario (N)
- and then Is_Recorded_Top_Level_Scenario (N)
- then
- -- Performance node: list traversal
+ -------------------------
+ -- Kill_SPARK_Scenario --
+ -------------------------
- for Index in Scenarios.First .. Scenarios.Last loop
- if Scenarios.Table (Index) = N then
- Scenarios.Table (Index) := Empty;
+ procedure Kill_SPARK_Scenario is
+ package Scenarios renames SPARK_Scenarios;
- -- The top-level scenario is no longer recorded
+ begin
+ if Is_Recorded_SPARK_Scenario (N) then
- Set_Is_Recorded_Top_Level_Scenario (N, False);
- return;
- end if;
- end loop;
+ -- Performance note: list traversal
+
+ for Index in Scenarios.First .. Scenarios.Last loop
+ if Scenarios.Table (Index) = N then
+ Scenarios.Table (Index) := Empty;
+
+ -- The SPARK scenario is no longer recorded
+
+ Set_Is_Recorded_SPARK_Scenario (N, False);
+ return;
+ end if;
+ end loop;
+
+ -- A recorded SPARK scenario must be in the table of recorded
+ -- SPARK scenarios.
+
+ pragma Assert (False);
+ end if;
+ end Kill_SPARK_Scenario;
+
+ -----------------------------
+ -- Kill_Top_Level_Scenario --
+ -----------------------------
+
+ procedure Kill_Top_Level_Scenario is
+ package Scenarios renames Top_Level_Scenarios;
+
+ begin
+ if Is_Recorded_Top_Level_Scenario (N) then
+
+ -- Performance node: list traversal
+
+ for Index in Scenarios.First .. Scenarios.Last loop
+ if Scenarios.Table (Index) = N then
+ Scenarios.Table (Index) := Empty;
+
+ -- The top-level scenario is no longer recorded
+
+ Set_Is_Recorded_Top_Level_Scenario (N, False);
+ return;
+ end if;
+ end loop;
+
+ -- A recorded top-level scenario must be in the table of recorded
+ -- top-level scenarios.
+
+ pragma Assert (False);
+ end if;
+ end Kill_Top_Level_Scenario;
- -- A recorded top-level scenario must be in the table of recorded
- -- top-level scenarios.
+ -- Start of processing for Kill_Elaboration_Scenario
+
+ begin
+ -- Eliminate a recorded scenario when it appears within dead code
+ -- because it will not be executed at elaboration time.
- pragma Assert (False);
+ if Is_Scenario (N) then
+ Kill_SPARK_Scenario;
+ Kill_Top_Level_Scenario;
end if;
end Kill_Elaboration_Scenario;
Info_Msg => False,
In_SPARK => True);
+ elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+ Error_Msg_N
+ ("read of refinement constituents during elaboration in SPARK",
+ N);
+
elsif Is_Suitable_Variable_Reference (N) then
Info_Variable_Reference
(Ref => N,
-- enough to meet the requirement.
else
- Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+ Elab_Attrs := Elaboration_Status (Unit_Id);
-- The pragma must be either Elaborate_All or be as strong as the
-- requirement.
procedure Output_Instantiation (N : Node_Id);
-- Emit a specific diagnostic message for instantiation N
+ procedure Output_SPARK_Refined_State_Pragma (N : Node_Id);
+ -- Emit a specific diagnostic message for Refined_State pragma N
+
procedure Output_Variable_Assignment (N : Node_Id);
-- Emit a specific diagnostic message for assignment statement N
end if;
end Output_Instantiation;
+ ---------------------------------------
+ -- Output_SPARK_Refined_State_Pragma --
+ ---------------------------------------
+
+ procedure Output_SPARK_Refined_State_Pragma (N : Node_Id) is
+ begin
+ Error_Msg_Sloc := Sloc (N);
+ Error_Msg_N ("\\ refinement constituents read #", Error_Nod);
+ end Output_SPARK_Refined_State_Pragma;
+
--------------------------------
-- Output_Variable_Assignment --
--------------------------------
if Is_Read (N) then
Error_Msg_NE ("\\ variable & read #", Error_Nod, Var_Id);
+
+ else
+ pragma Assert (False);
+ null;
end if;
end Output_Variable_Reference;
elsif Is_Suitable_Instantiation (N) then
Output_Instantiation (N);
+ -- Pragma Refined_State
+
+ elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+ Output_SPARK_Refined_State_Pragma (N);
+
-- Variable assignments
elsif Nkind (N) = N_Assignment_Statement then
Scenario_Stack.Decrement_Last;
end Pop_Active_Scenario;
- --------------------
- -- Process_Access --
- --------------------
+ --------------------------------
+ -- Process_Activation_Generic --
+ --------------------------------
+
+ procedure Process_Activation_Generic
+ (Call : Node_Id;
+ Call_Attrs : Call_Attributes;
+ In_Init_Cond : Boolean;
+ In_Partial_Fin : Boolean;
+ 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_Init_Cond => In_Init_Cond,
+ In_Partial_Fin => In_Partial_Fin,
+ 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_Generic
+
+ 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_Generic;
+
+ ------------------------------------
+ -- Process_Conditional_ABE_Access --
+ ------------------------------------
- procedure Process_Access
+ procedure Process_Conditional_ABE_Access
(Attr : Node_Id;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean)
is
Target_Attrs : Target_Attributes;
- -- Start of processing for Process_Access
+ -- Start of processing for Process_Conditional_ABE_Access
begin
-- Output relevant information when switch -gnatel (info messages on
-- the target is ensured processing the corresponding call marker.
if Debug_Flag_Dot_O then
- Process_Scenario
+ Process_Conditional_ABE
(N => Build_Access_Marker (Target_Id),
+ In_Init_Cond => In_Init_Cond,
In_Partial_Fin => In_Partial_Fin,
In_Task_Body => In_Task_Body);
Ensure_Prior_Elaboration
(N => Attr,
Unit_Id => Target_Attrs.Unit_Id,
+ Prag_Nam => Name_Elaborate_All,
In_Partial_Fin => In_Partial_Fin,
In_Task_Body => In_Task_Body);
end if;
- end Process_Access;
+ end Process_Conditional_ABE_Access;
- -----------------------------
- -- Process_Activation_Call --
- -----------------------------
+ ---------------------------------------------
+ -- Process_Conditional_ABE_Activation_Impl --
+ ---------------------------------------------
- procedure Process_Activation_Call
+ procedure Process_Conditional_ABE_Activation_Impl
(Call : Node_Id;
Call_Attrs : Call_Attributes;
+ Obj_Id : Entity_Id;
+ Task_Attrs : Task_Attributes;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
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.
+ 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.
- procedure Process_Task_Objects (List : List_Id);
- -- Perform ABE checks and diagnostics for all task objects found in
- -- the list List.
+ Root : constant Node_Id := Root_Scenario;
- -------------------------
- -- Process_Task_Object --
- -------------------------
+ begin
+ -- Output relevant information when switch -gnatel (info messages on
+ -- implicit Elaborate[_All] pragmas) is in effect.
- procedure Process_Task_Object (Obj_Id : Entity_Id; Typ : Entity_Id) is
- Base_Typ : constant Entity_Id := Base_Type (Typ);
+ 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
+
+ -- Do not emit any ABE diagnostics when the activation occurs in
+ -- a partial finalization context because this leads to confusing
+ -- noise.
+
+ if In_Partial_Fin then
+ null;
+
+ -- 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.
+
+ elsif 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,
+ Prag_Nam => Name_Elaborate_All,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
+ end if;
+
+ Traverse_Body
+ (N => Task_Attrs.Body_Decl,
+ In_Init_Cond => In_Init_Cond,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => True);
+ end Process_Conditional_ABE_Activation_Impl;
+
+ procedure Process_Conditional_ABE_Activation is
+ new Process_Activation_Generic (Process_Conditional_ABE_Activation_Impl);
+
+ ----------------------------------
+ -- Process_Conditional_ABE_Call --
+ ----------------------------------
+
+ procedure Process_Conditional_ABE_Call
+ (Call : Node_Id;
+ Call_Attrs : Call_Attributes;
+ Target_Id : Entity_Id;
+ In_Init_Cond : Boolean;
+ In_Partial_Fin : Boolean;
+ 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,
+ -- primitive [Deep_]Initialize, or a block created for initialization
+ -- purposes.
+
+ function Is_Partial_Finalization_Proc return Boolean;
+ pragma Inline (Is_Partial_Finalization_Proc);
+ -- Determine whether call Call with target Target_Id invokes a partial
+ -- finalization procedure.
+
+ -------------------------------
+ -- In_Initialization_Context --
+ -------------------------------
- Comp_Id : Entity_Id;
- Task_Attrs : Task_Attributes;
+ function In_Initialization_Context (N : Node_Id) return Boolean is
+ Par : Node_Id;
+ Spec_Id : Entity_Id;
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_Partial_Fin => In_Partial_Fin,
- In_Task_Body => In_Task_Body);
+ -- Climb the parent chain looking for initialization actions
- -- Examine the component type when the object is an array
+ Par := Parent (N);
+ while Present (Par) loop
- elsif Is_Array_Type (Typ) and then Has_Task (Base_Typ) then
- Process_Task_Object (Obj_Id, Component_Type (Typ));
+ -- A block may be part of the initialization actions of a default
+ -- initialized object.
- -- Examine individual component types when the object is a record
+ if Nkind (Par) = N_Block_Statement
+ and then Is_Initialization_Block (Par)
+ then
+ return True;
- 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;
+ -- A subprogram body may denote an initialization routine
- --------------------------
- -- Process_Task_Objects --
- --------------------------
+ elsif Nkind (Par) = N_Subprogram_Body then
+ Spec_Id := Unique_Defining_Entity (Par);
- procedure Process_Task_Objects (List : List_Id) is
- Item : Node_Id;
- Item_Id : Entity_Id;
- Item_Typ : Entity_Id;
+ -- The current subprogram body denotes a type init proc or
+ -- primitive [Deep_]Initialize.
- begin
- -- Examine the contents of the list looking for an object declaration
- -- of a task type or one that contains a task within.
+ 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;
- Item := First (List);
- while Present (Item) loop
- if Nkind (Item) = N_Object_Declaration then
- Item_Id := Defining_Entity (Item);
- Item_Typ := Etype (Item_Id);
+ -- Prevent the search from going too far
- if Has_Task (Item_Typ) then
- Process_Task_Object (Item_Id, Item_Typ);
- end if;
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
end if;
- Next (Item);
+ Par := Parent (Par);
end loop;
- end Process_Task_Objects;
-
- -- Local variables
- Context : Node_Id;
- Spec : Node_Id;
+ return False;
+ end In_Initialization_Context;
- -- Start of processing for Process_Activation_Call
+ ----------------------------------
+ -- Is_Partial_Finalization_Proc --
+ ----------------------------------
- begin
- -- Nothing to do when the activation is a guaranteed ABE
+ function Is_Partial_Finalization_Proc return Boolean is
+ begin
+ -- To qualify, the target must denote primitive [Deep_]Finalize or a
+ -- finalizer procedure, and the call must appear in an initialization
+ -- context.
- if Is_Known_Guaranteed_ABE (Call) then
- return;
- end if;
+ return
+ (Is_Controlled_Proc (Target_Id, Name_Finalize)
+ or else Is_Finalizer_Proc (Target_Id)
+ or else Is_TSS (Target_Id, TSS_Deep_Finalize))
+ and then In_Initialization_Context (Call);
+ end Is_Partial_Finalization_Proc;
- -- 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.
+ -- Local variables
- Context := Parent (Call);
+ Init_Cond_On : Boolean;
+ Partial_Fin_On : Boolean;
+ SPARK_Rules_On : Boolean;
+ Target_Attrs : Target_Attributes;
- -- 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.
+ -- Start of processing for Process_Conditional_ABE_Call
- if Nkind (Context) = N_Handled_Sequence_Of_Statements
- and then Nkind (Parent (Context)) = N_Package_Body
- then
- Context := Parent (Context);
- end if;
+ begin
+ Extract_Target_Attributes
+ (Target_Id => Target_Id,
+ Attrs => Target_Attrs);
- -- Process all task objects defined in both the spec and body when the
- -- activation call precedes the "begin" of a package body.
+ -- The call occurs in an initial condition context when a prior
+ -- scenario is already in that mode, or when the target denotes
+ -- an Initial_Condition procedure.
- if Nkind (Context) = N_Package_Body then
- Spec :=
- Specification
- (Unit_Declaration_Node (Corresponding_Spec (Context)));
+ Init_Cond_On :=
+ In_Init_Cond or else Is_Initial_Condition_Proc (Target_Id);
- Process_Task_Objects (Visible_Declarations (Spec));
- Process_Task_Objects (Private_Declarations (Spec));
- Process_Task_Objects (Declarations (Context));
+ -- The call occurs in a partial finalization context when a prior
+ -- scenario is already in that mode, or when the target denotes a
+ -- [Deep_]Finalize primitive or a finalizer within an initialization
+ -- context.
- -- Process all task objects defined in the spec when the activation call
- -- appears at the end of a package spec.
+ Partial_Fin_On := In_Partial_Fin or else Is_Partial_Finalization_Proc;
- elsif Nkind (Context) = N_Package_Specification then
- Process_Task_Objects (Visible_Declarations (Context));
- Process_Task_Objects (Private_Declarations (Context));
+ -- The SPARK rules are in effect when both the call and target are
+ -- subject to SPARK_Mode On.
- -- 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.
+ SPARK_Rules_On :=
+ Call_Attrs.SPARK_Mode_On and Target_Attrs.SPARK_Mode_On;
- else
- pragma Assert (Nkind (Context) = N_Handled_Sequence_Of_Statements);
+ -- Output relevant information when switch -gnatel (info messages on
+ -- implicit Elaborate[_All] pragmas) is in effect.
- Process_Task_Objects (Statements (Context));
+ if Elab_Info_Messages then
+ Info_Call
+ (Call => Call,
+ Target_Id => Target_Id,
+ Info_Msg => True,
+ In_SPARK => SPARK_Rules_On);
end if;
- end Process_Activation_Call;
- ---------------------------------------------
- -- Process_Activation_Conditional_ABE_Impl --
- ---------------------------------------------
+ -- Check whether the invocation of an entry clashes with an existing
+ -- restriction.
- procedure Process_Activation_Conditional_ABE_Impl
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Obj_Id : Entity_Id;
- Task_Attrs : Task_Attributes;
- In_Partial_Fin : Boolean;
- 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.
+ if Is_Protected_Entry (Target_Id) then
+ Check_Restriction (No_Entry_Calls_In_Elaboration_Code, Call);
- Root : constant Node_Id := Root_Scenario;
+ elsif Is_Task_Entry (Target_Id) then
+ Check_Restriction (No_Entry_Calls_In_Elaboration_Code, Call);
- begin
- -- Output relevant information when switch -gnatel (info messages on
- -- implicit Elaborate[_All] pragmas) is in effect.
+ -- Task entry calls are never processed because the entry being
+ -- invoked does not have a corresponding "body", it has a select.
- if Elab_Info_Messages then
- Error_Msg_NE
- ("info: activation of & during elaboration", Call, Obj_Id);
+ return;
end if;
- -- Nothing to do when the activation is a guaranteed ABE
+ -- 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 task is in the same unit, but outside this context.
+ -- Nothing to do when the root scenario appears at the declaration level
+ -- and the target is in the same unit, but outside this context.
- -- task type Task_Typ; -- task declaration
+ -- function B ...; -- target declaration
-- procedure Proc is
-- function A ... is
-- begin
-- if Some_Condition then
- -- declare
- -- T : Task_Typ;
- -- begin
- -- <activation call> -- activation site
- -- end;
+ -- return B; -- call site
-- ...
-- end A;
-- X : ... := A; -- root scenario
-- ...
- -- task body Task_Typ is
+ -- function B ... is
-- ...
- -- end Task_Typ;
+ -- 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 in effect. Note that -gnatd.v (enforce SPARK
+ -- elaboration rules in SPARK code) is intentionally not taken into
+ -- account here because Process_Conditional_ABE_Call_SPARK has two
+ -- separate modes of operation.
+
+ elsif SPARK_Rules_On then
+ Process_Conditional_ABE_Call_SPARK
+ (Call => Call,
+ Target_Id => Target_Id,
+ Target_Attrs => Target_Attrs,
+ In_Init_Cond => Init_Cond_On,
+ In_Partial_Fin => Partial_Fin_On,
+ In_Task_Body => In_Task_Body);
+
+ -- Otherwise the Ada rules are in effect
+
+ else
+ Process_Conditional_ABE_Call_Ada
+ (Call => Call,
+ Call_Attrs => Call_Attrs,
+ Target_Id => Target_Id,
+ Target_Attrs => Target_Attrs,
+ In_Partial_Fin => Partial_Fin_On,
+ In_Task_Body => In_Task_Body);
+ end if;
+
+ -- Inspect the target body (and barried function) for other suitable
+ -- elaboration scenarios.
+
+ Traverse_Body
+ (N => Target_Attrs.Body_Barf,
+ In_Init_Cond => Init_Cond_On,
+ In_Partial_Fin => Partial_Fin_On,
+ In_Task_Body => In_Task_Body);
+
+ Traverse_Body
+ (N => Target_Attrs.Body_Decl,
+ In_Init_Cond => Init_Cond_On,
+ In_Partial_Fin => Partial_Fin_On,
+ In_Task_Body => In_Task_Body);
+ end Process_Conditional_ABE_Call;
+
+ --------------------------------------
+ -- Process_Conditional_ABE_Call_Ada --
+ --------------------------------------
+
+ procedure Process_Conditional_ABE_Call_Ada
+ (Call : Node_Id;
+ Call_Attrs : Call_Attributes;
+ Target_Id : Entity_Id;
+ Target_Attrs : Target_Attributes;
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean)
+ 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.
- -- 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.
+ Root : constant Node_Id := Root_Scenario;
- -- Performance note: parent traversal
+ 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.
- elsif Is_Up_Level_Target (Task_Attrs.Task_Decl) then
+ if Call_Attrs.Is_Dispatching then
return;
- -- Nothing to do when the activation is ABE-safe
+ -- Nothing to do when the call is ABE-safe
-- generic
- -- package Gen is
- -- task type Task_Typ;
- -- end Gen;
+ -- function Gen ...;
- -- package body Gen is
- -- task body Task_Typ is
- -- begin
- -- ...
- -- end Task_Typ;
+ -- function Gen ... is
+ -- begin
+ -- ...
-- 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;
+ -- function Inst is new Gen;
+ -- X : ... := Inst; -- safe call
-- ...
- elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then
-
- -- Note that the task body must still be examined for any nested
- -- scenarios.
-
- null;
+ elsif Is_Safe_Call (Call, Target_Attrs) then
+ return;
- -- The activation call and the task body are both in the main unit
+ -- The call and the target body are both in the main unit
- elsif Present (Task_Attrs.Body_Decl)
- and then In_Extended_Main_Code_Unit (Task_Attrs.Body_Decl)
+ elsif Present (Target_Attrs.Body_Decl)
+ and then In_Extended_Main_Code_Unit (Target_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.
+ -- If the root scenario appears prior to the target body, then this
+ -- is a possible ABE with respect to the root scenario.
- -- task type Task_Typ;
+ -- function B ...;
-- 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;
+ -- return B; -- call site
-- ...
-- end A;
- -- X : ... := A; -- root scenario
+ -- X : ... := A; -- root scenario
- -- task body Task_Typ is -- task body
+ -- function B ... is -- target body
-- ...
- -- end Task_Typ;
+ -- end B;
- -- Y : ... := A; -- root scenario
+ -- 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.
+ -- 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, Task_Attrs.Body_Decl) then
+ if Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl) then
- -- Do not emit any ABE diagnostics when the activation occurs in
- -- a partial finalization context because this leads to confusing
+ -- Do not emit any ABE diagnostics when the call occurs in a
+ -- partial finalization context because this leads to confusing
-- noise.
if In_Partial_Fin then
-- noise.
elsif 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);
+ 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 (Obj_Id);
+ Output_Active_Scenarios (Call);
end if;
-- Install a conditional run-time ABE check to verify that the
- -- task body has been elaborated prior to the activation call.
+ -- target body has been elaborated prior to the 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);
+ Target_Id => Target_Attrs.Spec_Id,
+ Target_Decl => Target_Attrs.Spec_Decl,
+ Target_Body => Target_Attrs.Body_Decl);
end if;
end if;
- -- Otherwise the task body is not available in this compilation or it
+ -- 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 task body has been elaborated prior to the activation call
- -- when the dynamic model is in effect.
+ -- 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 => Task_Attrs.Unit_Id);
+ Id => Target_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.
+ -- Ensure that the unit with the target body is elaborated prior to the
+ -- main unit. The implicit Elaborate[_All] is generated only when the
+ -- call has elaboration checks enabled. This behaviour parallels that of
+ -- the old ABE mechanism.
- else
+ if Call_Attrs.Elab_Checks_OK then
Ensure_Prior_Elaboration
(N => Call,
- Unit_Id => Task_Attrs.Unit_Id,
+ Unit_Id => Target_Attrs.Unit_Id,
+ Prag_Nam => Name_Elaborate_All,
In_Partial_Fin => In_Partial_Fin,
In_Task_Body => In_Task_Body);
end if;
+ end Process_Conditional_ABE_Call_Ada;
- Traverse_Body
- (N => Task_Attrs.Body_Decl,
- In_Partial_Fin => In_Partial_Fin,
- 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 --
- --------------------------------------------
+ ----------------------------------------
+ -- Process_Conditional_ABE_Call_SPARK --
+ ----------------------------------------
- procedure Process_Activation_Guaranteed_ABE_Impl
+ procedure Process_Conditional_ABE_Call_SPARK
(Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Obj_Id : Entity_Id;
- Task_Attrs : Task_Attributes;
+ Target_Id : Entity_Id;
+ Target_Attrs : Target_Attributes;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean)
is
- pragma Unreferenced (Call_Attrs);
- pragma Unreferenced (In_Partial_Fin);
- 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.
+ Region : Node_Id;
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;
+ -- The call and the target body are both in the main unit
- -- with Gen;
- -- procedure Main is
- -- package Nested is
- -- ...
- -- end Nested;
+ if Present (Target_Attrs.Body_Decl)
+ and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
+ then
+ -- If the call appears prior to the target body, then the call must
+ -- appear within the early call region of the target body.
- -- package body Nested is
- -- package Inst is new Gen;
- -- T : Inst.Task_Typ;
- -- [begin]
- -- <activation call> -- safe activation
- -- end Nested;
- -- ...
+ -- function B ...;
- elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then
- return;
+ -- X : ... := B; -- call site
- -- 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.
+ -- <preelaborable construct 1> --+
+ -- ... | early call region
+ -- <preelaborable construct N> --+
- -- procedure Guaranteed_ABE is
- -- task type Task_Typ;
+ -- function B ... is -- target body
+ -- ...
+ -- end B;
+
+ -- When the call to B is not nested within some other scenario, the
+ -- call is automatically illegal because it can never appear in the
+ -- early call region of B's body. This is equivalent to a guaranteed
+ -- ABE.
+
+ -- <preelaborable construct 1> --+
+ -- |
+ -- function B ...; |
+ -- |
+ -- function A ... is |
+ -- begin | early call region
+ -- if Some_Condition then
+ -- return B; -- call site
+ -- ...
+ -- end A; |
+ -- |
+ -- <preelaborable construct N> --+
- -- package Nested is
- -- ...
- -- end Nested;
+ -- function B ... is -- target body
+ -- ...
+ -- end B;
- -- package body Nested is
- -- T : Task_Typ;
- -- [begin]
- -- <activation call> -- guaranteed ABE
- -- end Nested;
+ -- When the call to B is nested within some other scenario, the call
+ -- is always ABE-safe. It is not immediately obvious why this is the
+ -- case. The elaboration safety follows from the early call region
+ -- rule being applied to ALL calls preceding their associated bodies.
- -- task body Task_Typ is
- -- ...
- -- end Task_Typ;
- -- ...
+ -- In the example above, the call to B is safe as long as the call to
+ -- A is safe. There are several cases to consider:
- -- Performance note: parent traversal
+ -- <call 1 to A>
+ -- function B ...;
- 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);
+ -- <call 2 to A>
+ -- function A ... is
+ -- begin
+ -- if Some_Condition then
+ -- return B;
+ -- ...
+ -- end A;
- -- Mark the activation call as a guaranteed ABE
+ -- <call 3 to A>
+ -- function B ... is
+ -- ...
+ -- end B;
- Set_Is_Known_Guaranteed_ABE (Call);
+ -- * Call 1 - This call is either nested within some scenario or not,
+ -- which falls under the two general cases outlined above.
- -- Install a run-time ABE failue because this activation call will
- -- always result in an ABE.
+ -- * Call 2 - This is the same case as Call 1.
- if Check_OK then
- Install_ABE_Failure
- (N => Call,
- Ins_Nod => Call);
- end if;
- end if;
- end Process_Activation_Guaranteed_ABE_Impl;
+ -- * Call 3 - The placement of this call limits the range of B's
+ -- early call region unto call 3, therefore the call to B is no
+ -- longer within the early call region of B's body, making it ABE-
+ -- unsafe and therefore illegal.
- procedure Process_Activation_Guaranteed_ABE is
- new Process_Activation_Call (Process_Activation_Guaranteed_ABE_Impl);
+ if Earlier_In_Extended_Unit (Call, Target_Attrs.Body_Decl) then
- ------------------
- -- Process_Call --
- ------------------
+ -- Do not emit any ABE diagnostics when the call occurs in an
+ -- initial condition context because this leads to incorrect
+ -- diagnostics.
- procedure Process_Call
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Target_Id : Entity_Id;
- In_Partial_Fin : Boolean;
- 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,
- -- primitive [Deep_]Initialize, or a block created for initialization
- -- purposes.
+ if In_Init_Cond then
+ null;
- function Is_Partial_Finalization_Proc return Boolean;
- pragma Inline (Is_Partial_Finalization_Proc);
- -- Determine whether call Call with target Target_Id invokes a partial
- -- finalization procedure.
+ -- Do not emit any ABE diagnostics when the call occurs in a
+ -- partial finalization context because this leads to confusing
+ -- noise.
- -------------------------------
- -- In_Initialization_Context --
- -------------------------------
+ elsif In_Partial_Fin then
+ null;
- function In_Initialization_Context (N : Node_Id) return Boolean is
- Par : Node_Id;
- Spec_Id : Entity_Id;
+ -- 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.
- begin
- -- Climb the parent chain looking for initialization actions
+ elsif Static_Elaboration_Checks then
- Par := Parent (N);
- while Present (Par) loop
+ -- Ensure that a call which textually precedes the subprogram
+ -- body it invokes appears within the early call region of the
+ -- subprogram body.
- -- A block may be part of the initialization actions of a default
- -- initialized object.
+ -- IMPORTANT: This check must always be performed even when
+ -- -gnatd.v (enforce SPARK elaboration rules in SPARK code) is
+ -- not specified because the static model cannot guarantee the
+ -- absence of elaboration issues in the presence of dispatching
+ -- calls.
- if Nkind (Par) = N_Block_Statement
- and then Is_Initialization_Block (Par)
- then
- return True;
+ Region := Find_Early_Call_Region (Target_Attrs.Body_Decl);
- -- A subprogram body may denote an initialization routine
+ if Earlier_In_Extended_Unit (Call, Region) then
+ Error_Msg_NE
+ ("call must appear within early call region of subprogram "
+ & "body & (SPARK RM 7.7(3))", Call, Target_Id);
- elsif Nkind (Par) = N_Subprogram_Body then
- Spec_Id := Unique_Defining_Entity (Par);
+ Error_Msg_Sloc := Sloc (Region);
+ Error_Msg_N ("\region starts #", Call);
- -- The current subprogram body denotes a type init proc or
- -- primitive [Deep_]Initialize.
+ Error_Msg_Sloc := Sloc (Target_Attrs.Body_Decl);
+ Error_Msg_N ("\region ends #", Call);
- 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;
+ Output_Active_Scenarios (Call);
end if;
+ end if;
- -- Prevent the search from going too far
+ -- Otherwise the call appears after the target body. The call is
+ -- ABE-safe as a consequence of applying the early call region rule
+ -- to ALL calls preceding their associated bodies.
- elsif Is_Body_Or_Package_Declaration (Par) then
- exit;
- end if;
+ else
+ null;
+ end if;
+ end if;
- Par := Parent (Par);
- end loop;
+ -- 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.
- return False;
- end In_Initialization_Context;
+ -- IMPORTANT: This check must be performed only when -gnatd.v (enforce
+ -- SPARK elaboration rules in SPARK code) is active because the static
+ -- model can ensure the prior elaboration of the unit which contains a
+ -- body by installing an implicit Elaborate[_All] pragma.
- ----------------------------------
- -- Is_Partial_Finalization_Proc --
- ----------------------------------
+ if Debug_Flag_Dot_V then
+ 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;
- function Is_Partial_Finalization_Proc return Boolean is
- begin
- -- To qualify, the target must denote primitive [Deep_]Finalize or a
- -- finalizer procedure, and the call must appear in an initialization
- -- context.
+ -- Otherwise ensure that the unit with the target body is elaborated
+ -- prior to the main unit.
- return
- (Is_Controlled_Proc (Target_Id, Name_Finalize)
- or else Is_Finalizer_Proc (Target_Id)
- or else Is_TSS (Target_Id, TSS_Deep_Finalize))
- and then In_Initialization_Context (Call);
- end Is_Partial_Finalization_Proc;
+ else
+ Ensure_Prior_Elaboration
+ (N => Call,
+ Unit_Id => Target_Attrs.Unit_Id,
+ Prag_Nam => Name_Elaborate_All,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
+ end if;
+ end Process_Conditional_ABE_Call_SPARK;
- -- Local variables
+ -------------------------------------------
+ -- Process_Conditional_ABE_Instantiation --
+ -------------------------------------------
- Partial_Fin_On : Boolean;
- SPARK_Rules_On : Boolean;
- Target_Attrs : Target_Attributes;
+ procedure Process_Conditional_ABE_Instantiation
+ (Exp_Inst : Node_Id;
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean)
+ is
+ Gen_Attrs : Target_Attributes;
+ Gen_Id : Entity_Id;
+ Inst : Node_Id;
+ Inst_Attrs : Instantiation_Attributes;
+ Inst_Id : Entity_Id;
- -- Start of processing for Process_Call
+ SPARK_Rules_On : Boolean;
+ -- This flag is set when the SPARK rules are in effect
begin
- Extract_Target_Attributes
- (Target_Id => Target_Id,
- Attrs => Target_Attrs);
-
- -- The call occurs in a partial finalization context when a prior
- -- scenario is already in that mode, or when the target denotes a
- -- [Deep_]Finalize primitive or a finalizer within an initialization
- -- context.
+ Extract_Instantiation_Attributes
+ (Exp_Inst => Exp_Inst,
+ Inst => Inst,
+ Inst_Id => Inst_Id,
+ Gen_Id => Gen_Id,
+ Attrs => Inst_Attrs);
- Partial_Fin_On := In_Partial_Fin or else Is_Partial_Finalization_Proc;
+ Extract_Target_Attributes (Gen_Id, Gen_Attrs);
- -- The SPARK rules are in effect when both the call and target are
- -- subject to SPARK_Mode On.
+ -- The SPARK rules are in effect when both the instantiation and generic
+ -- are subject to SPARK_Mode On.
- SPARK_Rules_On :=
- Call_Attrs.SPARK_Mode_On and Target_Attrs.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_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;
+ Info_Instantiation
+ (Inst => Inst,
+ Gen_Id => Gen_Id,
+ Info_Msg => True,
+ In_SPARK => SPARK_Rules_On);
end if;
- -- Nothing to do when the call is a guaranteed ABE
+ -- Nothing to do when the instantiation is a guaranteed ABE
- if Is_Known_Guaranteed_ABE (Call) then
+ if Is_Known_Guaranteed_ABE (Inst) 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.
+ -- and the generic is in the same unit, but outside this context.
- -- function B ...; -- target declaration
+ -- generic
+ -- procedure Gen is ...; -- generic declaration
-- procedure Proc is
-- function A ... is
-- begin
-- if Some_Condition then
- -- return B; -- call site
+ -- declare
+ -- procedure I is new Gen; -- instantiation site
+ -- ...
-- ...
-- end A;
-- X : ... := A; -- root scenario
-- ...
- -- function B ... is
+ -- procedure Gen is
-- ...
- -- end B;
+ -- end Gen;
-- 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.
+ -- 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 (Target_Attrs.Spec_Decl) then
+ 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.
+ -- The SPARK rules are 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,
- In_Partial_Fin => In_Partial_Fin);
+ elsif SPARK_Rules_On then
+ Process_Conditional_ABE_Instantiation_SPARK
+ (Inst => Inst,
+ Gen_Id => Gen_Id,
+ Gen_Attrs => Gen_Attrs,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
-- 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_Partial_Fin => Partial_Fin_On,
+ Process_Conditional_ABE_Instantiation_Ada
+ (Exp_Inst => Exp_Inst,
+ Inst => Inst,
+ Inst_Attrs => Inst_Attrs,
+ Gen_Id => Gen_Id,
+ Gen_Attrs => Gen_Attrs,
+ In_Partial_Fin => In_Partial_Fin,
In_Task_Body => In_Task_Body);
end if;
+ end Process_Conditional_ABE_Instantiation;
- -- Inspect the target body (and barried function) for other suitable
- -- elaboration scenarios.
-
- Traverse_Body (Target_Attrs.Body_Barf, Partial_Fin_On, In_Task_Body);
- Traverse_Body (Target_Attrs.Body_Decl, Partial_Fin_On, In_Task_Body);
- end Process_Call;
-
- ----------------------
- -- Process_Call_Ada --
- ----------------------
+ -----------------------------------------------
+ -- Process_Conditional_ABE_Instantiation_Ada --
+ -----------------------------------------------
- procedure Process_Call_Ada
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Target_Id : Entity_Id;
- Target_Attrs : Target_Attributes;
+ procedure Process_Conditional_ABE_Instantiation_Ada
+ (Exp_Inst : Node_Id;
+ Inst : Node_Id;
+ Inst_Attrs : Instantiation_Attributes;
+ Gen_Id : Entity_Id;
+ Gen_Attrs : Target_Attributes;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean)
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.
-
- 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.
+ 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.
- if Call_Attrs.Is_Dispatching then
- return;
+ Root : constant Node_Id := Root_Scenario;
- -- Nothing to do when the call is ABE-safe
+ begin
+ -- Nothing to do when the instantiation is ABE-safe
-- generic
- -- function Gen ...;
+ -- package Gen is
+ -- ...
+ -- end Gen;
- -- function Gen ... is
- -- begin
+ -- package body Gen is
-- ...
-- end Gen;
-- with Gen;
-- procedure Main is
- -- function Inst is new Gen;
- -- X : ... := Inst; -- safe call
+ -- package Inst is new Gen (ABE); -- safe instantiation
-- ...
- elsif Is_Safe_Call (Call, Target_Attrs) then
+ if Is_Safe_Instantiation (Inst, Gen_Attrs) then
return;
- -- The call and the target body are both in the main unit
+ -- The instantiation and the generic body are both in the main unit
- elsif Present (Target_Attrs.Body_Decl)
- and then In_Extended_Main_Code_Unit (Target_Attrs.Body_Decl)
+ elsif Present (Gen_Attrs.Body_Decl)
+ and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
then
- Process_Call_Conditional_ABE
- (Call => Call,
- Call_Attrs => Call_Attrs,
- Target_Id => Target_Id,
- Target_Attrs => Target_Attrs,
- In_Partial_Fin => In_Partial_Fin);
+ -- If the root scenario appears prior to the generic body, then this
+ -- is a possible ABE with respect to the root scenario.
- -- 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.
+ -- generic
+ -- package Gen is
+ -- ...
+ -- end Gen;
- elsif Dynamic_Elaboration_Checks and then Check_OK then
- Install_ABE_Check
- (N => Call,
- Ins_Nod => Call,
- Id => Target_Attrs.Unit_Id);
- end if;
+ -- function A ... is
+ -- begin
+ -- if Some_Condition then
+ -- declare
+ -- package Inst is new Gen; -- instantiation site
+ -- ...
+ -- end A;
- -- Ensure that the unit with the target body is elaborated prior to the
- -- main unit. The implicit Elaborate[_All] is generated only when the
- -- call has elaboration checks enabled. This behaviour parallels that of
- -- the old ABE mechanism.
+ -- X : ... := A; -- root scenario
- if Call_Attrs.Elab_Checks_OK then
- Ensure_Prior_Elaboration
- (N => Call,
- Unit_Id => Target_Attrs.Unit_Id,
- In_Partial_Fin => In_Partial_Fin,
- In_Task_Body => In_Task_Body);
- end if;
- end Process_Call_Ada;
+ -- package body Gen is -- generic body
+ -- ...
+ -- end Gen;
- ----------------------------------
- -- Process_Call_Conditional_ABE --
- ----------------------------------
+ -- Y : ... := A; -- root scenario
- procedure Process_Call_Conditional_ABE
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Target_Id : Entity_Id;
- Target_Attrs : Target_Attributes;
- In_Partial_Fin : Boolean)
- 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.
+ -- 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.
- Root : constant Node_Id := Root_Scenario;
+ if Earlier_In_Extended_Unit (Root, Gen_Attrs.Body_Decl) then
- begin
- -- If the root scenario appears prior to the target body, then this is a
- -- possible ABE with respect to the root scenario.
+ -- Do not emit any ABE diagnostics when the instantiation occurs
+ -- in partial finalization context because this leads to unwanted
+ -- noise.
- -- function B ...;
+ if In_Partial_Fin then
+ null;
- -- function A ... is
- -- begin
- -- if Some_Condition then
- -- return B; -- call site
- -- ...
- -- end A;
+ -- 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.
- -- X : ... := A; -- root scenario
+ elsif 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);
- -- function B ... is -- target body
- -- ...
- -- end B;
+ Output_Active_Scenarios (Inst);
+ end if;
- -- Y : ... := A; -- root scenario
+ -- Install a conditional run-time ABE check to verify that the
+ -- generic body has been elaborated prior to the instantiation.
- -- 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 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;
- if Earlier_In_Extended_Unit (Root, Target_Attrs.Body_Decl) then
+ -- 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.
- -- Do not emit any ABE diagnostics when the call occurs in a partial
- -- finalization context because this leads to confusing noise.
+ 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;
- if In_Partial_Fin then
- null;
+ -- Ensure that the unit with the generic body is elaborated prior to
+ -- the main unit. No implicit pragma Elaborate is generated if the
+ -- instantiation has elaboration checks suppressed. This behaviour
+ -- parallels that of the old ABE mechanism.
- -- 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 Inst_Attrs.Elab_Checks_OK then
+ Ensure_Prior_Elaboration
+ (N => Inst,
+ Unit_Id => Gen_Attrs.Unit_Id,
+ Prag_Nam => Name_Elaborate,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
+ end if;
+ end Process_Conditional_ABE_Instantiation_Ada;
- elsif 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);
+ -------------------------------------------------
+ -- Process_Conditional_ABE_Instantiation_SPARK --
+ -------------------------------------------------
- Output_Active_Scenarios (Call);
- end if;
+ procedure Process_Conditional_ABE_Instantiation_SPARK
+ (Inst : Node_Id;
+ Gen_Id : Entity_Id;
+ Gen_Attrs : Target_Attributes;
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean)
+ is
+ Req_Nam : Name_Id;
- -- Install a conditional run-time ABE check to verify that the target
- -- body has been elaborated prior to the call.
+ 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 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);
+ -- IMPORTANT: This check must be performed only when -gnatd.v (enforce
+ -- SPARK elaboration rules in SPARK code) is active because the static
+ -- model can ensure the prior elaboration of the unit which contains a
+ -- body by installing an implicit Elaborate[_All] pragma.
+
+ if Debug_Flag_Dot_V then
+ 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);
+
+ -- Otherwise ensure that the unit with the target body is elaborated
+ -- prior to the main unit.
+
+ else
+ Ensure_Prior_Elaboration
+ (N => Inst,
+ Unit_Id => Gen_Attrs.Unit_Id,
+ Prag_Nam => Name_Elaborate,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
end if;
- end Process_Call_Conditional_ABE;
+ end Process_Conditional_ABE_Instantiation_SPARK;
- ---------------------------------
- -- Process_Call_Guaranteed_ABE --
- ---------------------------------
+ -------------------------------------------------
+ -- Process_Conditional_ABE_Variable_Assignment --
+ -------------------------------------------------
- procedure Process_Call_Guaranteed_ABE
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Target_Id : Entity_Id)
- is
- Target_Attrs : Target_Attributes;
+ procedure Process_Conditional_ABE_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
- Extract_Target_Attributes
- (Target_Id => Target_Id,
- Attrs => Target_Attrs);
+ -- The SPARK rules are in effect when both the assignment and the
+ -- variable are subject to SPARK_Mode On.
- -- Nothing to do when the root scenario appears at the declaration level
- -- and the target is in the same unit, but outside this context.
+ SPARK_Rules_On :=
+ Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On
+ and then Is_SPARK_Mode_On_Node (Asmt);
- -- function B ...; -- target declaration
+ -- Output relevant information when switch -gnatel (info messages on
+ -- implicit Elaborate[_All] pragmas) is in effect.
- -- procedure Proc is
- -- function A ... is
- -- begin
- -- if Some_Condition then
- -- return B; -- call site
- -- ...
- -- end A;
+ 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;
- -- X : ... := A; -- root scenario
- -- ...
+ -- 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.
- -- function B ... is
- -- ...
- -- end B;
+ if SPARK_Rules_On then
+ Process_Conditional_ABE_Variable_Assignment_SPARK
+ (Asmt => Asmt,
+ Var_Id => Var_Id);
- -- 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.
+ -- Otherwise the Ada rules are in effect
- -- Performance note: parent traversal
+ else
+ Process_Conditional_ABE_Variable_Assignment_Ada
+ (Asmt => Asmt,
+ Var_Id => Var_Id);
+ end if;
+ end Process_Conditional_ABE_Variable_Assignment;
- if Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
- return;
+ -----------------------------------------------------
+ -- Process_Conditional_ABE_Variable_Assignment_Ada --
+ -----------------------------------------------------
- -- Nothing to do when the call is ABE-safe
+ procedure Process_Conditional_ABE_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);
- -- generic
- -- function Gen ...;
+ 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.
- -- function Gen ... is
- -- begin
- -- ...
- -- end Gen;
+ 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
- -- with Gen;
- -- procedure Main is
- -- function Inst is new Gen;
- -- X : ... := Inst; -- safe call
- -- ...
+ Set_Elaborate_Body_Desirable (Spec_Id);
- elsif Is_Safe_Call (Call, Target_Attrs) then
- return;
+ Error_Msg_NE
+ ("??variable & can be accessed by clients before this "
+ & "initialization", Asmt, Var_Id);
- -- 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.
+ Error_Msg_NE
+ ("\add pragma ""Elaborate_Body"" to spec & to ensure proper "
+ & "initialization", Asmt, Spec_Id);
- -- procedure Guaranteed_ABE is
- -- function Func ...;
+ Output_Active_Scenarios (Asmt);
+ end if;
+ end Process_Conditional_ABE_Variable_Assignment_Ada;
- -- package Nested is
- -- Obj : ... := Func; -- guaranteed ABE
- -- end Nested;
+ -------------------------------------------------------
+ -- Process_Conditional_ABE_Variable_Assignment_SPARK --
+ -------------------------------------------------------
- -- function Func ... is
- -- ...
- -- end Func;
- -- ...
+ procedure Process_Conditional_ABE_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);
- -- Performance note: parent traversal
+ 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.
- elsif Is_Guaranteed_ABE
- (N => Call,
- Target_Decl => Target_Attrs.Spec_Decl,
- Target_Body => Target_Attrs.Body_Decl)
+ if Is_Initialized (Var_Decl)
+ and then not Has_Pragma_Elaborate_Body (Spec_Id)
then
- Error_Msg_NE ("??cannot call & before body seen", Call, Target_Id);
- Error_Msg_N ("\Program_Error will be raised at run time", Call);
+ Error_Msg_NE
+ ("variable & modified by elaboration code in package body",
+ Asmt, Var_Id);
- -- Mark the call as a guarnateed ABE
+ Error_Msg_NE
+ ("\add pragma ""Elaborate_Body"" to spec & to ensure full "
+ & "initialization", Asmt, Spec_Id);
- Set_Is_Known_Guaranteed_ABE (Call);
+ Output_Active_Scenarios (Asmt);
+ end if;
+ end Process_Conditional_ABE_Variable_Assignment_SPARK;
- -- 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.
+ ------------------------------------------------
+ -- Process_Conditional_ABE_Variable_Reference --
+ ------------------------------------------------
- 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;
+ procedure Process_Conditional_ABE_Variable_Reference (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);
+
+ if Is_Read (Ref) then
+ Process_Conditional_ABE_Variable_Reference_Read
+ (Ref => Ref,
+ Var_Id => Var_Id,
+ Attrs => Var_Attrs);
end if;
- end Process_Call_Guaranteed_ABE;
+ end Process_Conditional_ABE_Variable_Reference;
- ------------------------
- -- Process_Call_SPARK --
- ------------------------
+ -----------------------------------------------------
+ -- Process_Conditional_ABE_Variable_Reference_Read --
+ -----------------------------------------------------
- procedure Process_Call_SPARK
- (Call : Node_Id;
- Call_Attrs : Call_Attributes;
- Target_Id : Entity_Id;
- Target_Attrs : Target_Attributes;
- In_Partial_Fin : Boolean)
+ procedure Process_Conditional_ABE_Variable_Reference_Read
+ (Ref : Node_Id;
+ Var_Id : Entity_Id;
+ Attrs : Variable_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.
+ -- Output relevant information when switch -gnatel (info messages on
+ -- implicit Elaborate[_All] pragmas) is in effect.
- 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);
+ 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 call is ABE-safe
-
- -- generic
- -- function Gen ...;
+ -- Nothing to do when the variable appears within the main unit because
+ -- diagnostics on reads are relevant only for external variables.
- -- function Gen ... is
- -- begin
- -- ...
- -- end Gen;
+ if Is_Same_Unit (Attrs.Unit_Id, Cunit_Entity (Main_Unit)) then
+ null;
- -- with Gen;
- -- procedure Main is
- -- function Inst is new Gen;
- -- X : ... := Inst; -- safe call
- -- ...
+ -- Nothing to do when the variable is already initialized. Note that the
+ -- variable may be further modified by the external unit.
- if Is_Safe_Call (Call, Target_Attrs) then
- return;
+ elsif Is_Initialized (Declaration_Node (Var_Id)) then
+ null;
- -- The call and the target body are both in the main unit
+ -- Nothing to do when the external unit guarantees the initialization of
+ -- the variable by means of pragma Elaborate_Body.
- 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,
- In_Partial_Fin => In_Partial_Fin);
+ elsif Has_Pragma_Elaborate_Body (Attrs.Unit_Id) then
+ null;
- -- 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.
+ -- 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
- null;
+ Meet_Elaboration_Requirement
+ (N => Ref,
+ Target_Id => Var_Id,
+ Req_Nam => Name_Elaborate);
end if;
- end Process_Call_SPARK;
+ end Process_Conditional_ABE_Variable_Reference_Read;
- ----------------------------
- -- Process_Guaranteed_ABE --
- ----------------------------
+ -----------------------------
+ -- Process_Conditional_ABE --
+ -----------------------------
- procedure Process_Guaranteed_ABE (N : Node_Id) is
+ -- NOTE: The body of this routine is intentionally out of order because it
+ -- invokes an instantiated subprogram (Process_Conditional_ABE_Activation).
+ -- Placing the body in alphabetical order will result in a guaranteed ABE.
+
+ procedure Process_Conditional_ABE
+ (N : Node_Id;
+ In_Init_Cond : Boolean := False;
+ In_Partial_Fin : Boolean := False;
+ In_Task_Body : Boolean := False)
+ is
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
Push_Active_Scenario (N);
- -- Only calls, instantiations, and task activations may result in a
- -- guaranteed ABE.
+ -- 'Access
- if Is_Suitable_Call (N) then
- Extract_Call_Attributes
- (Call => N,
- Target_Id => Target_Id,
- Attrs => Call_Attrs);
+ if Is_Suitable_Access (N) then
+ Process_Conditional_ABE_Access
+ (Attr => N,
+ In_Init_Cond => In_Init_Cond,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
- if Is_Activation_Proc (Target_Id) then
- Process_Activation_Guaranteed_ABE
- (Call => N,
- Call_Attrs => Call_Attrs,
- In_Partial_Fin => False,
- In_Task_Body => False);
+ -- Calls
- else
- Process_Call_Guaranteed_ABE
- (Call => N,
- Call_Attrs => Call_Attrs,
- Target_Id => Target_Id);
- end if;
+ elsif Is_Suitable_Call (N) then
- elsif Is_Suitable_Instantiation (N) then
- Process_Instantiation_Guaranteed_ABE (N);
- end if;
+ -- 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.
- -- Remove the current scenario from the stack of active scenarios once
- -- all ABE diagnostics and checks have been performed.
+ if In_Main_Context (N) then
+ Extract_Call_Attributes
+ (Call => N,
+ Target_Id => Target_Id,
+ Attrs => Call_Attrs);
- Pop_Active_Scenario (N);
- end Process_Guaranteed_ABE;
+ if Is_Activation_Proc (Target_Id) then
+ Process_Conditional_ABE_Activation
+ (Call => N,
+ Call_Attrs => Call_Attrs,
+ In_Init_Cond => In_Init_Cond,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
- ---------------------------
- -- Process_Instantiation --
- ---------------------------
+ else
+ Process_Conditional_ABE_Call
+ (Call => N,
+ Call_Attrs => Call_Attrs,
+ Target_Id => Target_Id,
+ In_Init_Cond => In_Init_Cond,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
+ end if;
+ end if;
- procedure Process_Instantiation
- (Exp_Inst : Node_Id;
- In_Partial_Fin : Boolean;
- In_Task_Body : Boolean)
- is
- Gen_Attrs : Target_Attributes;
- Gen_Id : Entity_Id;
- Inst : Node_Id;
- Inst_Attrs : Instantiation_Attributes;
- Inst_Id : Entity_Id;
+ -- Instantiations
- SPARK_Rules_On : Boolean;
- -- This flag is set when the SPARK rules are in effect
+ elsif Is_Suitable_Instantiation (N) then
+ Process_Conditional_ABE_Instantiation
+ (Exp_Inst => N,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
- begin
- Extract_Instantiation_Attributes
- (Exp_Inst => Exp_Inst,
- Inst => Inst,
- Inst_Id => Inst_Id,
- Gen_Id => Gen_Id,
- Attrs => Inst_Attrs);
+ -- Variable assignments
- Extract_Target_Attributes (Gen_Id, Gen_Attrs);
+ elsif Is_Suitable_Variable_Assignment (N) then
+ Process_Conditional_ABE_Variable_Assignment (N);
- -- The SPARK rules are in effect when both the instantiation and generic
- -- are subject to SPARK_Mode On.
+ -- Variable references
- SPARK_Rules_On := Inst_Attrs.SPARK_Mode_On and Gen_Attrs.SPARK_Mode_On;
+ elsif Is_Suitable_Variable_Reference (N) then
- -- Output relevant information when switch -gnatel (info messages on
- -- implicit Elaborate[_All] pragmas) is in effect.
+ -- In general, only variable references 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
+ -- variable references also receive corresponding variable reference
+ -- markers (see Build_Varaible_Reference_Marker). Regardless of the
+ -- reason, external variable references must not be processed.
- if Elab_Info_Messages then
- Info_Instantiation
- (Inst => Inst,
- Gen_Id => Gen_Id,
- Info_Msg => True,
- In_SPARK => SPARK_Rules_On);
+ if In_Main_Context (N) then
+ Process_Conditional_ABE_Variable_Reference (N);
+ end if;
end if;
- -- Nothing to do when the instantiation is a guaranteed ABE
+ -- Remove the current scenario from the stack of active scenarios once
+ -- all ABE diagnostics and checks have been performed.
- if Is_Known_Guaranteed_ABE (Inst) then
- return;
+ Pop_Active_Scenario (N);
+ end Process_Conditional_ABE;
- -- Nothing to do when the root scenario appears at the declaration level
- -- and the generic is in the same unit, but outside this context.
+ --------------------------------------------
+ -- Process_Guaranteed_ABE_Activation_Impl --
+ --------------------------------------------
+
+ procedure Process_Guaranteed_ABE_Activation_Impl
+ (Call : Node_Id;
+ Call_Attrs : Call_Attributes;
+ Obj_Id : Entity_Id;
+ Task_Attrs : Task_Attributes;
+ In_Init_Cond : Boolean;
+ In_Partial_Fin : Boolean;
+ In_Task_Body : Boolean)
+ is
+ pragma Unreferenced (Call_Attrs);
+ pragma Unreferenced (In_Init_Cond);
+ pragma Unreferenced (In_Partial_Fin);
+ 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.
- -- generic
- -- procedure Gen is ...; -- generic declaration
+ -- task type Task_Typ; -- task declaration
-- procedure Proc is
-- function A ... is
-- begin
-- if Some_Condition then
-- declare
- -- procedure I is new Gen; -- instantiation site
- -- ...
+ -- T : Task_Typ;
+ -- begin
+ -- <activation call> -- activation site
+ -- end;
-- ...
-- end A;
-- X : ... := A; -- root scenario
-- ...
- -- procedure Gen is
+ -- task body Task_Typ is
-- ...
- -- end Gen;
+ -- end Task_Typ;
- -- 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.
+ -- 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 (Gen_Attrs.Spec_Decl) then
+ if Is_Up_Level_Target (Task_Attrs.Task_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,
- In_Partial_Fin => In_Partial_Fin);
-
- -- 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_Partial_Fin => In_Partial_Fin,
- 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_Partial_Fin : Boolean;
- 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
+ -- 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 Inst is new Gen (ABE); -- safe instantiation
+ -- 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;
-- ...
- if Is_Safe_Instantiation (Inst, Gen_Attrs) then
+ elsif Is_Safe_Activation (Call, Task_Attrs.Task_Decl) then
return;
- -- The instantiation and the generic body are both in the main unit
+ -- 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.
- elsif Present (Gen_Attrs.Body_Decl)
- and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
+ -- 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
- Process_Instantiation_Conditional_ABE
- (Exp_Inst => Exp_Inst,
- Inst => Inst,
- Inst_Attrs => Inst_Attrs,
- Gen_Id => Gen_Id,
- Gen_Attrs => Gen_Attrs,
- In_Partial_Fin => In_Partial_Fin);
+ 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);
- -- 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.
+ -- Mark the activation call as a guaranteed ABE
- 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;
+ Set_Is_Known_Guaranteed_ABE (Call);
- -- 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.
+ -- Install a run-time ABE failue because this activation call will
+ -- always result in an ABE.
- if Inst_Attrs.Elab_Checks_OK then
- Ensure_Prior_Elaboration
- (N => Inst,
- Unit_Id => Gen_Attrs.Unit_Id,
- In_Partial_Fin => In_Partial_Fin,
- In_Task_Body => In_Task_Body);
+ if Check_OK then
+ Install_ABE_Failure
+ (N => Call,
+ Ins_Nod => Call);
+ end if;
end if;
- end Process_Instantiation_Ada;
+ end Process_Guaranteed_ABE_Activation_Impl;
- -------------------------------------------
- -- Process_Instantiation_Conditional_ABE --
- -------------------------------------------
+ procedure Process_Guaranteed_ABE_Activation is
+ new Process_Activation_Generic (Process_Guaranteed_ABE_Activation_Impl);
- procedure Process_Instantiation_Conditional_ABE
- (Exp_Inst : Node_Id;
- Inst : Node_Id;
- Inst_Attrs : Instantiation_Attributes;
- Gen_Id : Entity_Id;
- Gen_Attrs : Target_Attributes;
- In_Partial_Fin : 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.
+ ---------------------------------
+ -- Process_Guaranteed_ABE_Call --
+ ---------------------------------
- Root : constant Node_Id := Root_Scenario;
+ procedure Process_Guaranteed_ABE_Call
+ (Call : Node_Id;
+ Call_Attrs : Call_Attributes;
+ Target_Id : Entity_Id)
+ is
+ Target_Attrs : Target_Attributes;
begin
- -- If the root scenario appears prior to the generic body, then this is
- -- a possible ABE with respect to the root scenario.
+ Extract_Target_Attributes
+ (Target_Id => Target_Id,
+ Attrs => Target_Attrs);
- -- generic
- -- package Gen is
- -- ...
- -- end Gen;
+ -- 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 A ... is
- -- begin
- -- if Some_Condition then
- -- declare
- -- package Inst is new Gen; -- instantiation site
+ -- 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 A;
+ -- 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;
- -- X : ... := A; -- root scenario
+ -- Nothing to do when the call is ABE-safe
+
+ -- generic
+ -- function Gen ...;
- -- package body Gen is -- generic body
+ -- function Gen ... is
+ -- begin
-- ...
-- end Gen;
- -- Y : ... := A; -- root scenario
+ -- with Gen;
+ -- procedure Main is
+ -- function Inst is new Gen;
+ -- X : ... := Inst; -- safe call
+ -- ...
- -- 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.
+ elsif Is_Safe_Call (Call, Target_Attrs) then
+ return;
- if Earlier_In_Extended_Unit (Root, Gen_Attrs.Body_Decl) then
+ -- 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.
- -- Do not emit any ABE diagnostics when the instantiation occurs in a
- -- partial finalization context because this leads to unwanted noise.
+ -- procedure Guaranteed_ABE is
+ -- function Func ...;
- if In_Partial_Fin then
- null;
+ -- package Nested is
+ -- Obj : ... := Func; -- guaranteed ABE
+ -- end Nested;
+
+ -- function Func ... is
+ -- ...
+ -- end Func;
+ -- ...
+
+ -- Performance note: parent traversal
- -- 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.
+ 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);
- elsif 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);
+ -- Mark the call as a guarnateed ABE
- Output_Active_Scenarios (Inst);
- end if;
+ Set_Is_Known_Guaranteed_ABE (Call);
- -- Install a conditional run-time ABE check to verify that the
- -- generic body has been elaborated prior to the instantiation.
+ -- 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 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);
+ 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_Instantiation_Conditional_ABE;
+ end Process_Guaranteed_ABE_Call;
------------------------------------------
- -- Process_Instantiation_Guaranteed_ABE --
+ -- Process_Guaranteed_ABE_Instantiation --
------------------------------------------
- procedure Process_Instantiation_Guaranteed_ABE (Exp_Inst : Node_Id) is
+ procedure Process_Guaranteed_ABE_Instantiation (Exp_Inst : Node_Id) is
Gen_Attrs : Target_Attributes;
Gen_Id : Entity_Id;
Inst : Node_Id;
("??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;
- In_Partial_Fin : Boolean)
- 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,
- In_Partial_Fin => In_Partial_Fin);
-
- -- 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_Reference --
- --------------------------------
-
- procedure Process_Variable_Reference (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);
-
- if Is_Read (Ref) then
- Process_Variable_Reference_Read
- (Ref => Ref,
- Var_Id => Var_Id,
- Attrs => Var_Attrs);
- end if;
- end Process_Variable_Reference;
-
- -------------------------------------
- -- Process_Variable_Reference_Read --
- -------------------------------------
-
- procedure Process_Variable_Reference_Read
- (Ref : Node_Id;
- Var_Id : Entity_Id;
- Attrs : Variable_Attributes)
- is
- begin
- -- 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 (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 (Attrs.Unit_Id) then
- null;
+ -- Mark the instantiation as a guarantee ABE. This automatically
+ -- suppresses the instantiation of the generic body.
- -- 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.
+ Set_Is_Known_Guaranteed_ABE (Inst);
- else
- Meet_Elaboration_Requirement
- (N => Ref,
- Target_Id => Var_Id,
- Req_Nam => Name_Elaborate);
- end if;
- end Process_Variable_Reference_Read;
+ -- 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.
- --------------------------
- -- Push_Active_Scenario --
- --------------------------
+ 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_Guaranteed_ABE_Instantiation;
- procedure Push_Active_Scenario (N : Node_Id) is
- begin
- Scenario_Stack.Append (N);
- end Push_Active_Scenario;
+ ----------------------------
+ -- Process_Guaranteed_ABE --
+ ----------------------------
- ----------------------
- -- Process_Scenario --
- ----------------------
+ -- NOTE: The body of this routine is intentionally out of order because it
+ -- invokes an instantiated subprogram (Process_Guaranteed_ABE_Activation).
+ -- Placing the body in alphabetical order will result in a guaranteed ABE.
- procedure Process_Scenario
- (N : Node_Id;
- In_Partial_Fin : Boolean := False;
- In_Task_Body : Boolean := False)
- is
+ procedure Process_Guaranteed_ABE (N : Node_Id) is
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
Push_Active_Scenario (N);
- -- 'Access
-
- if Is_Suitable_Access (N) then
- Process_Access (N, In_Partial_Fin, 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.
+ -- Only calls, instantiations, and task activations may result in a
+ -- guaranteed ABE.
- if In_Main_Context (N) then
- Extract_Call_Attributes
- (Call => N,
- Target_Id => Target_Id,
- Attrs => Call_Attrs);
+ 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_Conditional_ABE
- (Call => N,
- Call_Attrs => Call_Attrs,
- In_Partial_Fin => In_Partial_Fin,
- In_Task_Body => In_Task_Body);
+ if Is_Activation_Proc (Target_Id) then
+ Process_Guaranteed_ABE_Activation
+ (Call => N,
+ Call_Attrs => Call_Attrs,
+ In_Init_Cond => False,
+ In_Partial_Fin => False,
+ In_Task_Body => False);
- else
- Process_Call
- (Call => N,
- Call_Attrs => Call_Attrs,
- Target_Id => Target_Id,
- In_Partial_Fin => In_Partial_Fin,
- In_Task_Body => In_Task_Body);
- end if;
+ else
+ Process_Guaranteed_ABE_Call
+ (Call => N,
+ Call_Attrs => Call_Attrs,
+ Target_Id => Target_Id);
end if;
- -- Instantiations
-
elsif Is_Suitable_Instantiation (N) then
- Process_Instantiation (N, In_Partial_Fin, In_Task_Body);
-
- -- Variable assignments
-
- elsif Is_Suitable_Variable_Assignment (N) then
- Process_Variable_Assignment (N);
-
- -- Variable references
-
- elsif Is_Suitable_Variable_Reference (N) then
-
- -- In general, only variable references 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
- -- variable references also receive corresponding variable reference
- -- markers (see Build_Varaible_Reference_Marker). Regardless of the
- -- reason, external variable references must not be processed.
-
- if In_Main_Context (N) then
- Process_Variable_Reference (N);
- end if;
+ Process_Guaranteed_ABE_Instantiation (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;
+ end Process_Guaranteed_ABE;
+
+ --------------------------
+ -- Push_Active_Scenario --
+ --------------------------
+
+ procedure Push_Active_Scenario (N : Node_Id) is
+ begin
+ Scenario_Stack.Append (N);
+ end Push_Active_Scenario;
---------------------------------
-- Record_Elaboration_Scenario --
procedure Record_Elaboration_Scenario (N : Node_Id) is
Level : Enclosing_Level_Kind;
+ Any_Level_OK : Boolean;
+ -- This flag is set when a particular scenario is allowed to appear at
+ -- any level.
+
Declaration_Level_OK : Boolean;
-- This flag is set when a particular scenario is allowed to appear at
-- the declaration level.
+ Library_Level_OK : Boolean;
+ -- This flag is set when a particular scenario is allowed to appear at
+ -- the library level.
+
begin
- -- Assume that the scenario must not appear at the declaration level
+ -- Assume that the scenario cannot appear on any level
+ Any_Level_OK := False;
Declaration_Level_OK := False;
+ Library_Level_OK := False;
-- Nothing to do for ASIS. As a result, no ABE checks and diagnostics
-- are performed in this mode.
-- 'Access for entries, operators, and subprograms
-- Assignments to variables
-- Calls (includes task activation)
+ -- Derived types
-- Instantiations
+ -- Pragma Refined_State
-- Reads of variables
elsif Is_Suitable_Access (N) then
+ Library_Level_OK := True;
-- Signal any enclosing local exception handlers that the 'Access may
-- raise Program_Error due to a failed ABE check when switch -gnatd.o
elsif Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N) then
Declaration_Level_OK := True;
+ Library_Level_OK := True;
-- Signal any enclosing local exception handlers that the call or
-- instantiation may raise Program_Error due to a failed ABE check.
Possible_Local_Raise (N, Standard_Program_Error);
+ elsif Is_Suitable_SPARK_Derived_Type (N) then
+ Any_Level_OK := True;
+
+ elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+ Library_Level_OK := True;
+
elsif Is_Suitable_Variable_Assignment (N)
or else Is_Suitable_Variable_Reference (N)
then
- null;
+ Library_Level_OK := True;
-- Otherwise the input does not denote a suitable scenario
if Static_Elaboration_Checks then
- -- Performance note: parent traversal
+ -- Certain scenarios are allowed to appear at any level. This check
+ -- is performed here in order to save on a parent traversal.
- Level := Find_Enclosing_Level (N);
+ if Any_Level_OK then
+ null;
- -- Declaration-level scenario
+ -- Otherwise the scenario must appear at a specific level
- if Declaration_Level_OK and then Level = Declaration_Level then
- null;
+ else
+ -- Performance note: parent traversal
- -- Library-level scenario
+ Level := Find_Enclosing_Level (N);
- elsif Level in Library_Level then
- null;
+ -- Declaration-level scenario
- -- Instantiation library-level scenario
+ if Declaration_Level_OK and then Level = Declaration_Level then
+ null;
- elsif Level = Instantiation then
- null;
+ -- Library-level scenario
- -- Otherwise the scenario does not appear at the proper level and
- -- cannot possibly act as a top-level scenario.
+ elsif Library_Level_OK
+ and then Level in Library_Or_Instantiation_Level
+ then
+ null;
- else
- return;
+ -- 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;
end if;
+ -- Derived types subject to SPARK_Mode On require elaboration-related
+ -- checks even though the type may not be declared within elaboration
+ -- code. The types are recorded in a separate table which is examined
+ -- during the Processing phase. Note that the checks must be delayed
+ -- because the bodies of overriding primitives are not available yet.
+
+ if Is_Suitable_SPARK_Derived_Type (N) then
+ Record_SPARK_Elaboration_Scenario (N);
+
+ -- Nothing left to do for derived types
+
+ return;
+
+ -- Instantiations of generics both subject to SPARK_Mode On require
+ -- elaboration-related checks even though the instantiations may not
+ -- appear within elaboration code. The instantiations are recored in
+ -- a separate table which is examined during the Procesing phase. Note
+ -- that the checks must be delayed because it is not known yet whether
+ -- the generic unit has a body or not.
+
+ -- IMPORTANT: A SPARK instantiation is also a normal instantiation which
+ -- is subject to common conditional and guaranteed ABE checks.
+
+ elsif Is_Suitable_SPARK_Instantiation (N) then
+ Record_SPARK_Elaboration_Scenario (N);
+
+ -- External constituents that refine abstract states which appear in
+ -- pragma Initializes require elaboration-related checks even though
+ -- a Refined_State pragma lacks any elaboration semantic.
+
+ elsif Is_Suitable_SPARK_Refined_State_Pragma (N) then
+ Record_SPARK_Elaboration_Scenario (N);
+
+ -- Nothing left to do for pragma Refined_State
+
+ return;
+ 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.
end Record_Elaboration_Scenario;
---------------------------------------
+ -- Record_SPARK_Elaboration_Scenario --
+ ---------------------------------------
+
+ procedure Record_SPARK_Elaboration_Scenario (N : Node_Id) is
+ begin
+ SPARK_Scenarios.Append (N);
+ Set_Is_Recorded_SPARK_Scenario (N);
+ end Record_SPARK_Elaboration_Scenario;
+
+ -----------------------------------
+ -- Recorded_SPARK_Scenarios_Hash --
+ -----------------------------------
+
+ function Recorded_SPARK_Scenarios_Hash
+ (Key : Node_Id) return Recorded_SPARK_Scenarios_Index
+ is
+ begin
+ return
+ Recorded_SPARK_Scenarios_Index (Key mod Recorded_SPARK_Scenarios_Max);
+ end Recorded_SPARK_Scenarios_Hash;
+
+ ---------------------------------------
-- Recorded_Top_Level_Scenarios_Hash --
---------------------------------------
(Key mod Recorded_Top_Level_Scenarios_Max);
end Recorded_Top_Level_Scenarios_Hash;
+ --------------------------
+ -- Reset_Visited_Bodies --
+ --------------------------
+
+ procedure Reset_Visited_Bodies is
+ begin
+ if Visited_Bodies_In_Use then
+ Visited_Bodies_In_Use := False;
+ Visited_Bodies.Reset;
+ end if;
+ end Reset_Visited_Bodies;
+
-------------------
-- Root_Scenario --
-------------------
return Stack.Table (Stack.First);
end Root_Scenario;
+ ---------------------------
+ -- Set_Early_Call_Region --
+ ---------------------------
+
+ procedure Set_Early_Call_Region (Body_Id : Entity_Id; Start : Node_Id) is
+ begin
+ pragma Assert (Ekind_In (Body_Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Procedure,
+ E_Subprogram_Body));
+
+ Early_Call_Regions_In_Use := True;
+ Early_Call_Regions.Set (Body_Id, Start);
+ end Set_Early_Call_Region;
+
+ ----------------------------
+ -- Set_Elaboration_Status --
+ ----------------------------
+
+ procedure Set_Elaboration_Status
+ (Unit_Id : Entity_Id;
+ Val : Elaboration_Attributes)
+ is
+ begin
+ Elaboration_Statuses_In_Use := True;
+ Elaboration_Statuses.Set (Unit_Id, Val);
+ end Set_Elaboration_Status;
+
+ ------------------------------------
+ -- Set_Is_Recorded_SPARK_Scenario --
+ ------------------------------------
+
+ procedure Set_Is_Recorded_SPARK_Scenario
+ (N : Node_Id;
+ Val : Boolean := True)
+ is
+ begin
+ Recorded_SPARK_Scenarios_In_Use := True;
+ Recorded_SPARK_Scenarios.Set (N, Val);
+ end Set_Is_Recorded_SPARK_Scenario;
+
----------------------------------------
-- Set_Is_Recorded_Top_Level_Scenario --
----------------------------------------
Val : Boolean := True)
is
begin
+ Recorded_Top_Level_Scenarios_In_Use := True;
Recorded_Top_Level_Scenarios.Set (N, Val);
end Set_Is_Recorded_Top_Level_Scenario;
+ -------------------------
+ -- Set_Is_Visited_Body --
+ -------------------------
+
+ procedure Set_Is_Visited_Body (Subp_Body : Node_Id) is
+ begin
+ Visited_Bodies_In_Use := True;
+ Visited_Bodies.Set (Subp_Body, True);
+ end Set_Is_Visited_Body;
+
-------------------------------
-- Static_Elaboration_Checks --
-------------------------------
procedure Traverse_Body
(N : Node_Id;
+ In_Init_Cond : Boolean;
In_Partial_Fin : Boolean;
In_Task_Body : Boolean)
is
procedure Process_Nested_Scenarios (Nested : Elist_Id);
pragma Inline (Process_Nested_Scenarios);
- -- Invoke Process_Scenario on each individual scenario whith appears in
+ -- Invoke Process_Conditional_ABE on each individual scenario found in
-- list Nested.
---------------------------------------
elsif Is_Suitable_Scenario (Nod) then
Save_Scenario (Nod);
- Process_Scenario (Nod, In_Partial_Fin, In_Task_Body);
+
+ Process_Conditional_ABE
+ (N => Nod,
+ In_Init_Cond => In_Init_Cond,
+ In_Partial_Fin => In_Partial_Fin,
+ In_Task_Body => In_Task_Body);
end if;
return OK;
begin
Nested_Elmt := First_Elmt (Nested);
while Present (Nested_Elmt) loop
- Process_Scenario
+ Process_Conditional_ABE
(N => Node (Nested_Elmt),
+ In_Init_Cond => In_Init_Cond,
In_Partial_Fin => In_Partial_Fin,
In_Task_Body => In_Task_Body);
-- Nothing to do if the body was already traversed during the processing
-- of the same top-level scenario.
- if Visited_Bodies.Get (N) then
+ if Is_Visited_Body (N) then
return;
-- Otherwise mark the body as traversed
else
- Visited_Bodies.Set (N, True);
+ Set_Is_Visited_Body (N);
end if;
Nested := Nested_Scenarios (Defining_Entity (N));
---------------------------------
procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id) is
- package Scenarios renames Top_Level_Scenarios;
+ procedure Update_SPARK_Scenario;
+ pragma Inline (Update_SPARK_Scenario);
+ -- Update the contents of table SPARK_Scenarios if Old_N is recorded
+ -- there.
+
+ procedure Update_Top_Level_Scenario;
+ pragma Inline (Update_Top_Level_Scenario);
+ -- Update the contexts of table Top_Level_Scenarios if Old_N is recorded
+ -- there.
+
+ ---------------------------
+ -- Update_SPARK_Scenario --
+ ---------------------------
+
+ procedure Update_SPARK_Scenario is
+ package Scenarios renames SPARK_Scenarios;
+
+ begin
+ if Is_Recorded_SPARK_Scenario (Old_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;
+
+ -- The old SPARK scenario is no longer recorded, but the new
+ -- one is.
+
+ Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
+ Set_Is_Recorded_Top_Level_Scenario (New_N);
+ return;
+ end if;
+ end loop;
+
+ -- A recorded SPARK scenario must be in the table of recorded
+ -- SPARK scenarios.
+
+ pragma Assert (False);
+ end if;
+ end Update_SPARK_Scenario;
+
+ -------------------------------
+ -- Update_Top_Level_Scenario --
+ -------------------------------
+
+ procedure Update_Top_Level_Scenario is
+ package Scenarios renames Top_Level_Scenarios;
+
+ begin
+ if Is_Recorded_Top_Level_Scenario (Old_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;
+
+ -- The old top-level scenario is no longer recorded, but the
+ -- new one is.
+
+ Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
+ Set_Is_Recorded_Top_Level_Scenario (New_N);
+ return;
+ end if;
+ end loop;
+
+ -- A recorded top-level scenario must be in the table of recorded
+ -- top-level scenarios.
+
+ pragma Assert (False);
+ end if;
+ end Update_Top_Level_Scenario;
+
+ -- Start of processing for Update_Elaboration_Requirement
begin
-- Nothing to do when the old and new scenarios are one and the same
-- potential run-time conditional ABE check or a guaranteed ABE failure
-- is inserted at the proper place in the tree.
- elsif Is_Scenario (Old_N)
- and then Is_Recorded_Top_Level_Scenario (Old_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;
-
- -- The old top-level scenario is no longer recorded, but the
- -- new one is.
-
- Set_Is_Recorded_Top_Level_Scenario (Old_N, False);
- Set_Is_Recorded_Top_Level_Scenario (New_N);
- return;
- end if;
- end loop;
-
- -- A recorded top-level scenario must be in the table of recorded
- -- top-level scenarios.
-
- pragma Assert (False);
+ elsif Is_Scenario (Old_N) then
+ Update_SPARK_Scenario;
+ Update_Top_Level_Scenario;
end if;
end Update_Elaboration_Scenario;
projects / platform / upstream / gcc.git / commitdiff