Google Git
Sign in
gnu / gcc / 926d9947847a0683cf34de6fc231209747576088 / . / gcc / ada / sem_prag.adb
blob: 4fe9007aacbe8473a4512432f907bb2ed72ab01c [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ P R A G --
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2015, 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 Csets; use Csets;
with Debug; use Debug;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
with Exp_Dist; use Exp_Dist;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
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_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.CN; use Sinfo.CN;
with Sinput; use Sinput;
with Stringt; use Stringt;
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;
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 --
-------------------------------------
procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id);
-- Subsidiary routine to the analysis of pragmas Depends, Global and
-- Refined_State. Append an entity to a list. If the list is empty, create
-- a new list.
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.
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.
function Check_Kind (Nam : Name_Id) return Name_Id;
-- This function is used in connection with pragmas Assert, Check,
-- and assertion aspects and pragmas, to determine if Check pragmas
-- (or corresponding assertion aspects or pragmas) are currently active
-- as determined by the presence of -gnata on the command line (which
-- sets the default), and the appearance of pragmas Check_Policy and
-- Assertion_Policy as configuration pragmas either in a configuration
-- pragma file, or at the start of the current unit, or locally given
-- Check_Policy and Assertion_Policy pragmas that are currently active.
--
-- The value returned is one of the names Check, Ignore, Disable (On
-- returns Check, and Off returns Ignore).
--
-- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
-- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
-- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
-- _Post, _Invariant, or _Type_Invariant, which are special names used
-- in identifiers to represent these attribute references.
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Subp_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 Subp_Id subject to Inline_Always.
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 Duplication_Error (Prag : Node_Id; Prev : Node_Id);
-- Subsidiary to routines Find_Related_Package_Or_Body and
-- Find_Related_Subprogram_Or_Body. Emit an error on pragma Prag that
-- duplicates previous pragma Prev.
function Find_Related_Package_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas Abstract_State, Initial_Condition,
-- Initializes and Refined_State. Find the declaration of the related
-- package [body] subject to pragma Prag. The return value is either
-- N_Package_Declaration, N_Package_Body or Empty if the placement of
-- the pragma is illegal. If flag Do_Checks is set, the routine reports
-- duplicate pragmas.
function Get_Argument
(Prag : Node_Id;
Spec_Id : Entity_Id := Empty) return Node_Id;
-- Obtain the argument of pragma Prag depending on context and the nature
-- of the pragma. The argument is extracted in the following manner:
--
-- When the pragma is generated from an aspect, return the corresponding
-- aspect for ASIS or when Spec_Id denotes a generic subprogram.
--
-- Otherwise return the first argument of Prag
--
-- Spec_Id denotes the entity of the subprogram spec where Prag resides
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_Type. 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);
-- 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.
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.
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.
--------------
-- Add_Item --
--------------
procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id) is
begin
Append_New_Elmt (Item, To => To_List);
end Add_Item;
-------------------------------
-- 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 >= Get_Char_Code ('a')
and then CC <= Get_Char_Code ('z')
then
Store_String_Char (CC - 32);
elsif Opt.External_Name_Exp_Casing = Lowercase
and then CC >= Get_Char_Code ('A')
and then CC <= 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 --
-----------------------------------------
procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id) is
Others_Seen : Boolean := False;
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;
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
Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
end if;
Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
-- The contract case is malformed
else
Error_Msg_N ("wrong syntax in contract case", CCase);
end if;
end Analyze_Contract_Case;
-- Local variables
All_Cases : Node_Id;
CCase : Node_Id;
Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
Restore_Scope : Boolean := False;
-- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
begin
Set_Analyzed (N);
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
Subp_Id := Defining_Entity (Subp_Decl);
All_Cases := Expression (Get_Argument (N, Subp_Id));
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser of the analysis of the
-- pragma failed to produce an aggregate.
pragma Assert (Nkind (All_Cases) = N_Aggregate);
if Present (Component_Associations (All_Cases)) then
-- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining
-- to subprogram declarations. Skip the installation for subprogram
-- bodies because the formals are already visible.
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 (All_Cases));
while Present (CCase) loop
Analyze_Contract_Case (CCase);
Next (CCase);
end loop;
-- 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);
if Restore_Scope then
End_Scope;
end if;
else
Error_Msg_N ("wrong syntax for constract cases", N);
end if;
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);
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 Subp_Id'Result is processed
Spec_Id : Entity_Id;
-- The entity of the subprogram subject to pragma [Refined_]Depends
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_Id : Entity_Id;
-- The entity of the subprogram [body or stub] subject to 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.
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_In_Parameter - "parameter"
-- E_In_Out_Parameter - "parameter"
-- E_Out_Parameter - "parameter"
-- 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 fulfils 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 Is_Formal (Item_Id) then
Add_Str_To_Name_Buffer ("parameter");
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, variables 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
Is_Output : constant Boolean := not Is_Input;
Grouped : Node_Id;
Item_Id : Entity_Id;
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 Function'Result in the context of a dependency clause
elsif Is_Attribute_Result (Item) then
Non_Null_Seen := True;
-- It is sufficent to analyze the prefix of 'Result in order to
-- establish legality of the attribute.
Analyze (Prefix (Item));
-- The prefix of 'Result must denote the function for which
-- pragma Depends applies (SPARK RM 6.1.5(11)).
if not Is_Entity_Name (Prefix (Item))
or else Ekind (Spec_Id) /= E_Function
or else Entity (Prefix (Item)) /= Spec_Id
then
Error_Msg_Name_1 := Name_Result;
SPARK_Msg_N
("prefix of attribute % must denote the enclosing "
& "function", Item);
-- Function'Result is allowed to appear on the output side of a
-- dependency clause (SPARK RM 6.1.5(6)).
elsif 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
if Ekind_In (Item_Id, E_Abstract_State,
E_In_Parameter,
E_In_Out_Parameter,
E_Out_Parameter,
E_Variable)
then
-- Ensure that the item fulfils 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
Add_Item (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
Add_Item (Item_Id, All_Inputs_Seen);
end if;
-- State related checks (SPARK RM 6.1.5(3))
if Ekind (Item_Id) = E_Abstract_State then
if 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;
-- 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;
end if;
-- When the item renames an entire object, replace the
-- item with a reference to the object.
if Present (Renamed_Object (Entity (Item))) 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
Add_Item (Item_Id, States_Seen);
end if;
if Ekind_In (Item_Id, E_Abstract_State, E_Variable)
and then Present (Encapsulating_State (Item_Id))
then
Add_Item (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, or state",
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, or state", 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) = E_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
begin
Item_Is_Input := False;
Item_Is_Output := False;
-- Abstract state cases
if Ekind (Item_Id) = E_Abstract_State then
-- When pragma Global is present, the mode of the state may be
-- further constrained by setting a more restrictive mode.
if Global_Seen then
if Appears_In (Subp_Inputs, Item_Id) then
Item_Is_Input := True;
end if;
if Appears_In (Subp_Outputs, Item_Id) then
Item_Is_Output := True;
end if;
-- Otherwise the state has a default IN OUT mode
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
-- Parameter cases
elsif Ekind (Item_Id) = E_In_Parameter then
Item_Is_Input := True;
elsif Ekind (Item_Id) = E_In_Out_Parameter then
Item_Is_Input := True;
Item_Is_Output := True;
elsif Ekind (Item_Id) = E_Out_Parameter then
if Scope (Item_Id) = Spec_Id then
-- An OUT parameter of the related subprogram has mode IN
-- if its type is unconstrained or tagged because array
-- bounds, discriminants or tags can be read.
if Is_Unconstrained_Or_Tagged_Item (Item_Id) then
Item_Is_Input := True;
end if;
Item_Is_Output := True;
-- An OUT parameter of an enclosing subprogram behaves as a
-- read-write variable in which case the mode is IN OUT.
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
-- Variable cases
else pragma Assert (Ekind (Item_Id) = E_Variable);
-- When pragma Global is present, the mode of the variable may
-- be further constrained by setting a more restrictive mode.
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.
if Appears_In (Subp_Inputs, Item_Id)
or else Is_Unconstrained_Or_Tagged_Item (Item_Id)
then
Item_Is_Input := True;
end if;
if Appears_In (Subp_Outputs, Item_Id) then
Item_Is_Output := True;
end if;
-- Otherwise the variable has a default IN OUT mode
else
Item_Is_Input := True;
Item_Is_Output := True;
end if;
end if;
end Find_Role;
----------------
-- Role_Error --
----------------
procedure Role_Error
(Item_Is_Input : Boolean;
Item_Is_Output : Boolean)
is
Error_Msg : Name_Id;
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");
Error_Msg := Name_Find;
SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
Error_Msg_Name_1 := Chars (Subp_Id);
SPARK_Msg_NE
("\& 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");
Error_Msg := Name_Find;
SPARK_Msg_NE (Get_Name_String (Error_Msg), 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 : Node_Id; Item_Id : Entity_Id);
-- Emit an error concerning the illegal usage of an item
-----------------
-- Usage_Error --
-----------------
procedure Usage_Error (Item : Node_Id; Item_Id : Entity_Id) is
Error_Msg : Name_Id;
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(8)).
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
(" & must appear in at least one input dependence list");
Error_Msg := Name_Find;
SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, 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
(" & must appear in exactly one output dependence list");
Error_Msg := Name_Find;
SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, 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, Item_Id);
-- States and global variables are not used properly only when
-- the subprogram is subject to pragma Global.
elsif Global_Seen then
Usage_Error (Item, 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 -
-- we 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 it 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
Clause : Node_Id;
Deps : Node_Id;
Errors : Nat;
Last_Clause : Node_Id;
Subp_Decl : Node_Id;
Restore_Scope : Boolean := False;
-- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
-- Start of processing for Analyze_Depends_In_Decl_Part
begin
Set_Analyzed (N);
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
Deps := Expression (Get_Argument (N, Subp_Id));
-- The logic in this routine is used to analyze both pragma Depends and
-- pragma Refined_Depends since they have the same syntax and base
-- semantics. Find the entity of the corresponding spec when analyzing
-- Refined_Depends.
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-- Empty dependency list
if Nkind (Deps) = N_Null then
-- Gather all states, variables 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
return;
end if;
if Present (Component_Associations (Deps)) then
Last_Clause := Last (Component_Associations (Deps));
-- Gather all states, variables 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);
-- Ensure that the formal parameters are visible when analyzing
-- all clauses. This falls out of the general rule of aspects
-- pertaining to subprogram declarations. Skip the installation
-- for subprogram bodies because the formals are already visible.
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;
Clause := First (Component_Associations (Deps));
while Present (Clause) loop
Errors := Serious_Errors_Detected;
-- Normalization 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. Normalization is disabled
-- in ASIS mode as it alters the tree by introducing new nodes
-- similar to expansion.
if Serious_Errors_Detected = Errors and then not ASIS_Mode 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);
return;
end if;
-- The top level dependency relation is malformed. This is a syntax
-- error, always report.
else
Error_Msg_N ("malformed dependency relation", Deps);
return;
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);
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
Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1));
begin
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 not Is_Effectively_Volatile (Obj_Id) then
SPARK_Msg_N
("external property % must apply to a volatile object", N);
end if;
-- 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 (Expr) then
Analyze_And_Resolve (Expr, Standard_Boolean);
if Is_OK_Static_Expression (Expr) then
Expr_Val := Is_True (Expr_Value (Expr));
else
SPARK_Msg_N ("expression of % must be static", 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
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.
Spec_Id : Entity_Id;
-- The entity of the subprogram subject to pragma [Refined_]Global
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.
Subp_Id : Entity_Id;
-- The entity of the subprogram [body or stub] subject to 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.
-- 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. 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
("global item cannot reference parameter of subprogram",
Item, Spec_Id);
return;
end if;
-- A constant cannot act as a global item (SPARK RM 6.1.4(7)).
-- Do this check first to provide a better error diagnostic.
elsif Ekind (Item_Id) = E_Constant then
SPARK_Msg_N ("global item cannot denote a constant", Item);
-- A formal object may act as a global item inside a generic
elsif Is_Formal_Object (Item_Id) then
null;
-- The only legal references are those to abstract states and
-- variables (SPARK RM 6.1.4(4)).
elsif not Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
SPARK_Msg_N
("global item must denote variable or state", Item);
return;
end if;
-- State related checks
if Ekind (Item_Id) = E_Abstract_State then
-- 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(8)).
if 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;
-- 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;
-- 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 Is_Effectively_Volatile (Item_Id)
then
-- An effectively volatile object cannot appear as a global
-- item of a function (SPARK RM 7.1.3(9)).
if Ekind_In (Spec_Id, E_Function, E_Generic_Function) 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.
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 (SPARK RM 7.1.3(11))",
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 Present (Renamed_Object (Entity (Item))) 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 variable or state", Item);
return;
end if;
-- Verify that an output does not appear as an input in an
-- enclosing subprogram.
if Nam_In (Global_Mode, 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(11)).
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
Add_Item (Item_Id, Seen);
if Ekind (Item_Id) = E_Abstract_State then
Add_Item (Item_Id, States_Seen);
end if;
if Ekind_In (Item_Id, E_Abstract_State, E_Variable)
and then Present (Encapsulating_State (Item_Id))
then
Add_Item (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
-- subject to pragma [Refined_]Global.
Context := Scope (Subp_Id);
while Present (Context) and then Context /= Standard_Standard loop
if Is_Subprogram (Context)
and then
(Present (Get_Pragma (Context, Pragma_Global))
or else
Present (Get_Pragma (Context, Pragma_Refined_Global)))
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 in an enclosing subprogram (SPARK RM 6.1.4(12)).
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);
SPARK_Msg_NE
("\item already appears as input of subprogram &",
Item, Context);
-- 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) = E_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_In (List, 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 : Node_Id;
Subp_Decl : Node_Id;
Restore_Scope : Boolean := False;
-- Set True if we do a Push_Scope requiring a Pop_Scope on exit
-- Start of processing for Analyze_Global_In_Decl_Part
begin
Set_Analyzed (N);
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
Items := Expression (Get_Argument (N, Subp_Id));
-- The logic in this routine is used to analyze both pragma Global and
-- pragma Refined_Global since they have the same syntax and base
-- semantics. Find the entity of the corresponding spec when analyzing
-- Refined_Global.
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-- 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
-- Ensure that the formal parameters are visible when processing an
-- item. 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;
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);
end Analyze_Global_In_Decl_Part;
--------------------------------------------
-- Analyze_Initial_Condition_In_Decl_Part --
--------------------------------------------
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
Expr : constant Node_Id := Expression (Get_Argument (N));
begin
Set_Analyzed (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);
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
-- Analyze_Initializes_In_Decl_Part --
--------------------------------------
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id) is
Pack_Spec : constant Node_Id := Parent (N);
Pack_Id : constant Entity_Id := Defining_Entity (Parent (Pack_Spec));
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.
Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False;
-- Flags used to check the legality of a null initialization list
States_And_Vars : Elist_Id := No_Elist;
-- A list of all abstract states and variables 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_Variables;
-- Inspect the visible declarations of the related package and gather
-- the entities of all abstract states and variables in States_And_Vars.
---------------------------------
-- Analyze_Initialization_Item --
---------------------------------
procedure Analyze_Initialization_Item (Item : Node_Id) is
Item_Id : Entity_Id;
begin
-- Null initialization list
if Nkind (Item) = 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 items", Item);
else
Null_Seen := True;
end if;
-- Initialization item
else
Non_Null_Seen := True;
if Null_Seen then
SPARK_Msg_N
("cannot mix null and non-null initialization items", Item);
end if;
Analyze (Item);
Resolve_State (Item);
if Is_Entity_Name (Item) then
Item_Id := Entity_Of (Item);
if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
-- The state or variable must be declared in the visible
-- declarations of the package (SPARK RM 7.1.5(7)).
if not Contains (States_And_Vars, 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
Add_Item (Item_Id, Items_Seen);
if Ekind (Item_Id) = E_Abstract_State then
Add_Item (Item_Id, States_Seen);
end if;
if Present (Encapsulating_State (Item_Id)) then
Add_Item (Item_Id, Constits_Seen);
end if;
end if;
-- The item references something that is not a state or a
-- variable (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
("initialization item must denote variable 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 variable or state", Item);
end if;
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 Ekind_In (Input_Id, E_Abstract_State,
E_In_Parameter,
E_In_Out_Parameter,
E_Out_Parameter,
E_Variable)
then
-- The input cannot denote states or variables declared
-- within the related package.
if Within_Scope (Input_Id, Current_Scope) then
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("input item & cannot denote a visible variable or "
& "state of package % (SPARK RM 7.1.5(4))",
Input, Input_Id);
-- Detect a duplicate use of the same input item
-- (SPARK RM 7.1.5(5)).
elsif Contains (Inputs_Seen, Input_Id) then
SPARK_Msg_N ("duplicate input item", Input);
-- Input is legal, add it to the list of processed inputs
else
Add_Item (Input_Id, Inputs_Seen);
if Ekind (Input_Id) = E_Abstract_State then
Add_Item (Input_Id, States_Seen);
end if;
if Ekind_In (Input_Id, E_Abstract_State, E_Variable)
and then Present (Encapsulating_State (Input_Id))
then
Add_Item (Input_Id, Constits_Seen);
end if;
end if;
-- The input references something that is not a state or a
-- variable (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
("input item must denote variable or state", Input);
end if;
-- Some form of illegal construct masquerading as a name
-- (SPARK RM 7.1.5(3)).
else
SPARK_Msg_N
("input item must denote variable 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_Variables --
----------------------------------
procedure Collect_States_And_Variables is
Decl : Node_Id;
begin
-- Collect the abstract states defined in the package (if any)
if Present (Abstract_States (Pack_Id)) then
States_And_Vars := New_Copy_Elist (Abstract_States (Pack_Id));
end if;
-- Collect all variables the 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 Nkind (Decl) = N_Object_Declaration
and then Ekind (Defining_Entity (Decl)) = E_Variable
and then Comes_From_Source (Decl)
then
Add_Item (Defining_Entity (Decl), States_And_Vars);
end if;
Next (Decl);
end loop;
end if;
end Collect_States_And_Variables;
-- Local variables
Inits : constant Node_Id := Expression (Get_Argument (N));
Init : Node_Id;
-- Start of processing for Analyze_Initializes_In_Decl_Part
begin
Set_Analyzed (N);
-- 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_Variables;
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);
end Analyze_Initializes_In_Decl_Part;
--------------------
-- Analyze_Pragma --
--------------------
procedure Analyze_Pragma (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
Prag_Id : Pragma_Id;
Pname : Name_Id;
-- 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.
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;
-- First four 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 Acquire_Warning_Match_String (Arg : Node_Id);
-- Used by pragma Warnings (Off, string), and Warn_As_Error (string) to
-- get the given string argument, and place it in Name_Buffer, adding
-- leading and trailing asterisks if they are not already present. The
-- caller has already checked that Arg is a static string expression.
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_Part_Of
(Item_Id : Entity_Id;
State : Node_Id;
Indic : Node_Id;
Legal : out Boolean);
-- Subsidiary to the analysis of pragmas Abstract_State and Part_Of.
-- Perform full analysis of indicator Part_Of. Item_Id is the entity of
-- an abstract state, variable or package instantiation. State is the
-- encapsulating state. Indic is the Part_Of indicator. Flag Legal is
-- set when the indicator is legal.
procedure Analyze_Pre_Post_Condition;
-- Subsidiary to the analysis of pragmas Precondition and Postcondition
procedure Analyze_Refined_Pragma
(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. Check 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 properly placed.
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_Declaration_Order (First : Node_Id; Second : Node_Id);
-- Subsidiary routine to the analysis of pragmas Abstract_State,
-- Initial_Condition and Initializes. Determine whether pragma First
-- appears before pragma Second. If this is not the case, emit an error.
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_Constraint (Constr : Node_Id);
-- Constr is a constraint from an N_Subtype_Indication node from a
-- component constraint in an Unchecked_Union type. 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.
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 Create_Generic_Template
(Prag : Node_Id;
Subp_Id : Entity_Id);
-- Subsidiary routine to the processing of pragmas Contract_Cases,
-- Depends, Global, Postcondition, Precondition and Test_Case. Create
-- a generic template for pragma Prag when Prag is a source construct
-- and the related context denoted by Subp_Id is a generic subprogram.
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 and Refined_State. 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 placing the message, Pragma_Exit is raised. Note: this routine
-- calls Fix_Error (see spec of that procedure for details).
procedure Error_Pragma_Arg (Msg1, Msg2 : String; Arg : Node_Id);
pragma No_Return (Error_Pragma_Arg);
-- Similar to above form of Error_Pragma_Arg except that two messages
-- are provided, the second is a continuation comment starting with \.
procedure Error_Pragma_Arg_Ident (Msg : String; Arg : Node_Id);
pragma No_Return (Error_Pragma_Arg_Ident);
-- Outputs error message for current pragma. The message may contain a %
-- that will be replaced with the pragma name. The parameter Arg must be
-- a pragma argument association with a non-empty identifier (i.e. its
-- Chars field must be set), and the error message is placed on the
-- identifier. The message is placed using Error_Msg_N so the message
-- may also contain an & insertion character which will reference
-- the identifier. After placing the message, Pragma_Exit is raised.
-- Note: this routine calls Fix_Error (see spec of that procedure for
-- details).
procedure Error_Pragma_Ref (Msg : String; Ref : Entity_Id);
pragma No_Return (Error_Pragma_Ref);
-- Outputs error message for current pragma. The message may contain
-- a % that will be replaced with the pragma name. The parameter Ref
-- must be an entity whose name can be referenced by & and sloc by #.
-- After placing the message, Pragma_Exit is raised. Note: this routine
-- calls Fix_Error (see spec of that procedure for details).
function Find_Lib_Unit_Name return Entity_Id;
-- Used for a library unit pragma to find the entity to which the
-- library unit pragma applies, returns the entity found.
procedure Find_Program_Unit_Name (Id : Node_Id);
-- If the pragma is a compilation unit pragma, the id must denote the
-- compilation unit in the same compilation, and the pragma must appear
-- in the list of preceding or trailing pragmas. If it is a program
-- unit pragma that is not a compilation unit pragma, then the
-- identifier must be visible.
function Find_Unique_Parameterless_Procedure
(Name : Entity_Id;
Arg : Node_Id) return Entity_Id;
-- Used for a procedure pragma to find the unique parameterless
-- procedure identified by Name, returns it if it exists, otherwise
-- errors out and uses Arg as the pragma argument for the message.
function Fix_Error (Msg : String) return String;
-- This is called prior to issuing an error message. Msg is the normal
-- error message issued in the pragma case. This routine checks for the
-- case of a pragma coming from an aspect in the source, and returns a
-- message suitable for the aspect case as follows:
--
-- Each substring "pragma" is replaced by "aspect"
--
-- If "argument of" is at the start of the error message text, it is
-- replaced by "entity for".
--
-- If "argument" is at the start of the error message text, it is
-- replaced by "entity".
--
-- So for example, "argument of pragma X must be discrete type"
-- returns "entity for aspect X must be a discrete type".
-- Finally Error_Msg_Name_1 is set to the name of the aspect (which may
-- be different from the pragma name). If the current pragma results
-- from rewriting another pragma, then Error_Msg_Name_1 is set to the
-- original pragma name.
procedure Gather_Associations
(Names : Name_List;
Args : out Args_List);
-- This procedure is used to gather the arguments for a pragma that
-- permits arbitrary ordering of parameters using the normal rules
-- for named and positional parameters. The Names argument is a list
-- of Name_Id values that corresponds to the allowed pragma argument
-- association identifiers in order. The result returned in Args is
-- a list of corresponding expressions that are the pragma arguments.
-- Note that this is a list of expressions, not of pragma argument
-- associations (Gather_Associations has completely checked all the
-- optional identifiers when it returns). An entry in Args is Empty
-- on return if the corresponding argument is not present.
procedure GNAT_Pragma;
-- Called for all GNAT defined pragmas to check the relevant restriction
-- (No_Implementation_Pragmas).
function Is_Before_First_Decl
(Pragma_Node : Node_Id;
Decls : List_Id) return Boolean;
-- Return True if Pragma_Node is before the first declarative item in
-- Decls where Decls is the list of declarative items.
function Is_Configuration_Pragma return Boolean;
-- Determines if the placement of the current pragma is appropriate
-- for a configuration pragma.
function Is_In_Context_Clause return Boolean;
-- Returns True if pragma appears within the context clause of a unit,
-- and False for any other placement (does not generate any messages).
function Is_Static_String_Expression (Arg : Node_Id) return Boolean;
-- Analyzes the argument, and determines if it is a static string
-- expression, returns True if so, False if non-static or not String.
-- A special case is that a string literal returns True in Ada 83 mode
-- (which has no such thing as static string expressions). Note that
-- the call analyzes its argument, so this cannot be used for the case
-- where an identifier might not be declared.
procedure Pragma_Misplaced;
pragma No_Return (Pragma_Misplaced);
-- Issue fatal error message for misplaced pragma
procedure Process_Atomic_Independent_Shared_Volatile;
-- Common processing for pragmas Atomic, Independent, Shared, Volatile.
-- Note that Shared is an obsolete Ada 83 pragma and treated as being
-- identical in effect to pragma Atomic.
procedure Process_Compile_Time_Warning_Or_Error;
-- Common processing for Compile_Time_Error and Compile_Time_Warning
procedure Process_Convention
(C : out Convention_Id;
Ent : out Entity_Id);
-- Common processing for Convention, Interface, Import and Export.
-- Checks first two arguments of pragma, and sets the appropriate
-- convention value in the specified entity or entities. On return
-- C is the convention, Ent is the referenced entity.
procedure Process_Disable_Enable_Atomic_Sync (Nam : Name_Id);
-- Common processing for Disable/Enable_Atomic_Synchronization. Nam is
-- Name_Suppress for Disable and Name_Unsuppress for Enable.
procedure Process_Extended_Import_Export_Object_Pragma
(Arg_Internal : Node_Id;
Arg_External : Node_Id;
Arg_Size : Node_Id);
-- Common processing for the pragmas Import/Export_Object. The three
-- arguments correspond to the three named parameters of the pragmas. An
-- argument is empty if the corresponding parameter is not present in
-- the pragma.
procedure Process_Extended_Import_Export_Internal_Arg
(Arg_Internal : Node_Id := Empty);
-- Common processing for all extended Import and Export pragmas. The
-- argument is the pragma parameter for the Internal argument. If
-- Arg_Internal is empty or inappropriate, an error message is posted.
-- Otherwise, on normal return, the Entity_Field of Arg_Internal is
-- set to identify the referenced entity.
procedure Process_Extended_Import_Export_Subprogram_Pragma
(Arg_Internal : Node_Id;
Arg_External : Node_Id;
Arg_Parameter_Types : Node_Id;
Arg_Result_Type : Node_Id := Empty;
Arg_Mechanism : Node_Id;
Arg_Result_Mechanism : Node_Id := Empty);
-- Common processing for all extended Import and Export pragmas applying
-- to subprograms. The caller omits any arguments that do not apply to
-- the pragma in question (for example, Arg_Result_Type can be non-Empty
-- only in the Import_Function and Export_Function cases). The argument
-- names correspond to the allowed pragma association identifiers.
procedure Process_Generic_List;
-- Common processing for Share_Generic and Inline_Generic
procedure Process_Import_Or_Interface;
-- Common processing for Import or Interface
procedure Process_Import_Predefined_Type;
-- Processing for completing a type with pragma Import. This is used
-- to declare types that match predefined C types, especially for cases
-- without corresponding Ada predefined type.
type Inline_Status is (Suppressed, Disabled, Enabled);
-- Inline status of a subprogram, indicated as follows:
-- Suppressed: inlining is suppressed for the subprogram
-- Disabled: no inlining is requested for the subprogram
-- Enabled: inlining is requested/required for the subprogram
procedure Process_Inline (Status : Inline_Status);
-- Common processing for Inline, Inline_Always and No_Inline. Parameter
-- indicates the inline status specified by the pragma.
procedure Process_Interface_Name
(Subprogram_Def : Entity_Id;
Ext_Arg : Node_Id;
Link_Arg : Node_Id);
-- Given the last two arguments of pragma Import, pragma Export, or
-- pragma Interface_Name, performs validity checks and sets the
-- Interface_Name field of the given subprogram entity to the
-- appropriate external or link name, depending on the arguments given.
-- Ext_Arg is always present, but Link_Arg may be missing. Note that
-- Ext_Arg may represent the Link_Name if Link_Arg is missing, and
-- appropriate named notation is used for Ext_Arg. If neither Ext_Arg
-- nor Link_Arg is present, the interface name is set to the default
-- from the subprogram name.
procedure Process_Interrupt_Or_Attach_Handler;
-- Common processing for Interrupt and Attach_Handler pragmas
procedure Process_Restrictions_Or_Restriction_Warnings (Warn : Boolean);
-- Common processing for Restrictions and Restriction_Warnings pragmas.
-- Warn is True for Restriction_Warnings, or for Restrictions if the
-- flag Treat_Restrictions_As_Warnings is set, and False if this flag
-- is not set in the Restrictions case.
procedure Process_Suppress_Unsuppress (Suppress_Case : Boolean);
-- Common processing for Suppress and Unsuppress. The boolean parameter
-- Suppress_Case is True for the Suppress case, and False for the
-- Unsuppress case.
procedure Record_Independence_Check (N : Node_Id; E : Entity_Id);
-- Subsidiary to the analysis of pragmas Independent[_Components].
-- Record such a pragma N applied to entity E for future checks.
procedure Set_Exported (E : Entity_Id; Arg : Node_Id);
-- This procedure sets the Is_Exported flag for the given entity,
-- checking that the entity was not previously imported. Arg is
-- the argument that specified the entity. A check is also made
-- for exporting inappropriate entities.
procedure Set_Extended_Import_Export_External_Name
(Internal_Ent : Entity_Id;
Arg_External : Node_Id);
-- Common processing for all extended import export pragmas. The first
-- argument, Internal_Ent, is the internal entity, which has already
-- been checked for validity by the caller. Arg_External is from the
-- Import or Export pragma, and may be null if no External parameter
-- was present. If Arg_External is present and is a non-null string
-- (a null string is treated as the default), then the Interface_Name
-- field of Internal_Ent is set appropriately.
procedure Set_Imported (E : Entity_Id);
-- This procedure sets the Is_Imported flag for the given entity,
-- checking that it is not previously exported or imported.
procedure Set_Mechanism_Value (Ent : Entity_Id; Mech_Name : Node_Id);
-- Mech is a parameter passing mechanism (see Import_Function syntax
-- for MECHANISM_NAME). This routine checks that the mechanism argument
-- has the right form, and if not issues an error message. If the
-- argument has the right form then the Mechanism field of Ent is
-- set appropriately.
procedure Set_Rational_Profile;
-- Activate the set of configuration pragmas and permissions that make
-- up the Rational profile.
procedure Set_Ravenscar_Profile (N : Node_Id);
-- Activate the set of configuration pragmas and restrictions that make
-- up the Ravenscar Profile. N is the corresponding pragma node, which
-- is used for error messages on any constructs violating the profile.
----------------------------------
-- Acquire_Warning_Match_String --
----------------------------------
procedure Acquire_Warning_Match_String (Arg : Node_Id) is
begin
String_To_Name_Buffer
(Strval (Expr_Value_S (Get_Pragma_Arg (Arg))));
-- Add asterisk at start if not already there
if Name_Len > 0 and then Name_Buffer (1) /= '*' then
Name_Buffer (2 .. Name_Len + 1) :=
Name_Buffer (1 .. Name_Len);
Name_Buffer (1) := '*';
Name_Len := Name_Len + 1;
end if;
-- Add asterisk at end if not already there
if Name_Buffer (Name_Len) /= '*' then
Name_Len := Name_Len + 1;
Name_Buffer (Name_Len) := '*';
end if;
end Acquire_Warning_Match_String;
---------------------
-- Ada_2005_Pragma --
---------------------
procedure Ada_2005_Pragma is
begin
if Ada_Version <= Ada_95 then
Check_Restriction (No_Implementation_Pragmas, N);
end if;
end Ada_2005_Pragma;
---------------------
-- Ada_2012_Pragma --
---------------------
procedure Ada_2012_Pragma is
begin
if Ada_Version <= Ada_2005 then
Check_Restriction (No_Implementation_Pragmas, N);
end if;
end Ada_2012_Pragma;
---------------------
-- Analyze_Part_Of --
---------------------
procedure Analyze_Part_Of
(Item_Id : Entity_Id;
State : Node_Id;
Indic : Node_Id;
Legal : out Boolean)
is
Pack_Id : Entity_Id;
Placement : State_Space_Kind;
Parent_Unit : Entity_Id;
State_Id : Entity_Id;
begin
-- Assume that the pragma/option is illegal
Legal := False;
if Nkind_In (State, N_Expanded_Name,
N_Identifier,
N_Selected_Component)
then
Analyze (State);
Resolve_State (State);
if Is_Entity_Name (State)
and then Ekind (Entity (State)) = E_Abstract_State
then
State_Id := Entity (State);
else
SPARK_Msg_N
("indicator Part_Of must denote an abstract state", State);
return;
end if;
-- This is a syntax error, always report
else
Error_Msg_N
("indicator Part_Of must denote an abstract state", State);
return;
end if;
-- Determine where the state, variable or the package instantiation
-- lives with respect to the enclosing packages or package bodies (if
-- any). This placement dictates the legality of the encapsulating
-- state.
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 (State_Id));
SPARK_Msg_NE
("\& is not part of the hidden state of package %",
Indic, Item_Id);
-- 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 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 Is_Private_Descendant (Pack_Id)
then
-- A variable or state abstraction which is part of the
-- visible state of a private child unit (or one of its public
-- descendants) must have its Part_Of indicator specified. The
-- Part_Of indicator must denote a state abstraction declared
-- by either the parent unit of the private unit or by a public
-- descendant of that parent unit.
-- Find nearest private ancestor (which can be the current unit
-- itself).
Parent_Unit := Pack_Id;
while Present (Parent_Unit) loop
exit when Private_Present
(Parent (Unit_Declaration_Node (Parent_Unit)));
Parent_Unit := Scope (Parent_Unit);
end loop;
Parent_Unit := Scope (Parent_Unit);
if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then
SPARK_Msg_NE
("indicator Part_Of must denote an abstract state of& "
& "or public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
elsif Scope (State_Id) = Parent_Unit
or else (Is_Ancestor_Package (Parent_Unit, Scope (State_Id))
and then
not Is_Private_Descendant (Scope (State_Id)))
then
null;
else
SPARK_Msg_NE
("indicator Part_Of must denote an abstract state of& "
& "or public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
end if;
-- Indicator Part_Of is not needed when the related package is not
-- a 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);
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
if Scope (State_Id) /= Pack_Id then
SPARK_Msg_NE
("indicator Part_Of must designate an abstract state of "
& "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
Error_Msg_Name_1 := Chars (Pack_Id);
SPARK_Msg_NE
("\& is declared in the private part of package %",
Indic, Item_Id);
end if;
-- 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 (State_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;
end if;
Legal := True;
end Analyze_Part_Of;
--------------------------------
-- Analyze_Pre_Post_Condition --
--------------------------------
procedure Analyze_Pre_Post_Condition is
Prag_Iden : constant Node_Id := Pragma_Identifier (N);
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
Duplicates_OK : Boolean := False;
-- Flag set when a pre/postcondition allows multiple pragmas of the
-- same kind.
In_Body_OK : Boolean := False;
-- Flag set when a pre/postcondition is allowed to appear on a body
-- even though the subprogram may have a spec.
Is_Pre_Post : Boolean := False;
-- Flag set when the pragma is one of Pre, Pre_Class, Post or
-- Post_Class.
begin
-- Change the name of pragmas Pre, Pre_Class, Post and Post_Class to
-- offer uniformity among the various kinds of pre/postconditions by
-- rewriting the pragma identifier. This allows the retrieval of the
-- original pragma name by routine Original_Aspect_Pragma_Name.
if Comes_From_Source (N) then
if Nam_In (Pname, Name_Pre, Name_Pre_Class) then
Is_Pre_Post := True;
Set_Class_Present (N, Pname = Name_Pre_Class);
Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Precondition));
elsif Nam_In (Pname, Name_Post, Name_Post_Class) then
Is_Pre_Post := True;
Set_Class_Present (N, Pname = Name_Post_Class);
Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Postcondition));
end if;
end if;
-- Determine the semantics with respect to duplicates and placement
-- in a body. Pragmas Precondition and Postcondition were introduced
-- before aspects and are not subject to the same aspect-like rules.
if Nam_In (Pname, Name_Precondition, Name_Postcondition) then
Duplicates_OK := True;
In_Body_OK := True;
end if;
GNAT_Pragma;
-- Pragmas Pre, Pre_Class, Post and Post_Class allow for a single
-- argument without an identifier.
if Is_Pre_Post then
Check_Arg_Count (1);
Check_No_Identifiers;
-- Pragmas Precondition and Postcondition have complex argument
-- profile.
else
Check_At_Least_N_Arguments (1);
Check_At_Most_N_Arguments (2);
Check_Optional_Identifier (Arg1, Name_Check);
if Present (Arg2) then
Check_Optional_Identifier (Arg2, Name_Message);
Preanalyze_Spec_Expression
(Get_Pragma_Arg (Arg2), Standard_String);
end if;
end if;
-- For a pragma PPC in the extended main source unit, record enabled
-- status in SCO.
-- ??? nothing checks that the pragma is in the main source unit
if Is_Checked (N) and then not Split_PPC (N) then
Set_SCO_Pragma_Enabled (Loc);
end if;
-- Ensure the proper placement of the pragma
Subp_Decl :=
Find_Related_Subprogram_Or_Body (N, Do_Checks => not Duplicates_OK);
-- When a pre/postcondition pragma applies to an abstract subprogram,
-- its original form must be an aspect with 'Class.
if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then
if not From_Aspect_Specification (N) then
Error_Pragma
("pragma % cannot be applied to abstract subprogram");
elsif not Class_Present (N) then
Error_Pragma
("aspect % requires ''Class for abstract subprogram");
end if;
-- Entry declaration
elsif Nkind (Subp_Decl) = N_Entry_Declaration then
null;
-- Generic subprogram declaration
elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
-- Subprogram body
elsif Nkind (Subp_Decl) = N_Subprogram_Body
and then (No (Corresponding_Spec (Subp_Decl)) or In_Body_OK)
then
null;
-- Subprogram body stub
elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
and then (No (Corresponding_Spec_Of_Stub (Subp_Decl)) or In_Body_OK)
then
null;
-- Subprogram declaration
elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
-- AI05-0230: When a pre/postcondition pragma applies to a null
-- procedure, its original form must be an aspect with 'Class.
if Nkind (Specification (Subp_Decl)) = N_Procedure_Specification
and then Null_Present (Specification (Subp_Decl))
and then From_Aspect_Specification (N)
and then not Class_Present (N)
then
Error_Pragma ("aspect % requires ''Class for null procedure");
end if;
-- Otherwise the placement is illegal
else
Pragma_Misplaced;
return;
end if;
Subp_Id := Defining_Entity (Subp_Decl);
-- Construct a generic template for the pragma when the context is a
-- generic subprogram and the pragma is a source construct.
Create_Generic_Template (N, Subp_Id);
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
if Nkind_In (Subp_Decl, N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
Analyze_Pre_Post_Condition_In_Decl_Part (N);
end if;
-- Chain the pragma on the contract for further processing
Add_Contract_Item (N, Subp_Id);
end Analyze_Pre_Post_Condition;
----------------------------
-- Analyze_Refined_Pragma --
----------------------------
procedure Analyze_Refined_Pragma
(Spec_Id : out Entity_Id;
Body_Id : out Entity_Id;
Legal : out Boolean)
is
Body_Decl : Node_Id;
Spec_Decl : Node_Id;
begin
-- Assume that the pragma is illegal
Spec_Id := Empty;
Body_Id := Empty;
Legal := False;
GNAT_Pragma;
Check_Arg_Count (1);
Check_No_Identifiers;
-- Verify the placement of the pragma and check for duplicates. The
-- pragma must apply to a subprogram body [stub].
Body_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
-- Extract the entities of the spec and body
if Nkind (Body_Decl) = N_Subprogram_Body then
Body_Id := Defining_Entity (Body_Decl);
Spec_Id := Corresponding_Spec (Body_Decl);
elsif Nkind (Body_Decl) = N_Subprogram_Body_Stub then
Body_Id := Defining_Entity (Body_Decl);
Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
else
Pragma_Misplaced;
return;
end if;
-- The pragma must apply to the second declaration of a subprogram.
-- In other words, the body [stub] cannot acts as a spec.
if No (Spec_Id) then
Error_Pragma ("pragma % cannot apply to a stand alone body");
return;
-- Catch the case where the subprogram body is a subunit and acts as
-- the third declaration of the subprogram.
elsif Nkind (Parent (Body_Decl)) = N_Subunit then
Error_Pragma ("pragma % cannot apply to a subunit");
return;
end if;
-- The pragma can only apply to the body [stub] of a subprogram
-- declared in the visible part of a package. Retrieve the context of
-- the subprogram declaration.
Spec_Decl := Unit_Declaration_Node (Spec_Id);
if Nkind (Parent (Spec_Decl)) /= N_Package_Specification then
Error_Pragma
("pragma % must apply to the body of a subprogram declared in a "
& "package specification");
return;
end if;
-- If we get here, then the pragma is legal
if Nam_In (Pname, Name_Refined_Depends,
Name_Refined_Global,
Name_Refined_State)
then
Ensure_Aggregate_Form (Get_Argument (N));
end if;
Legal := True;
end Analyze_Refined_Pragma;
--------------------------
-- Check_Ada_83_Warning --
--------------------------
procedure Check_Ada_83_Warning is
begin
if Ada_Version = Ada_83 and then Comes_From_Source (N) then
Error_Msg_N ("(Ada 83) pragma& is non-standard??", N);
end if;
end Check_Ada_83_Warning;
---------------------
-- Check_Arg_Count --
---------------------
procedure Check_Arg_Count (Required : Nat) is
begin
if Arg_Count /= Required then
Error_Pragma ("wrong number of arguments for pragma%");
end if;
end Check_Arg_Count;
--------------------------------
-- Check_Arg_Is_External_Name --
--------------------------------
procedure Check_Arg_Is_External_Name (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
if Nkind (Argx) = N_Identifier then
return;
else
Analyze_And_Resolve (Argx, Standard_String);
if Is_OK_Static_Expression (Argx) then
return;
elsif Etype (Argx) = Any_Type then
raise Pragma_Exit;
-- An interesting special case, if we have a string literal and
-- we are in Ada 83 mode, then we allow it even though it will
-- not be flagged as static. This allows expected Ada 83 mode
-- use of external names which are string literals, even though
-- technically these are not static in Ada 83.
elsif Ada_Version = Ada_83
and then Nkind (Argx) = N_String_Literal
then
return;
-- Static expression that raises Constraint_Error. This has
-- already been flagged, so just exit from pragma processing.
elsif Is_OK_Static_Expression (Argx) then
raise Pragma_Exit;
-- Here we have a real error (non-static expression)
else
Error_Msg_Name_1 := Pname;
declare
Msg : constant String :=
"argument for pragma% must be a identifier or "
& "static string expression!";
begin
Flag_Non_Static_Expr (Fix_Error (Msg), Argx);
raise Pragma_Exit;
end;
end if;
end if;
end Check_Arg_Is_External_Name;
-----------------------------
-- Check_Arg_Is_Identifier --
-----------------------------
procedure Check_Arg_Is_Identifier (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
if Nkind (Argx) /= N_Identifier then
Error_Pragma_Arg
("argument for pragma% must be identifier", Argx);
end if;
end Check_Arg_Is_Identifier;
----------------------------------
-- Check_Arg_Is_Integer_Literal --
----------------------------------
procedure Check_Arg_Is_Integer_Literal (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
if Nkind (Argx) /= N_Integer_Literal then
Error_Pragma_Arg
("argument for pragma% must be integer literal", Argx);
end if;
end Check_Arg_Is_Integer_Literal;
-------------------------------------------
-- Check_Arg_Is_Library_Level_Local_Name --
-------------------------------------------
-- LOCAL_NAME ::=
-- DIRECT_NAME
-- | DIRECT_NAME'ATTRIBUTE_DESIGNATOR
-- | library_unit_NAME
procedure Check_Arg_Is_Library_Level_Local_Name (Arg : Node_Id) is
begin
Check_Arg_Is_Local_Name (Arg);
if not Is_Library_Level_Entity (Entity (Get_Pragma_Arg (Arg)))
and then Comes_From_Source (N)
then
Error_Pragma_Arg
("argument for pragma% must be library level entity", Arg);
end if;
end Check_Arg_Is_Library_Level_Local_Name;
-----------------------------
-- Check_Arg_Is_Local_Name --
-----------------------------
-- LOCAL_NAME ::=
-- DIRECT_NAME
-- | DIRECT_NAME'ATTRIBUTE_DESIGNATOR
-- | library_unit_NAME
procedure Check_Arg_Is_Local_Name (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Analyze (Argx);
if Nkind (Argx) not in N_Direct_Name
and then (Nkind (Argx) /= N_Attribute_Reference
or else Present (Expressions (Argx))
or else Nkind (Prefix (Argx)) /= N_Identifier)
and then (not Is_Entity_Name (Argx)
or else not Is_Compilation_Unit (Entity (Argx)))
then
Error_Pragma_Arg ("argument for pragma% must be local name", Argx);
end if;
-- No further check required if not an entity name
if not Is_Entity_Name (Argx) then
null;
else
declare
OK : Boolean;
Ent : constant Entity_Id := Entity (Argx);
Scop : constant Entity_Id := Scope (Ent);
begin
-- Case of a pragma applied to a compilation unit: pragma must
-- occur immediately after the program unit in the compilation.
if Is_Compilation_Unit (Ent) then
declare
Decl : constant Node_Id := Unit_Declaration_Node (Ent);
begin
-- Case of pragma placed immediately after spec
if Parent (N) = Aux_Decls_Node (Parent (Decl)) then
OK := True;
-- Case of pragma placed immediately after body
elsif Nkind (Decl) = N_Subprogram_Declaration
and then Present (Corresponding_Body (Decl))
then
OK := Parent (N) =
Aux_Decls_Node
(Parent (Unit_Declaration_Node
(Corresponding_Body (Decl))));
-- All other cases are illegal
else
OK := False;
end if;
end;
-- Special restricted placement rule from 10.2.1(11.8/2)
elsif Is_Generic_Formal (Ent)
and then Prag_Id = Pragma_Preelaborable_Initialization
then
OK := List_Containing (N) =
Generic_Formal_Declarations
(Unit_Declaration_Node (Scop));
-- If this is an aspect applied to a subprogram body, the
-- pragma is inserted in its declarative part.
elsif From_Aspect_Specification (N)
and then Ent = Current_Scope
and then
Nkind (Unit_Declaration_Node (Ent)) = N_Subprogram_Body
then
OK := True;
-- If the aspect is a predicate (possibly others ???) and the
-- context is a record type, this is a discriminant expression
-- within a type declaration, that freezes the predicated
-- subtype.
elsif From_Aspect_Specification (N)
and then Prag_Id = Pragma_Predicate
and then Ekind (Current_Scope) = E_Record_Type
and then Scop = Scope (Current_Scope)
then
OK := True;
-- Default case, just check that the pragma occurs in the scope
-- of the entity denoted by the name.
else
OK := Current_Scope = Scop;
end if;
if not OK then
Error_Pragma_Arg
("pragma% argument must be in same declarative part", Arg);
end if;
end;
end if;
end Check_Arg_Is_Local_Name;
---------------------------------
-- Check_Arg_Is_Locking_Policy --
---------------------------------
procedure Check_Arg_Is_Locking_Policy (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Is_Locking_Policy_Name (Chars (Argx)) then
Error_Pragma_Arg ("& is not a valid locking policy name", Argx);
end if;
end Check_Arg_Is_Locking_Policy;
-----------------------------------------------
-- Check_Arg_Is_Partition_Elaboration_Policy --
-----------------------------------------------
procedure Check_Arg_Is_Partition_Elaboration_Policy (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Is_Partition_Elaboration_Policy_Name (Chars (Argx)) then
Error_Pragma_Arg
("& is not a valid partition elaboration policy name", Argx);
end if;
end Check_Arg_Is_Partition_Elaboration_Policy;
-------------------------
-- Check_Arg_Is_One_Of --
-------------------------
procedure Check_Arg_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Nam_In (Chars (Argx), N1, N2) then
Error_Msg_Name_2 := N1;
Error_Msg_Name_3 := N2;
Error_Pragma_Arg ("argument for pragma% must be% or%", Argx);
end if;
end Check_Arg_Is_One_Of;
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2, N3 : Name_Id)
is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Nam_In (Chars (Argx), N1, N2, N3) then
Error_Pragma_Arg ("invalid argument for pragma%", Argx);
end if;
end Check_Arg_Is_One_Of;
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2, N3, N4 : Name_Id)
is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Nam_In (Chars (Argx), N1, N2, N3, N4) then
Error_Pragma_Arg ("invalid argument for pragma%", Argx);
end if;
end Check_Arg_Is_One_Of;
procedure Check_Arg_Is_One_Of
(Arg : Node_Id;
N1, N2, N3, N4, N5 : Name_Id)
is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Nam_In (Chars (Argx), N1, N2, N3, N4, N5) then
Error_Pragma_Arg ("invalid argument for pragma%", Argx);
end if;
end Check_Arg_Is_One_Of;
---------------------------------
-- Check_Arg_Is_Queuing_Policy --
---------------------------------
procedure Check_Arg_Is_Queuing_Policy (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Is_Queuing_Policy_Name (Chars (Argx)) then
Error_Pragma_Arg ("& is not a valid queuing policy name", Argx);
end if;
end Check_Arg_Is_Queuing_Policy;
---------------------------------------
-- Check_Arg_Is_OK_Static_Expression --
---------------------------------------
procedure Check_Arg_Is_OK_Static_Expression
(Arg : Node_Id;
Typ : Entity_Id := Empty)
is
begin
Check_Expr_Is_OK_Static_Expression (Get_Pragma_Arg (Arg), Typ);
end Check_Arg_Is_OK_Static_Expression;
------------------------------------------
-- Check_Arg_Is_Task_Dispatching_Policy --
------------------------------------------
procedure Check_Arg_Is_Task_Dispatching_Policy (Arg : Node_Id) is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
begin
Check_Arg_Is_Identifier (Argx);
if not Is_Task_Dispatching_Policy_Name (Chars (Argx)) then
Error_Pragma_Arg
("& is not an allowed task dispatching policy name", Argx);
end if;
end Check_Arg_Is_Task_Dispatching_Policy;
---------------------
-- Check_Arg_Order --
---------------------
procedure Check_Arg_Order (Names : Name_List) is
Arg : Node_Id;
Highest_So_Far : Natural := 0;
-- Highest index in Names seen do far
begin
Arg := Arg1;
for J in 1 .. Arg_Count loop
if Chars (Arg) /= No_Name then
for K in Names'Range loop
if Chars (Arg) = Names (K) then
if K < Highest_So_Far then
Error_Msg_Name_1 := Pname;
Error_Msg_N
("parameters out of order for pragma%", Arg);
Error_Msg_Name_1 := Names (K);
Error_Msg_Name_2 := Names (Highest_So_Far);
Error_Msg_N ("\% must appear before %", Arg);
raise Pragma_Exit;
else
Highest_So_Far := K;
end if;
end if;
end loop;
end if;
Arg := Next (Arg);
end loop;
end Check_Arg_Order;
--------------------------------
-- Check_At_Least_N_Arguments --
--------------------------------
procedure Check_At_Least_N_Arguments (N : Nat) is
begin
if Arg_Count < N then
Error_Pragma ("too few arguments for pragma%");
end if;
end Check_At_Least_N_Arguments;
-------------------------------
-- Check_At_Most_N_Arguments --
-------------------------------
procedure Check_At_Most_N_Arguments (N : Nat) is
Arg : Node_Id;
begin
if Arg_Count > N then
Arg := Arg1;
for J in 1 .. N loop
Next (Arg);
Error_Pragma_Arg ("too many arguments for pragma%", Arg);
end loop;
end if;
end Check_At_Most_N_Arguments;
---------------------
-- Check_Component --
---------------------
procedure Check_Component
(Comp : Node_Id;
UU_Typ : Entity_Id;
In_Variant_Part : Boolean := False)
is
Comp_Id : constant Entity_Id := Defining_Identifier (Comp);
Sindic : constant Node_Id :=
Subtype_Indication (Component_Definition (Comp));
Typ : constant Entity_Id := Etype (Comp_Id);
begin
-- Ada 2005 (AI-216): If a component subtype is subject to a per-
-- object constraint, then the component type shall be an Unchecked_
-- Union.
if Nkind (Sindic) = N_Subtype_Indication
and then Has_Per_Object_Constraint (Comp_Id)
and then not Is_Unchecked_Union (Etype (Subtype_Mark (Sindic)))
then
Error_Msg_N
("component subtype subject to per-object constraint "
& "must be an Unchecked_Union", Comp);
-- Ada 2012 (AI05-0026): For an unchecked union type declared within
-- the body of a generic unit, or within the body of any of its
-- descendant library units, no part of the type of a component
-- declared in a variant_part of the unchecked union type shall be of
-- a formal private type or formal private extension declared within
-- the formal part of the generic unit.
elsif Ada_Version >= Ada_2012
and then In_Generic_Body (UU_Typ)
and then In_Variant_Part
and then Is_Private_Type (Typ)
and then Is_Generic_Type (Typ)
then
Error_Msg_N
("component of unchecked union cannot be of generic type", Comp);
elsif Needs_Finalization (Typ) then
Error_Msg_N
("component of unchecked union cannot be controlled", Comp);
elsif Has_Task (Typ) then
Error_Msg_N
("component of unchecked union cannot have tasks", Comp);
end if;
end Check_Component;
-----------------------------
-- Check_Declaration_Order --
-----------------------------
procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id) is
procedure Check_Aspect_Specification_Order;
-- Inspect the aspect specifications of the context to determine the
-- proper order.
--------------------------------------
-- Check_Aspect_Specification_Order --
--------------------------------------
procedure Check_Aspect_Specification_Order is
Asp_First : constant Node_Id := Corresponding_Aspect (First);
Asp_Second : constant Node_Id := Corresponding_Aspect (Second);
Asp : Node_Id;
begin
-- Both aspects must be part of the same aspect specification list
pragma Assert
(List_Containing (Asp_First) = List_Containing (Asp_Second));
-- Try to reach Second starting from First in a left to right
-- traversal of the aspect specifications.
Asp := Next (Asp_First);
while Present (Asp) loop
-- The order is ok, First is followed by Second
if Asp = Asp_Second then
return;
end if;
Next (Asp);
end loop;
-- If we get here, then the aspects are out of order
SPARK_Msg_N ("aspect % cannot come after aspect %", First);
end Check_Aspect_Specification_Order;
-- Local variables
Stmt : Node_Id;
-- Start of processing for Check_Declaration_Order
begin
-- Cannot check the order if one of the pragmas is missing
if No (First) or else No (Second) then
return;
end if;
-- Set up the error names in case the order is incorrect
Error_Msg_Name_1 := Pragma_Name (First);
Error_Msg_Name_2 := Pragma_Name (Second);
if From_Aspect_Specification (First) then
-- Both pragmas are actually aspects, check their declaration
-- order in the associated aspect specification list. Otherwise
-- First is an aspect and Second a source pragma.
if From_Aspect_Specification (Second) then
Check_Aspect_Specification_Order;
end if;
-- Abstract_States is a source pragma
else
if From_Aspect_Specification (Second) then
SPARK_Msg_N ("pragma % cannot come after aspect %", First);
-- Both pragmas are source constructs. Try to reach First from
-- Second by traversing the declarations backwards.
else
Stmt := Prev (Second);
while Present (Stmt) loop
-- The order is ok, First is followed by Second
if Stmt = First then