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