Google Git
Sign in
gnu / gcc / refs/tags/basepoints/gcc-13 / . / gcc / ada / sem_prag.adb
blob: f9169eeedd7de415e11ec6cc71035d6e64332241 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ P R A G --
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-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. --
-- --
------------------------------------------------------------------------------
-- This unit contains the semantic processing for all pragmas, both language
-- and implementation defined. For most pragmas, the parser only does the
-- most basic job of checking the syntax, so Sem_Prag also contains the code
-- to complete the syntax checks. Certain pragmas are handled partially or
-- completely by the parser (see Par.Prag for further details).
with Aspects; use Aspects;
with Atree; use Atree;
with Casing; use Casing;
with Checks; use Checks;
with Contracts; use Contracts;
with Csets; use Csets;
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_Dist; use Exp_Dist;
with Exp_Util; use Exp_Util;
with Expander; use Expander;
with Freeze; use Freeze;
with Ghost; use Ghost;
with GNAT_CUDA; use GNAT_CUDA;
with Gnatvsn; use Gnatvsn;
with Lib; use Lib;
with Lib.Writ; use Lib.Writ;
with Lib.Xref; use Lib.Xref;
with Namet.Sp; use Namet.Sp;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Output; use Output;
with Par_SCO; use Par_SCO;
with Restrict; use Restrict;
with Rident; use Rident;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Ch3; use Sem_Ch3;
with Sem_Ch6; use Sem_Ch6;
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch12; use Sem_Ch12;
with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Dist; use Sem_Dist;
with Sem_Elab; use Sem_Elab;
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
with Sem_Intr; use Sem_Intr;
with Sem_Mech; use Sem_Mech;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
with Sem_Warn; use Sem_Warn;
with Stand; use Stand;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
with Sinfo.CN; use Sinfo.CN;
with Sinput; use Sinput;
with Stringt; use Stringt;
with Strub; use Strub;
with Stylesw; use Stylesw;
with Table;
with Targparm; use Targparm;
with Tbuild; use Tbuild;
with Ttypes;
with Uintp; use Uintp;
with Uname; use Uname;
with Urealp; use Urealp;
with Validsw; use Validsw;
with Warnsw; use Warnsw;
with System.Case_Util;
package body Sem_Prag is
----------------------------------------------
-- Common Handling of Import-Export Pragmas --
----------------------------------------------
-- In the following section, a number of Import_xxx and Export_xxx pragmas
-- are defined by GNAT. These are compatible with the DEC pragmas of the
-- same name, and all have the following common form and processing:
-- pragma Export_xxx
-- [Internal =>] LOCAL_NAME
-- [, [External =>] EXTERNAL_SYMBOL]
-- [, other optional parameters ]);
-- pragma Import_xxx
-- [Internal =>] LOCAL_NAME
-- [, [External =>] EXTERNAL_SYMBOL]
-- [, other optional parameters ]);
-- EXTERNAL_SYMBOL ::=
-- IDENTIFIER
-- | static_string_EXPRESSION
-- The internal LOCAL_NAME designates the entity that is imported or
-- exported, and must refer to an entity in the current declarative
-- part (as required by the rules for LOCAL_NAME).
-- The external linker name is designated by the External parameter if
-- given, or the Internal parameter if not (if there is no External
-- parameter, the External parameter is a copy of the Internal name).
-- If the External parameter is given as a string, then this string is
-- treated as an external name (exactly as though it had been given as an
-- External_Name parameter for a normal Import pragma).
-- If the External parameter is given as an identifier (or there is no
-- External parameter, so that the Internal identifier is used), then
-- the external name is the characters of the identifier, translated
-- to all lower case letters.
-- Note: the external name specified or implied by any of these special
-- Import_xxx or Export_xxx pragmas override an external or link name
-- specified in a previous Import or Export pragma.
-- Note: these and all other DEC-compatible GNAT pragmas allow full use of
-- named notation, following the standard rules for subprogram calls, i.e.
-- parameters can be given in any order if named notation is used, and
-- positional and named notation can be mixed, subject to the rule that all
-- positional parameters must appear first.
-- Note: All these pragmas are implemented exactly following the DEC design
-- and implementation and are intended to be fully compatible with the use
-- of these pragmas in the DEC Ada compiler.
--------------------------------------------
-- Checking for Duplicated External Names --
--------------------------------------------
-- It is suspicious if two separate Export pragmas use the same external
-- name. The following table is used to diagnose this situation so that
-- an appropriate warning can be issued.
-- The Node_Id stored is for the N_String_Literal node created to hold
-- the value of the external name. The Sloc of this node is used to
-- cross-reference the location of the duplication.
package Externals is new Table.Table (
Table_Component_Type => Node_Id,
Table_Index_Type => Int,
Table_Low_Bound => 0,
Table_Initial => 100,
Table_Increment => 100,
Table_Name => "Name_Externals");
-------------------------------------
-- Local Subprograms and Variables --
-------------------------------------
function Adjust_External_Name_Case (N : Node_Id) return Node_Id;
-- This routine is used for possible casing adjustment of an explicit
-- external name supplied as a string literal (the node N), according to
-- the casing requirement of Opt.External_Name_Casing. If this is set to
-- As_Is, then the string literal is returned unchanged, but if it is set
-- to Uppercase or Lowercase, then a new string literal with appropriate
-- casing is constructed.
procedure Analyze_Part_Of
(Indic : Node_Id;
Item_Id : Entity_Id;
Encap : Node_Id;
Encap_Id : out Entity_Id;
Legal : out Boolean);
-- Subsidiary to Analyze_Part_Of_In_Decl_Part, Analyze_Part_Of_Option and
-- Analyze_Pragma. Perform full analysis of indicator Part_Of. Indic is the
-- Part_Of indicator. Item_Id is the entity of an abstract state, object or
-- package instantiation. Encap denotes the encapsulating state or single
-- concurrent type. Encap_Id is the entity of Encap. Flag Legal is set when
-- the indicator is legal.
function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean;
-- Subsidiary to analysis of pragmas Depends, Global and Refined_Depends.
-- Query whether a particular item appears in a mixed list of nodes and
-- entities. It is assumed that all nodes in the list have entities.
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Spec_Id : Entity_Id);
-- Subsidiary to the analysis of pragmas Contract_Cases, Postcondition,
-- Precondition, Refined_Post, and Test_Case. Emit a warning when pragma
-- Prag is associated with subprogram Spec_Id subject to Inline_Always,
-- and assertions are enabled.
procedure Check_State_And_Constituent_Use
(States : Elist_Id;
Constits : Elist_Id;
Context : Node_Id);
-- Subsidiary to the analysis of pragmas [Refined_]Depends, [Refined_]
-- Global and Initializes. Determine whether a state from list States and a
-- corresponding constituent from list Constits (if any) appear in the same
-- context denoted by Context. If this is the case, emit an error.
procedure Contract_Freeze_Error
(Contract_Id : Entity_Id;
Freeze_Id : Entity_Id);
-- Subsidiary to the analysis of pragmas Contract_Cases, Part_Of, Post, and
-- Pre. Emit a freezing-related error message where Freeze_Id is the entity
-- of a body which caused contract freezing and Contract_Id denotes the
-- entity of the affected contstruct.
procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id);
-- Subsidiary to all Find_Related_xxx routines. Emit an error on pragma
-- Prag that duplicates previous pragma Prev.
function Find_Encapsulating_State
(States : Elist_Id;
Constit_Id : Entity_Id) return Entity_Id;
-- Given the entity of a constituent Constit_Id, find the corresponding
-- encapsulating state which appears in States. The routine returns Empty
-- if no such state is found.
function Find_Related_Context
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas
-- Async_Readers
-- Async_Writers
-- Constant_After_Elaboration
-- Effective_Reads
-- Effective_Writers
-- No_Caching
-- Part_Of
-- Find the first source declaration or statement found while traversing
-- the previous node chain starting from pragma Prag. If flag Do_Checks is
-- set, the routine reports duplicate pragmas. The routine returns Empty
-- when reaching the start of the node chain.
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
-- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
-- Get_SPARK_Mode_From_Annotation. Convert a name into a corresponding
-- value of type SPARK_Mode_Type.
function Has_Extra_Parentheses (Clause : Node_Id) return Boolean;
-- Subsidiary to the analysis of pragmas Depends and Refined_Depends.
-- Determine whether dependency clause Clause is surrounded by extra
-- parentheses. If this is the case, issue an error message.
function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean;
-- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of
-- pragma Depends. Determine whether the type of dependency item Item is
-- tagged, unconstrained array, unconstrained record or a record with at
-- least one unconstrained component.
procedure Record_Possible_Body_Reference
(State_Id : Entity_Id;
Ref : Node_Id);
-- Subsidiary to the analysis of pragmas [Refined_]Depends and [Refined_]
-- Global. Given an abstract state denoted by State_Id and a reference Ref
-- to it, determine whether the reference appears in a package body that
-- will eventually refine the state. If this is the case, record the
-- reference for future checks (see Analyze_Refined_State_In_Decls).
procedure Resolve_State (N : Node_Id);
-- Handle the overloading of state names by functions. When N denotes a
-- function, this routine finds the corresponding state and sets the entity
-- of N to that of the state.
procedure Rewrite_Assertion_Kind
(N : Node_Id;
From_Policy : Boolean := False);
-- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
-- then it is rewritten as an identifier with the corresponding special
-- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas Check
-- and Check_Policy. If the names are Precondition or Postcondition, this
-- combination is deprecated in favor of Assertion_Policy and Ada2012
-- Aspect names. The parameter From_Policy indicates that the pragma
-- is the old non-standard Check_Policy and not a rewritten pragma.
procedure Set_Elab_Unit_Name (N : Node_Id; With_Item : Node_Id);
-- Place semantic information on the argument of an Elaborate/Elaborate_All
-- pragma. Entity name for unit and its parents is taken from item in
-- previous with_clause that mentions the unit.
procedure Validate_Compile_Time_Warning_Or_Error
(N : Node_Id;
Eloc : Source_Ptr);
-- Common processing for Compile_Time_Error and Compile_Time_Warning of
-- pragma N. Called when the pragma is processed as part of its regular
-- analysis but also called after calling the back end to validate these
-- pragmas for size and alignment appropriateness.
procedure Defer_Compile_Time_Warning_Error_To_BE (N : Node_Id);
-- N is a pragma Compile_Time_Error or Compile_Warning_Error whose boolean
-- expression is not known at compile time during the front end. This
-- procedure makes an entry in a table. The actual checking is performed by
-- Validate_Compile_Time_Warning_Errors, which is invoked after calling the
-- back end.
Dummy : Integer := 0;
pragma Volatile (Dummy);
-- Dummy volatile integer used in bodies of ip/rv to prevent optimization
procedure ip;
pragma No_Inline (ip);
-- A dummy procedure called when pragma Inspection_Point is analyzed. This
-- is just to help debugging the front end. If a pragma Inspection_Point
-- is added to a source program, then breaking on ip will get you to that
-- point in the program.
procedure rv;
pragma No_Inline (rv);
-- This is a dummy function called by the processing for pragma Reviewable.
-- It is there for assisting front end debugging. By placing a Reviewable
-- pragma in the source program, a breakpoint on rv catches this place in
-- the source, allowing convenient stepping to the point of interest.
------------------------------------------------------
-- Table for Defer_Compile_Time_Warning_Error_To_BE --
------------------------------------------------------
-- The following table collects pragmas Compile_Time_Error and Compile_
-- Time_Warning for validation. Entries are made by calls to subprogram
-- Defer_Compile_Time_Warning_Error_To_BE, and the call to the procedure
-- Validate_Compile_Time_Warning_Errors does the actual error checking
-- and posting of warning and error messages. The reason for this delayed
-- processing is to take advantage of back-annotations of attributes size
-- and alignment values performed by the back end.
-- Note: the reason we store a Source_Ptr value instead of a Node_Id is
-- that by the time Validate_Compile_Time_Warning_Errors is called, Sprint
-- will already have modified all Sloc values if the -gnatD option is set.
type CTWE_Entry is record
Eloc : Source_Ptr;
-- Source location used in warnings and error messages
Prag : Node_Id;
-- Pragma Compile_Time_Error or Compile_Time_Warning
Scope : Node_Id;
-- The scope which encloses the pragma
end record;
package Compile_Time_Warnings_Errors is new Table.Table (
Table_Component_Type => CTWE_Entry,
Table_Index_Type => Int,
Table_Low_Bound => 1,
Table_Initial => 50,
Table_Increment => 200,
Table_Name => "Compile_Time_Warnings_Errors");
-------------------------------
-- Adjust_External_Name_Case --
-------------------------------
function Adjust_External_Name_Case (N : Node_Id) return Node_Id is
CC : Char_Code;
begin
-- Adjust case of literal if required
if Opt.External_Name_Exp_Casing = As_Is then
return N;
else
-- Copy existing string
Start_String;
-- Set proper casing
for J in 1 .. String_Length (Strval (N)) loop
CC := Get_String_Char (Strval (N), J);
if Opt.External_Name_Exp_Casing = Uppercase
and then CC in Get_Char_Code ('a') .. Get_Char_Code ('z')
then
Store_String_Char (CC - 32);
elsif Opt.External_Name_Exp_Casing = Lowercase
and then CC in Get_Char_Code ('A') .. Get_Char_Code ('Z')
then
Store_String_Char (CC + 32);
else
Store_String_Char (CC);
end if;
end loop;
return
Make_String_Literal (Sloc (N),
Strval => End_String);
end if;
end Adjust_External_Name_Case;
-----------------------------------------
-- Analyze_Contract_Cases_In_Decl_Part --
-----------------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Analyze_Contract_Cases_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty)
is
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Others_Seen : Boolean := False;
-- This flag is set when an "others" choice is encountered. It is used
-- to detect multiple illegal occurrences of "others".
procedure Analyze_Contract_Case (CCase : Node_Id);
-- Verify the legality of a single contract case
---------------------------
-- Analyze_Contract_Case --
---------------------------
procedure Analyze_Contract_Case (CCase : Node_Id) is
Case_Guard : Node_Id;
Conseq : Node_Id;
Errors : Nat;
Extra_Guard : Node_Id;
begin
if Nkind (CCase) = N_Component_Association then
Case_Guard := First (Choices (CCase));
Conseq := Expression (CCase);
-- Each contract case must have exactly one case guard
Extra_Guard := Next (Case_Guard);
if Present (Extra_Guard) then
Error_Msg_N
("contract case must have exactly one case guard",
Extra_Guard);
end if;
-- Check placement of OTHERS if available (SPARK RM 6.1.3(1))
if Nkind (Case_Guard) = N_Others_Choice then
if Others_Seen then
Error_Msg_N
("only one OTHERS choice allowed in contract cases",
Case_Guard);
else
Others_Seen := True;
end if;
elsif Others_Seen then
Error_Msg_N
("OTHERS must be the last choice in contract cases", N);
end if;
-- Preanalyze the case guard and consequence
if Nkind (Case_Guard) /= N_Others_Choice then
Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
-- Emit a clarification message when the case guard contains
-- at least one undefined reference, possibly due to contract
-- freezing.
if Errors /= Serious_Errors_Detected
and then Present (Freeze_Id)
and then Has_Undefined_Reference (Case_Guard)
then
Contract_Freeze_Error (Spec_Id, Freeze_Id);
end if;
end if;
Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
-- Emit a clarification message when the consequence contains
-- at least one undefined reference, possibly due to contract
-- freezing.
if Errors /= Serious_Errors_Detected
and then Present (Freeze_Id)
and then Has_Undefined_Reference (Conseq)
then
Contract_Freeze_Error (Spec_Id, Freeze_Id);
end if;
-- The contract case is malformed
else
Error_Msg_N ("wrong syntax in contract case", CCase);
end if;
end Analyze_Contract_Case;
-- Local variables
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
-- Save the Ghost-related attributes to restore on exit
CCase : Node_Id;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
begin
-- Do not analyze the pragma multiple times
if Is_Analyzed_Pragma (N) then
return;
end if;
-- Set the Ghost mode in effect from the pragma. Due to the delayed
-- analysis of the pragma, the Ghost mode at point of declaration and
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
Set_Ghost_Mode (N);
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser or the analysis of the
-- pragma failed to produce an aggregate, e.g. when the contract is
-- "null" or a "(null record)".
pragma Assert
(if Nkind (CCases) = N_Aggregate
then Null_Record_Present (CCases)
xor (Present (Component_Associations (CCases))
or
Present (Expressions (CCases)))
else Nkind (CCases) = N_Null);
-- Only CASE_GUARD => CONSEQUENCE clauses are allowed
if Nkind (CCases) = N_Aggregate
and then Present (Component_Associations (CCases))
and then No (Expressions (CCases))
then
-- Check that the expression is a proper aggregate (no parentheses)
if Paren_Count (CCases) /= 0 then
Error_Msg_F -- CODEFIX
("redundant parentheses", CCases);
end if;
-- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining
-- to subprogram declarations.
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
if Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
else
Install_Formals (Spec_Id);
end if;
end if;
CCase := First (Component_Associations (CCases));
while Present (CCase) loop
Analyze_Contract_Case (CCase);
Next (CCase);
end loop;
if Restore_Scope then
End_Scope;
end if;
-- Currently it is not possible to inline pre/postconditions on a
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-- Otherwise the pragma is illegal
else
Error_Msg_N ("wrong syntax for contract cases", N);
end if;
Set_Is_Analyzed_Pragma (N);
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
-- Analyze_Depends_In_Decl_Part --
----------------------------------
procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
All_Inputs_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the inputs processed so far.
-- The list is populated with unique entities because the same input
-- may appear in multiple input lists.
All_Outputs_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the outputs processed so far.
-- The list is populated with unique entities because output items are
-- unique in a dependence relation.
Constits_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all constituents processed so far.
-- It aids in detecting illegal usage of a state and a corresponding
-- constituent in pragma [Refinde_]Depends.
Global_Seen : Boolean := False;
-- A flag set when pragma Global has been processed
Null_Output_Seen : Boolean := False;
-- A flag used to track the legality of a null output
Result_Seen : Boolean := False;
-- A flag set when Spec_Id'Result is processed
States_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all states processed so far. It
-- helps in detecting illegal usage of a state and a corresponding
-- constituent in pragma [Refined_]Depends.
Subp_Inputs : Elist_Id := No_Elist;
Subp_Outputs : Elist_Id := No_Elist;
-- Two lists containing the full set of inputs and output of the related
-- subprograms. Note that these lists contain both nodes and entities.
Task_Input_Seen : Boolean := False;
Task_Output_Seen : Boolean := False;
-- Flags used to track the implicit dependence of a task unit on itself
procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id);
-- Subsidiary routine to Check_Role and Check_Usage. Add the item kind
-- to the name buffer. The individual kinds are as follows:
-- E_Abstract_State - "state"
-- E_Constant - "constant"
-- E_Generic_In_Out_Parameter - "generic parameter"
-- E_Generic_In_Parameter - "generic parameter"
-- E_In_Parameter - "parameter"
-- E_In_Out_Parameter - "parameter"
-- E_Loop_Parameter - "loop parameter"
-- E_Out_Parameter - "parameter"
-- E_Protected_Type - "current instance of protected type"
-- E_Task_Type - "current instance of task type"
-- E_Variable - "global"
procedure Analyze_Dependency_Clause
(Clause : Node_Id;
Is_Last : Boolean);
-- Verify the legality of a single dependency clause. Flag Is_Last
-- denotes whether Clause is the last clause in the relation.
procedure Check_Function_Return;
-- Verify that Funtion'Result appears as one of the outputs
-- (SPARK RM 6.1.5(10)).
procedure Check_Role
(Item : Node_Id;
Item_Id : Entity_Id;
Is_Input : Boolean;
Self_Ref : Boolean);
-- Ensure that an item fulfills its designated input and/or output role
-- as specified by pragma Global (if any) or the enclosing context. If
-- this is not the case, emit an error. Item and Item_Id denote the
-- attributes of an item. Flag Is_Input should be set when item comes
-- from an input list. Flag Self_Ref should be set when the item is an
-- output and the dependency clause has operator "+".
procedure Check_Usage
(Subp_Items : Elist_Id;
Used_Items : Elist_Id;
Is_Input : Boolean);
-- Verify that all items from Subp_Items appear in Used_Items. Emit an
-- error if this is not the case.
procedure Normalize_Clause (Clause : Node_Id);
-- Remove a self-dependency "+" from the input list of a clause
-----------------------------
-- Add_Item_To_Name_Buffer --
-----------------------------
procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id) is
begin
if Ekind (Item_Id) = E_Abstract_State then
Add_Str_To_Name_Buffer ("state");
elsif Ekind (Item_Id) = E_Constant then
Add_Str_To_Name_Buffer ("constant");
elsif Is_Formal_Object (Item_Id) then
Add_Str_To_Name_Buffer ("generic parameter");
elsif Is_Formal (Item_Id) then
Add_Str_To_Name_Buffer ("parameter");
elsif Ekind (Item_Id) = E_Loop_Parameter then
Add_Str_To_Name_Buffer ("loop parameter");
elsif Ekind (Item_Id) = E_Protected_Type
or else Is_Single_Protected_Object (Item_Id)
then
Add_Str_To_Name_Buffer ("current instance of protected type");
elsif Ekind (Item_Id) = E_Task_Type
or else Is_Single_Task_Object (Item_Id)
then
Add_Str_To_Name_Buffer ("current instance of task type");
elsif Ekind (Item_Id) = E_Variable then
Add_Str_To_Name_Buffer ("global");
-- The routine should not be called with non-SPARK items
else
raise Program_Error;
end if;
end Add_Item_To_Name_Buffer;
-------------------------------
-- Analyze_Dependency_Clause --
-------------------------------
procedure Analyze_Dependency_Clause
(Clause : Node_Id;
Is_Last : Boolean)
is
procedure Analyze_Input_List (Inputs : Node_Id);
-- Verify the legality of a single input list
procedure Analyze_Input_Output
(Item : Node_Id;
Is_Input : Boolean;
Self_Ref : Boolean;
Top_Level : Boolean;
Seen : in out Elist_Id;
Null_Seen : in out Boolean;
Non_Null_Seen : in out Boolean);
-- Verify the legality of a single input or output item. Flag
-- Is_Input should be set whenever Item is an input, False when it
-- denotes an output. Flag Self_Ref should be set when the item is an
-- output and the dependency clause has a "+". Flag Top_Level should
-- be set whenever Item appears immediately within an input or output
-- list. Seen is a collection of all abstract states, objects and
-- formals processed so far. Flag Null_Seen denotes whether a null
-- input or output has been encountered. Flag Non_Null_Seen denotes
-- whether a non-null input or output has been encountered.
------------------------
-- Analyze_Input_List --
------------------------
procedure Analyze_Input_List (Inputs : Node_Id) is
Inputs_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all inputs that appear in the
-- current input list.
Non_Null_Input_Seen : Boolean := False;
Null_Input_Seen : Boolean := False;
-- Flags used to check the legality of an input list
Input : Node_Id;
begin
-- Multiple inputs appear as an aggregate
if Nkind (Inputs) = N_Aggregate then
if Present (Component_Associations (Inputs)) then
SPARK_Msg_N
("nested dependency relations not allowed", Inputs);
elsif Present (Expressions (Inputs)) then
Input := First (Expressions (Inputs));
while Present (Input) loop
Analyze_Input_Output
(Item => Input,
Is_Input => True,
Self_Ref => False,
Top_Level => False,
Seen => Inputs_Seen,
Null_Seen => Null_Input_Seen,
Non_Null_Seen => Non_Null_Input_Seen);
Next (Input);
end loop;
-- Syntax error, always report
else
Error_Msg_N ("malformed input dependency list", Inputs);
end if;
-- Process a solitary input
else
Analyze_Input_Output
(Item => Inputs,
Is_Input => True,
Self_Ref => False,
Top_Level => False,
Seen => Inputs_Seen,
Null_Seen => Null_Input_Seen,
Non_Null_Seen => Non_Null_Input_Seen);
end if;
-- Detect an illegal dependency clause of the form
-- (null =>[+] null)
if Null_Output_Seen and then Null_Input_Seen then
SPARK_Msg_N
("null dependency clause cannot have a null input list",
Inputs);
end if;
end Analyze_Input_List;
--------------------------
-- Analyze_Input_Output --
--------------------------
procedure Analyze_Input_Output
(Item : Node_Id;
Is_Input : Boolean;
Self_Ref : Boolean;
Top_Level : Boolean;
Seen : in out Elist_Id;
Null_Seen : in out Boolean;
Non_Null_Seen : in out Boolean)
is
procedure Current_Task_Instance_Seen;
-- Set the appropriate global flag when the current instance of a
-- task unit is encountered.
--------------------------------
-- Current_Task_Instance_Seen --
--------------------------------
procedure Current_Task_Instance_Seen is
begin
if Is_Input then
Task_Input_Seen := True;
else
Task_Output_Seen := True;
end if;
end Current_Task_Instance_Seen;
-- Local variables
Is_Output : constant Boolean := not Is_Input;
Grouped : Node_Id;
Item_Id : Entity_Id;
-- Start of processing for Analyze_Input_Output
begin
-- Multiple input or output items appear as an aggregate
if Nkind (Item) = N_Aggregate then
if not Top_Level then
SPARK_Msg_N ("nested grouping of items not allowed", Item);
elsif Present (Component_Associations (Item)) then
SPARK_Msg_N
("nested dependency relations not allowed", Item);
-- Recursively analyze the grouped items
elsif Present (Expressions (Item)) then
Grouped := First (Expressions (Item));
while Present (Grouped) loop
Analyze_Input_Output
(Item => Grouped,
Is_Input => Is_Input,
Self_Ref => Self_Ref,
Top_Level => False,
Seen => Seen,
Null_Seen => Null_Seen,
Non_Null_Seen => Non_Null_Seen);
Next (Grouped);
end loop;
-- Syntax error, always report
else
Error_Msg_N ("malformed dependency list", Item);
end if;
-- Process attribute 'Result in the context of a dependency clause
elsif Is_Attribute_Result (Item) then
Non_Null_Seen := True;
Analyze (Item);
-- Attribute 'Result is allowed to appear on the output side of
-- a dependency clause (SPARK RM 6.1.5(6)).
if Is_Input then
SPARK_Msg_N ("function result cannot act as input", Item);
elsif Null_Seen then
SPARK_Msg_N
("cannot mix null and non-null dependency items", Item);
else
Result_Seen := True;
end if;
-- Detect multiple uses of null in a single dependency list or
-- throughout the whole relation. Verify the placement of a null
-- output list relative to the other clauses (SPARK RM 6.1.5(12)).
elsif Nkind (Item) = N_Null then
if Null_Seen then
SPARK_Msg_N
("multiple null dependency relations not allowed", Item);
elsif Non_Null_Seen then
SPARK_Msg_N
("cannot mix null and non-null dependency items", Item);
else
Null_Seen := True;
if Is_Output then
if not Is_Last then
SPARK_Msg_N
("null output list must be the last clause in a "
& "dependency relation", Item);
-- Catch a useless dependence of the form:
-- null =>+ ...
elsif Self_Ref then
SPARK_Msg_N
("useless dependence, null depends on itself", Item);
end if;
end if;
end if;
-- Default case
else
Non_Null_Seen := True;
if Null_Seen then
SPARK_Msg_N ("cannot mix null and non-null items", Item);
end if;
Analyze (Item);
Resolve_State (Item);
-- Find the entity of the item. If this is a renaming, climb
-- the renaming chain to reach the root object. Renamings of
-- non-entire objects do not yield an entity (Empty).
Item_Id := Entity_Of (Item);
if Present (Item_Id) then
-- Constants
if Ekind (Item_Id) in E_Constant | E_Loop_Parameter
or else
-- Current instances of concurrent types
Ekind (Item_Id) in E_Protected_Type | E_Task_Type
or else
-- Formal parameters
Ekind (Item_Id) in E_Generic_In_Out_Parameter
| E_Generic_In_Parameter
| E_In_Parameter
| E_In_Out_Parameter
| E_Out_Parameter
or else
-- States, variables
Ekind (Item_Id) in E_Abstract_State | E_Variable
then
-- A [generic] function is not allowed to have Output
-- items in its dependency relations. Note that "null"
-- and attribute 'Result are still valid items.
if Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Is_Input
then
SPARK_Msg_N
("output item is not applicable to function", Item);
end if;
-- The item denotes a concurrent type. Note that single
-- protected/task types are not considered here because
-- they behave as objects in the context of pragma
-- [Refined_]Depends.
if Ekind (Item_Id) in E_Protected_Type | E_Task_Type then
-- This use is legal as long as the concurrent type is
-- the current instance of an enclosing type.
if Is_CCT_Instance (Item_Id, Spec_Id) then
-- The dependence of a task unit on itself is
-- implicit and may or may not be explicitly
-- specified (SPARK RM 6.1.4).
if Ekind (Item_Id) = E_Task_Type then
Current_Task_Instance_Seen;
end if;
-- Otherwise this is not the current instance
else
SPARK_Msg_N
("invalid use of subtype mark in dependency "
& "relation", Item);
end if;
-- The dependency of a task unit on itself is implicit
-- and may or may not be explicitly specified
-- (SPARK RM 6.1.4).
elsif Is_Single_Task_Object (Item_Id)
and then Is_CCT_Instance (Etype (Item_Id), Spec_Id)
then
Current_Task_Instance_Seen;
end if;
-- Ensure that the item fulfills its role as input and/or
-- output as specified by pragma Global or the enclosing
-- context.
Check_Role (Item, Item_Id, Is_Input, Self_Ref);
-- Detect multiple uses of the same state, variable or
-- formal parameter. If this is not the case, add the
-- item to the list of processed relations.
if Contains (Seen, Item_Id) then
SPARK_Msg_NE
("duplicate use of item &", Item, Item_Id);
else
Append_New_Elmt (Item_Id, Seen);
end if;
-- Detect illegal use of an input related to a null
-- output. Such input items cannot appear in other
-- input lists (SPARK RM 6.1.5(13)).
if Is_Input
and then Null_Output_Seen
and then Contains (All_Inputs_Seen, Item_Id)
then
SPARK_Msg_N
("input of a null output list cannot appear in "
& "multiple input lists", Item);
end if;
-- Add an input or a self-referential output to the list
-- of all processed inputs.
if Is_Input or else Self_Ref then
Append_New_Elmt (Item_Id, All_Inputs_Seen);
end if;
-- State related checks (SPARK RM 6.1.5(3))
if Ekind (Item_Id) = E_Abstract_State then
-- Package and subprogram bodies are instantiated
-- individually in a separate compiler pass. Due to
-- this mode of instantiation, the refinement of a
-- state may no longer be visible when a subprogram
-- body contract is instantiated. Since the generic
-- template is legal, do not perform this check in
-- the instance to circumvent this oddity.
if In_Instance then
null;
-- An abstract state with visible refinement cannot
-- appear in pragma [Refined_]Depends as its place
-- must be taken by some of its constituents
-- (SPARK RM 6.1.4(7)).
elsif Has_Visible_Refinement (Item_Id) then
SPARK_Msg_NE
("cannot mention state & in dependence relation",
Item, Item_Id);
SPARK_Msg_N ("\use its constituents instead", Item);
return;
-- If the reference to the abstract state appears in
-- an enclosing package body that will eventually
-- refine the state, record the reference for future
-- checks.
else
Record_Possible_Body_Reference
(State_Id => Item_Id,
Ref => Item);
end if;
elsif Ekind (Item_Id) in E_Constant | E_Variable
and then Present (Ultimate_Overlaid_Entity (Item_Id))
then
SPARK_Msg_NE
("overlaying object & cannot appear in Depends",
Item, Item_Id);
SPARK_Msg_NE
("\use the overlaid object & instead",
Item, Ultimate_Overlaid_Entity (Item_Id));
return;
end if;
-- When the item renames an entire object, replace the
-- item with a reference to the object.
if Entity (Item) /= Item_Id then
Rewrite (Item,
New_Occurrence_Of (Item_Id, Sloc (Item)));
Analyze (Item);
end if;
-- Add the entity of the current item to the list of
-- processed items.
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
-- The variable may eventually become a constituent of a
-- single protected/task type. Record the reference now
-- and verify its legality when analyzing the contract of
-- the variable (SPARK RM 9.3).
elsif Ekind (Item_Id) = E_Variable then
Record_Possible_Part_Of_Reference
(Var_Id => Item_Id,
Ref => Item);
end if;
if Ekind (Item_Id) in E_Abstract_State
| E_Constant
| E_Variable
and then Present (Encapsulating_State (Item_Id))
then
Append_New_Elmt (Item_Id, Constits_Seen);
end if;
-- All other input/output items are illegal
-- (SPARK RM 6.1.5(1)).
else
SPARK_Msg_N
("item must denote parameter, variable, state or "
& "current instance of concurrent type", Item);
end if;
-- All other input/output items are illegal
-- (SPARK RM 6.1.5(1)). This is a syntax error, always report.
else
Error_Msg_N
("item must denote parameter, variable, state or current "
& "instance of concurrent type", Item);
end if;
end if;
end Analyze_Input_Output;
-- Local variables
Inputs : Node_Id;
Output : Node_Id;
Self_Ref : Boolean;
Non_Null_Output_Seen : Boolean := False;
-- Flag used to check the legality of an output list
-- Start of processing for Analyze_Dependency_Clause
begin
Inputs := Expression (Clause);
Self_Ref := False;
-- An input list with a self-dependency appears as operator "+" where
-- the actuals inputs are the right operand.
if Nkind (Inputs) = N_Op_Plus then
Inputs := Right_Opnd (Inputs);
Self_Ref := True;
end if;
-- Process the output_list of a dependency_clause
Output := First (Choices (Clause));
while Present (Output) loop
Analyze_Input_Output
(Item => Output,
Is_Input => False,
Self_Ref => Self_Ref,
Top_Level => True,
Seen => All_Outputs_Seen,
Null_Seen => Null_Output_Seen,
Non_Null_Seen => Non_Null_Output_Seen);
Next (Output);
end loop;
-- Process the input_list of a dependency_clause
Analyze_Input_List (Inputs);
end Analyze_Dependency_Clause;
---------------------------
-- Check_Function_Return --
---------------------------
procedure Check_Function_Return is
begin
if Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Result_Seen
then
SPARK_Msg_NE
("result of & must appear in exactly one output list",
N, Spec_Id);
end if;
end Check_Function_Return;
----------------
-- Check_Role --
----------------
procedure Check_Role
(Item : Node_Id;
Item_Id : Entity_Id;
Is_Input : Boolean;
Self_Ref : Boolean)
is
procedure Find_Role
(Item_Is_Input : out Boolean;
Item_Is_Output : out Boolean);
-- Find the input/output role of Item_Id. Flags Item_Is_Input and
-- Item_Is_Output are set depending on the role.
procedure Role_Error
(Item_Is_Input : Boolean;
Item_Is_Output : Boolean);
-- Emit an error message concerning the incorrect use of Item in
-- pragma [Refined_]Depends. Flags Item_Is_Input and Item_Is_Output
-- denote whether the item is an input and/or an output.
---------------
-- Find_Role --
---------------
procedure Find_Role
(Item_Is_Input : out Boolean;
Item_Is_Output : out Boolean)
is
-- A constant or an IN parameter of a procedure or a protected
-- entry, if it is of an access-to-variable type, should be
-- handled like a variable, as the underlying memory pointed-to
-- can be modified. Use Adjusted_Kind to do this adjustment.
Adjusted_Kind : Entity_Kind := Ekind (Item_Id);
begin
if (Ekind (Item_Id) in E_Constant | E_Generic_In_Parameter
or else
(Ekind (Item_Id) = E_In_Parameter
and then Ekind (Scope (Item_Id))
not in E_Function | E_Generic_Function))
and then Is_Access_Variable (Etype (Item_Id))
and then Ekind (Spec_Id) not in E_Function
| E_Generic_Function
then
Adjusted_Kind := E_Variable;
end if;
case Adjusted_Kind is
-- Abstract states
when E_Abstract_State =>
-- When pragma Global is present it determines the mode of
-- the abstract state.
if Global_Seen then
Item_Is_Input := Appears_In (Subp_Inputs, Item_Id);
Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
-- Otherwise the state has a default IN OUT mode, because it
-- behaves as a variable.
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
-- Constants and IN parameters
when E_Constant
| E_Generic_In_Parameter
| E_In_Parameter
| E_Loop_Parameter
=>
-- When pragma Global is present it determines the mode
-- of constant objects as inputs (and such objects cannot
-- appear as outputs in the Global contract).
if Global_Seen then
Item_Is_Input := Appears_In (Subp_Inputs, Item_Id);
else
Item_Is_Input := True;
end if;
Item_Is_Output := False;
-- Variables and IN OUT parameters, as well as constants and
-- IN parameters of access type which are handled like
-- variables.
when E_Generic_In_Out_Parameter
| E_In_Out_Parameter
| E_Variable
=>
-- When pragma Global is present it determines the mode of
-- the object.
if Global_Seen then
-- A variable has mode IN when its type is unconstrained
-- or tagged because array bounds, discriminants or tags
-- can be read.
Item_Is_Input :=
Appears_In (Subp_Inputs, Item_Id)
or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
-- Otherwise the variable has a default IN OUT mode
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
when E_Out_Parameter =>
-- An OUT parameter of the related subprogram; it cannot
-- appear in Global.
if Scope (Item_Id) = Spec_Id then
-- The parameter has mode IN if its type is unconstrained
-- or tagged because array bounds, discriminants or tags
-- can be read.
Item_Is_Input :=
Is_Unconstrained_Or_Tagged_Item (Item_Id);
Item_Is_Output := True;
-- An OUT parameter of an enclosing subprogram; it can
-- appear in Global and behaves as a read-write variable.
else
-- When pragma Global is present it determines the mode
-- of the object.
if Global_Seen then
-- A variable has mode IN when its type is
-- unconstrained or tagged because array
-- bounds, discriminants or tags can be read.
Item_Is_Input :=
Appears_In (Subp_Inputs, Item_Id)
or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
-- Otherwise the variable has a default IN OUT mode
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
end if;
-- Protected types
when E_Protected_Type =>
if Global_Seen then
-- A variable has mode IN when its type is unconstrained
-- or tagged because array bounds, discriminants or tags
-- can be read.
Item_Is_Input :=
Appears_In (Subp_Inputs, Item_Id)
or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
else
-- A protected type acts as a formal parameter of mode IN
-- when it applies to a protected function.
if Ekind (Spec_Id) = E_Function then
Item_Is_Input := True;
Item_Is_Output := False;
-- Otherwise the protected type acts as a formal of mode
-- IN OUT.
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
end if;
-- Task types
when E_Task_Type =>
-- When pragma Global is present it determines the mode of
-- the object.
if Global_Seen then
Item_Is_Input :=
Appears_In (Subp_Inputs, Item_Id)
or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
-- Otherwise task types act as IN OUT parameters
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
when others =>
raise Program_Error;
end case;
end Find_Role;
----------------
-- Role_Error --
----------------
procedure Role_Error
(Item_Is_Input : Boolean;
Item_Is_Output : Boolean)
is
begin
Name_Len := 0;
-- When the item is not part of the input and the output set of
-- the related subprogram, then it appears as extra in pragma
-- [Refined_]Depends.
if not Item_Is_Input and then not Item_Is_Output then
Add_Item_To_Name_Buffer (Item_Id);
Add_Str_To_Name_Buffer
(" & cannot appear in dependence relation");
SPARK_Msg_NE (To_String (Global_Name_Buffer), Item, Item_Id);
Error_Msg_Name_1 := Chars (Spec_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "\& is not part of the input or output "
& "set of subprogram %"), Item, Item_Id);
-- The mode of the item and its role in pragma [Refined_]Depends
-- are in conflict. Construct a detailed message explaining the
-- illegality (SPARK RM 6.1.5(5-6)).
else
if Item_Is_Input then
Add_Str_To_Name_Buffer ("read-only");
else
Add_Str_To_Name_Buffer ("write-only");
end if;
Add_Char_To_Name_Buffer (' ');
Add_Item_To_Name_Buffer (Item_Id);
Add_Str_To_Name_Buffer (" & cannot appear as ");
if Item_Is_Input then
Add_Str_To_Name_Buffer ("output");
else
Add_Str_To_Name_Buffer ("input");
end if;
Add_Str_To_Name_Buffer (" in dependence relation");
SPARK_Msg_NE (To_String (Global_Name_Buffer), Item, Item_Id);
end if;
end Role_Error;
-- Local variables
Item_Is_Input : Boolean;
Item_Is_Output : Boolean;
-- Start of processing for Check_Role
begin
Find_Role (Item_Is_Input, Item_Is_Output);
-- Input item
if Is_Input then
if not Item_Is_Input then
Role_Error (Item_Is_Input, Item_Is_Output);
end if;
-- Self-referential item
elsif Self_Ref then
if not Item_Is_Input or else not Item_Is_Output then
Role_Error (Item_Is_Input, Item_Is_Output);
end if;
-- Output item
elsif not Item_Is_Output then
Role_Error (Item_Is_Input, Item_Is_Output);
end if;
end Check_Role;
-----------------
-- Check_Usage --
-----------------
procedure Check_Usage
(Subp_Items : Elist_Id;
Used_Items : Elist_Id;
Is_Input : Boolean)
is
procedure Usage_Error (Item_Id : Entity_Id);
-- Emit an error concerning the illegal usage of an item
-----------------
-- Usage_Error --
-----------------
procedure Usage_Error (Item_Id : Entity_Id) is
begin
-- Input case
if Is_Input then
-- Unconstrained and tagged items are not part of the explicit
-- input set of the related subprogram, they do not have to be
-- present in a dependence relation and should not be flagged
-- (SPARK RM 6.1.5(5)).
if not Is_Unconstrained_Or_Tagged_Item (Item_Id) then
Name_Len := 0;
Add_Item_To_Name_Buffer (Item_Id);
Add_Str_To_Name_Buffer
(" & is missing from input dependence list");
SPARK_Msg_NE (To_String (Global_Name_Buffer), N, Item_Id);
SPARK_Msg_NE
("\add `null ='> &` dependency to ignore this input",
N, Item_Id);
end if;
-- Output case (SPARK RM 6.1.5(10))
else
Name_Len := 0;
Add_Item_To_Name_Buffer (Item_Id);
Add_Str_To_Name_Buffer
(" & is missing from output dependence list");
SPARK_Msg_NE (To_String (Global_Name_Buffer), N, Item_Id);
end if;
end Usage_Error;
-- Local variables
Elmt : Elmt_Id;
Item : Node_Id;
Item_Id : Entity_Id;
-- Start of processing for Check_Usage
begin
if No (Subp_Items) then
return;
end if;
-- Each input or output of the subprogram must appear in a dependency
-- relation.
Elmt := First_Elmt (Subp_Items);
while Present (Elmt) loop
Item := Node (Elmt);
if Nkind (Item) = N_Defining_Identifier then
Item_Id := Item;
else
Item_Id := Entity_Of (Item);
end if;
-- The item does not appear in a dependency
if Present (Item_Id)
and then not Contains (Used_Items, Item_Id)
then
if Is_Formal (Item_Id) then
Usage_Error (Item_Id);
-- The current instance of a protected type behaves as a formal
-- parameter (SPARK RM 6.1.4).
elsif Ekind (Item_Id) = E_Protected_Type
or else Is_Single_Protected_Object (Item_Id)
then
Usage_Error (Item_Id);
-- The current instance of a task type behaves as a formal
-- parameter (SPARK RM 6.1.4).
elsif Ekind (Item_Id) = E_Task_Type
or else Is_Single_Task_Object (Item_Id)
then
-- The dependence of a task unit on itself is implicit and
-- may or may not be explicitly specified (SPARK RM 6.1.4).
-- Emit an error if only one input/output is present.
if Task_Input_Seen /= Task_Output_Seen then
Usage_Error (Item_Id);
end if;
-- States and global objects are not used properly only when
-- the subprogram is subject to pragma Global.
elsif Global_Seen
and then Ekind (Item_Id) in E_Abstract_State
| E_Constant
| E_Loop_Parameter
| E_Protected_Type
| E_Task_Type
| E_Variable
| Formal_Kind
then
Usage_Error (Item_Id);
end if;
end if;
Next_Elmt (Elmt);
end loop;
end Check_Usage;
----------------------
-- Normalize_Clause --
----------------------
procedure Normalize_Clause (Clause : Node_Id) is
procedure Create_Or_Modify_Clause
(Output : Node_Id;
Outputs : Node_Id;
Inputs : Node_Id;
After : Node_Id;
In_Place : Boolean;
Multiple : Boolean);
-- Create a brand new clause to represent the self-reference or
-- modify the input and/or output lists of an existing clause. Output
-- denotes a self-referencial output. Outputs is the output list of a
-- clause. Inputs is the input list of a clause. After denotes the
-- clause after which the new clause is to be inserted. Flag In_Place
-- should be set when normalizing the last output of an output list.
-- Flag Multiple should be set when Output comes from a list with
-- multiple items.
-----------------------------
-- Create_Or_Modify_Clause --
-----------------------------
procedure Create_Or_Modify_Clause
(Output : Node_Id;
Outputs : Node_Id;
Inputs : Node_Id;
After : Node_Id;
In_Place : Boolean;
Multiple : Boolean)
is
procedure Propagate_Output
(Output : Node_Id;
Inputs : Node_Id);
-- Handle the various cases of output propagation to the input
-- list. Output denotes a self-referencial output item. Inputs
-- is the input list of a clause.
----------------------
-- Propagate_Output --
----------------------
procedure Propagate_Output
(Output : Node_Id;
Inputs : Node_Id)
is
function In_Input_List
(Item : Entity_Id;
Inputs : List_Id) return Boolean;
-- Determine whether a particulat item appears in the input
-- list of a clause.
-------------------
-- In_Input_List --
-------------------
function In_Input_List
(Item : Entity_Id;
Inputs : List_Id) return Boolean
is
Elmt : Node_Id;
begin
Elmt := First (Inputs);
while Present (Elmt) loop
if Entity_Of (Elmt) = Item then
return True;
end if;
Next (Elmt);
end loop;
return False;
end In_Input_List;
-- Local variables
Output_Id : constant Entity_Id := Entity_Of (Output);
Grouped : List_Id;
-- Start of processing for Propagate_Output
begin
-- The clause is of the form:
-- (Output =>+ null)
-- Remove null input and replace it with a copy of the output:
-- (Output => Output)
if Nkind (Inputs) = N_Null then
Rewrite (Inputs, New_Copy_Tree (Output));
-- The clause is of the form:
-- (Output =>+ (Input1, ..., InputN))
-- Determine whether the output is not already mentioned in the
-- input list and if not, add it to the list of inputs:
-- (Output => (Output, Input1, ..., InputN))
elsif Nkind (Inputs) = N_Aggregate then
Grouped := Expressions (Inputs);
if not In_Input_List
(Item => Output_Id,
Inputs => Grouped)
then
Prepend_To (Grouped, New_Copy_Tree (Output));
end if;
-- The clause is of the form:
-- (Output =>+ Input)
-- If the input does not mention the output, group the two
-- together:
-- (Output => (Output, Input))
elsif Entity_Of (Inputs) /= Output_Id then
Rewrite (Inputs,
Make_Aggregate (Loc,
Expressions => New_List (
New_Copy_Tree (Output),
New_Copy_Tree (Inputs))));
end if;
end Propagate_Output;
-- Local variables
Loc : constant Source_Ptr := Sloc (Clause);
New_Clause : Node_Id;
-- Start of processing for Create_Or_Modify_Clause
begin
-- A null output depending on itself does not require any
-- normalization.
if Nkind (Output) = N_Null then
return;
-- A function result cannot depend on itself because it cannot
-- appear in the input list of a relation (SPARK RM 6.1.5(10)).
elsif Is_Attribute_Result (Output) then
SPARK_Msg_N ("function result cannot depend on itself", Output);
return;
end if;
-- When performing the transformation in place, simply add the
-- output to the list of inputs (if not already there). This
-- case arises when dealing with the last output of an output
-- list. Perform the normalization in place to avoid generating
-- a malformed tree.
if In_Place then
Propagate_Output (Output, Inputs);
-- A list with multiple outputs is slowly trimmed until only
-- one element remains. When this happens, replace aggregate
-- with the element itself.
if Multiple then
Remove (Output);
Rewrite (Outputs, Output);
end if;
-- Default case
else
-- Unchain the output from its output list as it will appear in
-- a new clause. Note that we cannot simply rewrite the output
-- as null because this will violate the semantics of pragma
-- Depends.
Remove (Output);
-- Generate a new clause of the form:
-- (Output => Inputs)
New_Clause :=
Make_Component_Association (Loc,
Choices => New_List (Output),
Expression => New_Copy_Tree (Inputs));
-- The new clause contains replicated content that has already
-- been analyzed. There is not need to reanalyze or renormalize
-- it again.
Set_Analyzed (New_Clause);
Propagate_Output
(Output => First (Choices (New_Clause)),
Inputs => Expression (New_Clause));
Insert_After (After, New_Clause);
end if;
end Create_Or_Modify_Clause;
-- Local variables
Outputs : constant Node_Id := First (Choices (Clause));
Inputs : Node_Id;
Last_Output : Node_Id;
Next_Output : Node_Id;
Output : Node_Id;
-- Start of processing for Normalize_Clause
begin
-- A self-dependency appears as operator "+". Remove the "+" from the
-- tree by moving the real inputs to their proper place.
if Nkind (Expression (Clause)) = N_Op_Plus then
Rewrite (Expression (Clause), Right_Opnd (Expression (Clause)));
Inputs := Expression (Clause);
-- Multiple outputs appear as an aggregate
if Nkind (Outputs) = N_Aggregate then
Last_Output := Last (Expressions (Outputs));
Output := First (Expressions (Outputs));
while Present (Output) loop
-- Normalization may remove an output from its list,
-- preserve the subsequent output now.
Next_Output := Next (Output);
Create_Or_Modify_Clause
(Output => Output,
Outputs => Outputs,
Inputs => Inputs,
After => Clause,
In_Place => Output = Last_Output,
Multiple => True);
Output := Next_Output;
end loop;
-- Solitary output
else
Create_Or_Modify_Clause
(Output => Outputs,
Outputs => Empty,
Inputs => Inputs,
After => Empty,
In_Place => True,
Multiple => False);
end if;
end if;
end Normalize_Clause;
-- Local variables
Deps : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl);
Clause : Node_Id;
Errors : Nat;
Last_Clause : Node_Id;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Depends_In_Decl_Part
begin
-- Do not analyze the pragma multiple times
if Is_Analyzed_Pragma (N) then
return;
end if;
-- Empty dependency list
if Nkind (Deps) = N_Null then
-- Gather all states, objects and formal parameters that the
-- subprogram may depend on. These items are obtained from the
-- parameter profile or pragma [Refined_]Global (if available).
Collect_Subprogram_Inputs_Outputs
(Subp_Id => Subp_Id,
Subp_Inputs => Subp_Inputs,
Subp_Outputs => Subp_Outputs,
Global_Seen => Global_Seen);
-- Verify that every input or output of the subprogram appear in a
-- dependency.
Check_Usage (Subp_Inputs, All_Inputs_Seen, True);
Check_Usage (Subp_Outputs, All_Outputs_Seen, False);
Check_Function_Return;
-- Dependency clauses appear as component associations of an aggregate
elsif Nkind (Deps) = N_Aggregate then
-- Do not attempt to perform analysis of a syntactically illegal
-- clause as this will lead to misleading errors.
if Has_Extra_Parentheses (Deps) then
goto Leave;
end if;
if Present (Component_Associations (Deps)) then
Last_Clause := Last (Component_Associations (Deps));
-- Gather all states, objects and formal parameters that the
-- subprogram may depend on. These items are obtained from the
-- parameter profile or pragma [Refined_]Global (if available).
Collect_Subprogram_Inputs_Outputs
(Subp_Id => Subp_Id,
Subp_Inputs => Subp_Inputs,
Subp_Outputs => Subp_Outputs,
Global_Seen => Global_Seen);
-- When pragma [Refined_]Depends appears on a single concurrent
-- type, it is relocated to the anonymous object.
if Is_Single_Concurrent_Object (Spec_Id) then
null;
-- Ensure that the formal parameters are visible when analyzing
-- all clauses. This falls out of the general rule of aspects
-- pertaining to subprogram declarations.
elsif not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
if Ekind (Spec_Id) = E_Task_Type then
-- Task discriminants cannot appear in the [Refined_]Depends
-- contract, but must be present for the analysis so that we
-- can reject them with an informative error message.
if Has_Discriminants (Spec_Id) then
Install_Discriminants (Spec_Id);
end if;
elsif Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
else
Install_Formals (Spec_Id);
end if;
end if;
Clause := First (Component_Associations (Deps));
while Present (Clause) loop
Errors := Serious_Errors_Detected;
-- The normalization mechanism may create extra clauses that
-- contain replicated input and output names. There is no need
-- to reanalyze them.
if not Analyzed (Clause) then
Set_Analyzed (Clause);
Analyze_Dependency_Clause
(Clause => Clause,
Is_Last => Clause = Last_Clause);
end if;
-- Do not normalize a clause if errors were detected (count
-- of Serious_Errors has increased) because the inputs and/or
-- outputs may denote illegal items.
if Serious_Errors_Detected = Errors then
Normalize_Clause (Clause);
end if;
Next (Clause);
end loop;
if Restore_Scope then
End_Scope;
end if;
-- Verify that every input or output of the subprogram appear in a
-- dependency.
Check_Usage (Subp_Inputs, All_Inputs_Seen, True);
Check_Usage (Subp_Outputs, All_Outputs_Seen, False);
Check_Function_Return;
-- The dependency list is malformed. This is a syntax error, always
-- report.
else
Error_Msg_N ("malformed dependency relation", Deps);
goto Leave;
end if;
-- The top level dependency relation is malformed. This is a syntax
-- error, always report.
else
Error_Msg_N ("malformed dependency relation", Deps);
goto Leave;
end if;
-- Ensure that a state and a corresponding constituent do not appear
-- together in pragma [Refined_]Depends.
Check_State_And_Constituent_Use
(States => States_Seen,
Constits => Constits_Seen,
Context => N);
<<Leave>>
Set_Is_Analyzed_Pragma (N);
end Analyze_Depends_In_Decl_Part;
--------------------------------------------
-- Analyze_External_Property_In_Decl_Part --
--------------------------------------------
procedure Analyze_External_Property_In_Decl_Part
(N : Node_Id;
Expr_Val : out Boolean)
is
Prag_Id : constant Pragma_Id := Get_Pragma_Id (Pragma_Name (N));
Arg1 : constant Node_Id :=
First (Pragma_Argument_Associations (N));
Obj_Decl : constant Node_Id := Find_Related_Context (N);
Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl);
Expr : Node_Id;
begin
-- Do not analyze the pragma multiple times, but set the output
-- parameter to the argument specified by the pragma.
if Is_Analyzed_Pragma (N) then
goto Leave;
end if;
Error_Msg_Name_1 := Pragma_Name (N);
-- An external property pragma must apply to an effectively volatile
-- object other than a formal subprogram parameter (SPARK RM 7.1.3(2)).
-- The check is performed at the end of the declarative region due to a
-- possible out-of-order arrangement of pragmas:
-- Obj : ...;
-- pragma Async_Readers (Obj);
-- pragma Volatile (Obj);
if Prag_Id /= Pragma_No_Caching
and then not Is_Effectively_Volatile (Obj_Id)
then
if Ekind (Obj_Id) = E_Variable
and then No_Caching_Enabled (Obj_Id)
then
SPARK_Msg_N
("illegal combination of external property % and property "
& """No_Caching"" (SPARK RM 7.1.2(6))", N);
else
SPARK_Msg_N
("external property % must apply to a volatile type or object",
N);
end if;
-- Pragma No_Caching should only apply to volatile variables of
-- a non-effectively volatile type (SPARK RM 7.1.2).
elsif Prag_Id = Pragma_No_Caching then
if Is_Effectively_Volatile (Etype (Obj_Id)) then
SPARK_Msg_N ("property % must not apply to an object of "
& "an effectively volatile type", N);
elsif not Is_Volatile (Obj_Id) then
SPARK_Msg_N ("property % must apply to a volatile object", N);
end if;
end if;
Set_Is_Analyzed_Pragma (N);
<<Leave>>
-- Ensure that the Boolean expression (if present) is static. A missing
-- argument defaults the value to True (SPARK RM 7.1.2(5)).
Expr_Val := True;
if Present (Arg1) then
Expr := Get_Pragma_Arg (Arg1);
if Is_OK_Static_Expression (Expr) then
Expr_Val := Is_True (Expr_Value (Expr));
end if;
end if;
end Analyze_External_Property_In_Decl_Part;
---------------------------------
-- Analyze_Global_In_Decl_Part --
---------------------------------
procedure Analyze_Global_In_Decl_Part (N : Node_Id) is
Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl);
Constits_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all constituents processed so far.
-- It aids in detecting illegal usage of a state and a corresponding
-- constituent in pragma [Refinde_]Global.
Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the items processed so far. It
-- plays a role in detecting distinct entities.
States_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all states processed so far. It
-- helps in detecting illegal usage of a state and a corresponding
-- constituent in pragma [Refined_]Global.
In_Out_Seen : Boolean := False;
Input_Seen : Boolean := False;
Output_Seen : Boolean := False;
Proof_Seen : Boolean := False;
-- Flags used to verify the consistency of modes
procedure Analyze_Global_List
(List : Node_Id;
Global_Mode : Name_Id := Name_Input);
-- Verify the legality of a single global list declaration. Global_Mode
-- denotes the current mode in effect.
-------------------------
-- Analyze_Global_List --
-------------------------
procedure Analyze_Global_List
(List : Node_Id;
Global_Mode : Name_Id := Name_Input)
is
procedure Analyze_Global_Item
(Item : Node_Id;
Global_Mode : Name_Id);
-- Verify the legality of a single global item declaration denoted by
-- Item. Global_Mode denotes the current mode in effect.
procedure Check_Duplicate_Mode
(Mode : Node_Id;
Status : in out Boolean);
-- Flag Status denotes whether a particular mode has been seen while
-- processing a global list. This routine verifies that Mode is not a
-- duplicate mode and sets the flag Status (SPARK RM 6.1.4(9)).
procedure Check_Mode_Restriction_In_Enclosing_Context
(Item : Node_Id;
Item_Id : Entity_Id);
-- Verify that an item of mode In_Out or Output does not appear as
-- an input in the Global aspect of an enclosing subprogram or task
-- unit. If this is the case, emit an error. Item and Item_Id are
-- respectively the item and its entity.
procedure Check_Mode_Restriction_In_Function (Mode : Node_Id);
-- Mode denotes either In_Out or Output. Depending on the kind of the
-- related subprogram, emit an error if those two modes apply to a
-- function (SPARK RM 6.1.4(10)).
-------------------------
-- Analyze_Global_Item --
-------------------------
procedure Analyze_Global_Item
(Item : Node_Id;
Global_Mode : Name_Id)
is
Item_Id : Entity_Id;
begin
-- Detect one of the following cases
-- with Global => (null, Name)
-- with Global => (Name_1, null, Name_2)
-- with Global => (Name, null)
if Nkind (Item) = N_Null then
SPARK_Msg_N ("cannot mix null and non-null global items", Item);
return;
end if;
Analyze (Item);
Resolve_State (Item);
-- Find the entity of the item. If this is a renaming, climb the
-- renaming chain to reach the root object. Renamings of non-
-- entire objects do not yield an entity (Empty).
Item_Id := Entity_Of (Item);
if Present (Item_Id) then
-- A global item may denote a formal parameter of an enclosing
-- subprogram (SPARK RM 6.1.4(6)). Do this check first to
-- provide a better error diagnostic.
if Is_Formal (Item_Id) then
if Scope (Item_Id) = Spec_Id then
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item cannot reference "
& "parameter of subprogram &"), Item, Spec_Id);
return;
end if;
-- A global item may denote a concurrent type as long as it is
-- the current instance of an enclosing protected or task type
-- (SPARK RM 6.1.4).
elsif Ekind (Item_Id) in E_Protected_Type | E_Task_Type then
if Is_CCT_Instance (Item_Id, Spec_Id) then
-- Pragma [Refined_]Global associated with a protected
-- subprogram cannot mention the current instance of a
-- protected type because the instance behaves as a
-- formal parameter.
if Ekind (Item_Id) = E_Protected_Type then
if Scope (Spec_Id) = Item_Id then
Error_Msg_Name_1 := Chars (Item_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item of subprogram & "
& "cannot reference current instance of "
& "protected type %"), Item, Spec_Id);
return;
end if;
-- Pragma [Refined_]Global associated with a task type
-- cannot mention the current instance of a task type
-- because the instance behaves as a formal parameter.
else pragma Assert (Ekind (Item_Id) = E_Task_Type);
if Spec_Id = Item_Id then
Error_Msg_Name_1 := Chars (Item_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item of subprogram & "
& "cannot reference current instance of task "
& "type %"), Item, Spec_Id);
return;
end if;
end if;
-- Otherwise the global item denotes a subtype mark that is
-- not a current instance.
else
SPARK_Msg_N
("invalid use of subtype mark in global list", Item);
return;
end if;
-- A global item may denote the anonymous object created for a
-- single protected/task type as long as the current instance
-- is the same single type (SPARK RM 6.1.4).
elsif Is_Single_Concurrent_Object (Item_Id)
and then Is_CCT_Instance (Etype (Item_Id), Spec_Id)
then
-- Pragma [Refined_]Global associated with a protected
-- subprogram cannot mention the current instance of a
-- protected type because the instance behaves as a formal
-- parameter.
if Is_Single_Protected_Object (Item_Id) then
if Scope (Spec_Id) = Etype (Item_Id) then
Error_Msg_Name_1 := Chars (Item_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item of subprogram & "
& "cannot reference current instance of protected "
& "type %"), Item, Spec_Id);
return;
end if;
-- Pragma [Refined_]Global associated with a task type
-- cannot mention the current instance of a task type
-- because the instance behaves as a formal parameter.
else pragma Assert (Is_Single_Task_Object (Item_Id));
if Spec_Id = Item_Id then
Error_Msg_Name_1 := Chars (Item_Id);
SPARK_Msg_NE
(Fix_Msg (Spec_Id, "global item of subprogram & "
& "cannot reference current instance of task "
& "type %"), Item, Spec_Id);
return;
end if;
end if;
-- A formal object may act as a global item inside a generic
elsif Is_Formal_Object (Item_Id) then
null;
elsif Ekind (Item_Id) in E_Constant | E_Variable
and then Present (Ultimate_Overlaid_Entity (Item_Id))
then
SPARK_Msg_NE
("overlaying object & cannot appear in Global",
Item, Item_Id);
SPARK_Msg_NE
("\use the overlaid object & instead",
Item, Ultimate_Overlaid_Entity (Item_Id));
return;
-- The only legal references are those to abstract states,
-- objects and various kinds of constants (SPARK RM 6.1.4(4)).
elsif Ekind (Item_Id) not in E_Abstract_State
| E_Constant
| E_Loop_Parameter
| E_Variable
then
SPARK_Msg_N
("global item must denote object, state or current "
& "instance of concurrent type", Item);
if Is_Named_Number (Item_Id) then
SPARK_Msg_NE
("\named number & is not an object", Item, Item_Id);
end if;
return;
end if;
-- State related checks
if Ekind (Item_Id) = E_Abstract_State then
-- Package and subprogram bodies are instantiated
-- individually in a separate compiler pass. Due to this
-- mode of instantiation, the refinement of a state may
-- no longer be visible when a subprogram body contract
-- is instantiated. Since the generic template is legal,
-- do not perform this check in the instance to circumvent
-- this oddity.
if In_Instance then
null;
-- An abstract state with visible refinement cannot appear
-- in pragma [Refined_]Global as its place must be taken by
-- some of its constituents (SPARK RM 6.1.4(7)).
elsif Has_Visible_Refinement (Item_Id) then
SPARK_Msg_NE
("cannot mention state & in global refinement",
Item, Item_Id);
SPARK_Msg_N ("\use its constituents instead", Item);
return;
-- An external state which has Async_Writers or
-- Effective_Reads enabled cannot appear as a global item
-- of a nonvolatile function (SPARK RM 7.1.3(8)).
elsif Is_External_State (Item_Id)
and then (Async_Writers_Enabled (Item_Id)
or else Effective_Reads_Enabled (Item_Id))
and then Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Is_Volatile_Function (Spec_Id)
then
SPARK_Msg_NE
("external state & cannot act as global item of "
& "nonvolatile function", Item, Item_Id);
return;
-- If the reference to the abstract state appears in an
-- enclosing package body that will eventually refine the
-- state, record the reference for future checks.
else
Record_Possible_Body_Reference
(State_Id => Item_Id,
Ref => Item);
end if;
-- Constant related checks
elsif Ekind (Item_Id) = E_Constant then
-- Constant is a read-only item, therefore it cannot act as
-- an output.
if Global_Mode in Name_In_Out | Name_Output then
-- Constant of an access-to-variable type is a read-write
-- item in procedures, generic procedures, protected
-- entries and tasks.
if Is_Access_Variable (Etype (Item_Id))
and then (Ekind (Spec_Id) in E_Entry
| E_Entry_Family
| E_Procedure
| E_Generic_Procedure
| E_Task_Type
or else Is_Single_Task_Object (Spec_Id))
then
null;
else
SPARK_Msg_NE
("constant & cannot act as output", Item, Item_Id);
return;
end if;
end if;
-- Loop parameter related checks
elsif Ekind (Item_Id) = E_Loop_Parameter then
-- A loop parameter is a read-only item, therefore it cannot
-- act as an output.
if Global_Mode in Name_In_Out | Name_Output then
SPARK_Msg_NE
("loop parameter & cannot act as output",
Item, Item_Id);
return;
end if;
-- Variable related checks. These are only relevant when
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
elsif SPARK_Mode = On
and then Ekind (Item_Id) = E_Variable
and then Is_Effectively_Volatile_For_Reading (Item_Id)
then
-- The current instance of a protected unit is not an
-- effectively volatile object, unless the protected unit
-- is already volatile for another reason (SPARK RM 7.1.2).
if Is_Single_Protected_Object (Item_Id)
and then Is_CCT_Instance (Etype (Item_Id), Spec_Id)
and then not Is_Effectively_Volatile_For_Reading
(Item_Id, Ignore_Protected => True)
then
null;
-- An effectively volatile object for reading cannot appear
-- as a global item of a nonvolatile function (SPARK RM
-- 7.1.3(8)).
elsif Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Is_Volatile_Function (Spec_Id)
then
Error_Msg_NE
("volatile object & cannot act as global item of a "
& "function", Item, Item_Id);
return;
-- An effectively volatile object with external property
-- Effective_Reads set to True must have mode Output or
-- In_Out (SPARK RM 7.1.3(10)).
elsif Effective_Reads_Enabled (Item_Id)
and then Global_Mode = Name_Input
then
Error_Msg_NE
("volatile object & with property Effective_Reads must "
& "have mode In_Out or Output", Item, Item_Id);
return;
end if;
end if;
-- When the item renames an entire object, replace the item
-- with a reference to the object.
if Entity (Item) /= Item_Id then
Rewrite (Item, New_Occurrence_Of (Item_Id, Sloc (Item)));
Analyze (Item);
end if;
-- Some form of illegal construct masquerading as a name
-- (SPARK RM 6.1.4(4)).
else
Error_Msg_N
("global item must denote object, state or current instance "
& "of concurrent type", Item);
return;
end if;
-- Verify that an output does not appear as an input in an
-- enclosing subprogram.
if Global_Mode in Name_In_Out | Name_Output then
Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id);
end if;
-- The same entity might be referenced through various way.
-- Check the entity of the item rather than the item itself
-- (SPARK RM 6.1.4(10)).
if Contains (Seen, Item_Id) then
SPARK_Msg_N ("duplicate global item", Item);
-- Add the entity of the current item to the list of processed
-- items.
else
Append_New_Elmt (Item_Id, Seen);
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
-- The variable may eventually become a constituent of a single
-- protected/task type. Record the reference now and verify its
-- legality when analyzing the contract of the variable
-- (SPARK RM 9.3).
elsif Ekind (Item_Id) = E_Variable then
Record_Possible_Part_Of_Reference
(Var_Id => Item_Id,
Ref => Item);
end if;
if Ekind (Item_Id) in E_Abstract_State | E_Constant | E_Variable
and then Present (Encapsulating_State (Item_Id))
then
Append_New_Elmt (Item_Id, Constits_Seen);
end if;
end if;
end Analyze_Global_Item;
--------------------------
-- Check_Duplicate_Mode --
--------------------------
procedure Check_Duplicate_Mode
(Mode : Node_Id;
Status : in out Boolean)
is
begin
if Status then
SPARK_Msg_N ("duplicate global mode", Mode);
end if;
Status := True;
end Check_Duplicate_Mode;
-------------------------------------------------
-- Check_Mode_Restriction_In_Enclosing_Context --
-------------------------------------------------
procedure Check_Mode_Restriction_In_Enclosing_Context
(Item : Node_Id;
Item_Id : Entity_Id)
is
Context : Entity_Id;
Dummy : Boolean;
Inputs : Elist_Id := No_Elist;
Outputs : Elist_Id := No_Elist;
begin
-- Traverse the scope stack looking for enclosing subprograms or
-- tasks subject to pragma [Refined_]Global.
Context := Scope (Subp_Id);
while Present (Context) and then Context /= Standard_Standard loop
-- For a single task type, retrieve the corresponding object to
-- which pragma [Refined_]Global is attached.
if Ekind (Context) = E_Task_Type
and then Is_Single_Concurrent_Type (Context)
then
Context := Anonymous_Object (Context);
end if;
if Is_Subprogram_Or_Entry (Context)
or else Ekind (Context) = E_Task_Type
or else Is_Single_Task_Object (Context)
then
Collect_Subprogram_Inputs_Outputs
(Subp_Id => Context,
Subp_Inputs => Inputs,
Subp_Outputs => Outputs,
Global_Seen => Dummy);
-- The item is classified as In_Out or Output but appears as
-- an Input or a formal parameter of mode IN in an enclosing
-- subprogram or task unit (SPARK RM 6.1.4(13)).
if Appears_In (Inputs, Item_Id)
and then not Appears_In (Outputs, Item_Id)
then
SPARK_Msg_NE
("global item & cannot have mode In_Out or Output",
Item, Item_Id);
if Is_Subprogram_Or_Entry (Context) then
SPARK_Msg_NE
(Fix_Msg (Subp_Id, "\item already appears as input "
& "of subprogram &"), Item, Context);
else
SPARK_Msg_NE
(Fix_Msg (Subp_Id, "\item already appears as input "
& "of task &"), Item, Context);
end if;
-- Stop the traversal once an error has been detected
exit;
end if;
end if;
Context := Scope (Context);
end loop;
end Check_Mode_Restriction_In_Enclosing_Context;
----------------------------------------
-- Check_Mode_Restriction_In_Function --
----------------------------------------
procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is
begin
if Ekind (Spec_Id) in E_Function | E_Generic_Function then
SPARK_Msg_N
("global mode & is not applicable to functions", Mode);
end if;
end Check_Mode_Restriction_In_Function;
-- Local variables
Assoc : Node_Id;
Item : Node_Id;
Mode : Node_Id;
-- Start of processing for Analyze_Global_List
begin
if Nkind (List) = N_Null then
Set_Analyzed (List);
-- Single global item declaration
elsif Nkind (List) in N_Expanded_Name
| N_Identifier
| N_Selected_Component
then
Analyze_Global_Item (List, Global_Mode);
-- Simple global list or moded global list declaration
elsif Nkind (List) = N_Aggregate then
Set_Analyzed (List);
-- The declaration of a simple global list appear as a collection
-- of expressions.
if Present (Expressions (List)) then
if Present (Component_Associations (List)) then
SPARK_Msg_N
("cannot mix moded and non-moded global lists", List);
end if;
Item := First (Expressions (List));
while Present (Item) loop
Analyze_Global_Item (Item, Global_Mode);
Next (Item);
end loop;
-- The declaration of a moded global list appears as a collection
-- of component associations where individual choices denote
-- modes.
elsif Present (Component_Associations (List)) then
if Present (Expressions (List)) then
SPARK_Msg_N
("cannot mix moded and non-moded global lists", List);
end if;
Assoc := First (Component_Associations (List));
while Present (Assoc) loop
Mode := First (Choices (Assoc));
if Nkind (Mode) = N_Identifier then
if Chars (Mode) = Name_In_Out then
Check_Duplicate_Mode (Mode, In_Out_Seen);
Check_Mode_Restriction_In_Function (Mode);
elsif Chars (Mode) = Name_Input then
Check_Duplicate_Mode (Mode, Input_Seen);
elsif Chars (Mode) = Name_Output then
Check_Duplicate_Mode (Mode, Output_Seen);
Check_Mode_Restriction_In_Function (Mode);
elsif Chars (Mode) = Name_Proof_In then
Check_Duplicate_Mode (Mode, Proof_Seen);
else
SPARK_Msg_N ("invalid mode selector", Mode);
end if;
else
SPARK_Msg_N ("invalid mode selector", Mode);
end if;
-- Items in a moded list appear as a collection of
-- expressions. Reuse the existing machinery to analyze
-- them.
Analyze_Global_List
(List => Expression (Assoc),
Global_Mode => Chars (Mode));
Next (Assoc);
end loop;
-- Invalid tree
else
raise Program_Error;
end if;
-- Any other attempt to declare a global item is illegal. This is a
-- syntax error, always report.
else
Error_Msg_N ("malformed global list", List);
end if;
end Analyze_Global_List;
-- Local variables
Items : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Global_In_Decl_Part
begin
-- Do not analyze the pragma multiple times
if Is_Analyzed_Pragma (N) then
return;
end if;
-- There is nothing to be done for a null global list
if Nkind (Items) = N_Null then
Set_Analyzed (Items);
-- Analyze the various forms of global lists and items. Note that some
-- of these may be malformed in which case the analysis emits error
-- messages.
else
-- When pragma [Refined_]Global appears on a single concurrent type,
-- it is relocated to the anonymous object.
if Is_Single_Concurrent_Object (Spec_Id) then
null;
-- Ensure that the formal parameters are visible when processing an
-- item. This falls out of the general rule of aspects pertaining to
-- subprogram declarations.
elsif not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
if Ekind (Spec_Id) = E_Task_Type then
-- Task discriminants cannot appear in the [Refined_]Global
-- contract, but must be present for the analysis so that we
-- can reject them with an informative error message.
if Has_Discriminants (Spec_Id) then
Install_Discriminants (Spec_Id);
end if;
elsif Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
else
Install_Formals (Spec_Id);
end if;
end if;
Analyze_Global_List (Items);
if Restore_Scope then
End_Scope;
end if;
end if;
-- Ensure that a state and a corresponding constituent do not appear
-- together in pragma [Refined_]Global.
Check_State_And_Constituent_Use
(States => States_Seen,
Constits => Constits_Seen,
Context => N);
Set_Is_Analyzed_Pragma (N);
end Analyze_Global_In_Decl_Part;
--------------------------------------------
-- Analyze_Initial_Condition_In_Decl_Part --
--------------------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
-- Save the Ghost-related attributes to restore on exit
begin
-- Do not analyze the pragma multiple times
if Is_Analyzed_Pragma (N) then
return;
end if;
-- Set the Ghost mode in effect from the pragma. Due to the delayed
-- analysis of the pragma, the Ghost mode at point of declaration and
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
Set_Ghost_Mode (N);
-- The expression is preanalyzed because it has not been moved to its
-- final place yet. A direct analysis may generate side effects and this
-- is not desired at this point.
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
Set_Is_Analyzed_Pragma (N);
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
-- Analyze_Initializes_In_Decl_Part --
--------------------------------------
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id) is
Pack_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Constits_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all constituents processed so far.
-- It aids in detecting illegal usage of a state and a corresponding
-- constituent in pragma Initializes.
Items_Seen : Elist_Id := No_Elist;
-- A list of all initialization items processed so far. This list is
-- used to detect duplicate items.
States_And_Objs : Elist_Id := No_Elist;
-- A list of all abstract states and objects declared in the visible
-- declarations of the related package. This list is used to detect the
-- legality of initialization items.
States_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all states processed so far. It
-- helps in detecting illegal usage of a state and a corresponding
-- constituent in pragma Initializes.
procedure Analyze_Initialization_Item (Item : Node_Id);
-- Verify the legality of a single initialization item
procedure Analyze_Initialization_Item_With_Inputs (Item : Node_Id);
-- Verify the legality of a single initialization item followed by a
-- list of input items.
procedure Collect_States_And_Objects (Pack_Decl : Node_Id);
-- Inspect the visible declarations of the related package and gather
-- the entities of all abstract states and objects in States_And_Objs.
---------------------------------
-- Analyze_Initialization_Item --
---------------------------------
procedure Analyze_Initialization_Item (Item : Node_Id) is
Item_Id : Entity_Id;
begin
Analyze (Item);
Resolve_State (Item);
if Is_Entity_Name (Item) then
Item_Id := Entity_Of (Item);
if Present (Item_Id)
and then Ekind (Item_Id) in
E_Abstract_State | E_Constant | E_Variable
then
-- When the initialization item is undefined, it appears as
-- Any_Id. Do not continue with the analysis of the item.
if Item_Id = Any_Id then
null;
elsif Ekind (Item_Id) in E_Constant | E_Variable
and then Present (Ultimate_Overlaid_Entity (Item_Id))
then
SPARK_Msg_NE
("overlaying object & cannot appear in Initializes",
Item, Item_Id);
SPARK_Msg_NE
("\use the overlaid object & instead",
Item, Ultimate_Overlaid_Entity (Item_Id));
-- The state or variable must be declared in the visible
-- declarations of the package (SPARK RM 7.1.5(7)).
elsif not Contains (States_And_Objs, Item_Id) then
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("initialization item & must appear in the visible "
& "declarations of package %", Item, Item_Id);
-- Detect a duplicate use of the same initialization item
-- (SPARK RM 7.1.5(5)).
elsif Contains (Items_Seen, Item_Id) then
SPARK_Msg_N ("duplicate initialization item", Item);
-- The item is legal, add it to the list of processed states
-- and variables.
else
Append_New_Elmt (Item_Id, Items_Seen);
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
end if;
if Present (Encapsulating_State (Item_Id)) then
Append_New_Elmt (Item_Id, Constits_Seen);
end if;
end if;
-- The item references something that is not a state or object
-- (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
("initialization item must denote object or state", Item);
end if;
-- Some form of illegal construct masquerading as a name
-- (SPARK RM 7.1.5(3)). This is a syntax error, always report.
else
Error_Msg_N
("initialization item must denote object or state", Item);
end if;
end Analyze_Initialization_Item;
---------------------------------------------
-- Analyze_Initialization_Item_With_Inputs --
---------------------------------------------
procedure Analyze_Initialization_Item_With_Inputs (Item : Node_Id) is
Inputs_Seen : Elist_Id := No_Elist;
-- A list of all inputs processed so far. This list is used to detect
-- duplicate uses of an input.
Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False;
-- Flags used to check the legality of an input list
procedure Analyze_Input_Item (Input : Node_Id);
-- Verify the legality of a single input item
------------------------
-- Analyze_Input_Item --
------------------------
procedure Analyze_Input_Item (Input : Node_Id) is
Input_Id : Entity_Id;
begin
-- Null input list
if Nkind (Input) = N_Null then
if Null_Seen then
SPARK_Msg_N
("multiple null initializations not allowed", Item);
elsif Non_Null_Seen then
SPARK_Msg_N
("cannot mix null and non-null initialization item", Item);
else
Null_Seen := True;
end if;
-- Input item
else
Non_Null_Seen := True;
if Null_Seen then
SPARK_Msg_N
("cannot mix null and non-null initialization item", Item);
end if;
Analyze (Input);
Resolve_State (Input);
if Is_Entity_Name (Input) then
Input_Id := Entity_Of (Input);
if Present (Input_Id)
and then Ekind (Input_Id) in E_Abstract_State
| E_Constant
| E_Generic_In_Out_Parameter
| E_Generic_In_Parameter
| E_In_Parameter
| E_In_Out_Parameter
| E_Out_Parameter
| E_Protected_Type
| E_Task_Type
| E_Variable
then
-- The input cannot denote states or objects declared
-- within the related package (SPARK RM 7.1.5(4)).
if Within_Scope (Input_Id, Current_Scope) then
-- Do not consider generic formal parameters or their
-- respective mappings to generic formals. Even though
-- the formals appear within the scope of the package,
-- it is allowed for an initialization item to depend
-- on an input item.
if Is_Formal_Object (Input_Id) then
null;
elsif Ekind (Input_Id) in E_Constant | E_Variable
and then Present (Corresponding_Generic_Association
(Declaration_Node (Input_Id)))
then
null;
else
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("input item & cannot denote a visible object or "
& "state of package %", Input, Input_Id);
return;
end if;
end if;
if Ekind (Input_Id) in E_Constant | E_Variable
and then Present (Ultimate_Overlaid_Entity (Input_Id))
then
SPARK_Msg_NE
("overlaying object & cannot appear in Initializes",
Input, Input_Id);
SPARK_Msg_NE
("\use the overlaid object & instead",
Input, Ultimate_Overlaid_Entity (Input_Id));
return;
end if;
-- Detect a duplicate use of the same input item
-- (SPARK RM 7.1.5(5)).
if Contains (Inputs_Seen, Input_Id) then
SPARK_Msg_N ("duplicate input item", Input);
return;
end if;
-- At this point it is known that the input is legal. Add
-- it to the list of processed inputs.
Append_New_Elmt (Input_Id, Inputs_Seen);
if Ekind (Input_Id) = E_Abstract_State then
Append_New_Elmt (Input_Id, States_Seen);
end if;
if Ekind (Input_Id) in E_Abstract_State
| E_Constant
| E_Variable
and then Present (Encapsulating_State (Input_Id))
then
Append_New_Elmt (Input_Id, Constits_Seen);
end if;
-- The input references something that is not a state or an
-- object (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
("input item must denote object or state", Input);
end if;
-- Some form of illegal construct masquerading as a name
-- (SPARK RM 7.1.5(3)). This is a syntax error, always report.
else
Error_Msg_N
("input item must denote object or state", Input);
end if;
end if;
end Analyze_Input_Item;
-- Local variables
Inputs : constant Node_Id := Expression (Item);
Elmt : Node_Id;
Input : Node_Id;
Name_Seen : Boolean := False;
-- A flag used to detect multiple item names
-- Start of processing for Analyze_Initialization_Item_With_Inputs
begin
-- Inspect the name of an item with inputs
Elmt := First (Choices (Item));
while Present (Elmt) loop
if Name_Seen then
SPARK_Msg_N ("only one item allowed in initialization", Elmt);
else
Name_Seen := True;
Analyze_Initialization_Item (Elmt);
end if;
Next (Elmt);
end loop;
-- Multiple input items appear as an aggregate
if Nkind (Inputs) = N_Aggregate then
if Present (Expressions (Inputs)) then
Input := First (Expressions (Inputs));
while Present (Input) loop
Analyze_Input_Item (Input);
Next (Input);
end loop;
end if;
if Present (Component_Associations (Inputs)) then
SPARK_Msg_N
("inputs must appear in named association form", Inputs);
end if;
-- Single input item
else
Analyze_Input_Item (Inputs);
end if;
end Analyze_Initialization_Item_With_Inputs;
--------------------------------
-- Collect_States_And_Objects --
--------------------------------
procedure Collect_States_And_Objects (Pack_Decl : Node_Id) is
Pack_Spec : constant Node_Id := Specification (Pack_Decl);
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Decl : Node_Id;
State_Elmt : Elmt_Id;
begin
-- Collect the abstract states defined in the package (if any)
if Has_Non_Null_Abstract_State (Pack_Id) then
State_Elmt := First_Elmt (Abstract_States (Pack_Id));
while Present (State_Elmt) loop
Append_New_Elmt (Node (State_Elmt), States_And_Objs);
Next_Elmt (State_Elmt);
end loop;
end if;
-- Collect all objects that appear in the visible declarations of the
-- related package.
if Present (Visible_Declarations (Pack_Spec)) then
Decl := First (Visible_Declarations (Pack_Spec));
while Present (Decl) loop
if Comes_From_Source (Decl)
and then Nkind (Decl) in N_Object_Declaration
| N_Object_Renaming_Declaration
then
Append_New_Elmt (Defining_Entity (Decl), States_And_Objs);
elsif Nkind (Decl) = N_Package_Declaration then
Collect_States_And_Objects (Decl);
elsif Is_Single_Concurrent_Type_Declaration (Decl) then
Append_New_Elmt
(Anonymous_Object (Defining_Entity (Decl)),
States_And_Objs);
end if;
Next (Decl);
end loop;
end if;
end Collect_States_And_Objects;
-- Local variables
Inits : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
Init : Node_Id;
-- Start of processing for Analyze_Initializes_In_Decl_Part
begin
-- Do not analyze the pragma multiple times
if Is_Analyzed_Pragma (N) then
return;
end if;
-- Nothing to do when the initialization list is empty
if Nkind (Inits) = N_Null then
return;
end if;
-- Single and multiple initialization clauses appear as an aggregate. If
-- this is not the case, then either the parser or the analysis of the
-- pragma failed to produce an aggregate.
pragma Assert (Nkind (Inits) = N_Aggregate);
-- Initialize the various lists used during analysis
Collect_States_And_Objects (Pack_Decl);
if Present (Expressions (Inits)) then
Init := First (Expressions (Inits));
while Present (Init) loop
Analyze_Initialization_Item (Init);
Next (Init);
end loop;
end if;
if Present (Component_Associations (Inits)) then
Init := First (Component_Associations (Inits));
while Present (Init) loop
Analyze_Initialization_Item_With_Inputs (Init);
Next (Init);
end loop;
end if;
-- Ensure that a state and a corresponding constituent do not appear
-- together in pragma Initializes.
Check_State_And_Constituent_Use
(States => States_Seen,
Constits => Constits_Seen,
Context => N);
Set_Is_Analyzed_Pragma (N);
end Analyze_Initializes_In_Decl_Part;
---------------------
-- Analyze_Part_Of --
---------------------
procedure Analyze_Part_Of
(Indic : Node_Id;
Item_Id : Entity_Id;
Encap : Node_Id;
Encap_Id : out Entity_Id;
Legal : out Boolean)
is
procedure Check_Part_Of_Abstract_State;
pragma Inline (Check_Part_Of_Abstract_State);
-- Verify the legality of indicator Part_Of when the encapsulator is an
-- abstract state.
procedure Check_Part_Of_Concurrent_Type;
pragma Inline (Check_Part_Of_Concurrent_Type);
-- Verify the legality of indicator Part_Of when the encapsulator is a
-- single concurrent type.
----------------------------------
-- Check_Part_Of_Abstract_State --
----------------------------------
procedure Check_Part_Of_Abstract_State is
Pack_Id : Entity_Id;
Placement : State_Space_Kind;
Parent_Unit : Entity_Id;
begin
-- Determine where the object, package instantiation or state lives
-- with respect to the enclosing packages or package bodies.
Find_Placement_In_State_Space
(Item_Id => Item_Id,
Placement => Placement,
Pack_Id => Pack_Id);
-- The item appears in a non-package construct with a declarative
-- part (subprogram, block, etc). As such, the item is not allowed
-- to be a part of an encapsulating state because the item is not
-- visible.
if Placement = Not_In_Package then
SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
Error_Msg_Name_1 := Chars (Scope (Encap_Id));
SPARK_Msg_NE
("\& is not part of the hidden state of package %",
Indic, Item_Id);
return;
-- The item appears in the visible state space of some package. In
-- general this scenario does not warrant Part_Of except when the
-- package is a nongeneric private child unit and the encapsulating
-- state is declared in a parent unit or a public descendant of that
-- parent unit.
elsif Placement = Visible_State_Space then
if Is_Child_Unit (Pack_Id)
and then not Is_Generic_Unit (Pack_Id)
and then Is_Private_Descendant (Pack_Id)
then
-- A variable or state abstraction which is part of the visible
-- state of a nongeneric private child unit or its public
-- descendants must have its Part_Of indicator specified. The
-- Part_Of indicator must denote a state declared by either the
-- parent unit of the private unit or by a public descendant of
-- that parent unit.
-- Find the nearest private ancestor (which can be the current
-- unit itself).
Parent_Unit := Pack_Id;
while Present (Parent_Unit) loop
exit when Is_Private_Library_Unit (Parent_Unit);
Parent_Unit := Scope (Parent_Unit);
end loop;
Parent_Unit := Scope (Parent_Unit);
if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
SPARK_Msg_NE
("indicator Part_Of must denote abstract state of & or of "
& "its public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
return;
elsif Scope (Encap_Id) = Parent_Unit
or else
(Is_Ancestor_Package (Parent_Unit, Scope (Encap_Id))
and then not Is_Private_Descendant (Scope (Encap_Id)))
then
null;
else
SPARK_Msg_NE
("indicator Part_Of must denote abstract state of & or of "
& "its public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
return;
end if;
-- Indicator Part_Of is not needed when the related package is
-- not a nongeneric private child unit or a public descendant
-- thereof.
else
SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("\& is declared in the visible part of package %",
Indic, Item_Id);
return;
end if;
-- When the item appears in the private state space of a package, the
-- encapsulating state must be declared in the same package.
elsif Placement = Private_State_Space then
-- In the case of the abstract state of a nongeneric private
-- child package, it may be encapsulated in the state of a
-- public descendant of its parent package.
declare
function Is_Public_Descendant
(Child, Ancestor : Entity_Id)
return Boolean;
-- Return True if Child is a public descendant of Pack
--------------------------
-- Is_Public_Descendant --
--------------------------
function Is_Public_Descendant
(Child, Ancestor : Entity_Id)
return Boolean
is
P : Entity_Id := Child;
begin
while Is_Child_Unit (P)
and then not Is_Private_Library_Unit (P)
loop
if Scope (P) = Ancestor then
return True;
end if;
P := Scope (P);
end loop;
return False;
end Is_Public_Descendant;
-- Local variables
Immediate_Pack_Id : constant Entity_Id := Scope (Item_Id);
Is_State_Of_Private_Child : constant Boolean :=
Is_Child_Unit (Immediate_Pack_Id)
and then not Is_Generic_Unit (Immediate_Pack_Id)
and then Is_Private_Descendant (Immediate_Pack_Id);
Is_OK_Through_Sibling : Boolean := False;
begin
if Ekind (Item_Id) = E_Abstract_State
and then Is_State_Of_Private_Child
and then Is_Public_Descendant (Scope (Encap_Id), Pack_Id)
then
Is_OK_Through_Sibling := True;
end if;
if Scope (Encap_Id) /= Pack_Id
and then not Is_OK_Through_Sibling
then
if Is_State_Of_Private_Child then
SPARK_Msg_NE
("indicator Part_Of must denote abstract state of & "
& "or of its public descendant "
& "(SPARK RM 7.2.6(3))", Indic, Pack_Id);
else
SPARK_Msg_NE
("indicator Part_Of must denote an abstract state of "
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
end if;
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("\& is declared in the private part of package %",
Indic, Item_Id);
return;
end if;
end;
-- Items declared in the body state space of a package do not need
-- Part_Of indicators as the refinement has already been seen.
else
SPARK_Msg_N
("indicator Part_Of cannot appear in this context "
& "(SPARK RM 7.2.6(5))", Indic);
if Scope (Encap_Id) = Pack_Id then
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("\& is declared in the body of package %", Indic, Item_Id);
end if;
return;
end if;
-- At this point it is known that the Part_Of indicator is legal
Legal := True;
end Check_Part_Of_Abstract_State;
-----------------------------------
-- Check_Part_Of_Concurrent_Type --
-----------------------------------
procedure Check_Part_Of_Concurrent_Type is
function In_Proper_Order
(First : Node_Id;
Second : Node_Id) return Boolean;
pragma Inline (In_Proper_Order);
-- Determine whether node First precedes node Second
procedure Placement_Error;
pragma Inline (Placement_Error);
-- Emit an error concerning the illegal placement of the item with
-- respect to the single concurrent type.
---------------------
-- In_Proper_Order --
---------------------
function In_Proper_Order
(First : Node_Id;
Second : Node_Id) return Boolean
is
N : Node_Id;
begin
if List_Containing (First) = List_Containing (Second) then
N := First;
while Present (N) loop
if N = Second then
return True;
end if;
Next (N);
end loop;
end if;
return False;
end In_Proper_Order;
---------------------
-- Placement_Error --
---------------------
procedure Placement_Error is
begin
SPARK_Msg_N
("indicator Part_Of must denote a previously declared single "
& "protected type or single task type", Encap);
end Placement_Error;
-- Local variables
Conc_Typ : constant Entity_Id := Etype (Encap_Id);
Encap_Decl : constant Node_Id := Declaration_Node (Encap_Id);
Encap_Context : constant Node_Id := Parent (Encap_Decl);
Item_Context : Node_Id;
Item_Decl : Node_Id;
Prv_Decls : List_Id;
Vis_Decls : List_Id;
-- Start of processing for Check_Part_Of_Concurrent_Type
begin
-- Only abstract states and variables can act as constituents of an
-- encapsulating single concurrent type.
if Ekind (Item_Id) in E_Abstract_State | E_Variable then
null;
-- The constituent is a constant
elsif Ekind (Item_Id) = E_Constant then
Error_Msg_Name_1 := Chars (Encap_Id);
SPARK_Msg_NE
(Fix_Msg (Conc_Typ, "constant & cannot act as constituent of "
& "single protected type %"), Indic, Item_Id);
return;
-- The constituent is a package instantiation
else
Error_Msg_Name_1 := Chars (Encap_Id);
SPARK_Msg_NE
(Fix_Msg (Conc_Typ, "package instantiation & cannot act as "
& "constituent of single protected type %"), Indic, Item_Id);
return;
end if;
-- When the item denotes an abstract state of a nested package, use
-- the declaration of the package to detect proper placement.
-- package Pack is
-- task T;
-- package Nested
-- with Abstract_State => (State with Part_Of => T)
if Ekind (Item_Id) = E_Abstract_State then
Item_Decl := Unit_Declaration_Node (Scope (Item_Id));
else
Item_Decl := Declaration_Node (Item_Id);
end if;
Item_Context := Parent (Item_Decl);
-- The item and the single concurrent type must appear in the same
-- declarative region, with the item following the declaration of
-- the single concurrent type (SPARK RM 9(3)).
if Item_Context = Encap_Context then
if Nkind (Item_Context) in N_Package_Specification
| N_Protected_Definition
| N_Task_Definition
then
Prv_Decls := Private_Declarations (Item_Context);
Vis_Decls := Visible_Declarations (Item_Context);
-- The placement is OK when the single concurrent type appears
-- within the visible declarations and the item in the private
-- declarations.
--
-- package Pack is
-- protected PO ...
-- private
-- Constit : ... with Part_Of => PO;
-- end Pack;
if List_Containing (Encap_Decl) = Vis_Decls
and then List_Containing (Item_Decl) = Prv_Decls
then
null;
-- The placement is illegal when the item appears within the
-- visible declarations and the single concurrent type is in
-- the private declarations.
--
-- package Pack is
-- Constit : ... with Part_Of => PO;
-- private
-- protected PO ...
-- end Pack;
elsif List_Containing (Item_Decl) = Vis_Decls
and then List_Containing (Encap_Decl) = Prv_Decls
then
Placement_Error;
return;
-- Otherwise both the item and the single concurrent type are
-- in the same list. Ensure that the declaration of the single
-- concurrent type precedes that of the item.
elsif not In_Proper_Order
(First => Encap_Decl,
Second => Item_Decl)
then
Placement_Error;
return;
end if;
-- Otherwise both the item and the single concurrent type are
-- in the same list. Ensure that the declaration of the single
-- concurrent type precedes that of the item.
elsif not In_Proper_Order
(First => Encap_Decl,
Second => Item_Decl)
then
Placement_Error;
return;
end if;
-- Otherwise the item and the single concurrent type reside within
-- unrelated regions.
else
Error_Msg_Name_1 := Chars (Encap_Id);
SPARK_Msg_NE
(Fix_Msg (Conc_Typ, "constituent & must be declared "
& "immediately within the same region as single protected "
& "type %"), Indic, Item_Id);
return;
end if;
-- At this point it is known that the Part_Of indicator is legal
Legal := True;
end Check_Part_Of_Concurrent_Type;
-- Start of processing for Analyze_Part_Of
begin
-- Assume that the indicator is illegal
Encap_Id := Empty;
Legal := False;
if Nkind (Encap) in
N_Expanded_Name | N_Identifier | N_Selected_Component
then
Analyze (Encap);
Resolve_State (Encap);
Encap_Id := Entity (Encap);
-- The encapsulator is an abstract state
if Ekind (Encap_Id) = E_Abstract_State then
null;
-- The encapsulator is a single concurrent type (SPARK RM 9.3)
elsif Is_Single_Concurrent_Object (Encap_Id) then
null;
-- Otherwise the encapsulator is not a legal choice
else
SPARK_Msg_N
("indicator Part_Of must denote abstract state, single "
& "protected type or single task type", Encap);
return;
end if;
-- This is a syntax error, always report
else
Error_Msg_N
("indicator Part_Of must denote abstract state, single protected "
& "type or single task type", Encap);
return;
end if;
-- Catch a case where indicator Part_Of denotes the abstract view of a
-- variable which appears as an abstract state (SPARK RM 10.1.2 2).
if From_Limited_With (Encap_Id)
and then Present (Non_Limited_View (Encap_Id))
and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable
then
SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap);
SPARK_Msg_N ("\& denotes abstract view of object", Encap);
return;
end if;
-- The encapsulator is an abstract state
if Ekind (Encap_Id) = E_Abstract_State then
Check_Part_Of_Abstract_State;
-- The encapsulator is a single concurrent type
else
Check_Part_Of_Concurrent_Type;
end if;
end Analyze_Part_Of;
----------------------------------
-- Analyze_Part_Of_In_Decl_Part --
----------------------------------
procedure Analyze_Part_Of_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty)
is
Encap : constant Node_Id :=
Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
Errors : constant Nat := Serious_Errors_Detected;
Var_Decl : constant Node_Id := Find_Related_Context (N);
Var_Id : constant Entity_Id := Defining_Entity (Var_Decl);
Constits : Elist_Id;
Encap_Id : Entity_Id;
Legal : Boolean;
begin
-- Detect any discrepancies between the placement of the variable with
-- respect to general state space and the encapsulating state or single
-- concurrent type.
Analyze_Part_Of
(Indic => N,
Item_Id => Var_Id,
Encap => Encap,
Encap_Id => Encap_Id,
Legal => Legal);
-- The Part_Of indicator turns the variable into a constituent of the
-- encapsulating state or single concurrent type.
if Legal then
pragma Assert (Present (Encap_Id));
Constits := Part_Of_Constituents (Encap_Id);
if No (Constits) then
Constits := New_Elmt_List;
Set_Part_Of_Constituents (Encap_Id, Constits);
end if;
Append_Elmt (Var_Id, Constits);
Set_Encapsulating_State (Var_Id, Encap_Id);
-- A Part_Of constituent partially refines an abstract state. This
-- property does not apply to protected or task units.
if Ekind (Encap_Id) = E_Abstract_State then
Set_Has_Partial_Visible_Refinement (Encap_Id);
end if;
end if;
-- Emit a clarification message when the encapsulator is undefined,
-- possibly due to contract freezing.
if Errors /= Serious_Errors_Detected
and then Present (Freeze_Id)
and then Has_Undefined_Reference (Encap)
then
Contract_Freeze_Error (Var_Id, Freeze_Id);
end if;
end Analyze_Part_Of_In_Decl_Part;
--------------------
-- Analyze_Pragma --
--------------------
procedure Analyze_Pragma (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Pname : Name_Id := Pragma_Name (N);
-- Name of the source pragma, or name of the corresponding aspect for
-- pragmas which originate in a source aspect. In the latter case, the
-- name may be different from the pragma name.
Prag_Id : constant Pragma_Id := Get_Pragma_Id (Pname);
Pragma_Exit : exception;
-- This exception is used to exit pragma processing completely. It
-- is used when an error is detected, and no further processing is
-- required. It is also used if an earlier error has left the tree in
-- a state where the pragma should not be processed.
Arg_Count : Nat;
-- Number of pragma argument associations
Arg1 : Node_Id;
Arg2 : Node_Id;
Arg3 : Node_Id;
Arg4 : Node_Id;
Arg5 : Node_Id;
-- First five pragma arguments (pragma argument association nodes, or
-- Empty if the corresponding argument does not exist).
type Name_List is array (Natural range <>) of Name_Id;
type Args_List is array (Natural range <>) of Node_Id;
-- Types used for arguments to Check_Arg_Order and Gather_Associations
-----------------------
-- Local Subprograms --
-----------------------
procedure Ada_2005_Pragma;
-- Called for pragmas defined in Ada 2005, that are not in Ada 95. In
-- Ada 95 mode, these are implementation defined pragmas, so should be
-- caught by the No_Implementation_Pragmas restriction.
procedure Ada_2012_Pragma;
-- Called for pragmas defined in Ada 2012, that are not in Ada 95 or 05.
-- In Ada 95 or 05 mode, these are implementation defined pragmas, so
-- should be caught by the No_Implementation_Pragmas restriction.
procedure Analyze_Depends_Global
(Spec_Id : out Entity_Id;
Subp_Decl : out Node_Id;
Legal : out Boolean);
-- Subsidiary to the analysis of pragmas Depends and Global. Verify the
-- legality of the placement and related context of the pragma. Spec_Id
-- is the entity of the related subprogram. Subp_Decl is the declaration
-- of the related subprogram. Sets flag Legal when the pragma is legal.
procedure Analyze_If_Present (Id : Pragma_Id);
-- Inspect the remainder of the list containing pragma N and look for
-- a pragma that matches Id. If found, analyze the pragma.
procedure Analyze_Pre_Post_Condition;
-- Subsidiary to the analysis of pragmas Precondition and Postcondition
procedure Analyze_Refined_Depends_Global_Post
(Spec_Id : out Entity_Id;
Body_Id : out Entity_Id;
Legal : out Boolean);
-- Subsidiary routine to the analysis of body pragmas Refined_Depends,
-- Refined_Global and Refined_Post. Verify the legality of the placement
-- and related context of the pragma. Spec_Id is the entity of the
-- related subprogram. Body_Id is the entity of the subprogram body.
-- Flag Legal is set when the pragma is legal.
procedure Analyze_Unmodified_Or_Unused (Is_Unused : Boolean := False);
-- Perform full analysis of pragma Unmodified and the write aspect of
-- pragma Unused. Flag Is_Unused should be set when verifying the
-- semantics of pragma Unused.
procedure Analyze_Unreferenced_Or_Unused (Is_Unused : Boolean := False);
-- Perform full analysis of pragma Unreferenced and the read aspect of
-- pragma Unused. Flag Is_Unused should be set when verifying the
-- semantics of pragma Unused.
procedure Check_Ada_83_Warning;
-- Issues a warning message for the current pragma if operating in Ada
-- 83 mode (used for language pragmas that are not a standard part of
-- Ada 83). This procedure does not raise Pragma_Exit. Also notes use
-- of 95 pragma.
procedure Check_Arg_Count (Required : Nat);
-- Check argument count for pragma is equal to given parameter. If not,
-- then issue an error message and raise Pragma_Exit.
-- Note: all routines whose name is Check_Arg_Is_xxx take an argument
-- Arg which can either be a pragma argument association, in which case
-- the check is applied to the expression of the association or an
-- expression directly.
procedure Check_Arg_Is_External_Name (Arg : Node_Id);
-- Check that an argument has the right form for an EXTERNAL_NAME
-- parameter of an extended import/export pragma. The rule is that the
-- name must be an identifier or string literal (in Ada 83 mode) or a
-- static string expression (in Ada 95 mode).
procedure Check_Arg_Is_Identifier (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it is an
-- identifier. If not give error and raise Pragma_Exit.
procedure Check_Arg_Is_Integer_Literal (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it is an integer
-- literal. If not give error and raise Pragma_Exit.
procedure Check_Arg_Is_Library_Level_Local_Name (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it has the proper
-- syntactic form for a local name and meets the semantic requirements
-- for a local name. The local name is analyzed as part of the
-- processing for this call. In addition, the local name is required
-- to represent an entity at the library level.
procedure Check_Arg_Is_Local_Name (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it has the proper
-- syntactic form for a local name and meets the semantic requirements
-- for a local name. The local name is analyzed as part of the
-- processing for this call.
procedure Check_Arg_Is_Locking_Policy (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it is a valid
-- locking policy name. If not give error and raise Pragma_Exit.
procedure Check_Arg_Is_Partition_Elaboration_Policy (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it is a valid
-- elaboration policy name. If not give error and raise Pragma_Exit.
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2 : Name_Id);
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2, N3 : Name_Id);
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2, N3, N4 : Name_Id);
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2, N3, N4, N5 : Name_Id);
-- Check the specified argument Arg to make sure that it is an
-- identifier whose name matches either N1 or N2 (or N3, N4, N5 if
-- present). If not then give error and raise Pragma_Exit.
procedure Check_Arg_Is_Queuing_Policy (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it is a valid
-- queuing policy name. If not give error and raise Pragma_Exit.
procedure Check_Arg_Is_OK_Static_Expression
(Arg : Node_Id;
Typ : Entity_Id := Empty);
-- Check the specified argument Arg to make sure that it is a static
-- expression of the given type (i.e. it will be analyzed and resolved
-- using this type, which can be any valid argument to Resolve, e.g.
-- Any_Integer is OK). If not, given error and raise Pragma_Exit. If
-- Typ is left Empty, then any static expression is allowed. Includes
-- checking that the argument does not raise Constraint_Error.
procedure Check_Arg_Is_Task_Dispatching_Policy (Arg : Node_Id);
-- Check the specified argument Arg to make sure that it is a valid task
-- dispatching policy name. If not give error and raise Pragma_Exit.
procedure Check_Arg_Order (Names : Name_List);
-- Checks for an instance of two arguments with identifiers for the
-- current pragma which are not in the sequence indicated by Names,
-- and if so, generates a fatal message about bad order of arguments.
procedure Check_At_Least_N_Arguments (N : Nat);
-- Check there are at least N arguments present
procedure Check_At_Most_N_Arguments (N : Nat);
-- Check there are no more than N arguments present
procedure Check_Component
(Comp : Node_Id;
UU_Typ : Entity_Id;
In_Variant_Part : Boolean := False);
-- Examine an Unchecked_Union component for correct use of per-object
-- constrained subtypes, and for restrictions on finalizable components.
-- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part
-- should be set when Comp comes from a record variant.
procedure Check_Duplicate_Pragma (E : Entity_Id);
-- Check if a rep item of the same name as the current pragma is already
-- chained as a rep pragma to the given entity. If so give a message
-- about the duplicate, and then raise Pragma_Exit so does not return.
-- Note that if E is a type, then this routine avoids flagging a pragma
-- which applies to a parent type from which E is derived.
procedure Check_Duplicated_Export_Name (Nam : Node_Id);
-- Nam is an N_String_Literal node containing the external name set by
-- an Import or Export pragma (or extended Import or Export pragma).
-- This procedure checks for possible duplications if this is the export
-- case, and if found, issues an appropriate error message.
procedure Check_Expr_Is_OK_Static_Expression
(Expr : Node_Id;
Typ : Entity_Id := Empty);
-- Check the specified expression Expr to make sure that it is a static
-- expression of the given type (i.e. it will be analyzed and resolved
-- using this type, which can be any valid argument to Resolve, e.g.
-- Any_Integer is OK). If not, given error and raise Pragma_Exit. If
-- Typ is left Empty, then any static expression is allowed. Includes
-- checking that the expression does not raise Constraint_Error.
procedure Check_First_Subtype (Arg : Node_Id);
-- Checks that Arg, whose expression is an entity name, references a
-- first subtype.
procedure Check_Identifier (Arg : Node_Id; Id : Name_Id);
-- Checks that the given argument has an identifier, and if so, requires
-- it to match the given identifier name. If there is no identifier, or
-- a non-matching identifier, then an error message is given and
-- Pragma_Exit is raised.
procedure Check_Identifier_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id);
-- Checks that the given argument has an identifier, and if so, requires
-- it to match one of the given identifier names. If there is no
-- identifier, or a non-matching identifier, then an error message is
-- given and Pragma_Exit is raised.
procedure Check_In_Main_Program;
-- Common checks for pragmas that appear within a main program
-- (Priority, Main_Storage, Time_Slice, Relative_Deadline, CPU).
procedure Check_Interrupt_Or_Attach_Handler;
-- Common processing for first argument of pragma Interrupt_Handler or
-- pragma Attach_Handler.
procedure Check_Loop_Pragma_Placement;
-- Verify whether pragmas Loop_Invariant, Loop_Optimize and Loop_Variant
-- appear immediately within a construct restricted to loops, and that
-- pragmas Loop_Invariant and Loop_Variant are grouped together.
procedure Check_Is_In_Decl_Part_Or_Package_Spec;
-- Check that pragma appears in a declarative part, or in a package
-- specification, i.e. that it does not occur in a statement sequence
-- in a body.
procedure Check_No_Identifier (Arg : Node_Id);
-- Checks that the given argument does not have an identifier. If
-- an identifier is present, then an error message is issued, and
-- Pragma_Exit is raised.
procedure Check_No_Identifiers;
-- Checks that none of the arguments to the pragma has an identifier.
-- If any argument has an identifier, then an error message is issued,
-- and Pragma_Exit is raised.
procedure Check_No_Link_Name;
-- Checks that no link name is specified
procedure Check_Optional_Identifier (Arg : Node_Id; Id : Name_Id);
-- Checks if the given argument has an identifier, and if so, requires
-- it to match the given identifier name. If there is a non-matching
-- identifier, then an error message is given and Pragma_Exit is raised.
procedure Check_Optional_Identifier (Arg : Node_Id; Id : String);
-- Checks if the given argument has an identifier, and if so, requires
-- it to match the given identifier name. If there is a non-matching
-- identifier, then an error message is given and Pragma_Exit is raised.
-- In this version of the procedure, the identifier name is given as
-- a string with lower case letters.
procedure Check_Static_Boolean_Expression (Expr : Node_Id);
-- Subsidiary to the analysis of pragmas Async_Readers, Async_Writers,
-- Constant_After_Elaboration, Effective_Reads, Effective_Writes,
-- Extensions_Visible and Volatile_Function. Ensure that expression Expr
-- is an OK static boolean expression. Emit an error if this is not the
-- case.
procedure Check_Static_Constraint (Constr : Node_Id);
-- Constr is a constraint from an N_Subtype_Indication node from a
-- component constraint in an Unchecked_Union type, a range, or a
-- discriminant association. This routine checks that the constraint
-- is static as required by the restrictions for Unchecked_Union.
procedure Check_Valid_Configuration_Pragma;
-- Legality checks for placement of a configuration pragma
procedure Check_Valid_Library_Unit_Pragma;
-- Legality checks for library unit pragmas. A special case arises for
-- pragmas in generic instances that come from copies of the original
-- library unit pragmas in the generic templates. In the case of other
-- than library level instantiations these can appear in contexts which
-- would normally be invalid (they only apply to the original template
-- and to library level instantiations), and they are simply ignored,
-- which is implemented by rewriting them as null statements and
-- optionally raising Pragma_Exit to terminate analysis. An exception
-- is not always raised to avoid exception propagation during the
-- bootstrap, so all callers should check whether N has been rewritten.
procedure Check_Variant (Variant : Node_Id; UU_Typ : Entity_Id);
-- Check an Unchecked_Union variant for lack of nested variants and
-- presence of at least one component. UU_Typ is the related Unchecked_
-- Union type.
procedure Ensure_Aggregate_Form (Arg : Node_Id);
-- Subsidiary routine to the processing of pragmas Abstract_State,
-- Contract_Cases, Depends, Global, Initializes, Refined_Depends,
-- Refined_Global, Refined_State and Subprogram_Variant. Transform
-- argument Arg into an aggregate if not one already. N_Null is never
-- transformed. Arg may denote an aspect specification or a pragma
-- argument association.
procedure Error_Pragma (Msg : String);
pragma No_Return (Error_Pragma);
-- Outputs error message for current pragma. The message contains a %
-- that will be replaced with the pragma name, and the flag is placed
-- on the pragma itself. Pragma_Exit is then raised. Note: this routine
-- calls Fix_Error (see spec of that procedure for details).
procedure Error_Pragma_Arg (Msg : String; Arg : Node_Id);
pragma No_Return (Error_Pragma_Arg);
-- Outputs error message for current pragma. The message may contain
-- a % that will be replaced with the pragma name. The parameter Arg
-- may either be a pragma argument association, in which case the flag
-- is placed on the expression of this association, or an expression,
-- in which case the flag is placed directly on the expression. The
-- message is placed using Error_Msg_N, so the message may also contain
-- an & insertion character which will reference the given Arg value.
-- After placin