Google Git
Sign in
gnu / gcc / ddeb81e76461fc0075542d436dc962f3cf6fac92 / . / gcc / ada / sem_elab.adb
blob: cc5d0456cdc1fe0ef84cbb705ff3285f92faf758 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ E L A B --
-- --
-- B o d y --
-- --
-- Copyright (C) 1997-2018, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
-- for more details. You should have received a copy of the GNU General --
-- Public License distributed with GNAT; see file COPYING3. If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license. --
-- --
-- GNAT was originally developed by the GNAT team at New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
with Atree; use Atree;
with Checks; use Checks;
with Debug; use Debug;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
with Exp_Ch11; use Exp_Ch11;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Expander; use Expander;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Opt; use Opt;
with Output; use Output;
with Restrict; use Restrict;
with Rident; use Rident;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Cat; use Sem_Cat;
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinput; use Sinput;
with Snames; use Snames;
with Stand; use Stand;
with Table;
with Tbuild; use Tbuild;
with Uintp; use Uintp;
with Uname; use Uname;
with GNAT.HTable; use GNAT.HTable;
package body Sem_Elab is
-----------------------------------------
-- Access-before-elaboration mechanism --
-----------------------------------------
-- The access-before-elaboration (ABE) mechanism implemented in this unit
-- has the following objectives:
--
-- * Diagnose at compile-time or install run-time checks to prevent ABE
-- access to data and behaviour.
--
-- The high-level idea is to accurately diagnose ABE issues within a
-- single unit because the ABE mechanism can inspect the whole unit.
-- As soon as the elaboration graph extends to an external unit, the
-- diagnostics stop because the body of the unit may not be available.
-- Due to control and data flow, the ABE mechanism cannot accurately
-- determine whether a particular scenario will be elaborated or not.
-- Conditional ABE checks are therefore used to verify the elaboration
-- status of a local and external target at run time.
--
-- * Supply elaboration dependencies for a unit to binde
--
-- The ABE mechanism registers each outgoing elaboration edge for the
-- main unit in its ALI file. GNATbind and binde can then reconstruct
-- the full elaboration graph and determine the proper elaboration
-- order for all units in the compilation.
--
-- The ABE mechanism supports three models of elaboration:
--
-- * Dynamic model - This is the most permissive of the three models.
-- When the dynamic model is in effect, the mechanism performs very
-- little diagnostics and generates run-time checks to detect ABE
-- issues. The behaviour of this model is identical to that specified
-- by the Ada RM. This model is enabled with switch -gnatE.
--
-- * Static model - This is the middle ground of the three models. When
-- the static model is in effect, the mechanism diagnoses and installs
-- run-time checks to detect ABE issues in the main unit. In addition,
-- the mechanism generates implicit Elaborate or Elaborate_All pragmas
-- to ensure the prior elaboration of withed units. The model employs
-- textual order, with clause context, and elaboration-related source
-- pragmas. This is the default model.
--
-- * SPARK model - This is the most conservative of the three models and
-- impelements the semantics defined in SPARK RM 7.7. The SPARK model
-- is in effect only when a context resides in a SPARK_Mode On region,
-- otherwise the mechanism falls back to one of the previous models.
--
-- The ABE mechanism consists of a "recording" phase and a "processing"
-- phase.
-----------------
-- Terminology --
-----------------
-- * ABE - An attempt to activate, call, or instantiate a scenario which
-- has not been fully elaborated.
--
-- * Bridge target - A type of target. A bridge target is a link between
-- scenarios. It is usually a byproduct of expansion and does not have
-- any direct ABE ramifications.
--
-- * Call marker - A special node used to indicate the presence of a call
-- in the tree in case expansion transforms or eliminates the original
-- call. N_Call_Marker nodes do not have static and run-time semantics.
--
-- * Conditional ABE - A type of ABE. A conditional ABE occurs when the
-- elaboration or invocation of a target by a scenario within the main
-- unit causes an ABE, but does not cause an ABE for another scenarios
-- within the main unit.
--
-- * Declaration level - A type of enclosing level. A scenario or target is
-- at the declaration level when it appears within the declarations of a
-- block statement, entry body, subprogram body, or task body, ignoring
-- enclosing 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.
--
-- * Guaranteed ABE - A type of ABE. A guaranteed ABE occurs when the
-- elaboration or invocation of a target by all scenarios within the
-- main unit causes an ABE.
--
-- * Instantiation library level - A type of enclosing level. A scenario
-- or target is at the instantiation library level if it appears in an
-- instantiation library unit, ignoring enclosing packages.
--
-- * Library level - A type of enclosing level. A scenario or target is at
-- the library level if it appears in a package library unit, ignoring
-- enclosng packages.
--
-- * Non-library-level encapsulator - A construct that cannot be elaborated
-- on its own and requires elaboration by a top-level scenario.
--
-- * Scenario - A construct or context which may be elaborated or executed
-- by elaboration code. The scenarios recognized by the ABE mechanism are
-- as follows:
--
-- - '[Unrestricted_]Access of entries, operators, and subprograms
--
-- - Assignments to variables
--
-- - Calls to entries, operators, and subprograms
--
-- - Derived type declarations
--
-- - Instantiations
--
-- - Pragma Refined_State
--
-- - Reads of variables
--
-- - Task activation
--
-- * Target - A construct referenced by a scenario. The targets recognized
-- by the ABE mechanism are as follows:
--
-- - For '[Unrestricted_]Access of entries, operators, and subprograms,
-- the target is the entry, operator, or subprogram.
--
-- - For assignments to variables, the target is the variable
--
-- - For calls, the target is the entry, operator, or subprogram
--
-- - For 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
--
-- * Top-level scenario - A scenario which appears in a non-generic main
-- unit. Depending on the elaboration model is in effect, the following
-- addotional restrictions apply:
--
-- - Dynamic model - No restrictions
--
-- - SPARK model - Falls back to either the dynamic or static model
--
-- - Static model - The scenario must be at the library level
---------------------
-- Recording phase --
---------------------
-- The Recording phase coincides with the analysis/resolution phase of the
-- compiler. It has the following objectives:
--
-- * Record all top-level scenarios for examination by the Processing
-- phase.
--
-- Saving only a certain number of nodes improves the performance of
-- the ABE mechanism. This eliminates the need to examine the whole
-- tree in a separate pass.
--
-- * 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.
--
-- This diagnostic is carried out during the Recording phase because it
-- does not need the heavy recursive traversal done by the Processing
-- phase.
--
-- * Detect and diagnose guaranteed ABEs caused by instantiations,
-- calls, and task activation.
--
-- The issues detected by the ABE mechanism are reported as warnings
-- because they do not violate Ada semantics. Forward instantiations
-- may thus reach gigi, however gigi cannot handle certain kinds of
-- premature instantiations and may crash. To avoid this limitation,
-- the ABE mechanism must identify forward instantiations as early as
-- possible and suppress their bodies. Calls and task activations are
-- included in this category for completeness.
----------------------
-- Processing phase --
----------------------
-- The Processing phase is a separate pass which starts after instantiating
-- and/or inlining of bodies, but before the removal of Ghost code. It has
-- the following objectives:
--
-- * Examine all top-level scenarios saved during the Recording phase
--
-- The top-level scenarios act as roots for depth-first traversal of
-- the call/instantiation/task activation graph. The traversal stops
-- when an outgoing edge leaves the main unit.
--
-- * Examine all SPARK scenarios saved during the Recording phase
--
-- * Depending on the elaboration model in effect, perform the following
-- actions:
--
-- - Dynamic model - Install run-time conditional ABE checks.
--
-- - SPARK model - Enforce the SPARK elaboration rules
--
-- - Static model - Diagnose conditional ABEs, install run-time
-- conditional ABE checks, and guarantee the elaboration of
-- external units.
--
-- * Examine nested scenarios
--
-- Nested scenarios discovered during the depth-first traversal are
-- in turn subjected to the same actions outlined above and examined
-- for the next level of nested scenarios.
------------------
-- Architecture --
------------------
-- 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_Conditional_ABE_Instantiation |
-- | | |
-- | +--> Process_Conditional_ABE_Variable_Assignment |
-- | | |
-- | +--> Process_Conditional_ABE_Variable_Reference |
-- | |
-- +--------------------------------------------------------------------+
----------------------
-- Important points --
----------------------
-- The Processing phase starts after the analysis, resolution, expansion
-- phase has completed. As a result, no current semantic information is
-- available. The scope stack is empty, global flags such as In_Instance
-- or Inside_A_Generic become useless. To remedy this, the ABE mechanism
-- must either save or recompute semantic information.
-- Expansion heavily transforms calls and to some extent instantiations. To
-- remedy this, the ABE mechanism generates N_Call_Marker nodes in order to
-- capture the target and relevant attributes of the original call.
-- The diagnostics of the ABE mechanism depend on accurate source locations
-- to determine the spacial relation of nodes.
--------------
-- Switches --
--------------
-- The following switches may be used to control the behavior of the ABE
-- mechanism.
--
-- -gnatd_a stop elaboration checks on accept or select statement
--
-- The ABE mechanism stops the traversal of a task body when it
-- encounters an accept or a select statement. This behavior is
-- equivalent to restriction No_Entry_Calls_In_Elaboration_Code,
-- but without penalizing actual entry calls during elaboration.
--
-- -gnatd_e ignore entry calls and requeue statements for elaboration
--
-- The ABE mechanism does not generate N_Call_Marker nodes for
-- protected or task entry calls as well as requeue statements.
-- As a result, the calls and requeues are not recorded or
-- processed.
--
-- -gnatdE elaboration checks on predefined units
--
-- The ABE mechanism considers scenarios which appear in internal
-- units (Ada, GNAT, Interfaces, System).
--
-- -gnatd.G ignore calls through generic formal parameters for elaboration
--
-- The ABE mechanism does not generate N_Call_Marker nodes for
-- calls which occur in expanded instances, and invoke generic
-- actual subprograms through generic formal subprograms. As a
-- result, the calls are not recorded or processed.
--
-- -gnatd_i ignore activations and calls to instances for elaboration
--
-- The ABE mechanism ignores calls and task activations when they
-- target a subprogram or task type defined an external instance.
-- As a result, the calls and task activations are not processed.
--
-- -gnatdL ignore external calls from instances for elaboration
--
-- The ABE mechanism does not generate N_Call_Marker nodes for
-- calls which occur in expanded instances, do not invoke generic
-- actual subprograms through formal subprograms, and the target
-- is external to the instance. As a result, the calls are not
-- recorded or processed.
--
-- -gnatd.o conservative elaboration order for indirect calls
--
-- The ABE mechanism treats '[Unrestricted_]Access of an entry,
-- operator, or subprogram as an immediate invocation of the
-- target. As a result, it performs ABE checks and diagnostics on
-- the immediate call.
--
-- -gnatd_p ignore assertion pragmas for elaboration
--
-- The ABE mechanism does not generate N_Call_Marker nodes for
-- calls to subprograms which verify the run-time semantics of
-- the following assertion pragmas:
--
-- Default_Initial_Condition
-- Initial_Condition
-- Invariant
-- Invariant'Class
-- Post
-- Post'Class
-- Postcondition
-- Type_Invariant
-- Type_Invariant_Class
--
-- As a result, the assertion expressions of the pragmas are not
-- processed.
--
-- -gnatd.U ignore indirect calls for static elaboration
--
-- The ABE mechanism does not consider '[Unrestricted_]Access of
-- entries, operators, and subprograms. As a result, the scenarios
-- are not recorder or processed.
--
-- -gnatd.v enforce SPARK elaboration rules in SPARK code
--
-- The ABE mechanism applies some of the SPARK elaboration rules
-- defined in the SPARK reference manual, chapter 7.7. Note that
-- certain rules are always enforced, regardless of whether the
-- switch is active.
--
-- -gnatd.y disable implicit pragma Elaborate_All on task bodies
--
-- The ABE mechanism does not generate implicit Elaborate_All when
-- the need for the pragma came from a task body.
--
-- -gnatE dynamic elaboration checking mode enabled
--
-- The ABE mechanism assumes that any scenario is elaborated or
-- invoked by elaboration code. The ABE mechanism performs very
-- little diagnostics and generates condintional ABE checks to
-- detect ABE issues at run-time.
--
-- -gnatel turn on info messages on generated Elaborate[_All] pragmas
--
-- The ABE mechanism produces information messages on generated
-- implicit Elabote[_All] pragmas along with traceback showing
-- why the pragma was generated. In addition, the ABE mechanism
-- produces information messages for each scenario elaborated or
-- invoked by elaboration code.
--
-- -gnateL turn off info messages on generated Elaborate[_All] pragmas
--
-- The complementary switch for -gnatel.
--
-- -gnatH legacy elaboration checking mode enabled
--
-- When this switch is in effect, the pre-18.x ABE model becomes
-- the defacto ABE model. This ammounts to cutting off all entry
-- points into the new ABE mechanism, and giving full control to
-- the old ABE mechanism.
--
-- -gnatJ permissive elaboration checking mode enabled
--
-- This switch activates the following switches:
--
-- -gnatd_a
-- -gnatd_e
-- -gnatd.G
-- -gnatd_i
-- -gnatdL
-- -gnatd_p
-- -gnatd.U
-- -gnatd.y
--
-- IMPORTANT: The behavior of the ABE mechanism becomes more
-- permissive at the cost of accurate diagnostics and runtime
-- ABE checks.
--
-- -gnatw.f turn on warnings for suspicious Subp'Access
--
-- The ABE mechanism treats '[Unrestricted_]Access of an entry,
-- operator, or subprogram as a pseudo invocation of the target.
-- As a result, it performs ABE diagnostics on the pseudo call.
--
-- -gnatw.F turn off warnings for suspicious Subp'Access
--
-- The complementary switch for -gnatw.f.
--
-- -gnatwl turn on warnings for elaboration problems
--
-- The ABE mechanism produces warnings on detected ABEs along with
-- a traceback showing the graph of the ABE.
--
-- -gnatwL turn off warnings for elaboration problems
--
-- The complementary switch for -gnatwl.
---------------------------
-- Adding a new scenario --
---------------------------
-- The following steps describe how to add a new elaboration scenario and
-- preserve the existing architecture. Note that not all of the steps may
-- need to be carried out.
--
-- 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_Conditional_ABE_xxx. Include a call to it in
-- routine Process_Conditional_ABE.
--
-- 5) Add routine Process_Guaranteed_ABE_xxx. Include a call to it in
-- routine Process_Guaranteed_ABE.
--
-- 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.
--
-- 9) Add routine Extract_xxx_Attributes
--
-- 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. Note that not all of the steps may
-- need to be carried out.
--
-- 1) Add predicate Is_xxx.
--
-- 2) Update the following predicates
--
-- Is_Ada_Semantic_Target
-- Is_Assertion_Pragma_Target
-- Is_Bridge_Target
-- Is_SPARK_Semantic_Target
--
-- If necessary, create a new category.
--
-- 3) Update the appropriate Info_xxx routine.
--
-- 4) Update the appropriate Output_xxx routine.
--
-- 5) Update routine Extract_Target_Attributes. If necessary, create a
-- new Extract_xxx routine.
--------------------------
-- Debugging ABE issues --
--------------------------
-- * If the issue involves a call, ensure that the call is eligible for ABE
-- processing and receives a corresponding call marker. The routines of
-- interest are
--
-- Build_Call_Marker
-- Record_Elaboration_Scenario
-- * If the issue involves an arbitrary scenario, ensure that the scenario
-- is either recorded, or is successfully recognized while traversing a
-- body. The routines of interest are
--
-- Record_Elaboration_Scenario
-- Process_Conditional_ABE
-- Process_Guaranteed_ABE
-- Traverse_Body
-- * If the issue involves a circularity in the elaboration order, examine
-- the ALI files and look for the following encodings next to units:
--
-- E indicates a source Elaborate
--
-- EA indicates a source Elaborate_All
--
-- AD indicates an implicit Elaborate_All
--
-- ED indicates an implicit Elaborate
--
-- If possible, compare these encodings with those generated by the old
-- ABE mechanism. The routines of interest are
--
-- Ensure_Prior_Elaboration
----------------
-- Attributes --
----------------
-- 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
Elab_Checks_OK : Boolean;
-- This flag is set when the call has elaboration checks enabled
Elab_Warnings_OK : Boolean;
-- This flag is set when the call has elaboration warnings elabled
From_Source : Boolean;
-- This flag is set when the call comes from source
Ghost_Mode_Ignore : Boolean;
-- This flag is set when the call appears in a region subject to pragma
-- Ghost with policy Ignore.
In_Declarations : Boolean;
-- This flag is set when the call appears at the declaration level
Is_Dispatching : Boolean;
-- This flag is set when the call is dispatching
SPARK_Mode_On : Boolean;
-- This flag is set when the call appears in a region subject to pragma
-- SPARK_Mode with value On.
end record;
-- The following type captures relevant attributes which pertain to the
-- prior elaboration of a unit. This type is coupled together with a unit
-- to form a key -> value relationship.
type Elaboration_Attributes is record
Source_Pragma : Node_Id;
-- This attribute denotes a source Elaborate or Elaborate_All pragma
-- which guarantees the prior elaboration of some unit with respect
-- to the main unit. The pragma may come from the following contexts:
-- * The main unit
-- * The spec of the main unit (if applicable)
-- * Any parent spec of the main unit (if applicable)
-- * Any parent subunit of the main unit (if applicable)
-- The attribute remains Empty if no such pragma is available. Source
-- pragmas play a role in satisfying SPARK elaboration requirements.
With_Clause : Node_Id;
-- This attribute denotes an internally generated or source with clause
-- for some unit withed by the main unit. With clauses carry flags which
-- represent implicit Elaborate or Elaborate_All pragmas. These clauses
-- play a role in supplying the elaboration dependencies to binde.
end record;
No_Elaboration_Attributes : constant Elaboration_Attributes :=
(Source_Pragma => Empty,
With_Clause => Empty);
-- The following type captures relevant attributes which pertain to an
-- instantiation.
type Instantiation_Attributes is record
Elab_Checks_OK : Boolean;
-- This flag is set when the instantiation has elaboration checks
-- enabled.
Elab_Warnings_OK : Boolean;
-- This flag is set when the instantiation has elaboration warnings
-- enabled.
Ghost_Mode_Ignore : Boolean;
-- This flag is set when the instantiation appears in a region subject
-- to pragma Ghost with policy ignore, or starts one such region.
In_Declarations : Boolean;
-- This flag is set when the instantiation appears at the declaration
-- level.
SPARK_Mode_On : Boolean;
-- This flag is set when the instantiation appears in a region subject
-- to pragma SPARK_Mode with value On, or starts one such region.
end record;
-- The following type captures relevant attributes which pertain to the
-- state of the Processing phase.
type Processing_Attributes is record
Suppress_Implicit_Pragmas : Boolean;
-- This flag is set when the Processing phase must not generate any
-- implicit Elaborate[_All] pragmas.
Within_Initial_Condition : Boolean;
-- This flag is set when the Processing phase is currently examining a
-- scenario which was reached from an initial condition procedure.
Within_Instance : Boolean;
-- This flag is set when the Processing phase is currently examining a
-- scenario which was reached from a scenario defined in an instance.
Within_Partial_Finalization : Boolean;
-- This flag is set when the Processing phase is currently examining a
-- scenario which was reached from a partial finalization procedure.
Within_Task_Body : Boolean;
-- This flag is set when the Processing phase is currently examining a
-- scenario which was reached from a task body.
end record;
Initial_State : constant Processing_Attributes :=
(Suppress_Implicit_Pragmas => False,
Within_Initial_Condition => False,
Within_Instance => False,
Within_Partial_Finalization => False,
Within_Task_Body => False);
-- The following type captures relevant attributes which pertain to a
-- target.
type Target_Attributes is record
Elab_Checks_OK : Boolean;
-- This flag is set when the target has elaboration checks enabled
From_Source : Boolean;
-- This flag is set when the target comes from source
Ghost_Mode_Ignore : Boolean;
-- This flag is set when the target appears in a region subject to
-- pragma Ghost with policy ignore, or starts one such region.
SPARK_Mode_On : Boolean;
-- This flag is set when the target appears in a region subject to
-- pragma SPARK_Mode with value On, or starts one such region.
Spec_Decl : Node_Id;
-- This attribute denotes the declaration of Spec_Id
Unit_Id : Entity_Id;
-- This attribute denotes the top unit where Spec_Id resides
-- The semantics of the following attributes depend on the target
Body_Barf : Node_Id;
Body_Decl : Node_Id;
Spec_Id : Entity_Id;
-- The target is a generic package or a subprogram
--
-- * Body_Barf - Empty
--
-- * Body_Decl - This attribute denotes the generic or subprogram
-- body.
--
-- * Spec_Id - This attribute denotes the entity of the generic
-- package or subprogram.
-- The target is a protected entry
--
-- * Body_Barf - This attribute denotes the body of the barrier
-- function if expansion took place, otherwise it is Empty.
--
-- * Body_Decl - This attribute denotes the body of the procedure
-- which emulates the entry if expansion took place, otherwise it
-- denotes the body of the protected entry.
--
-- * Spec_Id - This attribute denotes the entity of the procedure
-- which emulates the entry if expansion took place, otherwise it
-- denotes the protected entry.
-- The target is a protected subprogram
--
-- * Body_Barf - Empty
--
-- * Body_Decl - This attribute denotes the body of the protected or
-- unprotected version of the protected subprogram if expansion took
-- place, otherwise it denotes the body of the protected subprogram.
--
-- * Spec_Id - This attribute denotes the entity of the protected or
-- unprotected version of the protected subprogram if expansion took
-- place, otherwise it is the entity of the protected subprogram.
-- The target is a task entry
--
-- * Body_Barf - Empty
--
-- * Body_Decl - This attribute denotes the body of the procedure
-- which emulates the task body if expansion took place, otherwise
-- it denotes the body of the task type.
--
-- * Spec_Id - This attribute denotes the entity of the procedure
-- which emulates the task body if expansion took place, otherwise
-- it denotes the entity of the task type.
end record;
-- The following type captures relevant attributes which pertain to a task
-- type.
type Task_Attributes is record
Body_Decl : Node_Id;
-- This attribute denotes the declaration of the procedure body which
-- emulates the behaviour of the task body.
Elab_Checks_OK : Boolean;
-- This flag is set when the task type has elaboration checks enabled
Ghost_Mode_Ignore : Boolean;
-- This flag is set when the task type appears in a region subject to
-- pragma Ghost with policy ignore, or starts one such region.
SPARK_Mode_On : Boolean;
-- This flag is set when the task type appears in a region subject to
-- pragma SPARK_Mode with value On, or starts one such region.
Spec_Id : Entity_Id;
-- This attribute denotes the entity of the initial declaration of the
-- procedure body which emulates the behaviour of the task body.
Task_Decl : Node_Id;
-- This attribute denotes the declaration of the task type
Unit_Id : Entity_Id;
-- This attribute denotes the entity of the compilation unit where the
-- task type resides.
end record;
-- The following type captures relevant attributes which pertain to a
-- variable.
type Variable_Attributes is record
Unit_Id : Entity_Id;
-- This attribute denotes the entity of the compilation unit where the
-- variable resides.
end 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 determines whether table Early_Call_Regions contains at least
-- 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_Statuses_Max : constant := 1009;
type Elaboration_Statuses_Index is range 0 .. Elaboration_Statuses_Max - 1;
function Elaboration_Statuses_Hash
(Key : Entity_Id) return Elaboration_Statuses_Index;
-- Obtain the hash value of entity Key
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 => Elaboration_Statuses_No_Element,
Key => Entity_Id,
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
-- recorded in table Top_Level_Scenarios.
Recorded_Top_Level_Scenarios_Max : constant := 503;
type Recorded_Top_Level_Scenarios_Index is
range 0 .. Recorded_Top_Level_Scenarios_Max - 1;
function Recorded_Top_Level_Scenarios_Hash
(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 => Recorded_Top_Level_Scenarios_No_Element,
Key => Node_Id,
Hash => Recorded_Top_Level_Scenarios_Hash,
Equal => "=");
-- The following table stores all active scenarios in a recursive traversal
-- starting from a top-level scenario. This table must be maintained in a
-- FIFO fashion.
package Scenario_Stack is new Table.Table
(Table_Component_Type => Node_Id,
Table_Index_Type => Int,
Table_Low_Bound => 1,
Table_Initial => 50,
Table_Increment => 100,
Table_Name => "Scenario_Stack");
-- The following table stores 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
-- LIFO fashion.
package Top_Level_Scenarios is new Table.Table
(Table_Component_Type => Node_Id,
Table_Index_Type => Int,
Table_Low_Bound => 1,
Table_Initial => 1000,
Table_Increment => 100,
Table_Name => "Top_Level_Scenarios");
-- The following table stores the bodies of all eligible scenarios visited
-- during a traversal starting from a top-level scenario. The contents of
-- this table must be reset upon each new traversal.
Visited_Bodies_Max : constant := 511;
type Visited_Bodies_Index is range 0 .. Visited_Bodies_Max - 1;
function Visited_Bodies_Hash (Key : Node_Id) return Visited_Bodies_Index;
-- Obtain the hash value of node Key
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 => 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);
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_Model_In_Effect (N : Node_Id);
pragma Inline (Check_SPARK_Model_In_Effect);
-- Determine whether a suitable elaboration model is currently in effect
-- for verifying the SPARK rules of scenario N. Emit a warning if this is
-- not the case.
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;
Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
pragma Inline (Elab_Msg_NE);
-- Wrapper around Error_Msg_NE. Emit message Msg concerning arbitrary node
-- N and entity. If flag Info_Msg is set, the routine emits an information
-- message, otherwise it emits an error. If flag In_SPARK is set, then
-- string " in SPARK" is added to the end of the message.
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;
State : Processing_Attributes);
-- 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. State denotes the current state of the
-- Processing phase.
procedure Ensure_Prior_Elaboration_Dynamic
(N : Node_Id;
Unit_Id : Entity_Id;
Prag_Nam : Name_Id);
-- Guarantee the elaboration of unit Unit_Id with respect to the main unit
-- by suggesting the use of Elaborate[_All] with name Prag_Nam. N denotes
-- the related scenario.
procedure Ensure_Prior_Elaboration_Static
(N : Node_Id;
Unit_Id : Entity_Id;
Prag_Nam : Name_Id);
-- Guarantee the elaboration of unit Unit_Id with respect to the main unit
-- by installing an implicit Elaborate[_All] pragma with name Prag_Nam. N
-- denotes the related scenario.
function Extract_Assignment_Name (Asmt : Node_Id) return Node_Id;
pragma Inline (Extract_Assignment_Name);
-- Obtain the Name attribute of assignment statement Asmt
procedure Extract_Call_Attributes
(Call : Node_Id;
Target_Id : out Entity_Id;
Attrs : out Call_Attributes);
pragma Inline (Extract_Call_Attributes);
-- Obtain attributes Attrs associated with call Call. Target_Id is the
-- entity of the call target.
function Extract_Call_Name (Call : Node_Id) return Node_Id;
pragma Inline (Extract_Call_Name);
-- Obtain the Name attribute of entry or subprogram call Call
procedure Extract_Instance_Attributes
(Exp_Inst : Node_Id;
Inst_Body : out Node_Id;
Inst_Decl : out Node_Id);
pragma Inline (Extract_Instance_Attributes);
-- Obtain body Inst_Body and spec Inst_Decl of expanded instance Exp_Inst
procedure Extract_Instantiation_Attributes
(Exp_Inst : Node_Id;
Inst : out Node_Id;
Inst_Id : out Entity_Id;
Gen_Id : out Entity_Id;
Attrs : out Instantiation_Attributes);
pragma Inline (Extract_Instantiation_Attributes);
-- Obtain attributes Attrs associated with expanded instantiation Exp_Inst.
-- Inst is the instantiation. Inst_Id is the entity of the instance. Gen_Id
-- is the entity of the generic unit being instantiated.
procedure Extract_Target_Attributes
(Target_Id : Entity_Id;
Attrs : out Target_Attributes);
-- Obtain attributes Attrs associated with an entry, package, or subprogram
-- denoted by Target_Id.
procedure Extract_Task_Attributes
(Typ : Entity_Id;
Attrs : out Task_Attributes);
pragma Inline (Extract_Task_Attributes);
-- Obtain attributes Attrs associated with task type Typ
procedure Extract_Variable_Reference_Attributes
(Ref : Node_Id;
Var_Id : out Entity_Id;
Attrs : out Variable_Attributes);
pragma Inline (Extract_Variable_Reference_Attributes);
-- Obtain attributes Attrs associated with reference Ref that mentions
-- variable Var_Id.
function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id;
pragma Inline (Find_Code_Unit);
-- Return the code unit which contains arbitrary node or entity N. This
-- is the unit of the file which physically contains the related construct
-- denoted by N except when N is within an instantiation. In that case the
-- unit is that of the top-level instantiation.
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_Statuses with all units which have prior
-- elaboration with respect to the main unit.
function Find_Enclosing_Instance (N : Node_Id) return Node_Id;
pragma Inline (Find_Enclosing_Instance);
-- Find the declaration or body of the nearest expanded instance which
-- encloses arbitrary node N. Return Empty if no such instance exists.
function Find_Top_Unit (N : Node_Or_Entity_Id) return Entity_Id;
pragma Inline (Find_Top_Unit);
-- Return the top unit which contains arbitrary node or entity N. The unit
-- is obtained by logically unwinding instantiations and subunits when N
-- resides within one.
function Find_Unit_Entity (N : Node_Id) return Entity_Id;
pragma Inline (Find_Unit_Entity);
-- Return the entity of unit N
function First_Formal_Type (Subp_Id : Entity_Id) return Entity_Id;
pragma Inline (First_Formal_Type);
-- Return the type of subprogram Subp_Id's first formal parameter. If the
-- subprogram lacks formal parameters, return Empty.
function Has_Body (Pack_Decl : Node_Id) return Boolean;
-- Determine whether package declaration Pack_Decl has a corresponding body
-- or would eventually have one.
function Has_Prior_Elaboration
(Unit_Id : Entity_Id;
Context_OK : Boolean := False;
Elab_Body_OK : Boolean := False;
Same_Unit_OK : Boolean := False) return Boolean;
pragma Inline (Has_Prior_Elaboration);
-- Determine whether unit Unit_Id is elaborated prior to the main unit.
-- If flag Context_OK is set, the routine considers the following case
-- as valid prior elaboration:
--
-- * Unit_Id is in the elaboration context of the main unit
--
-- If flag Elab_Body_OK is set, the routine considers the following case
-- as valid prior elaboration:
--
-- * Unit_Id has pragma Elaborate_Body and is not the main unit
--
-- If flag Same_Unit_OK is set, the routine considers the following cases
-- as valid prior elaboration:
--
-- * Unit_Id is the main unit
--
-- * Unit_Id denotes the spec of the main unit body
function In_External_Instance
(N : Node_Id;
Target_Decl : Node_Id) return Boolean;
pragma Inline (In_External_Instance);
-- Determine whether a target desctibed by its declaration Target_Decl
-- resides in a package instance which is external to scenario N.
function In_Main_Context (N : Node_Id) return Boolean;
pragma Inline (In_Main_Context);
-- Determine whether arbitrary node N appears within the main compilation
-- unit.
function In_Same_Context
(N1 : Node_Id;
N2 : Node_Id;
Nested_OK : Boolean := False) return Boolean;
-- Determine whether two arbitrary nodes N1 and N2 appear within the same
-- context ignoring enclosing library levels. Nested_OK should be set when
-- the context of N1 can enclose that of N2.
procedure Info_Call
(Call : Node_Id;
Target_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
-- Output information concerning call Call which invokes target Target_Id.
-- If flag Info_Msg is set, the routine emits an information message,
-- otherwise it emits an error. If flag In_SPARK is set, then the string
-- " in SPARK" is added to the end of the message.
procedure Info_Instantiation
(Inst : Node_Id;
Gen_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
pragma Inline (Info_Instantiation);
-- Output information concerning instantiation Inst which instantiates
-- generic unit Gen_Id. If flag Info_Msg is set, the routine emits an
-- information message, otherwise it emits an error. If flag In_SPARK
-- is set, then string " in SPARK" is added to the end of the message.
procedure Info_Variable_Reference
(Ref : Node_Id;
Var_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
pragma Inline (Info_Variable_Reference);
-- Output information concerning reference Ref which mentions variable
-- Var_Id. If flag Info_Msg is set, the routine emits an information
-- message, otherwise it emits an error. If flag In_SPARK is set, then
-- string " in SPARK" is added to the end of the message.
function Insertion_Node (N : Node_Id; Ins_Nod : Node_Id) return Node_Id;
pragma Inline (Insertion_Node);
-- Obtain the proper insertion node of an ABE check or failure for scenario
-- N and candidate insertion node Ins_Nod.
procedure Install_ABE_Check
(N : Node_Id;
Id : Entity_Id;
Ins_Nod : Node_Id);
-- Insert a run-time ABE check for elaboration scenario N which verifies
-- whether arbitrary entity Id is elaborated. The check in inserted prior
-- to node Ins_Nod.
procedure Install_ABE_Check
(N : Node_Id;
Target_Id : Entity_Id;
Target_Decl : Node_Id;
Target_Body : Node_Id;
Ins_Nod : Node_Id);
-- Insert a run-time ABE check for elaboration scenario N which verifies
-- whether target Target_Id with initial declaration Target_Decl and body
-- Target_Body is elaborated. The check is inserted prior to node Ins_Nod.
procedure Install_ABE_Failure (N : Node_Id; Ins_Nod : Node_Id);
-- Insert a Program_Error concerning a guaranteed ABE for elaboration
-- scenario N. The failure is inserted prior to node Node_Id.
function Is_Accept_Alternative_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Accept_Alternative_Proc);
-- Determine whether arbitrary entity Id denotes an internally generated
-- procedure which encapsulates the statements of an accept alternative.
function Is_Activation_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Activation_Proc);
-- Determine whether arbitrary entity Id denotes a runtime procedure in
-- charge with activating tasks.
function Is_Ada_Semantic_Target (Id : Entity_Id) return Boolean;
pragma Inline (Is_Ada_Semantic_Target);
-- Determine whether arbitrary entity Id denodes a source or internally
-- generated subprogram which emulates Ada semantics.
function Is_Assertion_Pragma_Target (Id : Entity_Id) return Boolean;
pragma Inline (Is_Assertion_Pragma_Target);
-- Determine whether arbitrary entity Id denotes a procedure which varifies
-- the run-time semantics of an assertion pragma.
function Is_Bodiless_Subprogram (Subp_Id : Entity_Id) return Boolean;
pragma Inline (Is_Bodiless_Subprogram);
-- Determine whether subprogram Subp_Id will never have a body
function Is_Controlled_Proc
(Subp_Id : Entity_Id;
Subp_Nam : Name_Id) return Boolean;
pragma Inline (Is_Controlled_Proc);
-- Determine whether subprogram Subp_Id denotes controlled type primitives
-- Adjust, Finalize, or Initialize as denoted by name Subp_Nam.
function Is_Default_Initial_Condition_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Default_Initial_Condition_Proc);
-- Determine whether arbitrary entity Id denotes internally generated
-- routine Default_Initial_Condition.
function Is_Finalizer_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Finalizer_Proc);
-- Determine whether arbitrary entity Id denotes internally generated
-- routine _Finalizer.
function Is_Guaranteed_ABE
(N : Node_Id;
Target_Decl : Node_Id;
Target_Body : Node_Id) return Boolean;
pragma Inline (Is_Guaranteed_ABE);
-- Determine whether scenario N with a target described by its initial
-- declaration Target_Decl and body Target_Decl results in a guaranteed
-- ABE.
function Is_Initial_Condition_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Initial_Condition_Proc);
-- Determine whether arbitrary entity Id denotes internally generated
-- routine Initial_Condition.
function Is_Initialized (Obj_Decl : Node_Id) return Boolean;
pragma Inline (Is_Initialized);
-- Determine whether object declaration Obj_Decl is initialized
function Is_Invariant_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Invariant_Proc);
-- Determine whether arbitrary entity Id denotes an invariant procedure
function Is_Non_Library_Level_Encapsulator (N : Node_Id) return Boolean;
pragma Inline (Is_Non_Library_Level_Encapsulator);
-- Determine whether arbitrary node N is a non-library encapsulator
function Is_Partial_Invariant_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Partial_Invariant_Proc);
-- Determine whether arbitrary entity Id denotes a partial invariant
-- procedure.
function Is_Postconditions_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Postconditions_Proc);
-- Determine whether arbitrary entity Id denotes internally generated
-- routine _Postconditions.
function Is_Preelaborated_Unit (Id : Entity_Id) return Boolean;
pragma Inline (Is_Preelaborated_Unit);
-- Determine whether arbitrary entity Id denotes a unit which is subject to
-- one of the following pragmas:
--
-- * Preelaborable
-- * Pure
-- * Remote_Call_Interface
-- * Remote_Types
-- * Shared_Passive
function Is_Protected_Entry (Id : Entity_Id) return Boolean;
pragma Inline (Is_Protected_Entry);
-- Determine whether arbitrary entity Id denotes a protected entry
function Is_Protected_Subp (Id : Entity_Id) return Boolean;
pragma Inline (Is_Protected_Subp);
-- Determine whether entity Id denotes a protected subprogram
function Is_Protected_Body_Subp (Id : Entity_Id) return Boolean;
pragma Inline (Is_Protected_Body_Subp);
-- Determine whether entity Id denotes the protected or unprotected version
-- of a protected subprogram.
function Is_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 N is a recorded top-level scenario
-- which appears in table Top_Level_Scenarios.
function Is_Safe_Activation
(Call : Node_Id;
Task_Decl : Node_Id) return Boolean;
pragma Inline (Is_Safe_Activation);
-- Determine whether call Call which activates a task object described by
-- declaration Task_Decl is always ABE-safe.
function Is_Safe_Call
(Call : Node_Id;
Target_Attrs : Target_Attributes) return Boolean;
pragma Inline (Is_Safe_Call);
-- Determine whether call Call which invokes a target described by
-- attributes Target_Attrs is always ABE-safe.
function Is_Safe_Instantiation
(Inst : Node_Id;
Gen_Attrs : Target_Attributes) return Boolean;
pragma Inline (Is_Safe_Instantiation);
-- Determine whether instance Inst which instantiates a generic unit
-- described by attributes Gen_Attrs is always ABE-safe.
function Is_Same_Unit
(Unit_1 : Entity_Id;
Unit_2 : Entity_Id) return Boolean;
pragma Inline (Is_Same_Unit);
-- Determine whether entities Unit_1 and Unit_2 denote the same unit
function Is_Scenario (N : Node_Id) return Boolean;
pragma Inline (Is_Scenario);
-- Determine whether attribute node N denotes a scenario. The scenario may
-- not necessarily be eligible for ABE processing.
function Is_SPARK_Semantic_Target (Id : Entity_Id) return Boolean;
pragma Inline (Is_SPARK_Semantic_Target);
-- Determine whether arbitrary entity Id nodes a source or internally
-- generated subprogram which emulates SPARK semantics.
function Is_Suitable_Access (N : Node_Id) return Boolean;
pragma Inline (Is_Suitable_Access);
-- Determine whether arbitrary node N denotes a suitable attribute for ABE
-- processing.
function Is_Suitable_Call (N : Node_Id) return Boolean;
pragma Inline (Is_Suitable_Call);
-- Determine whether arbitrary node N denotes a suitable call for ABE
-- processing.
function Is_Suitable_Instantiation (N : Node_Id) return Boolean;
pragma Inline (Is_Suitable_Instantiation);
-- Determine whether arbitrary node N is a suitable instantiation for ABE
-- processing.
function Is_Suitable_Scenario (N : Node_Id) return Boolean;
pragma Inline (Is_Suitable_Scenario);
-- Determine whether arbitrary node N is a suitable scenario for ABE
-- processing.
function Is_Suitable_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
-- processing.
function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean;
pragma Inline (Is_Suitable_Variable_Reference);
-- Determine whether arbitrary node N is a suitable variable reference for
-- ABE processing.
function Is_Task_Entry (Id : Entity_Id) return Boolean;
pragma Inline (Is_Task_Entry);
-- Determine whether arbitrary entity Id denotes a task entry
function Is_Up_Level_Target (Target_Decl : Node_Id) return Boolean;
pragma Inline (Is_Up_Level_Target);
-- Determine whether the current root resides at the declaration level. If
-- this is the case, determine whether a target described by declaration
-- Target_Decl is within a context which encloses the current root or is in
-- a different unit.
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;
Req_Nam : Name_Id);
-- Determine whether elaboration requirement Req_Nam for scenario N with
-- target Target_Id is met by the context of the main unit using the SPARK
-- rules. Req_Nam must denote either Elaborate or Elaborate_All. Emit an
-- error if this is not the case.
function Non_Private_View (Typ : Entity_Id) return Entity_Id;
pragma Inline (Non_Private_View);
-- Return the full view of private type Typ if available, otherwise return
-- type Typ.
procedure Output_Active_Scenarios (Error_Nod : Node_Id);
-- Output the contents of the active scenario stack from earliest to latest
-- to supplement an earlier error emitted for node Error_Nod.
procedure Pop_Active_Scenario (N : Node_Id);
pragma Inline (Pop_Active_Scenario);
-- Pop the top of the scenario stack. A check is made to ensure that the
-- scenario being removed is the same as N.
generic
with procedure Process_Single_Activation
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Obj_Id : Entity_Id;
Task_Attrs : Task_Attributes;
State : Processing_Attributes);
-- 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.
-- State is the current state of the Processing phase.
procedure Process_Activation_Generic
(Call : Node_Id;
Call_Attrs : Call_Attributes;
State : Processing_Attributes);
-- 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. State is the
-- current state of the Processing phase.
procedure Process_Conditional_ABE
(N : Node_Id;
State : Processing_Attributes := Initial_State);
-- Top-level dispatcher for processing of various elaboration scenarios.
-- Perform conditional ABE checks and diagnostics for scenario N. State
-- is the current state of the Processing phase.
procedure Process_Conditional_ABE_Access
(Attr : Node_Id;
State : Processing_Attributes);
-- Perform ABE checks and diagnostics for 'Access to entry, operator, or
-- subprogram denoted by Attr. State is the current state of the Processing
-- phase.
procedure Process_Conditional_ABE_Activation_Impl
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Obj_Id : Entity_Id;
Task_Attrs : Task_Attributes;
State : Processing_Attributes);
-- 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. State is the current state of the Processing phase.
procedure Process_Conditional_ABE_Call
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
State : Processing_Attributes);
-- 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. State is the current state of the
-- Processing phase.
procedure Process_Conditional_ABE_Call_Ada
(Call : Node_Id;
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
Target_Attrs : Target_Attributes;
State : Processing_Attributes);
-- 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. State is the current
-- state of the Processing phase.
procedure Process_Conditional_ABE_Call_SPARK
(Call : Node_Id;
Target_Id : Entity_Id;
Target_Attrs : Target_Attributes;
State : Processing_Attributes);
-- Perform ABE checks and diagnostics for call Call which invokes target
-- Target_Id using the SPARK rules. Target_Attrs denotes the attributes of
-- the target. State is the current state of the Processing phase.
procedure Process_Conditional_ABE_Instantiation
(Exp_Inst : Node_Id;
State : Processing_Attributes);
-- Top-level dispatcher for processing of instantiations. Perform ABE
-- checks and diagnostics for expanded instantiation Exp_Inst. State is
-- the current state of the Processing phase.
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;
State : Processing_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. State is the current state of the Processing
-- phase.
procedure Process_Conditional_ABE_Instantiation_SPARK
(Inst : Node_Id;
Gen_Id : Entity_Id;
Gen_Attrs : Target_Attributes;
State : Processing_Attributes);
-- Perform ABE checks and diagnostics for instantiation Inst of generic
-- Gen_Id using the SPARK rules. Gen_Attrs denotes the attributes of the
-- generic. State is the current state of the Processing phase.
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_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_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_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_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;
State : Processing_Attributes);
-- Perform common guaranteed ABE checks and diagnostics for call Call which
-- activates task Obj_Id ignoring the Ada or SPARK rules. Call_Attrs are
-- the attributes of the activation call. Task_Attrs are the attributes of
-- the task type. State is provided for compatibility and is not used.
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; State : Processing_Attributes);
-- Inspect the declarative and statement lists of subprogram body N for
-- suitable elaboration scenarios and process them. State is the current
-- state of the Processing phase.
procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id);
pragma Inline (Update_Elaboration_Scenario);
-- Update all relevant internal data structures when scenario Old_N is
-- transformed into scenario New_N by Atree.Rewrite.
-----------------------
-- Build_Call_Marker --
-----------------------
procedure Build_Call_Marker (N : Node_Id) is
function In_External_Context
(Call : Node_Id;
Target_Attrs : Target_Attributes) return Boolean;
pragma Inline (In_External_Context);
-- Determine whether a target described by attributes Target_Attrs is
-- external to call Call which must reside within an instance.
function In_Premature_Context (Call : Node_Id) return Boolean;
-- Determine whether call Call appears within a premature context
function Is_Bridge_Target (Id : Entity_Id) return Boolean;
pragma Inline (Is_Bridge_Target);
-- Determine whether arbitrary entity Id denotes a bridge target
function Is_Default_Expression (Call : Node_Id) return Boolean;
pragma Inline (Is_Default_Expression);
-- Determine whether call Call acts as the expression of a defaulted
-- parameter within a source call.
function Is_Generic_Formal_Subp (Subp_Id : Entity_Id) return Boolean;
pragma Inline (Is_Generic_Formal_Subp);
-- Determine whether subprogram Subp_Id denotes a generic formal
-- subprogram which appears in the "prologue" of an instantiation.
-------------------------
-- In_External_Context --
-------------------------
function In_External_Context
(Call : Node_Id;
Target_Attrs : Target_Attributes) return Boolean
is
Inst : Node_Id;
Inst_Body : Node_Id;
Inst_Decl : Node_Id;
begin
-- Performance note: parent traversal
Inst := Find_Enclosing_Instance (Call);
-- The call appears within an instance
if Present (Inst) then
-- The call comes from the main unit and the target does not
if In_Extended_Main_Code_Unit (Call)
and then not In_Extended_Main_Code_Unit (Target_Attrs.Spec_Decl)
then
return True;
-- Otherwise the target declaration must not appear within the
-- instance spec or body.
else
Extract_Instance_Attributes
(Exp_Inst => Inst,
Inst_Decl => Inst_Decl,
Inst_Body => Inst_Body);
-- Performance note: parent traversal
return not In_Subtree
(N => Target_Attrs.Spec_Decl,
Root1 => Inst_Decl,
Root2 => Inst_Body);
end if;
end if;
return False;
end In_External_Context;
--------------------------
-- In_Premature_Context --
--------------------------
function In_Premature_Context (Call : Node_Id) return Boolean is
Par : Node_Id;
begin
-- Climb the parent chain looking for premature contexts
Par := Parent (Call);
while Present (Par) loop
-- Aspect specifications and generic associations are premature
-- contexts because nested calls has not been relocated to their
-- final context.
if Nkind_In (Par, N_Aspect_Specification,
N_Generic_Association)
then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Par := Parent (Par);
end loop;
return False;
end In_Premature_Context;
----------------------
-- Is_Bridge_Target --
----------------------
function Is_Bridge_Target (Id : Entity_Id) return Boolean is
begin
return
Is_Accept_Alternative_Proc (Id)
or else Is_Finalizer_Proc (Id)
or else Is_Partial_Invariant_Proc (Id)
or else Is_Postconditions_Proc (Id)
or else Is_TSS (Id, TSS_Deep_Adjust)
or else Is_TSS (Id, TSS_Deep_Finalize)
or else Is_TSS (Id, TSS_Deep_Initialize);
end Is_Bridge_Target;
---------------------------
-- Is_Default_Expression --
---------------------------
function Is_Default_Expression (Call : Node_Id) return Boolean is
Outer_Call : constant Node_Id := Parent (Call);
Outer_Nam : Node_Id;
begin
-- To qualify, the node must appear immediately within a source call
-- which invokes a source target.
if Nkind_In (Outer_Call, N_Entry_Call_Statement,
N_Function_Call,
N_Procedure_Call_Statement)
and then Comes_From_Source (Outer_Call)
then
Outer_Nam := Extract_Call_Name (Outer_Call);
return
Is_Entity_Name (Outer_Nam)
and then Present (Entity (Outer_Nam))
and then Is_Subprogram_Or_Entry (Entity (Outer_Nam))
and then Comes_From_Source (Entity (Outer_Nam));
end if;
return False;
end Is_Default_Expression;
----------------------------
-- Is_Generic_Formal_Subp --
----------------------------
function Is_Generic_Formal_Subp (Subp_Id : Entity_Id) return Boolean is
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
Context : constant Node_Id := Parent (Subp_Decl);
begin
-- To qualify, the subprogram must rename a generic actual subprogram
-- where the enclosing context is an instantiation.
return
Nkind (Subp_Decl) = N_Subprogram_Renaming_Declaration
and then not Comes_From_Source (Subp_Decl)
and then Nkind_In (Context, N_Function_Specification,
N_Package_Specification,
N_Procedure_Specification)
and then Present (Generic_Parent (Context));
end Is_Generic_Formal_Subp;
-- Local variables
Call_Attrs : Call_Attributes;
Call_Nam : Node_Id;
Marker : Node_Id;
Target_Attrs : Target_Attributes;
Target_Id : Entity_Id;
-- Start of processing for Build_Call_Marker
begin
-- Nothing to do when switch -gnatH (legacy elaboration checking mode
-- enabled) is in effect because the legacy ABE mechanism does not need
-- to carry out this action.
if Legacy_Elaboration_Checks then
return;
-- Nothing to do for ASIS. As a result, ABE checks and diagnostics are
-- not performed in this mode.
elsif ASIS_Mode then
return;
-- Nothing to do when the call is being preanalyzed as the marker will
-- be inserted in the wrong place.
elsif Preanalysis_Active then
return;
-- Nothing to do when the input does not denote a call or a requeue
elsif not Nkind_In (N, N_Entry_Call_Statement,
N_Function_Call,
N_Procedure_Call_Statement,
N_Requeue_Statement)
then
return;
-- Nothing to do when the input denotes entry call or requeue statement,
-- and switch -gnatd_e (ignore entry calls and requeue statements for
-- elaboration) is in effect.
elsif Debug_Flag_Underscore_E
and then Nkind_In (N, N_Entry_Call_Statement, N_Requeue_Statement)
then
return;
end if;
Call_Nam := Extract_Call_Name (N);
-- Nothing to do when the call is erroneous or left in a bad state
if not (Is_Entity_Name (Call_Nam)
and then Present (Entity (Call_Nam))
and then Is_Subprogram_Or_Entry (Entity (Call_Nam)))
then
return;
-- Nothing to do when the call invokes a generic formal subprogram and
-- switch -gnatd.G (ignore calls through generic formal parameters for
-- elaboration) is in effect. This check must be performed with the
-- direct target of the call to avoid the side effects of mapping
-- actuals to formals using renamings.
elsif Debug_Flag_Dot_GG
and then Is_Generic_Formal_Subp (Entity (Call_Nam))
then
return;
-- Nothing to do when the call is analyzed/resolved too early within an
-- intermediate context. This check is saved for last because it incurs
-- a performance penalty.
-- Performance note: parent traversal
elsif In_Premature_Context (N) then
return;
end if;
Extract_Call_Attributes
(Call => N,
Target_Id => Target_Id,
Attrs => Call_Attrs);
Extract_Target_Attributes
(Target_Id => Target_Id,
Attrs => Target_Attrs);
-- Nothing to do when the call appears within the expanded spec or
-- body of an instantiated generic, the call does not invoke a generic
-- formal subprogram, the target is external to the instance, and switch
-- -gnatdL (ignore external calls from instances for elaboration) is in
-- effect.
if Debug_Flag_LL
and then not Is_Generic_Formal_Subp (Entity (Call_Nam))
-- Performance note: parent traversal
and then In_External_Context
(Call => N,
Target_Attrs => Target_Attrs)
then
return;
-- Nothing to do when the call invokes an assertion pragma procedure
-- and switch -gnatd_p (ignore assertion pragmas for elaboration) is
-- in effect.
elsif Debug_Flag_Underscore_P
and then Is_Assertion_Pragma_Target (Target_Id)
then
return;
-- Source calls to source targets are always considered because they
-- reflect the original call graph.
elsif Target_Attrs.From_Source and then Call_Attrs.From_Source then
null;
-- A call to a source function which acts as the default expression in
-- another call requires special detection.
elsif Target_Attrs.From_Source
and then Nkind (N) = N_Function_Call
and then Is_Default_Expression (N)
then
null;
-- The target emulates Ada semantics
elsif Is_Ada_Semantic_Target (Target_Id) then
null;
-- The target acts as a link between scenarios
elsif Is_Bridge_Target (Target_Id) then
null;
-- The target emulates SPARK semantics
elsif Is_SPARK_Semantic_Target (Target_Id) then
null;
-- Otherwise the call is not suitable for ABE processing. This prevents
-- the generation of call markers which will never play a role in ABE
-- diagnostics.
else
return;
end if;
-- At this point it is known that the call will play some role in ABE
-- checks and diagnostics. Create a corresponding call marker in case
-- the original call is heavily transformed by expansion later on.
Marker := Make_Call_Marker (Sloc (N));
-- Inherit the attributes of the original call
Set_Target (Marker, Target_Id);
Set_Is_Declaration_Level_Node (Marker, Call_Attrs.In_Declarations);
Set_Is_Dispatching_Call (Marker, Call_Attrs.Is_Dispatching);
Set_Is_Elaboration_Checks_OK_Node
(Marker, Call_Attrs.Elab_Checks_OK);
Set_Is_Elaboration_Warnings_OK_Node
(Marker, Call_Attrs.Elab_Warnings_OK);
Set_Is_Ignored_Ghost_Node (Marker, Call_Attrs.Ghost_Mode_Ignore);
Set_Is_Source_Call (Marker, Call_Attrs.From_Source);
Set_Is_SPARK_Mode_On_Node (Marker, Call_Attrs.SPARK_Mode_On);
-- The marker is inserted prior to the original call. This placement has
-- several desirable effects:
-- 1) The marker appears in the same context, in close proximity to
-- the call.
-- <marker>
-- <call>
-- 2) Inserting the marker prior to the call ensures that an ABE check
-- will take effect prior to the call.
-- <ABE check>
-- <marker>
-- <call>
-- 3) The above two properties are preserved even when the call is a
-- function which is subsequently relocated in order to capture its
-- result. Note that if the call is relocated to a new context, the
-- relocated call will receive a marker of its own.
-- <ABE check>
-- <maker>
-- Temp : ... := Func_Call ...;
-- ... Temp ...
-- The insertion must take place even when the call does not occur in
-- the main unit to keep the tree symmetric. This ensures that internal
-- name serialization is consistent in case the call marker causes the
-- tree to transform in some way.
Insert_Action (N, Marker);
-- The marker becomes the "corresponding" scenario for the call. Save
-- the marker for later processing by the ABE phase.
Record_Elaboration_Scenario (Marker);
end Build_Call_Marker;
-------------------------------------
-- Build_Variable_Reference_Marker --
-------------------------------------
procedure Build_Variable_Reference_Marker
(N : Node_Id;
Read : Boolean;
Write : Boolean)
is
function In_Pragma (Nod : Node_Id) return Boolean;
-- Determine whether arbitrary node Nod appears within a pragma
---------------
-- In_Pragma --
---------------
function In_Pragma (Nod : Node_Id) return Boolean is
Par : Node_Id;
begin
Par := Nod;
while Present (Par) loop
if Nkind (Par) = N_Pragma then
return True;
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
Par := Parent (Par);
end loop;
return False;
end In_Pragma;
-- Local variables
Marker : Node_Id;
Prag : Node_Id;
Var_Attrs : Variable_Attributes;
Var_Id : Entity_Id;
-- Start of processing for Build_Variable_Reference_Marker
begin
-- Nothing to do when switch -gnatH (legacy elaboration checking mode
-- enabled) is in effect because the legacy ABE mechanism does not need
-- to carry out this action.
if Legacy_Elaboration_Checks then
return;
-- Nothing to do for ASIS. As a result, ABE checks and diagnostics are
-- not performed in this mode.
elsif ASIS_Mode then
return;
-- Nothing to do when the reference is being preanalyzed as the marker
-- will be inserted in the wrong place.
elsif Preanalysis_Active then
return;
-- Nothing to do when the input does not denote a reference
elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then
return;
-- Nothing to do for internally-generated references
elsif not Comes_From_Source (N) then
return;
-- Nothing to do when the reference is erroneous, left in a bad state,
-- or does not denote a variable.
elsif not (Present (Entity (N))
and then Ekind (Entity (N)) = E_Variable
and then Entity (N) /= Any_Id)
then
return;
end if;
Extract_Variable_Reference_Attributes
(Ref => N,
Var_Id => Var_Id,
Attrs => Var_Attrs);
Prag := SPARK_Pragma (Var_Id);
if Comes_From_Source (Var_Id)
-- Both the variable and the reference must appear in SPARK_Mode On
-- regions because this scenario falls under the SPARK rules.
and then Present (Prag)
and then Get_SPARK_Mode_From_Annotation (Prag) = On
and then Is_SPARK_Mode_On_Node (N)
-- The reference must not be considered when it appears in a pragma.
-- If the pragma has run-time semantics, then the reference will be
-- reconsidered once the pragma is expanded.
-- Performance note: parent traversal
and then not In_Pragma (N)
then
null;
-- Otherwise the reference is not suitable for ABE processing. This
-- prevents the generation of variable markers which will never play
-- a role in ABE diagnostics.
else
return;
end if;
-- At this point it is known that the variable reference will play some
-- role in ABE checks and diagnostics. Create a corresponding variable
-- marker in case the original variable reference is folded or optimized
-- away.
Marker := Make_Variable_Reference_Marker (Sloc (N));
-- Inherit the attributes of the original variable reference
Set_Target (Marker, Var_Id);
Set_Is_Read (Marker, Read);
Set_Is_Write (Marker, Write);
-- The marker is inserted prior to the original variable reference. The
-- insertion must take place even when the reference does not occur in
-- the main unit to keep the tree symmetric. This ensures that internal
-- name serialization is consistent in case the variable marker causes
-- the tree to transform in some way.
Insert_Action (N, Marker);
-- The marker becomes the "corresponding" scenario for the reference.
-- Save the marker for later processing for the ABE phase.
Record_Elaboration_Scenario (Marker);
end Build_Variable_Reference_Marker;
---------------------------------
-- Check_Elaboration_Scenarios --
---------------------------------
procedure Check_Elaboration_Scenarios is
begin
-- Nothing to do when switch -gnatH (legacy elaboration checking mode
-- enabled) is in effect because the legacy ABE mechanism does not need
-- to carry out this action.
if Legacy_Elaboration_Checks then
return;
-- Nothing to do for ASIS. As a result, no ABE checks and diagnostics
-- are performed in this mode.
elsif ASIS_Mode then
return;
end if;
-- Examine the context of the main unit and record all units with prior
-- elaboration with respect to it.
Find_Elaborated_Units;
-- Examine each top-level scenario saved during the Recording phase 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;
Process_Conditional_ABE (Top_Level_Scenarios.Table (Index));
end loop;
-- Examine each SPARK scenario saved during the Recording phase which
-- is not necessarily executable during elaboration, but still requires
-- elaboration-related checks.
for Index in SPARK_Scenarios.First .. SPARK_Scenarios.Last loop
Check_SPARK_Scenario (SPARK_Scenarios.Table (Index));
end loop;
end Check_Elaboration_Scenarios;
------------------------------
-- Check_Preelaborated_Call --
------------------------------
procedure Check_Preelaborated_Call (Call : Node_Id) is
function In_Preelaborated_Context (N : Node_Id) return Boolean;
-- Determine whether arbitrary node appears in a preelaborated context
------------------------------
-- In_Preelaborated_Context --
------------------------------
function In_Preelaborated_Context (N : Node_Id) return Boolean is
Body_Id : constant Entity_Id := Find_Code_Unit (N);
Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
begin
-- The node appears within a package body whose corresponding spec is
-- subject to pragma Remote_Call_Interface or Remote_Types. This does
-- not result in a preelaborated context because the package body may
-- be on another machine.
if Ekind (Body_Id) = E_Package_Body
and then Ekind_In (Spec_Id, E_Generic_Package, E_Package)
and then (Is_Remote_Call_Interface (Spec_Id)
or else Is_Remote_Types (Spec_Id))
then
return False;
-- Otherwise the node appears within a preelaborated context when the
-- associated unit is preelaborated.
else
return Is_Preelaborated_Unit (Spec_Id);
end if;
end In_Preelaborated_Context;
-- Local variables
Call_Attrs : Call_Attributes;
Level : Enclosing_Level_Kind;
Target_Id : Entity_Id;
-- Start of processing for Check_Preelaborated_Call
begin
Extract_Call_Attributes
(Call => Call,
Target_Id => Target_Id,
Attrs => Call_Attrs);
-- Nothing to do when the call is internally generated because it is
-- assumed that it will never violate preelaboration.
if not Call_Attrs.From_Source then
return;
end if;
-- Performance note: parent traversal
Level := Find_Enclosing_Level (Call);
-- Library-level calls are always considered because they are part of
-- the associated unit's elaboration actions.
if Level in Library_Level then
null;
-- Calls at the library level of a generic package body must be checked
-- because they would render an instantiation illegal if the template is
-- marked as preelaborated. Note that this does not apply to calls at
-- the library level of a generic package spec.
elsif Level = Generic_Package_Body then
null;
-- Otherwise the call does not appear at the proper level and must not
-- be considered for this check.
else
return;
end if;
-- The call appears within a preelaborated unit. Emit a warning only for
-- internal uses, otherwise this is an error.
if In_Preelaborated_Context (Call) then
Error_Msg_Warn := GNAT_Mode;
Error_Msg_N
("<<non-static call not allowed in preelaborated unit", Call);
end if;
end Check_Preelaborated_Call;
------------------------------
-- Check_SPARK_Derived_Type --
------------------------------
procedure Check_SPARK_Derived_Type (Typ_Decl : Node_Id) is
Typ : constant Entity_Id := Defining_Entity (Typ_Decl);
-- NOTE: The routines within Check_SPARK_Derived_Type are intentionally
-- unnested to avoid deep indentation of code.
Stop_Check : exception;
-- This exception is raised when the freeze node violates the placement
-- rules.
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.
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.
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.
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.
--------------------------------
-- Check_Overriding_Primitive --
--------------------------------
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;
begin
Body_Id := Corresponding_Body (Prim_Decl);
-- 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.
if No (Body_Id) then
return;
-- The primitive overrides a parent or progenitor primitive
elsif Present (Overridden_Operation (Prim)) then
-- 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.
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.
else
return;
end if;
Body_Decl := Unit_Declaration_Node (Body_Id);
Region := Find_Early_Call_Region (Body_Decl);
-- The freeze node appears prior to the early call region of the
-- primitive body.
-- 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.
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);
Error_Msg_Sloc := Sloc (Region);
Error_Msg_N ("\region starts #", Typ_Decl);
Error_Msg_Sloc := Sloc (Body_Decl);
Error_Msg_N ("\region ends #", Typ_Decl);
Error_Msg_Sloc := Freeze_Node_Location (FNode);
Error_Msg_N ("\first freezing point #", Typ_Decl);
-- If applicable, suggest the use of pragma Elaborate_Body in the
-- associated package spec.
Suggest_Elaborate_Body
(N => FNode,
Body_Decl => Body_Decl,
Error_Nod => Typ_Decl);
raise Stop_Check;
end if;
end Check_Overriding_Primitive;
--------------------------
-- Freeze_Node_Location --
--------------------------
function Freeze_Node_Location (FNode : Node_Id) return Source_Ptr is
Context : constant Node_Id := Parent (FNode);
Loc : constant Source_Ptr := Sloc (FNode);
Prv_Decls : List_Id;
Vis_Decls : List_Id;
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.
if Nkind (Context) = N_Package_Specification then
Prv_Decls := Private_Declarations (Context);
Vis_Decls := Visible_Declarations (Context);
-- The freeze node appears in the private declarations of the
-- package.
if Present (Prv_Decls)
and then List_Containing (FNode) = Prv_Decls
then
null;
-- The freeze node appears in the visible declarations of the
-- package and there are no private declarations.
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;
-- Otherwise the freeze node is not in the "last" declarative list
-- of the package. Use the existing source location of the freeze
-- node.
else
return Loc;
end if;
-- 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.
if not Precedes_Source_Construct (FNode) then
return Sloc (End_Label (Context));
end if;
end if;
return Loc;
end Freeze_Node_Location;
-------------------------------
-- Precedes_Source_Construct --
-------------------------------
function Precedes_Source_Construct (N : Node_Id) return Boolean is
Decl : Node_Id;
begin
Decl := Next (N);
while Present (Decl) loop
if Comes_From_Source (Decl) then
return True;
-- A generated body for a source expression function is treated as
-- a source construct.
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;
Next (Decl);
end loop;
return False;
end Precedes_Source_Construct;
----------------------------
-- Suggest_Elaborate_Body --
----------------------------
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;
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 up to
-- 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;
-- Local variables
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;
exception
when Stop_Check =>
null;
end Check_SPARK_Derived_Type;
-------------------------------
-- Check_SPARK_Instantiation --
-------------------------------
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;
begin
Extract_Instantiation_Attributes
(Exp_Inst => Exp_Inst,
Inst => Inst,
Inst_Id => Inst_Id,
Gen_Id => Gen_Id,
Attrs => Inst_Attrs);
Extract_Target_Attributes (Gen_Id, Gen_Attrs);
-- The instantiation and the generic body are both in the main unit
if Present (Gen_Attrs.Body_Decl)
and then In_Extended_Main_Code_Unit (Gen_Attrs.Body_Decl)
-- If the instantiation appears prior to the generic body, then the
-- instantiation is illegal (SPARK RM 7.7(6)).
-- 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.
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;
---------------------------------
-- Check_SPARK_Model_In_Effect --
---------------------------------
SPARK_Model_Warning_Posted : Boolean := False;
-- This flag prevents the same SPARK model-related warning from being
-- emitted multiple times.
procedure Check_SPARK_Model_In_Effect (N : Node_Id) is
begin
-- Do not emit the warning multiple times as this creates useless noise
if SPARK_Model_Warning_Posted then
null;
-- SPARK rule verification requires the "strict" static model
elsif Static_Elaboration_Checks and not Relaxed_Elaboration_Checks then
null;
-- Any other combination of models does not guarantee the absence of ABE
-- problems for SPARK rule verification purposes. Note that there is no
-- need to check for the legacy ABE mechanism because the legacy code
-- has its own orthogonal processing for SPARK rules.
else
SPARK_Model_Warning_Posted := True;
Error_Msg_N
("??SPARK elaboration checks require static elaboration model", N);
if Dynamic_Elaboration_Checks then
Error_Msg_N ("\dynamic elaboration model is in effect", N);
else
pragma Assert (Relaxed_Elaboration_Checks);
Error_Msg_N ("\relaxed elaboration model is in effect", N);
end if;
end if;
end Check_SPARK_Model_In_Effect;
--------------------------
-- Check_SPARK_Scenario --
--------------------------
procedure Check_SPARK_Scenario (N : Node_Id) is
begin
-- Ensure that a suitable elaboration model is in effect for SPARK rule
-- verification.
Check_SPARK_Model_In_Effect (N);
-- Add the current scenario to the stack of active scenarios
Push_Active_Scenario (N);
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;
-- Remove the current scenario from the stack of active scenarios once
-- all ABE diagnostics and checks have been performed.
Pop_Active_Scenario (N);
end Check_SPARK_Scenario;
--------------------------------------
-- Check_SPARK_Refined_State_Pragma --
--------------------------------------
procedure Check_SPARK_Refined_State_Pragma (N : Node_Id) is
-- NOTE: The routines within Check_SPARK_Refined_State_Pragma are
-- intentionally unnested to avoid deep indentation of code.
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.
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.
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.
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.
-----------------------------
-- Check_SPARK_Constituent --
-----------------------------
procedure Check_SPARK_Constituent (Constit_Id : Entity_Id) is
Prag : Node_Id;
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;
Prag := SPARK_Pragma (Constit_Id);
-- The check applies only when the constituent is subject to pragma
-- SPARK_Mode On.
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.
-- 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.
if Debug_Flag_Dot_V then
Meet_Elaboration_Requirement
(N => N,
Target_Id => Constit_Id,
Req_Nam => Name_Elaborate);
-- Otherwise ensure that the unit with the external constituent is
-- elaborated prior to the main unit.
else
Ensure_Prior_Elaboration
(N => N,
Unit_Id => Find_Top_Unit (Constit_Id),
Prag_Nam => Name_Elaborate,
State => Initial_State);
end if;
end if;
end Check_SPARK_Constituent;
------------------------------
-- Check_SPARK_Constituents --
------------------------------
procedure Check_SPARK_Constituents (Constits : Elist_Id) is
Constit_Elmt : Elmt_Id;
begin
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;
-----------------------------------
-- Check_SPARK_Initialized_State --
-----------------------------------
procedure Check_SPARK_Initialized_State (State : Node_Id) is
Prag : Node_Id;
State_Id : Entity_Id;
begin
-- Nothing to do for "null" initialization items
if Nkind (State) = N_Null then
return;
-- Nothing to do for illegal states
elsif Error_Posted (State) then
return;
end if;
State_Id := Entity_Of (State);
-- Sanitize the state
if No (State_Id) then
return;
elsif Error_Posted (State_Id) then
return;
elsif Ekind (State_Id) /= E_Abstract_State then
return;
end if;
-- The check is performed only when the abstract state is subject to
-- SPARK_Mode On.
Prag := SPARK_Pragma (State_Id);
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;
------------------------------------
-- Check_SPARK_Initialized_States --
------------------------------------
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;
begin
if Present (Prag) then
Inits := Expression (Get_Argument (Prag, Pack_Id));
-- Avoid processing a "null" initialization list. The only other
-- alternative is an aggregate.
if Nkind (Inits) = N_Aggregate then
-- The initialization items appear in list form:
--
-- (state1, state2)
if Present (Expressions (Inits)) then
Init := First (Expressions (Inits));
while Present (Init) loop
Check_SPARK_Initialized_State (Init);
Next (Init);
end loop;
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;
-- Local variables
Pack_Body : constant Node_Id := Find_Related_Package_Or_Body (N);
-- Start of processing for Check_SPARK_Refined_State_Pragma
begin
-- Pragma Refined_State must be associated with a package body
pragma Assert
(Present (Pack_Body) and then Nkind (Pack_Body) = N_Package_Body);
-- Verify that each external contitunent of an abstract state mentioned
-- in pragma Initializes is properly elaborated.
Check_SPARK_Initialized_States (Unique_Defining_Entity (Pack_Body));
end Check_SPARK_Refined_State_Pragma;
----------------------
-- Compilation_Unit --
----------------------
function Compilation_Unit (Unit_Id : Entity_Id) return Node_Id is
Comp_Unit : Node_Id;
begin
Comp_Unit := Parent (Unit_Id);
-- Handle the case where a concurrent subunit is rewritten as a null
-- statement due to expansion activities.
if Nkind (Comp_Unit) = N_Null_Statement
and then Nkind_In (Original_Node (Comp_Unit), N_Protected_Body,
N_Task_Body)
then
Comp_Unit := Parent (Comp_Unit);
pragma Assert (Nkind (Comp_Unit) = N_Subunit);
-- Otherwise use the declaration node of the unit
else
Comp_Unit := Parent (Unit_Declaration_Node (Unit_Id));
end if;
-- Handle the case where a subprogram instantiation which acts as a
-- compilation unit is expanded into an anonymous package that wraps
-- the instantiated subprogram.
if Nkind (Comp_Unit) = N_Package_Specification
and then Nkind_In (Original_Node (Parent (Comp_Unit)),
N_Function_Instantiation,
N_Procedure_Instantiation)
then
Comp_Unit := Parent (Parent (Comp_Unit));
-- Handle the case where the compilation unit is a subunit
elsif Nkind (Comp_Unit) = N_Subunit then
Comp_Unit := Parent (Comp_Unit);
end if;
pragma Assert (Nkind (Comp_Unit) = N_Compilation_Unit);
return Comp_Unit;
end Compilation_Unit;
-----------------------
-- Early_Call_Region --
-----------------------
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 Early_Call_Regions_No_Element;
end Early_Call_Region;
-----------------------------
-- Early_Call_Regions_Hash --
-----------------------------
function Early_Call_Regions_Hash
(Key : Entity_Id) return Early_Call_Regions_Index
is
begin
return Early_Call_Regions_Index (Key mod Early_Call_Regions_Max);
end Early_Call_Regions_Hash;
-----------------
-- Elab_Msg_NE --
-----------------
procedure Elab_Msg_NE
(Msg : String;
N : Node_Id;
Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean)
is
function Prefix return String;
-- Obtain the prefix of the message
function Suffix return String;
-- Obtain the suffix of the message
------------
-- Prefix --
------------
function Prefix return String is
begin
if Info_Msg then
return "info: ";
else
return "";
end if;
end Prefix;
------------
-- Suffix --
------------
function Suffix return String is
begin
if In_SPARK then
return " in SPARK";
else
return "";
end if;
end Suffix;
-- Start of processing for Elab_Msg_NE
begin
Error_Msg_NE (Prefix & Msg & Suffix, N, Id);
end Elab_Msg_NE;
------------------------
-- Elaboration_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;
State : Processing_Attributes)
is
begin
pragma Assert (Nam_In (Prag_Nam, Name_Elaborate, Name_Elaborate_All));
-- Nothing to do when the caller has suppressed the generation of
-- implicit Elaborate[_All] pragmas.
if State.Suppress_Implicit_Pragmas then
return;
-- 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.
elsif State.Within_Partial_Finalization 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 State.Within_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);
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;
-- Mark the with clause depending on the pragma required
if Prag_Nam = Name_Elaborate then
Set_Elaborate_Desirable (Clause);
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));
end if;
-- Obtain the original entry or subprogram which the target may rename
-- except when the target is an instantiation. In this case the alias
-- is the internally generated subprogram which appears within the the
-- anonymous package created for the instantiation. Such an alias is not
-- a suitable target.
if not (Is_Subprogram (Target_Id)
and then Is_Generic_Instance (Target_Id))
then
Target_Id := Get_Renamed_Entity (Target_Id);
end if;
-- Set all attributes
Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Node (Call);
Attrs.Elab_Warnings_OK := Is_Elaboration_Warnings_OK_Node (Call);
Attrs.From_Source := From_Source;
Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Node (Call);
Attrs.In_Declarations := In_Declarations;
Attrs.Is_Dispatching := Is_Dispatching;
Attrs.SPARK_Mode_On := Is_SPARK_Mode_On_Node (Call);
end Extract_Call_Attributes;
-----------------------
-- Extract_Call_Name --
-----------------------
function Extract_Call_Name (Call : Node_Id) return Node_Id is
Nam : Node_Id;
begin
Nam := Name (Call);
-- When the call invokes an entry family, the name appears as an indexed
-- component.
if Nkind (Nam) = N_Indexed_Component then
Nam := Prefix (Nam);
end if;
-- When the call employs the object.operation form, the name appears as
-- a selected component.
if Nkind (Nam) = N_Selected_Component then
Nam := Selector_Name (Nam);
end if;
return Nam;
end Extract_Call_Name;
---------------------------------
-- Extract_Instance_Attributes --
---------------------------------
procedure Extract_Instance_Attributes
(Exp_Inst : Node_Id;
Inst_Body : out Node_Id;
Inst_Decl : out Node_Id)
is
Body_Id : Entity_Id;
begin
-- Assume that the attributes are unavailable
Inst_Body := Empty;
Inst_Decl := Empty;
-- Generic package or subprogram spec
if Nkind_In (Exp_Inst, N_Package_Declaration,
N_Subprogram_Declaration)
then
Inst_Decl := Exp_Inst;
Body_Id := Corresponding_Body (Inst_Decl);
if Present (Body_Id) then
Inst_Body := Unit_Declaration_Node (Body_Id);
end if;
-- Generic package or subprogram body
else
pragma Assert
(Nkind_In (Exp_Inst, N_Package_Body, N_Subprogram_Body));
Inst_Body := Exp_Inst;
Inst_Decl := Unit_Declaration_Node (Corresponding_Spec (Inst_Body));
end if;
end Extract_Instance_Attributes;
--------------------------------------
-- Extract_Instantiation_Attributes --
--------------------------------------
procedure Extract_Instantiation_Attributes
(Exp_Inst : Node_Id;
Inst : out Node_Id;
Inst_Id : out Entity_Id;
Gen_Id : out Entity_Id;
Attrs : out Instantiation_Attributes)
is
begin
Inst := Original_Node (Exp_Inst);
Inst_Id := Defining_Entity (Inst);
-- Traverse a possible chain of renamings to obtain the original generic
-- being instantiatied.
Gen_Id := Get_Renamed_Entity (Entity (Name (Inst)));
-- Set all attributes
Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Node (Inst);
Attrs.Elab_Warnings_OK := Is_Elaboration_Warnings_OK_Node (Inst);
Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Node (Inst);
Attrs.In_Declarations := Is_Declaration_Level_Node (Inst);
Attrs.SPARK_Mode_On := Is_SPARK_Mode_On_Node (Inst);
end Extract_Instantiation_Attributes;
-------------------------------
-- Extract_Target_Attributes --
-------------------------------
procedure Extract_Target_Attributes
(Target_Id : Entity_Id;
Attrs : out Target_Attributes)
is
procedure Extract_Package_Or_Subprogram_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id);
-- Obtain the attributes associated with a package or a subprogram.
-- Spec_Id is the package or subprogram. Body_Decl is the declaration
-- of the corresponding package or subprogram body.
procedure Extract_Protected_Entry_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id;
Body_Barf : out Node_Id);
-- Obtain the attributes associated with a protected entry [family].
-- Spec_Id is the entity of the protected body subprogram. Body_Decl
-- is the declaration of Spec_Id's corresponding body. Body_Barf is
-- the declaration of the barrier function body.
procedure Extract_Protected_Subprogram_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id);
-- Obtain the attributes associated with a protected subprogram. Formal
-- Spec_Id is the entity of the protected body subprogram. Body_Decl is
-- the declaration of Spec_Id's corresponding body.
procedure Extract_Task_Entry_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id);
-- Obtain the attributes associated with a task entry [family]. Formal
-- Spec_Id is the entity of the task body procedure. Body_Decl is the
-- declaration of Spec_Id's corresponding body.
----------------------------------------------
-- Extract_Package_Or_Subprogram_Attributes --
----------------------------------------------
procedure Extract_Package_Or_Subprogram_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id)
is
Body_Id : Entity_Id;
Init_Id : Entity_Id;
Spec_Decl : Node_Id;
begin
-- Assume that the body is not available
Body_Decl := Empty;
Spec_Id := Target_Id;
-- For body retrieval purposes, the entity of the initial declaration
-- is that of the spec.
Init_Id := Spec_Id;
-- The only exception to the above is a function which returns a
-- constrained array type in a SPARK-to-C compilation. In this case
-- the function receives a corresponding procedure which has an out
-- parameter. The proper body for ABE checks and diagnostics is that
-- of the procedure.
if Ekind (Init_Id) = E_Function
and then Rewritten_For_C (Init_Id)
then
Init_Id := Corresponding_Procedure (Init_Id);
end if;
-- Extract the attributes of the body
Spec_Decl := Unit_Declaration_Node (Init_Id);
-- The initial declaration is a stand alone subprogram body
if Nkind (Spec_Decl) = N_Subprogram_Body then
Body_Decl := Spec_Decl;
-- Otherwise the package or subprogram has a spec and a completing
-- body.
elsif Nkind_In (Spec_Decl, N_Generic_Package_Declaration,
N_Generic_Subprogram_Declaration,
N_Package_Declaration,
N_Subprogram_Body_Stub,
N_Subprogram_Declaration)
then
Body_Id := Corresponding_Body (Spec_Decl);
if Present (Body_Id) then
Body_Decl := Unit_Declaration_Node (Body_Id);
end if;
end if;
end Extract_Package_Or_Subprogram_Attributes;
----------------------------------------
-- Extract_Protected_Entry_Attributes --
----------------------------------------
procedure Extract_Protected_Entry_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id;
Body_Barf : out Node_Id)
is
Barf_Id : Entity_Id;
Body_Id : Entity_Id;
begin
-- Assume that the bodies are not available
Body_Barf := Empty;
Body_Decl := Empty;
-- When the entry [family] has already been expanded, it carries both
-- the procedure which emulates the behavior of the entry [family] as
-- well as the barrier function.
if Present (Protected_Body_Subprogram (Target_Id)) then
Spec_Id := Protected_Body_Subprogram (Target_Id);
-- Extract the attributes of the barrier function
Barf_Id :=
Corresponding_Body
(Unit_Declaration_Node (Barrier_Function (Target_Id)));
if Present (Barf_Id) then
Body_Barf := Unit_Declaration_Node (Barf_Id);
end if;
-- Otherwise no expansion took place
else
Spec_Id := Target_Id;
end if;
-- Extract the attributes of the entry body
Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id));
if Present (Body_Id) then
Body_Decl := Unit_Declaration_Node (Body_Id);
end if;
end Extract_Protected_Entry_Attributes;
---------------------------------------------
-- Extract_Protected_Subprogram_Attributes --
---------------------------------------------
procedure Extract_Protected_Subprogram_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id)
is
Body_Id : Entity_Id;
begin
-- Assume that the body is not available
Body_Decl := Empty;
-- When the protected subprogram has already been expanded, it
-- carries the subprogram which seizes the lock and invokes the
-- original statements.
if Present (Protected_Subprogram (Target_Id)) then
Spec_Id :=
Protected_Body_Subprogram (Protected_Subprogram (Target_Id));
-- Otherwise no expansion took place
else
Spec_Id := Target_Id;
end if;
-- Extract the attributes of the body
Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id));
if Present (Body_Id) then
Body_Decl := Unit_Declaration_Node (Body_Id);
end if;
end Extract_Protected_Subprogram_Attributes;
-----------------------------------
-- Extract_Task_Entry_Attributes --
-----------------------------------
procedure Extract_Task_Entry_Attributes
(Spec_Id : out Entity_Id;
Body_Decl : out Node_Id)
is
Task_Typ : constant Entity_Id := Non_Private_View (Scope (Target_Id));
Body_Id : Entity_Id;
begin
-- Assume that the body is not available
Body_Decl := Empty;
-- The the task type has already been expanded, it carries the
-- procedure which emulates the behavior of the task body.
if Present (Task_Body_Procedure (Task_Typ)) then
Spec_Id := Task_Body_Procedure (Task_Typ);
-- Otherwise no expansion took place
else
Spec_Id := Task_Typ;
end if;
-- Extract the attributes of the body
Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id));
if Present (Body_Id) then
Body_Decl := Unit_Declaration_Node (Body_Id);
end if;
end Extract_Task_Entry_Attributes;
-- Local variables
Prag : constant Node_Id := SPARK_Pragma (Target_Id);
Body_Barf : Node_Id;
Body_Decl : Node_Id;
Spec_Id : Entity_Id;
-- Start of processing for Extract_Target_Attributes
begin
-- Assume that the body of the barrier function is not available
Body_Barf := Empty;
-- The target is a protected entry [family]
if Is_Protected_Entry (Target_Id) then
Extract_Protected_Entry_Attributes
(Spec_Id => Spec_Id,
Body_Decl => Body_Decl,
Body_Barf => Body_Barf);
-- The target is a protected subprogram
elsif Is_Protected_Subp (Target_Id)
or else Is_Protected_Body_Subp (Target_Id)
then
Extract_Protected_Subprogram_Attributes
(Spec_Id => Spec_Id,
Body_Decl => Body_Decl);
-- The target is a task entry [family]
elsif Is_Task_Entry (Target_Id) then
Extract_Task_Entry_Attributes
(Spec_Id => Spec_Id,
Body_Decl => Body_Decl);
-- Otherwise the target is a package or a subprogram
else
Extract_Package_Or_Subprogram_Attributes
(Spec_Id => Spec_Id,
Body_Decl => Body_Decl);
end if;
-- Set all attributes
Attrs.Body_Barf := Body_Barf;
Attrs.Body_Decl := Body_Decl;
Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Id (Target_Id);
Attrs.From_Source := Comes_From_Source (Target_Id);
Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Entity (Target_Id);
Attrs.SPARK_Mode_On :=
Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = On;
Attrs.Spec_Decl := Unit_Declaration_Node (Spec_Id);
Attrs.Spec_Id := Spec_Id;
Attrs.Unit_Id := Find_Top_Unit (Target_Id);
-- At this point certain attributes should always be available
pragma Assert (Present (Attrs.Spec_Decl));
pragma Assert (Present (Attrs.Spec_Id));
pragma Assert (Present (Attrs.Unit_Id));
end Extract_Target_Attributes;
-----------------------------
-- Extract_Task_Attributes --
-----------------------------
procedure Extract_Task_Attributes
(Typ : Entity_Id;
Attrs : out Task_Attributes)
is
Task_Typ : constant Entity_Id := Non_Private_View (Typ);
Body_Decl : Node_Id;
Body_Id : Entity_Id;
Prag : Node_Id;
Spec_Id : Entity_Id;
begin
-- Assume that the body of the task procedure is not available
Body_Decl := Empty;
-- The initial declaration is that of the task body procedure
Spec_Id := Get_Task_Body_Procedure (Task_Typ);
Body_Id := Corresponding_Body (Unit_Declaration_Node (Spec_Id));
if Present (Body_Id) then
Body_Decl := Unit_Declaration_Node (Body_Id);
end if;
Prag := SPARK_Pragma (Task_Typ);
-- Set all attributes
Attrs.Body_Decl := Body_Decl;
Attrs.Elab_Checks_OK := Is_Elaboration_Checks_OK_Id (Task_Typ);
Attrs.Ghost_Mode_Ignore := Is_Ignored_Ghost_Entity (Task_Typ);
Attrs.SPARK_Mode_On :=
Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = On;
Attrs.Spec_Id := Spec_Id;
Attrs.Task_Decl := Declaration_Node (Task_Typ);
Attrs.Unit_Id := Find_Top_Unit (Task_Typ);
-- At this point certain attributes should always be available
pragma Assert (Present (Attrs.Spec_Id));
pragma Assert (Present (Attrs.Task_Decl));
pragma Assert (Present (Attrs.Unit_Id));
end Extract_Task_Attributes;
-------------------------------------------
-- Extract_Variable_Reference_Attributes --
-------------------------------------------
procedure Extract_Variable_Reference_Attributes
(Ref : Node_Id;
Var_Id : out Entity_Id;
Attrs : out Variable_Attributes)
is
function Get_Renamed_Variable (Id : Entity_Id) return Entity_Id;
-- Obtain the ultimate renamed variable of variable Id
--------------------------
-- Get_Renamed_Variable --
--------------------------
function Get_Renamed_Variable (Id : Entity_Id) return Entity_Id is
Ren_Id : Entity_Id;
begin
Ren_Id := Id;
while Present (Renamed_Entity (Ren_Id))
and then Nkind (Renamed_Entity (Ren_Id)) in N_Entity
loop
Ren_Id := Renamed_Entity (Ren_Id);
end loop;
return Ren_Id;
end Get_Renamed_Variable;
-- Start of processing for Extract_Variable_Reference_Attributes
begin
-- Extraction for variable reference markers
if Nkind (Ref) = N_Variable_Reference_Marker then
Var_Id := Target (Ref);
-- Extraction for expanded names and identifiers
else
Var_Id := Entity (Ref);
end if;
-- Obtain the original variable which the reference mentions
Var_Id := Get_Renamed_Variable (Var_Id);
Attrs.Unit_Id := Find_Top_Unit (Var_Id);
-- At this point certain attributes should always be available
pragma Assert (Present (Attrs.Unit_Id));
end Extract_Variable_Reference_Attributes;
--------------------
-- Find_Code_Unit --
--------------------
function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id is
begin
return Find_Unit_Entity (Unit (Cunit (Get_Code_Unit (N))));
end Find_Code_Unit;
----------------------------
-- Find_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
--