Google Git
Sign in
gnu / gcc / a8404c07e7fca388c02c39077865f7d5fa928430 / . / gcc / ada / sem_elab.adb
blob: a1e8f1ef30b1b8a289515524f1d33140665b5495 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ E L A B --
-- --
-- B o d y --
-- --
-- Copyright (C) 1997-2022, 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 ALI; use ALI;
with Atree; use Atree;
with Checks; use Checks;
with Debug; use Debug;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
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_Disp; use Sem_Disp;
with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
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 Warnsw; use Warnsw;
with GNAT; use GNAT;
with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables;
with GNAT.Lists; use GNAT.Lists;
with GNAT.Sets; use GNAT.Sets;
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 behavior.
--
-- 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 local and external targets at run time.
--
-- * Supply implicit elaboration dependencies for a unit to binde
--
-- The ABE mechanism creates implicit dependencies in the form of with
-- clauses subject to pragma Elaborate[_All] when the elaboration graph
-- reaches into an external unit. The implicit dependencies are encoded
-- in the ALI file of the main unit. GNATbind and binde then use these
-- dependencies to augment the library item graph and determine the
-- elaboration order of all units in the compilation.
--
-- * Supply pieces of the invocation graph for a unit to bindo
--
-- The ABE mechanism captures paths starting from elaboration code or
-- top level constructs that reach into an external unit. The paths are
-- encoded in the ALI file of the main unit in the form of declarations
-- which represent nodes, and relations which represent edges. GNATbind
-- and bindo then build the full invocation graph in order to augment
-- the library item graph and determine the elaboration order of 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 diagnoses and
-- installs run-time checks to detect ABE issues in the main unit.
-- The behavior 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 dependencies between units in the
-- form of with clauses subject to pragma Elaborate[_All] to ensure
-- the prior elaboration of withed units. This is the default model.
--
-- * SPARK model - This is the most conservative of the three models and
-- implements 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 invoke a scenario which has not been elaborated
-- yet.
--
-- * 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
-- 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
-- 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.
--
-- * Invocation - The act of activating a task, calling a subprogram, or
-- instantiating a generic.
--
-- * Invocation construct - An entry declaration, [single] protected type,
-- subprogram declaration, subprogram instantiation, or a [single] task
-- type declared in the visible, private, or body declarations of the
-- main unit.
--
-- * Invocation relation - A flow link between two invocation constructs
--
-- * Invocation signature - A set of attributes that uniquely identify an
-- invocation construct within the namespace of all ALI files.
--
-- * 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
-- enclosing 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 is invoked by elaboration code
-- or invocation construct. 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 invoked 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
------------------
-- 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 |
-- | | |
-- +- | ----------------------------------------------------------------+
-- |
-- |
-- +--> Internal_Representation
-- |
-- +--> Scenario_Storage
-- |
-- End of Compilation
-- |
-- +- | --------------------- Processing phase -------------------------+
-- | v |
-- | Check_Elaboration_Scenarios |
-- | | |
-- | +--> Check_Conditional_ABE_Scenarios |
-- | | | |
-- | | +--> Process_Conditional_ABE <----------------------+ |
-- | | | | |
-- | | +--> Process_Conditional_ABE_Activation | |
-- | | | | | |
-- | | | +-----------------------------+ | |
-- | | | | | |
-- | | +--> Process_Conditional_ABE_Call +---> Traverse_Body |
-- | | | | | |
-- | | | +-----------------------------+ |
-- | | | |
-- | | +--> Process_Conditional_ABE_Access_Taken |
-- | | +--> Process_Conditional_ABE_Instantiation |
-- | | +--> Process_Conditional_ABE_Variable_Assignment |
-- | | +--> Process_Conditional_ABE_Variable_Reference |
-- | | |
-- | +--> Check_SPARK_Scenario |
-- | | | |
-- | | +--> Process_SPARK_Scenario |
-- | | | |
-- | | +--> Process_SPARK_Derived_Type |
-- | | +--> Process_SPARK_Instantiation |
-- | | +--> Process_SPARK_Refined_State_Pragma |
-- | | |
-- | +--> Record_Invocation_Graph |
-- | | |
-- | +--> Process_Invocation_Body_Scenarios |
-- | +--> Process_Invocation_Spec_Scenarios |
-- | +--> Process_Main_Unit |
-- | | |
-- | +--> Process_Invocation_Scenario <-------------+ |
-- | | | |
-- | +--> Process_Invocation_Activation | |
-- | | | | |
-- | | +------------------------+ | |
-- | | | | |
-- | +--> Process_Invocation_Call +---> Traverse_Body |
-- | | | |
-- | +------------------------+ |
-- | |
-- +--------------------------------------------------------------------+
---------------------
-- Recording phase --
---------------------
-- The Recording phase coincides with the analysis/resolution phase of the
-- compiler. It has the following objectives:
--
-- * Record all suitable 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 invoked
-- 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 scenarios saved during the Recording phase, and perform
-- the following actions:
--
-- - Dynamic model
--
-- Diagnose conditional ABEs, and install run-time conditional ABE
-- checks for all scenarios.
--
-- - SPARK model
--
-- Enforce the SPARK elaboration rules
--
-- - Static model
--
-- Diagnose conditional ABEs, install run-time conditional ABE
-- checks only for scenarios are reachable from elaboration code,
-- and guarantee the elaboration of external units by creating
-- implicit with clauses subject to pragma Elaborate[_All].
--
-- * Examine library-level scenarios and invocation constructs, and
-- perform the following actions:
--
-- - Determine whether the flow of execution reaches into an external
-- unit. If this is the case, encode the path in the ALI file of
-- the main unit.
--
-- - Create declarations for invocation constructs in the ALI file of
-- the main unit.
----------------------
-- 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 spatial relation of nodes.
-----------------------------------------
-- Suppression of elaboration warnings --
-----------------------------------------
-- Elaboration warnings along multiple traversal paths rooted at a scenario
-- are suppressed when the scenario has elaboration warnings suppressed.
--
-- Root scenario
-- |
-- +-- Child scenario 1
-- | |
-- | +-- Grandchild scenario 1
-- | |
-- | +-- Grandchild scenario N
-- |
-- +-- Child scenario N
--
-- If the root scenario has elaboration warnings suppressed, then all its
-- child, grandchild, etc. scenarios will have their elaboration warnings
-- suppressed.
--
-- In addition to switch -gnatwL, pragma Warnings may be used to suppress
-- elaboration-related warnings when used in the following manner:
--
-- pragma Warnings ("L");
-- <scenario-or-target>
--
-- <target>
-- pragma Warnings (Off, target);
--
-- pragma Warnings (Off);
-- <scenario-or-target>
--
-- * To suppress elaboration warnings for '[Unrestricted_]Access of
-- entries, operators, and subprograms, either:
--
-- - Suppress the entry, operator, or subprogram, or
-- - Suppress the attribute, or
-- - Use switch -gnatw.f
--
-- * To suppress elaboration warnings for calls to entries, operators,
-- and subprograms, either:
--
-- - Suppress the entry, operator, or subprogram, or
-- - Suppress the call
--
-- * To suppress elaboration warnings for instantiations, suppress the
-- instantiation.
--
-- * To suppress elaboration warnings for task activations, either:
--
-- - Suppress the task object, or
-- - Suppress the task type, or
-- - Suppress the activation call
--------------
-- 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_F encode full invocation paths in ALI files
--
-- The ABE mechanism encodes the full path from an elaboration
-- procedure or invocable construct to an external target. The
-- path contains all intermediate activations, instantiations,
-- and calls.
--
-- -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_s stop elaboration checks on synchronous suspension
--
-- The ABE mechanism stops the traversal of a task body when it
-- encounters a call to one of the following routines:
--
-- Ada.Synchronous_Barriers.Wait_For_Release
-- Ada.Synchronous_Task_Control.Suspend_Until_True
--
-- -gnatd_T output trace information on invocation relation construction
--
-- The ABE mechanism outputs text information concerning relation
-- construction to standard output.
--
-- -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 de facto ABE model. This amounts 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_s
-- -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.
--------------------------
-- 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
-----------
-- Kinds --
-----------
-- The following type enumerates all possible elaboration phase statutes
type Elaboration_Phase_Status is
(Inactive,
-- The elaboration phase of the compiler has not started yet
Active,
-- The elaboration phase of the compiler is currently in progress
Completed);
-- The elaboration phase of the compiler has finished
Elaboration_Phase : Elaboration_Phase_Status := Inactive;
-- The status of the elaboration phase. Use routine Set_Elaboration_Phase
-- to alter its value.
-- The following type enumerates all subprogram body traversal modes
type Body_Traversal_Kind is
(Deep_Traversal,
-- The traversal examines the internals of a subprogram
No_Traversal);
-- The following type enumerates all operation modes
type Processing_Kind is
(Conditional_ABE_Processing,
-- The ABE mechanism detects and diagnoses conditional ABEs for library
-- and declaration-level scenarios.
Dynamic_Model_Processing,
-- The ABE mechanism installs conditional ABE checks for all eligible
-- scenarios when the dynamic model is in effect.
Guaranteed_ABE_Processing,
-- The ABE mechanism detects and diagnoses guaranteed ABEs caused by
-- calls, instantiations, and task activations.
Invocation_Construct_Processing,
-- The ABE mechanism locates all invocation constructs within the main
-- unit and utilizes them as roots of miltiple DFS traversals aimed at
-- detecting transitions from the main unit to an external unit.
Invocation_Body_Processing,
-- The ABE mechanism utilizes all library-level body scenarios as roots
-- of miltiple DFS traversals aimed at detecting transitions from the
-- main unit to an external unit.
Invocation_Spec_Processing,
-- The ABE mechanism utilizes all library-level spec scenarios as roots
-- of miltiple DFS traversals aimed at detecting transitions from the
-- main unit to an external unit.
SPARK_Processing,
-- The ABE mechanism detects and diagnoses violations of the SPARK
-- elaboration rules for SPARK-specific scenarios.
No_Processing);
-- The following type enumerates all possible scenario kinds
type Scenario_Kind is
(Access_Taken_Scenario,
-- An attribute reference which takes 'Access or 'Unrestricted_Access of
-- an entry, operator, or subprogram.
Call_Scenario,
-- A call which invokes an entry, operator, or subprogram
Derived_Type_Scenario,
-- A declaration of a derived type. This is a SPARK-specific scenario.
Instantiation_Scenario,
-- An instantiation which instantiates a generic package or subprogram.
-- This scenario is also subject to SPARK-specific rules.
Refined_State_Pragma_Scenario,
-- A Refined_State pragma. This is a SPARK-specific scenario.
Task_Activation_Scenario,
-- A call which activates objects of various task types
Variable_Assignment_Scenario,
-- An assignment statement which modifies the value of some variable
Variable_Reference_Scenario,
-- A reference to a variable. This is a SPARK-specific scenario.
No_Scenario);
-- The following type enumerates all possible consistency models of target
-- and scenario representations.
type Representation_Kind is
(Inconsistent_Representation,
-- A representation is said to be "inconsistent" when it is created from
-- a partially analyzed tree. In such an environment, certain attributes
-- such as a completing body may not be available yet.
Consistent_Representation,
-- A representation is said to be "consistent" when it is created from a
-- fully analyzed tree, where all attributes are available.
No_Representation);
-- The following type enumerates all possible target kinds
type Target_Kind is
(Generic_Target,
-- A generic unit being instantiated
Package_Target,
-- The package form of an instantiation
Subprogram_Target,
-- An entry, operator, or subprogram being invoked, or aliased through
-- 'Access or 'Unrestricted_Access.
Task_Target,
-- A task being activated by an activation call
Variable_Target,
-- A variable being updated through an assignment statement, or read
-- through a variable reference.
No_Target);
-----------
-- Types --
-----------
procedure Destroy (NE : in out Node_Or_Entity_Id);
pragma Inline (Destroy);
-- Destroy node or entity NE
function Hash (NE : Node_Or_Entity_Id) return Bucket_Range_Type;
pragma Inline (Hash);
-- Obtain the hash value of key NE
-- The following is a general purpose list for nodes and entities
package NE_List is new Doubly_Linked_Lists
(Element_Type => Node_Or_Entity_Id,
"=" => "=",
Destroy_Element => Destroy);
-- The following is a general purpose map which relates nodes and entities
-- to lists of nodes and entities.
package NE_List_Map is new Dynamic_Hash_Tables
(Key_Type => Node_Or_Entity_Id,
Value_Type => NE_List.Doubly_Linked_List,
No_Value => NE_List.Nil,
Expansion_Threshold => 1.5,
Expansion_Factor => 2,
Compression_Threshold => 0.3,
Compression_Factor => 2,
"=" => "=",
Destroy_Value => NE_List.Destroy,
Hash => Hash);
-- The following is a general purpose membership set for nodes and entities
package NE_Set is new Membership_Sets
(Element_Type => Node_Or_Entity_Id,
"=" => "=",
Hash => Hash);
-- The following type captures relevant attributes which pertain to the
-- in state of the Processing phase.
type Processing_In_State is record
Processing : Processing_Kind := No_Processing;
-- Operation mode of the Processing phase. Once set, this value should
-- not be changed.
Representation : Representation_Kind := No_Representation;
-- Required level of scenario and target representation. Once set, this
-- value should not be changed.
Suppress_Checks : Boolean := False;
-- This flag is set when the Processing phase must not generate any ABE
-- checks.
Suppress_Implicit_Pragmas : Boolean := False;
-- This flag is set when the Processing phase must not generate any
-- implicit Elaborate[_All] pragmas.
Suppress_Info_Messages : Boolean := False;
-- This flag is set when the Processing phase must not emit any info
-- messages.
Suppress_Up_Level_Targets : Boolean := False;
-- This flag is set when the Processing phase must ignore up-level
-- targets.
Suppress_Warnings : Boolean := False;
-- This flag is set when the Processing phase must not emit any warnings
-- on elaboration problems.
Traversal : Body_Traversal_Kind := No_Traversal;
-- The subprogram body traversal mode. Once set, this value should not
-- be changed.
Within_Generic : Boolean := False;
-- This flag is set when the Processing phase is currently within a
-- generic unit.
Within_Initial_Condition : Boolean := False;
-- This flag is set when the Processing phase is currently examining a
-- scenario which was reached from an initial condition procedure.
Within_Partial_Finalization : Boolean := False;
-- 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 := False;
-- This flag is set when the Processing phase is currently examining a
-- scenario which was reached from a task body.
end record;
-- The following constants define the various operational states of the
-- Processing phase.
-- The conditional ABE state is used when processing scenarios that appear
-- at the declaration, instantiation, and library levels to detect errors
-- and install conditional ABE checks.
Conditional_ABE_State : constant Processing_In_State :=
(Processing => Conditional_ABE_Processing,
Representation => Consistent_Representation,
Traversal => Deep_Traversal,
others => False);
-- The dynamic model state is used to install conditional ABE checks when
-- switch -gnatE (dynamic elaboration checking mode enabled) is in effect.
Dynamic_Model_State : constant Processing_In_State :=
(Processing => Dynamic_Model_Processing,
Representation => Consistent_Representation,
Suppress_Implicit_Pragmas => True,
Suppress_Info_Messages => True,
Suppress_Up_Level_Targets => True,
Suppress_Warnings => True,
Traversal => No_Traversal,
others => False);
-- The guaranteed ABE state is used when processing scenarios that appear
-- at the declaration, instantiation, and library levels to detect errors
-- and install guarateed ABE failures.
Guaranteed_ABE_State : constant Processing_In_State :=
(Processing => Guaranteed_ABE_Processing,
Representation => Inconsistent_Representation,
Suppress_Implicit_Pragmas => True,
Traversal => No_Traversal,
others => False);
-- The invocation body state is used when processing scenarios that appear
-- at the body library level to encode paths that start from elaboration
-- code and ultimately reach into external units.
Invocation_Body_State : constant Processing_In_State :=
(Processing => Invocation_Body_Processing,
Representation => Consistent_Representation,
Suppress_Checks => True,
Suppress_Implicit_Pragmas => True,
Suppress_Info_Messages => True,
Suppress_Up_Level_Targets => True,
Suppress_Warnings => True,
Traversal => Deep_Traversal,
others => False);
-- The invocation construct state is used when processing constructs that
-- appear within the spec and body of the main unit and eventually reach
-- into external units.
Invocation_Construct_State : constant Processing_In_State :=
(Processing => Invocation_Construct_Processing,
Representation => Consistent_Representation,
Suppress_Checks => True,
Suppress_Implicit_Pragmas => True,
Suppress_Info_Messages => True,
Suppress_Up_Level_Targets => True,
Suppress_Warnings => True,
Traversal => Deep_Traversal,
others => False);
-- The invocation spec state is used when processing scenarios that appear
-- at the spec library level to encode paths that start from elaboration
-- code and ultimately reach into external units.
Invocation_Spec_State : constant Processing_In_State :=
(Processing => Invocation_Spec_Processing,
Representation => Consistent_Representation,
Suppress_Checks => True,
Suppress_Implicit_Pragmas => True,
Suppress_Info_Messages => True,
Suppress_Up_Level_Targets => True,
Suppress_Warnings => True,
Traversal => Deep_Traversal,
others => False);
-- The SPARK state is used when verying SPARK-specific semantics of certain
-- scenarios.
SPARK_State : constant Processing_In_State :=
(Processing => SPARK_Processing,
Representation => Consistent_Representation,
Traversal => No_Traversal,
others => False);
-- The following type identifies a scenario representation
type Scenario_Rep_Id is new Natural;
No_Scenario_Rep : constant Scenario_Rep_Id := Scenario_Rep_Id'First;
First_Scenario_Rep : constant Scenario_Rep_Id := No_Scenario_Rep + 1;
-- The following type identifies a target representation
type Target_Rep_Id is new Natural;
No_Target_Rep : constant Target_Rep_Id := Target_Rep_Id'First;
First_Target_Rep : constant Target_Rep_Id := No_Target_Rep + 1;
--------------
-- Services --
--------------
-- The following package keeps track of all active scenarios during a DFS
-- traversal.
package Active_Scenarios is
-----------
-- Types --
-----------
-- The following type defines the position within the active scenario
-- stack.
type Active_Scenario_Pos is new Natural;
---------------------
-- Data structures --
---------------------
-- The following table stores all active scenarios in a DFS traversal.
-- This table must be maintained in a FIFO fashion.
package Active_Scenario_Stack is new Table.Table
(Table_Index_Type => Active_Scenario_Pos,
Table_Component_Type => Node_Id,
Table_Low_Bound => 1,
Table_Initial => 50,
Table_Increment => 200,
Table_Name => "Active_Scenario_Stack");
---------
-- API --
---------
procedure Output_Active_Scenarios
(Error_Nod : Node_Id;
In_State : Processing_In_State);
pragma Inline (Output_Active_Scenarios);
-- Output the contents of the active scenario stack from earliest to
-- latest to supplement an earlier error emitted for node Error_Nod.
-- In_State denotes the current state of the Processing phase.
procedure Pop_Active_Scenario (N : Node_Id);
pragma Inline (Pop_Active_Scenario);
-- Pop the top of the scenario stack. A check is made to ensure that the
-- scenario being removed is the same as N.
procedure Push_Active_Scenario (N : Node_Id);
pragma Inline (Push_Active_Scenario);
-- Push scenario N on top of the scenario stack
function Root_Scenario return Node_Id;
pragma Inline (Root_Scenario);
-- Return the scenario which started a DFS traversal
end Active_Scenarios;
use Active_Scenarios;
-- The following package provides the main entry point for task activation
-- processing.
package Activation_Processor is
-----------
-- Types --
-----------
type Activation_Processor_Ptr is access procedure
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Obj_Id : Entity_Id;
Obj_Rep : Target_Rep_Id;
Task_Typ : Entity_Id;
Task_Rep : Target_Rep_Id;
In_State : Processing_In_State);
-- Reference to a procedure that takes all attributes of an activation
-- and performs a desired action. Call is the activation call. Call_Rep
-- is the representation of the call. Obj_Id is the task object being
-- activated. Obj_Rep is the representation of the object. Task_Typ is
-- the task type whose body is being activated. Task_Rep denotes the
-- representation of the task type. In_State is the current state of
-- the Processing phase.
---------
-- API --
---------
procedure Process_Activation
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Processor : Activation_Processor_Ptr;
In_State : Processing_In_State);
-- Find all task objects activated by activation call Call and invoke
-- Processor on them. Call_Rep denotes the representation of the call.
-- In_State is the current state of the Processing phase.
end Activation_Processor;
use Activation_Processor;
-- The following package profides functionality for traversing subprogram
-- bodies in DFS manner and processing of eligible scenarios within.
package Body_Processor is
-----------
-- Types --
-----------
type Scenario_Predicate_Ptr is access function
(N : Node_Id) return Boolean;
-- Reference to a function which determines whether arbitrary node N
-- denotes a suitable scenario for processing.
type Scenario_Processor_Ptr is access procedure
(N : Node_Id; In_State : Processing_In_State);
-- Reference to a procedure which processes scenario N. In_State is the
-- current state of the Processing phase.
---------
-- API --
---------
procedure Traverse_Body
(N : Node_Id;
Requires_Processing : Scenario_Predicate_Ptr;
Processor : Scenario_Processor_Ptr;
In_State : Processing_In_State);
pragma Inline (Traverse_Body);
-- Traverse the declarations and handled statements of subprogram body
-- N, looking for scenarios that satisfy predicate Requires_Processing.
-- Routine Processor is invoked for each such scenario.
procedure Reset_Traversed_Bodies;
pragma Inline (Reset_Traversed_Bodies);
-- Reset the visited status of all subprogram bodies that have already
-- been processed by routine Traverse_Body.
-----------------
-- Maintenance --
-----------------
procedure Finalize_Body_Processor;
pragma Inline (Finalize_Body_Processor);
-- Finalize all internal data structures
procedure Initialize_Body_Processor;
pragma Inline (Initialize_Body_Processor);
-- Initialize all internal data structures
end Body_Processor;
use Body_Processor;
-- The following package provides functionality for installing ABE-related
-- checks and failures.
package Check_Installer is
---------
-- API --
---------
function Check_Or_Failure_Generation_OK return Boolean;
pragma Inline (Check_Or_Failure_Generation_OK);
-- Determine whether a conditional ABE check or guaranteed ABE failure
-- can be generated.
procedure Install_Dynamic_ABE_Checks;
pragma Inline (Install_Dynamic_ABE_Checks);
-- Install conditional ABE checks for all saved scenarios when the
-- dynamic model is in effect.
procedure Install_Scenario_ABE_Check
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id;
Disable : Scenario_Rep_Id);
pragma Inline (Install_Scenario_ABE_Check);
-- Install a conditional ABE check for scenario N to ensure that target
-- Targ_Id is properly elaborated. Targ_Rep is the representation of the
-- target. If the check is installed, disable the elaboration checks of
-- scenario Disable.
procedure Install_Scenario_ABE_Check
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id;
Disable : Target_Rep_Id);
pragma Inline (Install_Scenario_ABE_Check);
-- Install a conditional ABE check for scenario N to ensure that target
-- Targ_Id is properly elaborated. Targ_Rep is the representation of the
-- target. If the check is installed, disable the elaboration checks of
-- target Disable.
procedure Install_Scenario_ABE_Failure
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id;
Disable : Scenario_Rep_Id);
pragma Inline (Install_Scenario_ABE_Failure);
-- Install a guaranteed ABE failure for scenario N with target Targ_Id.
-- Targ_Rep denotes the representation of the target. If the failure is
-- installed, disable the elaboration checks of scenario Disable.
procedure Install_Scenario_ABE_Failure
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id;
Disable : Target_Rep_Id);
pragma Inline (Install_Scenario_ABE_Failure);
-- Install a guaranteed ABE failure for scenario N with target Targ_Id.
-- Targ_Rep denotes the representation of the target. If the failure is
-- installed, disable the elaboration checks of target Disable.
procedure Install_Unit_ABE_Check
(N : Node_Id;
Unit_Id : Entity_Id;
Disable : Scenario_Rep_Id);
pragma Inline (Install_Unit_ABE_Check);
-- Install a conditional ABE check for scenario N to ensure that unit
-- Unit_Id is properly elaborated. If the check is installed, disable
-- the elaboration checks of scenario Disable.
procedure Install_Unit_ABE_Check
(N : Node_Id;
Unit_Id : Entity_Id;
Disable : Target_Rep_Id);
pragma Inline (Install_Unit_ABE_Check);
-- Install a conditional ABE check for scenario N to ensure that unit
-- Unit_Id is properly elaborated. If the check is installed, disable
-- the elaboration checks of target Disable.
end Check_Installer;
use Check_Installer;
-- The following package provides the main entry point for conditional ABE
-- checks and diagnostics.
package Conditional_ABE_Processor is
---------
-- API --
---------
procedure Check_Conditional_ABE_Scenarios
(Iter : in out NE_Set.Iterator);
pragma Inline (Check_Conditional_ABE_Scenarios);
-- Perform conditional ABE checks and diagnostics for all scenarios
-- available through iterator Iter.
procedure Process_Conditional_ABE
(N : Node_Id;
In_State : Processing_In_State);
pragma Inline (Process_Conditional_ABE);
-- Perform conditional ABE checks and diagnostics for scenario N.
-- In_State denotes the current state of the Processing phase.
end Conditional_ABE_Processor;
use Conditional_ABE_Processor;
-- The following package provides functionality to emit errors, information
-- messages, and warnings.
package Diagnostics is
---------
-- API --
---------
procedure Elab_Msg_NE
(Msg : String;
N : Node_Id;
Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
pragma Inline (Elab_Msg_NE);
-- Wrapper around Error_Msg_NE. Emit message Msg concerning arbitrary
-- node N and entity. If flag Info_Msg is set, the routine emits an
-- information message, otherwise it emits an error. If flag In_SPARK
-- is set, then string " in SPARK" is added to the end of the message.
procedure Info_Call
(Call : Node_Id;
Subp_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
pragma Inline (Info_Call);
-- Output information concerning call Call that invokes subprogram
-- Subp_Id. When flag Info_Msg is set, the routine emits an information
-- message, otherwise it emits an error. When flag In_SPARK is set, " 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);
pragma Inline (Info_Variable_Reference);
-- Output information concerning reference Ref which mentions variable
-- Var_Id. The routine emits an error suffixed with " in SPARK".
end Diagnostics;
use Diagnostics;
-- The following package provides functionality to locate the early call
-- region of a subprogram body.
package Early_Call_Region_Processor is
---------
-- API --
---------
function Find_Early_Call_Region
(Body_Decl : Node_Id;
Assume_Elab_Body : Boolean := False;
Skip_Memoization : Boolean := False) return Node_Id;
pragma Inline (Find_Early_Call_Region);
-- Find the start of the early call region that belongs to subprogram
-- body Body_Decl as defined in SPARK RM 7.7. This routine finds the
-- early call region, memoizes it, and returns 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.
-----------------
-- Maintenance --
-----------------
procedure Finalize_Early_Call_Region_Processor;
pragma Inline (Finalize_Early_Call_Region_Processor);
-- Finalize all internal data structures
procedure Initialize_Early_Call_Region_Processor;
pragma Inline (Initialize_Early_Call_Region_Processor);
-- Initialize all internal data structures
end Early_Call_Region_Processor;
use Early_Call_Region_Processor;
-- The following package provides access to the elaboration statuses of all
-- units withed by the main unit.
package Elaborated_Units is
---------
-- API --
---------
procedure Collect_Elaborated_Units;
pragma Inline (Collect_Elaborated_Units);
-- Save the elaboration statuses of all units withed by the main unit
procedure Ensure_Prior_Elaboration
(N : Node_Id;
Unit_Id : Entity_Id;
Prag_Nam : Name_Id;
In_State : Processing_In_State);
pragma Inline (Ensure_Prior_Elaboration);
-- Guarantee the elaboration of unit Unit_Id with respect to the main
-- unit by either suggesting or installing an Elaborate[_All] pragma
-- denoted by Prag_Nam. N denotes the related scenario. In_State is the
-- current state of the Processing phase.
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
procedure Meet_Elaboration_Requirement
(N : Node_Id;
Targ_Id : Entity_Id;
Req_Nam : Name_Id;
In_State : Processing_In_State);
pragma Inline (Meet_Elaboration_Requirement);
-- Determine whether elaboration requirement Req_Nam for scenario N with
-- target Targ_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. In_State denotes the current state of
-- the Processing phase.
-----------------
-- Maintenance --
-----------------
procedure Finalize_Elaborated_Units;
pragma Inline (Finalize_Elaborated_Units);
-- Finalize all internal data structures
procedure Initialize_Elaborated_Units;
pragma Inline (Initialize_Elaborated_Units);
-- Initialize all internal data structures
end Elaborated_Units;
use Elaborated_Units;
-- The following package provides the main entry point for guaranteed ABE
-- checks and diagnostics.
package Guaranteed_ABE_Processor is
---------
-- API --
---------
procedure Process_Guaranteed_ABE
(N : Node_Id;
In_State : Processing_In_State);
pragma Inline (Process_Guaranteed_ABE);
-- Perform guaranteed ABE checks and diagnostics for scenario N.
-- In_State is the current state of the Processing phase.
end Guaranteed_ABE_Processor;
use Guaranteed_ABE_Processor;
-- The following package provides access to the internal representation of
-- scenarios and targets.
package Internal_Representation is
-----------
-- Types --
-----------
-- The following type enumerates all possible Ghost mode kinds
type Extended_Ghost_Mode is
(Is_Ignored,
Is_Checked_Or_Not_Specified);
-- The following type enumerates all possible SPARK mode kinds
type Extended_SPARK_Mode is
(Is_On,
Is_Off_Or_Not_Specified);
--------------
-- Builders --
--------------
function Scenario_Representation_Of
(N : Node_Id;
In_State : Processing_In_State) return Scenario_Rep_Id;
pragma Inline (Scenario_Representation_Of);
-- Obtain the id of elaboration scenario N's representation. The routine
-- constructs the representation if it is not available. In_State is the
-- current state of the Processing phase.
function Target_Representation_Of
(Id : Entity_Id;
In_State : Processing_In_State) return Target_Rep_Id;
pragma Inline (Target_Representation_Of);
-- Obtain the id of elaboration target Id's representation. The routine
-- constructs the representation if it is not available. In_State is the
-- current state of the Processing phase.
-------------------------
-- Scenario attributes --
-------------------------
function Activated_Task_Objects
(S_Id : Scenario_Rep_Id) return NE_List.Doubly_Linked_List;
pragma Inline (Activated_Task_Objects);
-- For Task_Activation_Scenario S_Id, obtain the list of task objects
-- the scenario is activating.
function Activated_Task_Type (S_Id : Scenario_Rep_Id) return Entity_Id;
pragma Inline (Activated_Task_Type);
-- For Task_Activation_Scenario S_Id, obtain the currently activated
-- task type.
procedure Disable_Elaboration_Checks (S_Id : Scenario_Rep_Id);
pragma Inline (Disable_Elaboration_Checks);
-- Disable elaboration checks of scenario S_Id
function Elaboration_Checks_OK (S_Id : Scenario_Rep_Id) return Boolean;
pragma Inline (Elaboration_Checks_OK);
-- Determine whether scenario S_Id may be subjected to elaboration
-- checks.
function Elaboration_Warnings_OK (S_Id : Scenario_Rep_Id) return Boolean;
pragma Inline (Elaboration_Warnings_OK);
-- Determine whether scenario S_Id may be subjected to elaboration
-- warnings.
function Ghost_Mode_Of
(S_Id : Scenario_Rep_Id) return Extended_Ghost_Mode;
pragma Inline (Ghost_Mode_Of);
-- Obtain the Ghost mode of scenario S_Id
function Is_Dispatching_Call (S_Id : Scenario_Rep_Id) return Boolean;
pragma Inline (Is_Dispatching_Call);
-- For Call_Scenario S_Id, determine whether the call is dispatching
function Is_Read_Reference (S_Id : Scenario_Rep_Id) return Boolean;
pragma Inline (Is_Read_Reference);
-- For Variable_Reference_Scenario S_Id, determine whether the reference
-- is a read.
function Kind (S_Id : Scenario_Rep_Id) return Scenario_Kind;
pragma Inline (Kind);
-- Obtain the nature of scenario S_Id
function Level (S_Id : Scenario_Rep_Id) return Enclosing_Level_Kind;
pragma Inline (Level);
-- Obtain the enclosing level of scenario S_Id
procedure Set_Activated_Task_Objects
(S_Id : Scenario_Rep_Id;
Task_Objs : NE_List.Doubly_Linked_List);
pragma Inline (Set_Activated_Task_Objects);
-- For Task_Activation_Scenario S_Id, set the list of task objects
-- activated by the scenario to Task_Objs.
procedure Set_Activated_Task_Type
(S_Id : Scenario_Rep_Id;
Task_Typ : Entity_Id);
pragma Inline (Set_Activated_Task_Type);
-- For Task_Activation_Scenario S_Id, set the currently activated task
-- type to Task_Typ.
function SPARK_Mode_Of
(S_Id : Scenario_Rep_Id) return Extended_SPARK_Mode;
pragma Inline (SPARK_Mode_Of);
-- Obtain the SPARK mode of scenario S_Id
function Target (S_Id : Scenario_Rep_Id) return Entity_Id;
pragma Inline (Target);
-- Obtain the target of scenario S_Id
-----------------------
-- Target attributes --
-----------------------
function Barrier_Body_Declaration (T_Id : Target_Rep_Id) return Node_Id;
pragma Inline (Barrier_Body_Declaration);
-- For Subprogram_Target T_Id, obtain the declaration of the barrier
-- function's body.
function Body_Declaration (T_Id : Target_Rep_Id) return Node_Id;
pragma Inline (Body_Declaration);
-- Obtain the declaration of the body which belongs to target T_Id
procedure Disable_Elaboration_Checks (T_Id : Target_Rep_Id);
pragma Inline (Disable_Elaboration_Checks);
-- Disable elaboration checks of target T_Id
function Elaboration_Checks_OK (T_Id : Target_Rep_Id) return Boolean;
pragma Inline (Elaboration_Checks_OK);
-- Determine whether target T_Id may be subjected to elaboration checks
function Elaboration_Warnings_OK (T_Id : Target_Rep_Id) return Boolean;
pragma Inline (Elaboration_Warnings_OK);
-- Determine whether target T_Id may be subjected to elaboration
-- warnings.
function Ghost_Mode_Of (T_Id : Target_Rep_Id) return Extended_Ghost_Mode;
pragma Inline (Ghost_Mode_Of);
-- Obtain the Ghost mode of target T_Id
function Kind (T_Id : Target_Rep_Id) return Target_Kind;
pragma Inline (Kind);
-- Obtain the nature of target T_Id
function SPARK_Mode_Of (T_Id : Target_Rep_Id) return Extended_SPARK_Mode;
pragma Inline (SPARK_Mode_Of);
-- Obtain the SPARK mode of target T_Id
function Spec_Declaration (T_Id : Target_Rep_Id) return Node_Id;
pragma Inline (Spec_Declaration);
-- Obtain the declaration of the spec which belongs to target T_Id
function Unit (T_Id : Target_Rep_Id) return Entity_Id;
pragma Inline (Unit);
-- Obtain the unit where the target is defined
function Variable_Declaration (T_Id : Target_Rep_Id) return Node_Id;
pragma Inline (Variable_Declaration);
-- For Variable_Target T_Id, obtain the declaration of the variable
-----------------
-- Maintenance --
-----------------
procedure Finalize_Internal_Representation;
pragma Inline (Finalize_Internal_Representation);
-- Finalize all internal data structures
procedure Initialize_Internal_Representation;
pragma Inline (Initialize_Internal_Representation);
-- Initialize all internal data structures
end Internal_Representation;
use Internal_Representation;
-- The following package provides functionality for recording pieces of the
-- invocation graph in the ALI file of the main unit.
package Invocation_Graph is
---------
-- API --
---------
procedure Record_Invocation_Graph;
pragma Inline (Record_Invocation_Graph);
-- Process all declaration, instantiation, and library level scenarios,
-- along with invocation construct within the spec and body of the main
-- unit to determine whether any of these reach into an external unit.
-- If such a path exists, encode in the ALI file of the main unit.
-----------------
-- Maintenance --
-----------------
procedure Finalize_Invocation_Graph;
pragma Inline (Finalize_Invocation_Graph);
-- Finalize all internal data structures
procedure Initialize_Invocation_Graph;
pragma Inline (Initialize_Invocation_Graph);
-- Initialize all internal data structures
end Invocation_Graph;
use Invocation_Graph;
-- The following package stores scenarios
package Scenario_Storage is
---------
-- API --
---------
procedure Add_Declaration_Scenario (N : Node_Id);
pragma Inline (Add_Declaration_Scenario);
-- Save declaration level scenario N
procedure Add_Dynamic_ABE_Check_Scenario (N : Node_Id);
pragma Inline (Add_Dynamic_ABE_Check_Scenario);
-- Save scenario N for conditional ABE check installation purposes when
-- the dynamic model is in effect.
procedure Add_Library_Body_Scenario (N : Node_Id);
pragma Inline (Add_Library_Body_Scenario);
-- Save library-level body scenario N
procedure Add_Library_Spec_Scenario (N : Node_Id);
pragma Inline (Add_Library_Spec_Scenario);
-- Save library-level spec scenario N
procedure Add_SPARK_Scenario (N : Node_Id);
pragma Inline (Add_SPARK_Scenario);
-- Save SPARK scenario N
procedure Delete_Scenario (N : Node_Id);
pragma Inline (Delete_Scenario);
-- Delete arbitrary scenario N
function Iterate_Declaration_Scenarios return NE_Set.Iterator;
pragma Inline (Iterate_Declaration_Scenarios);
-- Obtain an iterator over all declaration level scenarios
function Iterate_Dynamic_ABE_Check_Scenarios return NE_Set.Iterator;
pragma Inline (Iterate_Dynamic_ABE_Check_Scenarios);
-- Obtain an iterator over all scenarios that require a conditional ABE
-- check when the dynamic model is in effect.
function Iterate_Library_Body_Scenarios return NE_Set.Iterator;
pragma Inline (Iterate_Library_Body_Scenarios);
-- Obtain an iterator over all library level body scenarios
function Iterate_Library_Spec_Scenarios return NE_Set.Iterator;
pragma Inline (Iterate_Library_Spec_Scenarios);
-- Obtain an iterator over all library level spec scenarios
function Iterate_SPARK_Scenarios return NE_Set.Iterator;
pragma Inline (Iterate_SPARK_Scenarios);
-- Obtain an iterator over all SPARK scenarios
procedure Replace_Scenario (Old_N : Node_Id; New_N : Node_Id);
pragma Inline (Replace_Scenario);
-- Replace scenario Old_N with scenario New_N
-----------------
-- Maintenance --
-----------------
procedure Finalize_Scenario_Storage;
pragma Inline (Finalize_Scenario_Storage);
-- Finalize all internal data structures
procedure Initialize_Scenario_Storage;
pragma Inline (Initialize_Scenario_Storage);
-- Initialize all internal data structures
end Scenario_Storage;
use Scenario_Storage;
-- The following package provides various semantic predicates
package Semantics is
---------
-- API --
---------
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 denotes 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
-- verifies 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_Bridge_Target (Id : Entity_Id) return Boolean;
pragma Inline (Is_Bridge_Target);
-- Determine whether arbitrary entity Id denotes a bridge target
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_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_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_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 denotes a source or internally
-- generated subprogram which emulates SPARK semantics.
function Is_Subprogram_Inst (Id : Entity_Id) return Boolean;
pragma Inline (Is_Subprogram_Inst);
-- Determine whether arbitrary entity Id denotes a subprogram instance
function Is_Suitable_Access_Taken (N : Node_Id) return Boolean;
pragma Inline (Is_Suitable_Access_Taken);
-- 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_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
(Targ_Decl : Node_Id;
In_State : Processing_In_State) 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 with by declaration
-- Target_Decl is within a context which encloses the current root or is
-- in a different unit. In_State is the current state of the Processing
-- phase.
end Semantics;
use Semantics;
-- The following package provides the main entry point for SPARK-related
-- checks and diagnostics.
package SPARK_Processor is
---------
-- API --
---------
procedure Check_SPARK_Model_In_Effect;
pragma Inline (Check_SPARK_Model_In_Effect);
-- Determine whether a suitable elaboration model is currently in effect
-- for verifying SPARK rules. Emit a warning if this is not the case.
procedure Check_SPARK_Scenarios;
pragma Inline (Check_SPARK_Scenarios);
-- Examine SPARK scenarios which are not necessarily executable during
-- elaboration, but still requires elaboration-related checks.
end SPARK_Processor;
use SPARK_Processor;
-----------------------
-- Local subprograms --
-----------------------
function Assignment_Target (Asmt : Node_Id) return Node_Id;
pragma Inline (Assignment_Target);
-- Obtain the target of assignment statement Asmt
function Call_Name (Call : Node_Id) return Node_Id;
pragma Inline (Call_Name);
-- Obtain the name of an entry, operator, or subprogram call Call
function Canonical_Subprogram (Subp_Id : Entity_Id) return Entity_Id;
pragma Inline (Canonical_Subprogram);
-- Obtain the uniform canonical entity of subprogram Subp_Id
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 Elaboration_Phase_Active return Boolean;
pragma Inline (Elaboration_Phase_Active);
-- Determine whether the elaboration phase of the compilation has started
procedure Error_Preelaborated_Call (N : Node_Id);
-- Give an error or warning for a non-static/non-preelaborable call in a
-- preelaborated unit.
procedure Finalize_All_Data_Structures;
pragma Inline (Finalize_All_Data_Structures);
-- Destroy all internal data structures
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;
pragma Inline (Has_Body);
-- Determine whether package declaration Pack_Decl has a corresponding body
-- or would eventually have one.
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;
pragma Inline (In_Same_Context);
-- 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 Initialize_All_Data_Structures;
pragma Inline (Initialize_All_Data_Structures);
-- Create all internal data structures
function Instantiated_Generic (Inst : Node_Id) return Entity_Id;
pragma Inline (Instantiated_Generic);
-- Obtain the generic instantiated by instance Inst
function Is_Safe_Activation
(Call : Node_Id;
Task_Rep : Target_Rep_Id) return Boolean;
pragma Inline (Is_Safe_Activation);
-- Determine whether activation call Call which activates an object of a
-- task type described by representation Task_Rep is always ABE-safe.
function Is_Safe_Call
(Call : Node_Id;
Subp_Id : Entity_Id;
Subp_Rep : Target_Rep_Id) return Boolean;
pragma Inline (Is_Safe_Call);
-- Determine whether call Call which invokes entry, operator, or subprogram
-- Subp_Id is always ABE-safe. Subp_Rep is the representation of the entry,
-- operator, or subprogram.
function Is_Safe_Instantiation
(Inst : Node_Id;
Gen_Id : Entity_Id;
Gen_Rep : Target_Rep_Id) return Boolean;
pragma Inline (Is_Safe_Instantiation);
-- Determine whether instantiation Inst which instantiates generic Gen_Id
-- is always ABE-safe. Gen_Rep is the representation of the generic.
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 Main_Unit_Entity return Entity_Id;
pragma Inline (Main_Unit_Entity);
-- Return the entity of the main unit
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.
function Scenario (N : Node_Id) return Node_Id;
pragma Inline (Scenario);
-- Return the appropriate scenario node for scenario N
procedure Set_Elaboration_Phase (Status : Elaboration_Phase_Status);
pragma Inline (Set_Elaboration_Phase);
-- Change the status of the elaboration phase of the compiler to Status
procedure Spec_And_Body_From_Entity
(Id : Entity_Id;
Spec_Decl : out Node_Id;
Body_Decl : out Node_Id);
pragma Inline (Spec_And_Body_From_Entity);
-- Given arbitrary entity Id representing a construct with a spec and body,
-- retrieve declaration of the spec in Spec_Decl and the declaration of the
-- body in Body_Decl.
procedure Spec_And_Body_From_Node
(N : Node_Id;
Spec_Decl : out Node_Id;
Body_Decl : out Node_Id);
pragma Inline (Spec_And_Body_From_Node);
-- Given arbitrary node N representing a construct with a spec and body,
-- retrieve declaration of the spec in Spec_Decl and the declaration of
-- the body in Body_Decl.
function Static_Elaboration_Checks return Boolean;
pragma Inline (Static_Elaboration_Checks);
-- Determine whether the static model is in effect
function Unit_Entity (Unit_Id : Entity_Id) return Entity_Id;
pragma Inline (Unit_Entity);
-- Return the entity of the initial declaration for unit Unit_Id
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.
----------------------
-- Active_Scenarios --
----------------------
package body Active_Scenarios is
-----------------------
-- Local subprograms --
-----------------------
procedure Output_Access_Taken
(Attr : Node_Id;
Attr_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Access_Taken);
-- Emit a specific diagnostic message for 'Access attribute reference
-- Attr with representation Attr_Rep. The message is associated with
-- node Error_Nod.
procedure Output_Active_Scenario
(N : Node_Id;
Error_Nod : Node_Id;
In_State : Processing_In_State);
pragma Inline (Output_Active_Scenario);
-- Top level dispatcher for outputting a scenario. Emit a specific
-- diagnostic message for scenario N. The message is associated with
-- node Error_Nod. In_State is the current state of the Processing
-- phase.
procedure Output_Call
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Call);
-- Emit a diagnostic message for call Call with representation Call_Rep.
-- The message is associated with node Error_Nod.
procedure Output_Header (Error_Nod : Node_Id);
pragma Inline (Output_Header);
-- Emit a specific diagnostic message for the unit of the root scenario.
-- The message is associated with node Error_Nod.
procedure Output_Instantiation
(Inst : Node_Id;
Inst_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Instantiation);
-- Emit a specific diagnostic message for instantiation Inst with
-- representation Inst_Rep. The message is associated with node
-- Error_Nod.
procedure Output_Refined_State_Pragma
(Prag : Node_Id;
Prag_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Refined_State_Pragma);
-- Emit a specific diagnostic message for Refined_State pragma Prag
-- with representation Prag_Rep. The message is associated with node
-- Error_Nod.
procedure Output_Task_Activation
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Task_Activation);
-- Emit a specific diagnostic message for activation call Call
-- with representation Call_Rep. The message is associated with
-- node Error_Nod.
procedure Output_Variable_Assignment
(Asmt : Node_Id;
Asmt_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Variable_Assignment);
-- Emit a specific diagnostic message for assignment statement Asmt
-- with representation Asmt_Rep. The message is associated with node
-- Error_Nod.
procedure Output_Variable_Reference
(Ref : Node_Id;
Ref_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id);
pragma Inline (Output_Variable_Reference);
-- Emit a specific diagnostic message for read reference Ref with
-- representation Ref_Rep. The message is associated with node
-- Error_Nod.
-------------------
-- Output_Access --
-------------------
procedure Output_Access_Taken
(Attr : Node_Id;
Attr_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
Subp_Id : constant Entity_Id := Target (Attr_Rep);
begin
Error_Msg_Name_1 := Attribute_Name (Attr);
Error_Msg_Sloc := Sloc (Attr);
Error_Msg_NE ("\\ % of & taken #", Error_Nod, Subp_Id);
end Output_Access_Taken;
----------------------------
-- Output_Active_Scenario --
----------------------------
procedure Output_Active_Scenario
(N : Node_Id;
Error_Nod : Node_Id;
In_State : Processing_In_State)
is
Scen : constant Node_Id := Scenario (N);
Scen_Rep : Scenario_Rep_Id;
begin
-- 'Access
if Is_Suitable_Access_Taken (Scen) then
Output_Access_Taken
(Attr => Scen,
Attr_Rep => Scenario_Representation_Of (Scen, In_State),
Error_Nod => Error_Nod);
-- Call or task activation
elsif Is_Suitable_Call (Scen) then
Scen_Rep := Scenario_Representation_Of (Scen, In_State);
if Kind (Scen_Rep) = Call_Scenario then
Output_Call
(Call => Scen,
Call_Rep => Scen_Rep,
Error_Nod => Error_Nod);
else
pragma Assert (Kind (Scen_Rep) = Task_Activation_Scenario);
Output_Task_Activation
(Call => Scen,
Call_Rep => Scen_Rep,
Error_Nod => Error_Nod);
end if;
-- Instantiation
elsif Is_Suitable_Instantiation (Scen) then
Output_Instantiation
(Inst => Scen,
Inst_Rep => Scenario_Representation_Of (Scen, In_State),
Error_Nod => Error_Nod);
-- Pragma Refined_State
elsif Is_Suitable_SPARK_Refined_State_Pragma (Scen) then
Output_Refined_State_Pragma
(Prag => Scen,
Prag_Rep => Scenario_Representation_Of (Scen, In_State),
Error_Nod => Error_Nod);
-- Variable assignment
elsif Is_Suitable_Variable_Assignment (Scen) then
Output_Variable_Assignment
(Asmt => Scen,
Asmt_Rep => Scenario_Representation_Of (Scen, In_State),
Error_Nod => Error_Nod);
-- Variable reference
elsif Is_Suitable_Variable_Reference (Scen) then
Output_Variable_Reference
(Ref => Scen,
Ref_Rep => Scenario_Representation_Of (Scen, In_State),
Error_Nod => Error_Nod);
end if;
end Output_Active_Scenario;
-----------------------------
-- Output_Active_Scenarios --
-----------------------------
procedure Output_Active_Scenarios
(Error_Nod : Node_Id;
In_State : Processing_In_State)
is
package Scenarios renames Active_Scenario_Stack;
Header_Posted : Boolean := False;
begin
-- Output the contents of the active scenario stack starting from the
-- bottom, or the least recent scenario.
for Index in Scenarios.First .. Scenarios.Last loop
if not Header_Posted then
Output_Header (Error_Nod);
Header_Posted := True;
end if;
Output_Active_Scenario
(N => Scenarios.Table (Index),
Error_Nod => Error_Nod,
In_State => In_State);
end loop;
end Output_Active_Scenarios;
-----------------
-- Output_Call --
-----------------
procedure Output_Call
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
procedure Output_Accept_Alternative (Alt_Id : Entity_Id);
pragma Inline (Output_Accept_Alternative);
-- Emit a specific diagnostic message concerning accept alternative
-- with entity Alt_Id.
procedure Output_Call (Subp_Id : Entity_Id; Kind : String);
pragma Inline (Output_Call);
-- Emit a specific diagnostic message concerning a call of kind Kind
-- which invokes subprogram Subp_Id.
procedure Output_Type_Actions (Subp_Id : Entity_Id; Action : String);
pragma Inline (Output_Type_Actions);
-- Emit a specific diagnostic message concerning action Action of a
-- type performed by subprogram Subp_Id.
procedure Output_Verification_Call
(Pred : String;
Id : Entity_Id;
Id_Kind : String);
pragma Inline (Output_Verification_Call);
-- Emit a specific diagnostic message concerning the verification of
-- predicate Pred applied to related entity Id with kind Id_Kind.
-------------------------------
-- Output_Accept_Alternative --
-------------------------------
procedure Output_Accept_Alternative (Alt_Id : Entity_Id) is
Entry_Id : constant Entity_Id := Receiving_Entry (Alt_Id);
begin
pragma Assert (Present (Entry_Id));
Error_Msg_NE ("\\ entry & selected #", Error_Nod, Entry_Id);
end Output_Accept_Alternative;
-----------------
-- Output_Call --
-----------------
procedure Output_Call (Subp_Id : Entity_Id; Kind : String) is
begin
Error_Msg_NE ("\\ " & Kind & " & called #", Error_Nod, Subp_Id);
end Output_Call;
-------------------------
-- Output_Type_Actions --
-------------------------
procedure Output_Type_Actions
(Subp_Id : Entity_Id;
Action : String)
is
Typ : constant Entity_Id := First_Formal_Type (Subp_Id);
begin
pragma Assert (Present (Typ));
Error_Msg_NE
("\\ " & Action & " actions for type & #", Error_Nod, Typ);
end Output_Type_Actions;
------------------------------
-- Output_Verification_Call --
------------------------------
procedure Output_Verification_Call
(Pred : String;
Id : Entity_Id;
Id_Kind : String)
is
begin
pragma Assert (Present (Id));
Error_Msg_NE
("\\ " & Pred & " of " & Id_Kind & " & verified #",
Error_Nod, Id);
end Output_Verification_Call;
-- Local variables
Subp_Id : constant Entity_Id := Target (Call_Rep);
-- Start of processing for Output_Call
begin
Error_Msg_Sloc := Sloc (Call);
-- Accept alternative
if Is_Accept_Alternative_Proc (Subp_Id) then
Output_Accept_Alternative (Subp_Id);
-- Adjustment
elsif Is_TSS (Subp_Id, TSS_Deep_Adjust) then
Output_Type_Actions (Subp_Id, "adjustment");
-- Default_Initial_Condition
elsif Is_Default_Initial_Condition_Proc (Subp_Id) then
-- Only do output for a normal DIC procedure, since partial DIC
-- procedures are subsidiary to those.
if not Is_Partial_DIC_Procedure (Subp_Id) then
Output_Verification_Call
(Pred => "Default_Initial_Condition",
Id => First_Formal_Type (Subp_Id),
Id_Kind => "type");
end if;
-- Entries
elsif Is_Protected_Entry (Subp_Id) then
Output_Call (Subp_Id, "entry");
-- Task entry calls are never processed because the entry being
-- invoked does not have a corresponding "body", it has a select. A
-- task entry call appears in the stack of active scenarios for the
-- sole purpose of checking No_Entry_Calls_In_Elaboration_Code and
-- nothing more.
elsif Is_Task_Entry (Subp_Id) then
null;
-- Finalization
elsif Is_TSS (Subp_Id, TSS_Deep_Finalize) then
Output_Type_Actions (Subp_Id, "finalization");
-- Calls to _Finalizer procedures must not appear in the output
-- because this creates confusing noise.
elsif Is_Finalizer_Proc (Subp_Id) then
null;
-- Initial_Condition
elsif Is_Initial_Condition_Proc (Subp_Id) then
Output_Verification_Call
(Pred => "Initial_Condition",
Id => Find_Enclosing_Scope (Call),
Id_Kind => "package");
-- Initialization
elsif Is_Init_Proc (Subp_Id)
or else Is_TSS (Subp_Id, TSS_Deep_Initialize)
then
Output_Type_Actions (Subp_Id, "initialization");
-- Invariant
elsif Is_Invariant_Proc (Subp_Id) then
Output_Verification_Call
(Pred => "invariants",
Id => First_Formal_Type (Subp_Id),
Id_Kind => "type");
-- Partial invariant calls must not appear in the output because this
-- creates confusing noise. Note that a partial invariant is always
-- invoked by the "full" invariant which is already placed on the
-- stack.
elsif Is_Partial_Invariant_Proc (Subp_Id) then
null;
-- Subprograms must come last because some of the previous cases fall
-- under this category.
elsif Ekind (Subp_Id) = E_Function then
Output_Call (Subp_Id, "function");
elsif Ekind (Subp_Id) = E_Procedure then
Output_Call (Subp_Id, "procedure");
else
pragma Assert (False);
return;
end if;
end Output_Call;
-------------------
-- Output_Header --
-------------------
procedure Output_Header (Error_Nod : Node_Id) is
Unit_Id : constant Entity_Id := Find_Top_Unit (Root_Scenario);
begin
if Ekind (Unit_Id) = E_Package then
Error_Msg_NE ("\\ spec of unit & elaborated", Error_Nod, Unit_Id);
elsif Ekind (Unit_Id) = E_Package_Body then
Error_Msg_NE ("\\ body of unit & elaborated", Error_Nod, Unit_Id);
else
Error_Msg_NE ("\\ in body of unit &", Error_Nod, Unit_Id);
end if;
end Output_Header;
--------------------------
-- Output_Instantiation --
--------------------------
procedure Output_Instantiation
(Inst : Node_Id;
Inst_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
procedure Output_Instantiation (Gen_Id : Entity_Id; Kind : String);
pragma Inline (Output_Instantiation);
-- Emit a specific diagnostic message concerning an instantiation of
-- generic unit Gen_Id. Kind denotes the kind of the instantiation.
--------------------------
-- Output_Instantiation --
--------------------------
procedure Output_Instantiation (Gen_Id : Entity_Id; Kind : String) is
begin
Error_Msg_NE
("\\ " & Kind & " & instantiated as & #", Error_Nod, Gen_Id);
end Output_Instantiation;
-- Local variables
Gen_Id : constant Entity_Id := Target (Inst_Rep);
-- Start of processing for Output_Instantiation
begin
Error_Msg_Node_2 := Defining_Entity (Inst);
Error_Msg_Sloc := Sloc (Inst);
if Nkind (Inst) = N_Function_Instantiation then
Output_Instantiation (Gen_Id, "function");
elsif Nkind (Inst) = N_Package_Instantiation then
Output_Instantiation (Gen_Id, "package");
elsif Nkind (Inst) = N_Procedure_Instantiation then
Output_Instantiation (Gen_Id, "procedure");
else
pragma Assert (False);
return;
end if;
end Output_Instantiation;
---------------------------------
-- Output_Refined_State_Pragma --
---------------------------------
procedure Output_Refined_State_Pragma
(Prag : Node_Id;
Prag_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
pragma Unreferenced (Prag_Rep);
begin
Error_Msg_Sloc := Sloc (Prag);
Error_Msg_N ("\\ refinement constituents read #", Error_Nod);
end Output_Refined_State_Pragma;
----------------------------
-- Output_Task_Activation --
----------------------------
procedure Output_Task_Activation
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
pragma Unreferenced (Call_Rep);
function Find_Activator return Entity_Id;
-- Find the nearest enclosing construct which houses call Call
--------------------
-- Find_Activator --
--------------------
function Find_Activator return Entity_Id is
Par : Node_Id;
begin
-- Climb the parent chain looking for a package [body] or a
-- construct with a statement sequence.
Par := Parent (Call);
while Present (Par) loop
if Nkind (Par) in N_Package_Body | N_Package_Declaration then
return Defining_Entity (Par);
elsif Nkind (Par) = N_Handled_Sequence_Of_Statements then
return Defining_Entity (Parent (Par));
end if;
Par := Parent (Par);
end loop;
return Empty;
end Find_Activator;
-- Local variables
Activator : constant Entity_Id := Find_Activator;
-- Start of processing for Output_Task_Activation
begin
pragma Assert (Present (Activator));
Error_Msg_NE ("\\ local tasks of & activated", Error_Nod, Activator);
end Output_Task_Activation;
--------------------------------
-- Output_Variable_Assignment --
--------------------------------
procedure Output_Variable_Assignment
(Asmt : Node_Id;
Asmt_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
Var_Id : constant Entity_Id := Target (Asmt_Rep);
begin
Error_Msg_Sloc := Sloc (Asmt);
Error_Msg_NE ("\\ variable & assigned #", Error_Nod, Var_Id);
end Output_Variable_Assignment;
-------------------------------
-- Output_Variable_Reference --
-------------------------------
procedure Output_Variable_Reference
(Ref : Node_Id;
Ref_Rep : Scenario_Rep_Id;
Error_Nod : Node_Id)
is
Var_Id : constant Entity_Id := Target (Ref_Rep);
begin
Error_Msg_Sloc := Sloc (Ref);
Error_Msg_NE ("\\ variable & read #", Error_Nod, Var_Id);
end Output_Variable_Reference;
-------------------------
-- Pop_Active_Scenario --
-------------------------
procedure Pop_Active_Scenario (N : Node_Id) is
package Scenarios renames Active_Scenario_Stack;
Top : Node_Id renames Scenarios.Table (Scenarios.Last);
begin
pragma Assert (Top = N);
Scenarios.Decrement_Last;
end Pop_Active_Scenario;
--------------------------
-- Push_Active_Scenario --
--------------------------
procedure Push_Active_Scenario (N : Node_Id) is
begin
Active_Scenario_Stack.Append (N);
end Push_Active_Scenario;
-------------------
-- Root_Scenario --
-------------------
function Root_Scenario return Node_Id is
package Scenarios renames Active_Scenario_Stack;
begin
-- Ensure that the scenario stack has at least one active scenario in
-- it. The one at the bottom (index First) is the root scenario.
pragma Assert (Scenarios.Last >= Scenarios.First);
return Scenarios.Table (Scenarios.First);
end Root_Scenario;
end Active_Scenarios;
--------------------------
-- Activation_Processor --
--------------------------
package body Activation_Processor is
------------------------
-- Process_Activation --
------------------------
procedure Process_Activation
(Call : Node_Id;
Call_Rep : Scenario_Rep_Id;
Processor : Activation_Processor_Ptr;
In_State : Processing_In_State)
is
procedure Process_Task_Object (Obj_Id : Entity_Id; Typ : Entity_Id);
pragma Inline (Process_Task_Object);
-- Invoke Processor for task object Obj_Id of type Typ
procedure Process_Task_Objects
(Task_Objs : NE_List.Doubly_Linked_List);
pragma Inline (Process_Task_Objects);
-- Invoke Processor for all task objects found in list Task_Objs
procedure Traverse_List
(List : List_Id;
Task_Objs : NE_List.Doubly_Linked_List);
pragma Inline (Traverse_List);
-- Traverse declarative or statement list List while searching for
-- objects of a task type, or containing task components. If such an
-- object is found, first save it in list Task_Objs and then invoke
-- Processor on it.
-------------------------
-- Process_Task_Object --
-------------------------
procedure Process_Task_Object (Obj_Id : Entity_Id; Typ : Entity_Id) is
Root_Typ : constant Entity_Id :=
Non_Private_View (Root_Type (Typ));
Comp_Id : Entity_Id;
Obj_Rep : Target_Rep_Id;
Root_Rep : Target_Rep_Id;
New_In_State : Processing_In_State := In_State;
-- Each step of the Processing phase constitutes a new state
begin
if Is_Task_Type (Typ) then
Obj_Rep := Target_Representation_Of (Obj_Id, New_In_State);
Root_Rep := Target_Representation_Of (Root_Typ, New_In_State);
-- Warnings are suppressed when a prior scenario is already in
-- that mode, or when the object, activation call, or task type
-- have warnings suppressed. Update the state of the Processing
-- phase to reflect this.
New_In_State.Suppress_Warnings :=
New_In_State.Suppress_Warnings
or else not Elaboration_Warnings_OK (Call_Rep)
or else not Elaboration_Warnings_OK (Obj_Rep)
or else not Elaboration_Warnings_OK (Root_Rep);
-- Update the state of the Processing phase to indicate that
-- any further traversal is now within a task body.
New_In_State.Within_Task_Body := True;
-- Associate the current task type with the activation call
Set_Activated_Task_Type (Call_Rep, Root_Typ);
-- Process the activation of the current task object by calling
-- the supplied processor.
Processor.all
(Call => Call,
Call_Rep => Call_Rep,
Obj_Id => Obj_Id,
Obj_Rep => Obj_Rep,
Task_Typ => Root_Typ,
Task_Rep => Root_Rep,
In_State => New_In_State);
-- Reset the association between the current task and the
-- activtion call.
Set_Activated_Task_Type (Call_Rep, Empty);
-- Examine the component type when the object is an array
elsif Is_Array_Type (Typ) and then Has_Task (Root_Typ) then
Process_Task_Object
(Obj_Id => Obj_Id,
Typ => Component_Type (Typ));
-- Examine individual component types when the object is a record
elsif Is_Record_Type (Typ) and then Has_Task (Root_Typ) then
Comp_Id := First_Component (Typ);
while Present (Comp_Id) loop
Process_Task_Object
(Obj_Id => Obj_Id,
Typ => Etype (Comp_Id));
Next_Component (Comp_Id);
end loop;
end if;
end Process_Task_Object;
--------------------------
-- Process_Task_Objects --
--------------------------
procedure Process_Task_Objects
(Task_Objs : NE_List.Doubly_Linked_List)
is
Iter : NE_List.Iterator;
Obj_Id : Entity_Id;
begin
Iter := NE_List.Iterate (Task_Objs);
while NE_List.Has_Next (Iter) loop
NE_List.Next (Iter, Obj_Id);
Process_Task_Object
(Obj_Id => Obj_Id,
Typ => Etype (Obj_Id));
end loop;
end Process_Task_Objects;
-------------------
-- Traverse_List --
-------------------
procedure Traverse_List
(List : List_Id;
Task_Objs : NE_List.Doubly_Linked_List)
is
Item : Node_Id;
Item_Id : Entity_Id;
Item_Typ : Entity_Id;
begin
-- Examine the contents of the list looking for an object
-- declaration of a task type or one that contains a task
-- within.
Item := First (List);
while Present (Item) loop
if Nkind (Item) = N_Object_Declaration then
Item_Id := Defining_Entity (Item);
Item_Typ := Etype (Item_Id);
if Has_Task (Item_Typ) then
-- The object is either of a task type, or contains a
-- task component. Save it in the list of task objects
-- associated with the activation call.
NE_List.Append (Task_Objs, Item_Id);
Process_Task_Object
(Obj_Id => Item_Id,
Typ => Item_Typ);
end if;
end if;
Next (Item);
end loop;
end Traverse_List;
-- Local variables
Context : Node_Id;
Spec : Node_Id;
Task_Objs : NE_List.Doubly_Linked_List;
-- Start of processing for Process_Activation
begin
-- Nothing to do when the activation is a guaranteed ABE
if Is_Known_Guaranteed_ABE (Call) then
return;
end if;
Task_Objs := Activated_Task_Objects (Call_Rep);
-- The activation call has been processed at least once, and all
-- task objects have already been collected. Directly process the
-- objects without having to reexamine the context of the call.
if NE_List.Present (Task_Objs) then
Process_Task_Objects (Task_Objs);
-- Otherwise the activation call is being processed for the first
-- time. Collect all task objects in case the call is reprocessed
-- multiple times.
else
Task_Objs := NE_List.Create;
Set_Activated_Task_Objects (Call_Rep, Task_Objs);
-- Find the context of the activation call where all task objects
-- being activated are declared. This is usually the parent of the
-- call.
Context := Parent (Call);
-- Handle the case where the activation call appears within the
-- handled statements of a block or a body.
if Nkind (Context) = N_Handled_Sequence_Of_Statements then
Context := Parent (Context);
end if;
-- Process all task objects in both the spec and body when the
-- activation call appears in a package body.
if Nkind (Context) = N_Package_Body then
Spec :=
Specification
(Unit_Declaration_Node (Corresponding_Spec (Context)));
Traverse_List
(List => Visible_Declarations (Spec),
Task_Objs => Task_Objs);
Traverse_List
(List => Private_Declarations (Spec),
Task_Objs => Task_Objs);
Traverse_List
(List => Declarations (Context),
Task_Objs => Task_Objs);
-- Process all task objects in the spec when the activation call
-- appears in a package spec.
elsif Nkind (Context) = N_Package_Specification then
Traverse_List
(List => Visible_Declarations (Context),
Task_Objs => Task_Objs);
Traverse_List
(List => Private_Declarations (Context),
Task_Objs => Task_Objs);
-- Otherwise the context must be a block or a body. Process all
-- task objects found in the declarations.
else
pragma Assert
(Nkind (Context) in
N_Block_Statement | N_Entry_Body | N_Protected_Body |
N_Subprogram_Body | N_Task_Body);
Traverse_List
(List => Declarations (Context),
Task_Objs => Task_Objs);
end if;
end if;
end Process_Activation;
end Activation_Processor;
-----------------------
-- Assignment_Target --
-----------------------
function Assignment_Target (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 (Nam) in
N_Explicit_Dereference | N_Indexed_Component |
N_Selected_Component | N_Slice
loop
Nam := Prefix (Nam);
end loop;
return Nam;
end Assignment_Target;
--------------------
-- Body_Processor --
--------------------
package body Body_Processor is
---------------------
-- Data structures --
---------------------
-- The following map relates scenario lists to subprogram bodies
Nested_Scenarios_Map : NE_List_Map.Dynamic_Hash_Table := NE_List_Map.Nil;
-- The following set contains all subprogram bodies that have been
-- processed by routine Traverse_Body.
Traversed_Bodies_Set : NE_Set.Membership_Set := NE_Set.Nil;
-----------------------
-- Local subprograms --
-----------------------
function Is_Traversed_Body (N : Node_Id) return Boolean;
pragma Inline (Is_Traversed_Body);
-- Determine whether subprogram body N has already been traversed
function Nested_Scenarios
(N : Node_Id) return NE_List.Doubly_Linked_List;
pragma Inline (Nested_Scenarios);
-- Obtain the list of scenarios associated with subprogram body N
procedure Set_Is_Traversed_Body (N : Node_Id);
pragma Inline (Set_Is_Traversed_Body);
-- Mark subprogram body N as traversed
procedure Set_Nested_Scenarios
(N : Node_Id;
Scenarios : NE_List.Doubly_Linked_List);
pragma Inline (Set_Nested_Scenarios);
-- Associate scenario list Scenarios with subprogram body N
-----------------------------
-- Finalize_Body_Processor --
-----------------------------
procedure Finalize_Body_Processor is
begin
NE_List_Map.Destroy (Nested_Scenarios_Map);
NE_Set.Destroy (Traversed_Bodies_Set);
end Finalize_Body_Processor;
-------------------------------
-- Initialize_Body_Processor --
-------------------------------
procedure Initialize_Body_Processor is
begin
Nested_Scenarios_Map := NE_List_Map.Create (250);
Traversed_Bodies_Set := NE_Set.Create (250);
end Initialize_Body_Processor;
-----------------------
-- Is_Traversed_Body --
-----------------------
function Is_Traversed_Body (N : Node_Id) return Boolean is
pragma Assert (Present (N));
begin
return NE_Set.Contains (Traversed_Bodies_Set, N);
end Is_Traversed_Body;
----------------------
-- Nested_Scenarios --
----------------------
function Nested_Scenarios
(N : Node_Id) return NE_List.Doubly_Linked_List
is
pragma Assert (Present (N));
pragma Assert (Nkind (N) = N_Subprogram_Body);
begin
return NE_List_Map.Get (Nested_Scenarios_Map, N);
end Nested_Scenarios;
----------------------------
-- Reset_Traversed_Bodies --
----------------------------
procedure Reset_Traversed_Bodies is
begin
NE_Set.Reset (Traversed_Bodies_Set);
end Reset_Traversed_Bodies;
---------------------------
-- Set_Is_Traversed_Body --
---------------------------
procedure Set_Is_Traversed_Body (N : Node_Id) is
pragma Assert (Present (N));
begin
NE_Set.Insert (Traversed_Bodies_Set, N);
end Set_Is_Traversed_Body;
--------------------------
-- Set_Nested_Scenarios --
--------------------------
procedure Set_Nested_Scenarios
(N : Node_Id;
Scenarios : NE_List.Doubly_Linked_List)
is
pragma Assert (Present (N));
begin
NE_List_Map.Put (Nested_Scenarios_Map, N, Scenarios);
end Set_Nested_Scenarios;
-------------------
-- Traverse_Body --
-------------------
procedure Traverse_Body
(N : Node_Id;
Requires_Processing : Scenario_Predicate_Ptr;
Processor : Scenario_Processor_Ptr;
In_State : Processing_In_State)
is
Scenarios : NE_List.Doubly_Linked_List := NE_List.Nil;
-- The list of scenarios that appear within the declarations and
-- statement of subprogram body N. The variable is intentionally
-- global because Is_Potential_Scenario needs to populate it.
function In_Task_Body (Nod : Node_Id) return Boolean;
pragma Inline (In_Task_Body);
-- Determine whether arbitrary node Nod appears within a task body
function Is_Synchronous_Suspension_Call
(Nod : Node_Id) return Boolean;
pragma Inline (Is_Synchronous_Suspension_Call);
-- Determine whether arbitrary node Nod denotes a call to one of
-- these routines:
--
-- Ada.Synchronous_Barriers.Wait_For_Release
-- Ada.Synchronous_Task_Control.Suspend_Until_True
procedure Traverse_Collected_Scenarios;
pragma Inline (Traverse_Collected_Scenarios);
-- Traverse the already collected scenarios in list Scenarios by
-- invoking Processor on each individual one.
procedure Traverse_List (List : List_Id);
pragma Inline (Traverse_List);
-- Invoke Traverse_Potential_Scenarios on each node in list List
function Traverse_Potential_Scenario
(Scen : Node_Id) return Traverse_Result;
pragma Inline (Traverse_Potential_Scenario);
-- Determine whether arbitrary node Scen is a suitable scenario using
-- predicate Is_Scenario and traverse it by invoking Processor on it.
procedure Traverse_Potential_Scenarios is
new Traverse_Proc (Traverse_Potential_Scenario);
------------------
-- In_Task_Body --
------------------
function In_Task_Body (Nod : Node_Id) return Boolean is
Par : Node_Id;
begin
-- Climb the parent chain looking for a task body [procedure]
Par := Nod;
while Present (Par) loop
if Nkind (Par) = N_Task_Body then
return True;
elsif Nkind (Par) = N_Subprogram_Body
and then Is_Task_Body_Procedure (Par)
then
return True;
-- Prevent the search from going too far. Note that this test
-- shares nodes with the two cases above, and must come last.
elsif Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Par := Parent (Par);
end loop;
return False;
end In_Task_Body;
------------------------------------
-- Is_Synchronous_Suspension_Call --
------------------------------------
function Is_Synchronous_Suspension_Call
(Nod : Node_Id) return Boolean
is
Subp_Id : Entity_Id;
begin
-- To qualify, the call must invoke one of the runtime routines
-- which perform synchronous suspension.
if Is_Suitable_Call (Nod) then
Subp_Id := Target (Nod);
return
Is_RTE (Subp_Id, RE_Suspend_Until_True)
or else
Is_RTE (Subp_Id, RE_Wait_For_Release);
end if;
return False;
end Is_Synchronous_Suspension_Call;
----------------------------------
-- Traverse_Collected_Scenarios --
----------------------------------
procedure Traverse_Collected_Scenarios is
Iter : NE_List.Iterator;
Scen : Node_Id;
begin
Iter := NE_List.Iterate (Scenarios);
while NE_List.Has_Next (Iter) loop
NE_List.Next (Iter, Scen);
-- The current scenario satisfies the input predicate, process
-- it.
if Requires_Processing.all (Scen) then
Processor.all (Scen, In_State);
end if;
end loop;
end Traverse_Collected_Scenarios;
-------------------
-- Traverse_List --
-------------------
procedure Traverse_List (List : List_Id) is
Scen : Node_Id;
begin
Scen := First (List);
while Present (Scen) loop
Traverse_Potential_Scenarios (Scen);
Next (Scen);
end loop;
end Traverse_List;
---------------------------------
-- Traverse_Potential_Scenario --
---------------------------------
function Traverse_Potential_Scenario
(Scen : Node_Id) return Traverse_Result
is
begin
-- Special cases
-- Skip constructs which do not have elaboration of their own and
-- need to be elaborated by other means such as invocation, task
-- activation, etc.
if Is_Non_Library_Level_Encapsulator (Scen) then
return Skip;
-- Terminate the traversal of a task body when encountering an
-- accept or select statement, and
--
-- * Entry calls during elaboration are not allowed. In this
-- case the accept or select statement will cause the task
-- to block at elaboration time because there are no entry
-- calls to unblock it.
--
-- or
--
-- * Switch -gnatd_a (stop elaboration checks on accept or
-- select statement) is in effect.
elsif (Debug_Flag_Underscore_A
or else Restriction_Active
(No_Entry_Calls_In_Elaboration_Code))
and then Nkind (Original_Node (Scen)) in
N_Accept_Statement | N_Selective_Accept
then
return Abandon;
-- Terminate the traversal of a task body when encountering a
-- suspension call, and
--
-- * Entry calls during elaboration are not allowed. In this
-- case the suspension call emulates an entry call and will
-- cause the task to block at elaboration time.
--
-- or
--
-- * Switch -gnatd_s (stop elaboration checks on synchronous
-- suspension) is in effect.
--
-- Note that the guard should not be checking the state of flag
-- Within_Task_Body because only suspension calls which appear
-- immediately within the statements of the task are supported.
-- Flag Within_Task_Body carries over to deeper levels of the
-- traversal.
elsif (Debug_Flag_Underscore_S
or else Restriction_Active
(No_Entry_Calls_In_Elaboration_Code))
and then Is_Synchronous_Suspension_Call (Scen)
and then In_Task_Body (Scen)
then
return Abandon;
-- Certain nodes carry semantic lists which act as repositories
-- until expansion transforms the node and relocates the contents.
-- Examine these lists in case expansion is disabled.
elsif Nkind (Scen) in N_And_Then | N_Or_Else then
Traverse_List (Actions (Scen));
elsif Nkind (Scen) in N_Elsif_Part | N_Iteration_Scheme then
Traverse_List (Condition_Actions (Scen));
elsif Nkind (Scen) = N_If_Expression then
Traverse_List (Then_Actions (Scen));
Traverse_List (Else_Actions (Scen));
elsif Nkind (Scen) in
N_Component_Association
| N_Iterated_Component_Association
| N_Iterated_Element_Association
then
Traverse_List (Loop_Actions (Scen));
-- General case
-- The current node satisfies the input predicate, process it
elsif Requires_Processing.all (Scen) then
Processor.all (Scen, In_State);
end if;
-- Save a general scenario regardless of whether it satisfies the
-- input predicate. This allows for quick subsequent traversals of
-- general scenarios, even with different predicates.
if Is_Suitable_Access_Taken (Scen)
or else Is_Suitable_Call (Scen)
or else Is_Suitable_Instantiation (Scen)
or else Is_Suitable_Variable_Assignment (Scen)
or else Is_Suitable_Variable_Reference (Scen)
then
NE_List.Append (Scenarios, Scen);
end if;
return OK;
end Traverse_Potential_Scenario;
-- Start of processing for Traverse_Body
begin
-- Nothing to do when the traversal is suppressed
if In_State.Traversal = No_Traversal then
return;
-- Nothing to do when there is no input
elsif No (N) then
return;
-- Nothing to do when the input is not a subprogram body
elsif Nkind (N) /= N_Subprogram_Body then
return;
-- Nothing to do if the subprogram body was already traversed
elsif Is_Traversed_Body (N) then
return;
end if;
-- Mark the subprogram body as traversed
Set_Is_Traversed_Body (N);
Scenarios := Nested_Scenarios (N);
-- The subprogram body has been traversed at least once, and all
-- scenarios that appear within its declarations and statements
-- have already been collected. Directly retraverse the scenarios
-- without having to retraverse the subprogram body subtree.
if NE_List.Present (Scenarios) then
Traverse_Collected_Scenarios;
-- Otherwise the subprogram body is being traversed for the first
-- time. Collect all scenarios that appear within its declarations
-- and statements in case the subprogram body has to be retraversed
-- multiple times.
else
Scenarios := NE_List.Create;
Set_Nested_Scenarios (N, Scenarios);
Traverse_List (Declarations (N));
Traverse_Potential_Scenarios (Handled_Statement_Sequence (N));
end if;
end Traverse_Body;
end Body_Processor;
-----------------------
-- Build_Call_Marker --
-----------------------
procedure Build_Call_Marker (N : Node_Id) is
function In_External_Context
(Call : Node_Id;
Subp_Id : Entity_Id) return Boolean;
pragma Inline (In_External_Context);
-- Determine whether entry, operator, or subprogram Subp_Id is external
-- to call Call which must reside within an instance.
function In_Premature_Context (Call : Node_Id) return Boolean;
pragma Inline (In_Premature_Context);
-- Determine whether call Call appears within a premature context
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;
Subp_Id : Entity_Id) return Boolean
is
Spec_Decl : constant Entity_Id := Unit_Declaration_Node (Subp_Id);
Inst : Node_Id;
Inst_Body : Node_Id;
Inst_Spec : Node_Id;
begin
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 (Spec_Decl)
then
return True;
-- Otherwise the target declaration must not appear within the
-- instance spec or body.
else
Spec_And_Body_From_Node
(N => Inst,
Spec_Decl => Inst_Spec,
Body_Decl => Inst_Body);
return not In_Subtree
(N => Spec_Decl,
Root1 => Inst_Spec,
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 (Par) in 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_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 (Outer_Call) in N_Entry_Call_Statement
| N_Function_Call
| N_Procedure_Call_Statement
and then Comes_From_Source (Outer_Call)
then
Outer_Nam := 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 (Context) in N_Function_Specification
| N_Package_Specification
| N_Procedure_Specification
and then Present (Generic_Parent (Context));
end Is_Generic_Formal_Subp;
-- Local variables
Call_Nam : Node_Id;
Marker : Node_Id;
Subp_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 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 elaboration phase of the compiler is not
-- active.
elsif not Elaboration_Phase_Active then
return;
-- Nothing to do when the input does not denote a call or a requeue
elsif Nkind (N) not in 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 (N) in N_Entry_Call_Statement | N_Requeue_Statement
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.
elsif In_Premature_Context (N) then
return;
end if;
Call_Nam := 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;
end if;
Subp_Id := Canonical_Subprogram (Entity (Call_Nam));
-- 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.
if Debug_Flag_Dot_GG
and then Is_Generic_Formal_Subp (Entity (Call_Nam))
then
return;
-- Nothing to do when the call appears within the expanded spec or
-- body of an instantiated generic, the call does not invoke a generic
-- formal subprogram, the target is external to the instance, and switch
-- -gnatdL (ignore external calls from instances for elaboration) is in
-- effect. This 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_LL
and then not Is_Generic_Formal_Subp (Entity (Call_Nam))
and then In_External_Context
(Call => N,
Subp_Id => Subp_Id)
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 (Subp_Id)
then
return;
-- Static expression functions require no ABE processing
elsif Is_Static_Function (Subp_Id) then
return;
-- Source calls to source targets are always considered because they
-- reflect the original call graph.
elsif Comes_From_Source (N) and then Comes_From_Source (Subp_Id) then
null;
-- A call to a source function which acts as the default expression in
-- another call requires special detection.
elsif Comes_From_Source (Subp_Id)
and then Nkind (N) = N_Function_Call
and then Is_Default_Expression (N)
then
null;
-- The target emulates Ada semantics
elsif Is_Ada_Semantic_Target (Subp_Id) then
null;
-- The target acts as a link between scenarios
elsif Is_Bridge_Target (Subp_Id) then
null;
-- The target emulates SPARK semantics
elsif Is_SPARK_Semantic_Target (Subp_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_Is_Declaration_Level_Node
(Marker, Find_Enclosing_Level (N) = Declaration_Level);
Set_Is_Dispatching_Call
(Marker,
Nkind (N) in N_Subprogram_Call
and then Present (Controlling_Argument (N)));
Set_Is_Elaboration_Checks_OK_Node
(Marker, Is_Elaboration_Checks_OK_Node (N));
Set_Is_Elaboration_Warnings_OK_Node
(Marker, Is_Elaboration_Warnings_OK_Node (N));
Set_Is_Ignored_Ghost_Node (Marker, Is_Ignored_Ghost_Node (N));
Set_Is_Source_Call (Marker, Comes_From_Source (N));
Set_Is_SPARK_Mode_On_Node (Marker, Is_SPARK_Mode_On_Node (N));
Set_Target (Marker, Subp_Id);
-- Ada 2022 (AI12-0175): Calls to certain functions that are essentially
-- unchecked conversions are preelaborable.
if Ada_Version >= Ada_2022 then
Set_Is_Preelaborable_Call (Marker, Is_Preelaborable_Construct (N));
else
Set_Is_Preelaborable_Call (Marker, False);
end if;
-- 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 Ultimate_Variable (Var_Id : Entity_Id) return Entity_Id;
pragma Inline (Ultimate_Variable);
-- Obtain the ultimate renamed variable of variable Var_Id
-----------------------
-- Ultimate_Variable --
-----------------------
function Ultimate_Variable (Var_Id : Entity_Id) return Entity_Id is
pragma Assert (Ekind (Var_Id) = E_Variable);
Ren_Id : Entity_Id;
begin
Ren_Id := Var_Id;
while Present (Renamed_Object (Ren_Id))
and then Nkind (Renamed_Object (Ren_Id)) in N_Entity
loop
Ren_Id := Renamed_Object (Ren_Id);
end loop;
return Ren_Id;
end Ultimate_Variable;
-- Local variables
Var_Id : constant Entity_Id := Ultimate_Variable (Entity (N));
Marker : Node_Id;
-- Start of processing for Build_Variable_Reference_Marker
begin
-- Nothing to do when the elaboration phase of the compiler is not
-- active.
if not Elaboration_Phase_Active then
return;
end if;
Marker := Make_Variable_Reference_Marker (Sloc (N));
-- Inherit the attributes of the original variable reference
Set_Is_Elaboration_Checks_OK_Node
(Marker, Is_Elaboration_Checks_OK_Node (N));
Set_Is_Elaboration_Warnings_OK_Node
(Marker, Is_Elaboration_Warnings_OK_Node (N));
Set_Is_Read (Marker, Read);
Set_Is_SPARK_Mode_On_Node (Marker, Is_SPARK_Mode_On_Node (N));
Set_Is_Write (Marker, Write);
Set_Target (Marker, Var_Id);
-- 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;
---------------
-- Call_Name --
---------------
function 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 Call_Name;
--------------------------
-- Canonical_Subprogram --
--------------------------
function Canonical_Subprogram (Subp_Id : Entity_Id) return Entity_Id is
Canon_Id : Entity_Id;
begin
Canon_Id := Subp_Id;
-- Use the original protected subprogram when dealing with one of the
-- specialized lock-manipulating versions.
if Is_Protected_Body_Subp (Canon_Id) then
Canon_Id := Protected_Subprogram (Canon_Id);
end if;
-- Obtain the original subprogram except when the subprogram is also
-- an instantiation. In this case the alias is the internally generated
-- subprogram which appears within the anonymous package created for the
-- instantiation, making it unuitable.
if not Is_Generic_Instance (Canon_Id) then
Canon_Id := Get_Renamed_Entity (Canon_Id);
end if;
return Canon_Id;
end Canonical_Subprogram;
---------------------------------
-- Check_Elaboration_Scenarios --
---------------------------------
procedure Check_Elaboration_Scenarios is
Iter : NE_Set.Iterator;
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
Finalize_All_Data_Structures;
return;
-- Nothing to do when the elaboration phase of the compiler is not
-- active.
elsif not Elaboration_Phase_Active then
Finalize_All_Data_Structures;
return;
end if;
-- Restore the original elaboration model which was in effect when the
-- scenarios were first recorded. The model may be specified by pragma
-- Elaboration_Checks which appears on the initial declaration of the
-- main unit.
Install_Elaboration_Model (Unit_Entity (Main_Unit_Entity));
-- Examine the context of the main unit and record all units with prior
-- elaboration with respect to it.
Collect_Elaborated_Units;
-- Examine all scenarios saved during the Recording phase applying the
-- Ada or SPARK elaboration rules in order to detect and diagnose ABE
-- issues, install conditional ABE checks, and ensure the elaboration
-- of units.
Iter := Iterate_Declaration_Scenarios;
Check_Conditional_ABE_Scenarios (Iter);
Iter := Iterate_Library_Body_Scenarios;
Check_Conditional_ABE_Scenarios (Iter);
Iter := Iterate_Library_Spec_Scenarios;
Check_Conditional_ABE_Scenarios (Iter);
-- Examine each SPARK scenario saved during the Recording phase which
-- is not necessarily executable during elaboration, but still requires
-- elaboration-related checks.
Check_SPARK_Scenarios;
-- Add conditional ABE checks for all scenarios that require one when
-- the dynamic model is in effect.
Install_Dynamic_ABE_Checks;
-- Examine all scenarios saved during the Recording phase along with
-- invocation constructs within the spec and body of the main unit.
-- Record the declarations and paths that reach into an external unit
-- in the ALI file of the main unit.
Record_Invocation_Graph;
-- Destroy all internal data structures and complete the elaboration
-- phase of the compiler.
Finalize_All_Data_Structures;
Set_Elaboration_Phase (Completed);
end Check_Elaboration_Scenarios;
---------------------
-- Check_Installer --
---------------------
package body Check_Installer is
-----------------------
-- Local subprograms --
-----------------------
function ABE_Check_Or_Failure_OK
(N : Node_Id;
Targ_Id : Entity_Id;
Unit_Id : Entity_Id) return Boolean;
pragma Inline (ABE_Check_Or_Failure_OK);
-- Determine whether a conditional ABE check or guaranteed ABE failure
-- can be installed for scenario N with target Targ_Id which resides in
-- unit Unit_Id.
function Insertion_Node (N : Node_Id) return Node_Id;
pragma Inline (Insertion_Node);
-- Obtain the proper insertion node of an ABE check or failure for
-- scenario N.
procedure Insert_ABE_Check_Or_Failure (N : Node_Id; Check : Node_Id);
pragma Inline (Insert_ABE_Check_Or_Failure);
-- Insert conditional ABE check or guaranteed ABE failure Check prior to
-- scenario N.
procedure Install_Scenario_ABE_Check_Common
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id);
pragma Inline (Install_Scenario_ABE_Check_Common);
-- Install a conditional ABE check for scenario N to ensure that target
-- Targ_Id is properly elaborated. Targ_Rep is the representation of the
-- target.
procedure Install_Scenario_ABE_Failure_Common (N : Node_Id);
pragma Inline (Install_Scenario_ABE_Failure_Common);
-- Install a guaranteed ABE failure for scenario N
procedure Install_Unit_ABE_Check_Common
(N : Node_Id;
Unit_Id : Entity_Id);
pragma Inline (Install_Unit_ABE_Check_Common);
-- Install a conditional ABE check for scenario N to ensure that unit
-- Unit_Id is properly elaborated.
-----------------------------
-- ABE_Check_Or_Failure_OK --
-----------------------------
function ABE_Check_Or_Failure_OK
(N : Node_Id;
Targ_Id : Entity_Id;
Unit_Id : Entity_Id) return Boolean
is
pragma Unreferenced (Targ_Id);
Ins_Node : constant Node_Id := Insertion_Node (N);
begin
if not Check_Or_Failure_Generation_OK then
return False;
-- Nothing to do when the scenario denots a compilation unit because
-- there is no executable environment at that level.
elsif Nkind (Parent (Ins_Node)) = N_Compilation_Unit then
return False;
-- An ABE check or failure is not needed when the target is defined
-- in a unit which is elaborated prior to the main unit. This check
-- must also consider the following cases:
--
-- * The unit of the target appears in the context of the main unit
--
-- * The unit of the target is subject to pragma Elaborate_Body. An
-- ABE check MUST NOT be generated because the unit is always
-- elaborated prior to the main unit.
--
-- * The unit of the target is the main unit. An ABE check MUST be
-- added in this case because a conditional ABE may be raised
-- depending on the flow of execution within the main unit (flag
-- Same_Unit_OK is False).
elsif Has_Prior_Elaboration
(Unit_Id => Unit_Id,
Context_OK => True,
Elab_Body_OK => True)
then
return False;
end if;
return True;
end ABE_Check_Or_Failure_OK;
------------------------------------
-- Check_Or_Failure_Generation_OK --
------------------------------------
function Check_Or_Failure_Generation_OK return Boolean is
begin
-- An ABE check or failure is not needed when the compilation will
-- not produce an executable.
if Serious_Errors_Detected > 0 then
return False;
-- An ABE check or failure must not be installed when compiling for
-- GNATprove because raise statements are not supported.
elsif GNATprove_Mode then
return False;
end if;
return True;
end Check_Or_Failure_Generation_OK;
--------------------
-- Insertion_Node --
--------------------
function Insertion_Node (N : Node_Id) return Node_Id is
begin
-- When the scenario denotes an instantiation, the proper insertion
-- node is the instance spec. This ensures that the generic actuals
-- will not be evaluated prior to a potential ABE.
if Nkind (N) in N_Generic_Instantiation
and then Present (Instance_Spec (N))
then
return Instance_Spec (N);
-- Otherwise the proper insertion node is the scenario itself
else
return N;
end if;
end Insertion_Node;
---------------------------------
-- Insert_ABE_Check_Or_Failure --
---------------------------------
procedure Insert_ABE_Check_Or_Failure (N : Node_Id; Check : Node_Id) is
Ins_Nod : constant Node_Id := Insertion_Node (N);
Scop_Id : constant Entity_Id := Find_Enclosing_Scope (Ins_Nod);
begin
-- Install the nearest enclosing scope of the scenario as there must
-- be something on the scope stack.
Push_Scope (Scop_Id);
Insert_Action (Ins_Nod, Check);
Pop_Scope;
end Insert_ABE_Check_Or_Failure;
--------------------------------
-- Install_Dynamic_ABE_Checks --
--------------------------------
procedure Install_Dynamic_ABE_Checks is
Iter : NE_Set.Iterator;
N : Node_Id;
begin
if not Check_Or_Failure_Generation_OK then
return;
-- Nothing to do if the dynamic model is not in effect
elsif not Dynamic_Elaboration_Checks then
return;
end if;
-- Install a conditional ABE check for each saved scenario
Iter := Iterate_Dynamic_ABE_Check_Scenarios;
while NE_Set.Has_Next (Iter) loop
NE_Set.Next (Iter, N);
Process_Conditional_ABE
(N => N,
In_State => Dynamic_Model_State);
end loop;
end Install_Dynamic_ABE_Checks;
--------------------------------
-- Install_Scenario_ABE_Check --
--------------------------------
procedure Install_Scenario_ABE_Check
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id;
Disable : Scenario_Rep_Id)
is
begin
-- Nothing to do when the scenario does not need an ABE check
if not ABE_Check_Or_Failure_OK
(N => N,
Targ_Id => Targ_Id,
Unit_Id => Unit (Targ_Rep))
then
return;
end if;
-- Prevent multiple attempts to install the same ABE check
Disable_Elaboration_Checks (Disable);
Install_Scenario_ABE_Check_Common
(N => N,
Targ_Id => Targ_Id,
Targ_Rep => Targ_Rep);
end Install_Scenario_ABE_Check;
--------------------------------
-- Install_Scenario_ABE_Check --
--------------------------------
procedure Install_Scenario_ABE_Check
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id;
Disable : Target_Rep_Id)
is
begin
-- Nothing to do when the scenario does not need an ABE check
if not ABE_Check_Or_Failure_OK
(N => N,
Targ_Id => Targ_Id,
Unit_Id => Unit (Targ_Rep))
then
return;
end if;
-- Prevent multiple attempts to install the same ABE check
Disable_Elaboration_Checks (Disable);
Install_Scenario_ABE_Check_Common
(N => N,
Targ_Id => Targ_Id,
Targ_Rep => Targ_Rep);
end Install_Scenario_ABE_Check;
---------------------------------------
-- Install_Scenario_ABE_Check_Common --
---------------------------------------
procedure Install_Scenario_ABE_Check_Common
(N : Node_Id;
Targ_Id : Entity_Id;
Targ_Rep : Target_Rep_Id)
is
Targ_Body : constant Node_Id := Body_Declaration (Targ_Rep);
Targ_Decl : constant Node_Id := Spec_Declaration (Targ_Rep);
pragma Assert (Present (Targ_Body));
pragma Assert (Present (Targ_Decl));
procedure Build_Elaboration_Entity;
pragma Inline (Build_Elaboration_Entity);
-- Create a new elaboration flag for Targ_Id, insert it prior to
-- Targ_Decl, and set it after Targ_Body.
------------------------------
-- Build_Elaboration_Entity --
------------------------------
procedure Build_Elaboration_Entity is