blob: 44590aca63192bfbfb60f55bb3afac6de22e44eb [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ P R A G --
-- --
-- S p e c --
-- --
-- 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. --
-- --
------------------------------------------------------------------------------
-- Pragma handling is isolated in a separate package
-- (logically this processing belongs in chapter 4)
with Namet; use Namet;
with Opt; use Opt;
with Snames; use Snames;
with Types; use Types;
package Sem_Prag is
-- The following table lists all pragmas that emulate an Ada 2012 aspect
Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean :=
(Pragma_Abstract_State => True,
Pragma_All_Calls_Remote => True,
Pragma_Annotate => True,
Pragma_Async_Readers => True,
Pragma_Async_Writers => True,
Pragma_Asynchronous => True,
Pragma_Atomic => True,
Pragma_Atomic_Components => True,
Pragma_Attach_Handler => True,
Pragma_Constant_After_Elaboration => True,
Pragma_Contract_Cases => True,
Pragma_Convention => True,
Pragma_CPU => True,
Pragma_CUDA_Device => True,
Pragma_CUDA_Global => True,
Pragma_Default_Initial_Condition => True,
Pragma_Default_Storage_Pool => True,
Pragma_Depends => True,
Pragma_Discard_Names => True,
Pragma_Dispatching_Domain => True,
Pragma_Effective_Reads => True,
Pragma_Effective_Writes => True,
Pragma_Elaborate_Body => True,
Pragma_Export => True,
Pragma_Extensions_Visible => True,
Pragma_Favor_Top_Level => True,
Pragma_Ghost => True,
Pragma_Global => True,
Pragma_GNAT_Annotate => True,
Pragma_Import => True,
Pragma_Independent => True,
Pragma_Independent_Components => True,
Pragma_Initial_Condition => True,
Pragma_Initializes => True,
Pragma_Inline => True,
Pragma_Inline_Always => True,
Pragma_Interrupt_Handler => True,
Pragma_Interrupt_Priority => True,
Pragma_Invariant => True,
Pragma_Linker_Section => True,
Pragma_Lock_Free => True,
Pragma_No_Elaboration_Code_All => True,
Pragma_No_Return => True,
Pragma_Obsolescent => True,
Pragma_Pack => True,
Pragma_Part_Of => True,
Pragma_Persistent_BSS => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Preelaborable_Initialization => True,
Pragma_Preelaborate => True,
Pragma_Priority => True,
Pragma_Pure => True,
Pragma_Pure_Function => True,
Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
Pragma_Refined_State => True,
Pragma_Relative_Deadline => True,
Pragma_Remote_Access_Type => True,
Pragma_Remote_Call_Interface => True,
Pragma_Remote_Types => True,
Pragma_Secondary_Stack_Size => True,
Pragma_Shared => True,
Pragma_Shared_Passive => True,
Pragma_Simple_Storage_Pool_Type => True,
Pragma_SPARK_Mode => True,
Pragma_Storage_Size => True,
Pragma_Suppress => True,
Pragma_Suppress_Debug_Info => True,
Pragma_Suppress_Initialization => True,
Pragma_Test_Case => True,
Pragma_Thread_Local_Storage => True,
Pragma_Type_Invariant => True,
Pragma_Unchecked_Union => True,
Pragma_Universal_Aliasing => True,
Pragma_Unmodified => True,
Pragma_Unreferenced => True,
Pragma_Unreferenced_Objects => True,
Pragma_Unsuppress => True,
Pragma_Volatile => True,
Pragma_Volatile_Components => True,
Pragma_Volatile_Full_Access => True,
Pragma_Warnings => True,
others => False);
-- The following table lists all pragmas that act as an assertion
-- expression.
Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
(Pragma_Assert => True,
Pragma_Assert_And_Cut => True,
Pragma_Assume => True,
Pragma_Check => True,
Pragma_Contract_Cases => True,
Pragma_Default_Initial_Condition => True,
Pragma_Initial_Condition => True,
Pragma_Invariant => True,
Pragma_Loop_Invariant => True,
Pragma_Loop_Variant => True,
Pragma_Post => True,
Pragma_Post_Class => True,
Pragma_Postcondition => True,
Pragma_Pre => True,
Pragma_Pre_Class => True,
Pragma_Precondition => True,
Pragma_Predicate => True,
Pragma_Refined_Post => True,
Pragma_Test_Case => True,
Pragma_Type_Invariant => True,
Pragma_Type_Invariant_Class => True,
others => False);
-- The following table lists all the implementation-defined pragmas that
-- should apply to the anonymous object produced by the analysis of a
-- single protected or task type. The table should be synchronized with
-- Aspect_On_Anonymous_Object_OK in unit Aspects.
Pragma_On_Anonymous_Object_OK : constant array (Pragma_Id) of Boolean :=
(Pragma_Depends => True,
Pragma_Global => True,
Pragma_Part_Of => True,
others => False);
-- The following table lists all the implementation-defined pragmas that
-- may apply to a body stub (no language defined pragmas apply). The table
-- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects.
Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
(Pragma_Refined_Depends => True,
Pragma_Refined_Global => True,
Pragma_Refined_Post => True,
Pragma_SPARK_Mode => True,
Pragma_Warnings => True,
others => False);
-- The following table lists all pragmas which are significant in SPARK and
-- as a result get translated into verification conditions. The table is an
-- amalgamation of the pragmas listed in SPARK RM 16.1 and internally added
-- entries.
Pragma_Significant_In_SPARK : constant array (Pragma_Id) of Boolean :=
(Pragma_All_Calls_Remote => False,
Pragma_Asynchronous => False,
Pragma_Default_Storage_Pool => False,
Pragma_Discard_Names => False,
Pragma_Dispatching_Domain => False,
Pragma_Priority_Specific_Dispatching => False,
Pragma_Remote_Call_Interface => False,
Pragma_Remote_Types => False,
Pragma_Shared_Passive => False,
Pragma_Task_Dispatching_Policy => False,
Pragma_Unmodified => False,
Pragma_Unreferenced => False,
Pragma_Warnings => False,
others => True);
-----------------
-- Subprograms --
-----------------
procedure Analyze_Pragma (N : Node_Id);
-- Analyze procedure for pragma reference node N
procedure Analyze_Contract_Cases_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Contract_Cases. Freeze_Id is the
-- entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Depends. This routine is also
-- capable of performing basic analysis of pragma Refined_Depends.
procedure Analyze_External_Property_In_Decl_Part
(N : Node_Id;
Expr_Val : out Boolean);
-- Perform full analysis of delayed pragmas Async_Readers, Async_Writers,
-- Effective_Reads, Effective_Writes and No_Caching. Flag Expr_Val contains
-- the Boolean argument of the pragma or a default True if no argument
-- is present.
procedure Analyze_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Global. This routine is also
-- capable of performing basic analysis of pragma Refined_Global.
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initial_Condition
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
procedure Analyze_Part_Of_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Part_Of. Freeze_Id is the entity
-- of [generic] package body or [generic] subprogram body which caused the
-- "freezing" of the related contract where the pragma resides.
procedure Analyze_Pre_Post_Condition_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of pragmas Precondition and Postcondition.
-- Freeze_Id denotes the entity of [generic] package body or [generic]
-- subprogram body which caused "freezing" of the related contract where
-- the pragma resides.
procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
-- Preform full analysis of delayed pragma Refined_Depends. This routine
-- uses Analyze_Depends_In_Decl_Part as a starting point, then performs
-- various consistency checks between Depends and Refined_Depends.
procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Refined_Global. This routine
-- uses Analyze_Global_In_Decl_Part as a starting point, then performs
-- various consistency checks between Global and Refined_Global.
procedure Analyze_Refined_State_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Refined_State. Freeze_Id denotes
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Subprogram_Variant_In_Decl_Part
(N : Node_Id;
Freeze_Id : Entity_Id := Empty);
-- Perform full analysis of delayed pragma Subprogram_Variant. Freeze_Id is
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
-- Perform preanalysis of pragma Test_Case
function Build_Pragma_Check_Equivalent
(Prag : Node_Id;
Subp_Id : Entity_Id := Empty;
Inher_Id : Entity_Id := Empty;
Keep_Pragma_Id : Boolean := False) return Node_Id;
-- Transform a pre- or [refined] postcondition denoted by Prag into an
-- equivalent pragma Check. When the pre- or postcondition is inherited,
-- the routine replaces the references of all formals of Inher_Id
-- and primitive operations of its controlling type by references
-- to the corresponding entities of Subp_Id and the descendant type.
-- Keep_Pragma_Id is True when the newly created pragma should be
-- in fact of the same kind as the source pragma Prag. This is used
-- in GNATprove_Mode to generate the inherited pre- and postconditions.
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
-- the name of the aspect or pragma is not one of those recognized as
-- an assertion kind by an Assertion_Policy pragma, then the call has
-- no effect. Note that in the case of a pragma derived from an aspect,
-- the name we use for the purpose of this procedure is the aspect name,
-- which may be different from the pragma name (e.g. Precondition for
-- Pre aspect). In addition, 'Class aspects are recognized (and the
-- corresponding special names used in the processing).
--
-- If the name is a valid assertion kind name, then the Check_Policy pragma
-- chain is checked for a matching entry (or for an Assertion entry which
-- matches all possibilities). If a matching entry is found then the policy
-- is checked. If it is On or Check, then the Is_Checked flag is set in
-- the aspect or pragma node. If it is Off, Ignore, or Disable, then the
-- Is_Ignored flag is set in the aspect or pragma node. Additionally for
-- policy Disable, the Is_Disabled flag is set.
--
-- If no matching Check_Policy pragma is found then the effect depends on
-- whether -gnata was used, if so, then the call has no effect, otherwise
-- Is_Ignored (but not Is_Disabled) is set True.
procedure Check_External_Properties
(Item : Node_Id;
AR : Boolean;
AW : Boolean;
ER : Boolean;
EW : Boolean);
-- Flags AR, AW, ER and EW denote the static values of external properties
-- Async_Readers, Async_Writers, Effective_Reads and Effective_Writes. Item
-- is the related variable or state. Ensure legality of the combination and
-- issue an error for an illegal combination.
function Check_Kind (Nam : Name_Id) return Name_Id;
-- This function is used in connection with pragmas Assert, Check,
-- and assertion aspects and pragmas, to determine if Check pragmas
-- (or corresponding assertion aspects or pragmas) are currently active
-- as determined by the presence of -gnata on the command line (which
-- sets the default), and the appearance of pragmas Check_Policy and
-- Assertion_Policy as configuration pragmas either in a configuration
-- pragma file, or at the start of the current unit, or locally given
-- Check_Policy and Assertion_Policy pragmas that are currently active.
--
-- The value returned is one of the names Check, Ignore, Disable (On
-- returns Check, and Off returns Ignore).
--
-- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
-- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
-- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
-- _Post, _Invariant, or _Type_Invariant, which are special names used
-- in identifiers to represent these attribute references.
procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
-- Determine whether the placement within the state space of an abstract
-- state, variable or package instantiation denoted by Item_Id requires the
-- use of indicator/option Part_Of. If this is the case, emit an error.
procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id);
-- In GNATprove mode, when analyzing an overriding subprogram, check
-- whether the overridden operations have class-wide pre/postconditions,
-- and generate the corresponding pragmas. The pragmas are inserted after
-- the subprogram declaration, together with those generated for other
-- aspects of the subprogram.
procedure Collect_Subprogram_Inputs_Outputs
(Subp_Id : Entity_Id;
Synthesize : Boolean := False;
Subp_Inputs : in out Elist_Id;
Subp_Outputs : in out Elist_Id;
Global_Seen : out Boolean);
-- Subsidiary to the analysis of pragmas Depends, Global, Refined_Depends
-- and Refined_Global. Collect all inputs and outputs of subprogram Subp_Id
-- in lists Subp_Inputs (inputs) and Subp_Outputs (outputs). The inputs and
-- outputs are gathered from:
-- 1) The formal parameters of the subprogram
-- 2) The generic formal parameters of the generic subprogram
-- 3) The current instance of a concurrent type
-- 4) The items of pragma [Refined_]Global
-- or
-- 5) The items of pragma [Refined_]Depends if there is no pragma
-- [Refined_]Global present and flag Synthesize is set to True.
-- If the subprogram has no inputs and/or outputs, then the returned list
-- is No_Elist. Flag Global_Seen is set when the related subprogram has
-- pragma [Refined_]Global.
function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;
-- N is a pragma appearing in a configuration pragma file. Most such
-- pragmas are analyzed when the file is read, before parsing and analyzing
-- the main unit. However, the analysis of certain pragmas results in
-- adding information to the compiled main unit, and this cannot be done
-- till the main unit is processed. Such pragmas return True from this
-- function and in Frontend pragmas where Delay_Config_Pragma_Analyze is
-- True have their analysis delayed until after the main program is parsed
-- and analyzed.
function Find_Related_Package_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas
-- Abstract_State
-- Initial_Condition
-- Initializes
-- Refined_State
-- Find the declaration of the related package [body] subject to pragma
-- Prag. The return value is either N_Package_Declaration, N_Package_Body,
-- or Empty if the placement of the pragma is illegal. If flag Do_Checks is
-- set, the routine reports duplicate pragmas.
function Find_Related_Declaration_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas
-- Contract_Cases
-- Depends
-- Extensions_Visible
-- Global
-- Initializes
-- Max_Entry_Queue_Depth
-- Max_Entry_Queue_Length
-- Max_Queue_Length
-- Post
-- Post_Class
-- Postcondition
-- Pre
-- Pre_Class
-- Precondition
-- Refined_Depends
-- Refined_Global
-- Refined_Post
-- Refined_State
-- Test_Case
-- Volatile_Function
-- as well as attributes 'Old and 'Result. Find the declaration of the
-- related entry, subprogram or task type [body] subject to pragma Prag.
-- If flag Do_Checks is set, the routine reports duplicate pragmas and
-- detects improper use of refinement pragmas in stand alone expression
-- functions.
function Get_Argument
(Prag : Node_Id;
Context_Id : Entity_Id := Empty) return Node_Id;
-- Obtain the argument of pragma Prag depending on context and the nature
-- of the pragma. The argument is extracted in the following manner:
--
-- When the pragma is generated from an aspect, return the corresponding
-- aspect when Context_Id denotes a generic unit.
--
-- Otherwise return the first argument of Prag
--
-- Context denotes the entity of the function, package or procedure where
-- Prag resides.
function Get_SPARK_Mode_From_Annotation
(N : Node_Id) return SPARK_Mode_Type;
-- Given an aspect or pragma SPARK_Mode node, return corresponding mode id
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
-- before analyzing each new main source program.
function Is_Config_Static_String (Arg : Node_Id) return Boolean;
-- This is called for a configuration pragma that requires either string
-- literal or a concatenation of string literals. We cannot use normal
-- static string processing because it is too early in the case of the
-- pragma appearing in a configuration pragmas file. If Arg is of an
-- appropriate form, then this call obtains the string (doing any necessary
-- concatenations) and places it in Name_Buffer, setting Name_Len to its
-- length, and then returns True. If it is not of the correct form, then an
-- appropriate error message is posted, and False is returned.
function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean;
-- Determine whether pragma SPARK_Mode appears in the statement part of a
-- package body.
function Is_Enabled_Pragma (Prag : Node_Id) return Boolean;
-- Determine whether a Boolean-like SPARK pragma Prag is enabled. To be
-- considered enabled, the pragma must either:
-- * Appear without its Boolean expression
-- * The Boolean expression evaluates to "True"
--
-- Boolean-like SPARK pragmas differ from pure Boolean Ada pragmas in that
-- their optional Boolean expression must be static and cannot benefit from
-- forward references. The following are Boolean-like SPARK pragmas:
-- Async_Readers
-- Async_Writers
-- Constant_After_Elaboration
-- Effective_Reads
-- Effective_Writes
-- Extensions_Visible
-- Volatile_Function
function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
-- The node N is a node for an entity and the issue is whether the
-- occurrence is a reference for the purposes of giving warnings about
-- unreferenced variables. This function returns True if the reference is
-- not a reference from this point of view (e.g. the occurrence in a pragma
-- Pack) and False if it is a real reference (e.g. the occurrence in a
-- pragma Export);
function Is_Pragma_String_Literal (Par : Node_Id) return Boolean;
-- Given an N_Pragma_Argument_Association node, Par, which has the form of
-- an operator symbol, determines whether or not it should be treated as an
-- string literal. This is called by Sem_Ch6.Analyze_Operator_Symbol. If
-- True is returned, the argument is converted to a string literal. If
-- False is returned, then the argument is treated as an entity reference
-- to the operator.
function Is_Private_SPARK_Mode (N : Node_Id) return Boolean;
-- Determine whether pragma SPARK_Mode appears in the private part of a
-- package.
function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
-- Returns True if Nam is one of the names recognized as a valid assertion
-- kind by the Assertion_Policy pragma. Note that the 'Class cases are
-- represented by the corresponding special names Name_uPre, Name_uPost,
-- Name_uInvariant, and Name_uType_Invariant (_Pre, _Post, _Invariant,
-- and _Type_Invariant).
procedure Process_Compilation_Unit_Pragmas (N : Node_Id);
-- Called at the start of processing compilation unit N to deal with any
-- special issues regarding pragmas. In particular, we have to deal with
-- Suppress_All at this stage, since it can appear after the unit instead
-- of before (actually we allow it to appear anywhere).
procedure Relocate_Pragmas_To_Anonymous_Object
(Typ_Decl : Node_Id;
Obj_Decl : Node_Id);
-- Relocate all pragmas that appear in the visible declarations of task or
-- protected type declaration Typ_Decl after the declaration of anonymous
-- object Obj_Decl. Table Pragmas_On_Anonymous_Object_OK contains the list
-- of candidate pragmas.
procedure Relocate_Pragmas_To_Body
(Subp_Body : Node_Id;
Target_Body : Node_Id := Empty);
-- Resocate all pragmas that follow and apply to subprogram body Subp_Body
-- to its own declaration list. Candidate pragmas are classified in table
-- Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved
-- to the declarations of Target_Body. This formal should be set when
-- dealing with subprogram body stubs or expression functions.
procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id);
-- This routine is used to set an encoded interface name. The node S is
-- an N_String_Literal node for the external name to be set, and E is an
-- entity whose Interface_Name field is to be set. In the normal case where
-- S contains a name that is a valid C identifier, then S is simply set as
-- the value of the Interface_Name. Otherwise it is encoded as needed by
-- particular operating systems. See the body for details of the encoding.
procedure Set_Overflow_Mode (N : Node_Id);
-- Sets Sem.Scope_Suppress according to the overflow modes specified in
-- the pragma Overflow_Mode passed in argument. This should only be called
-- after N has been successfully analyzed.
function Test_Case_Arg
(Prag : Node_Id;
Arg_Nam : Name_Id;
From_Aspect : Boolean := False) return Node_Id;
-- Obtain argument "Name", "Mode", "Ensures" or "Requires" from Test_Case
-- pragma Prag as denoted by Arg_Nam. When From_Aspect is set, an attempt
-- is made to retrieve the argument from the corresponding aspect if there
-- is one. The returned argument has several formats:
--
-- N_Pragma_Argument_Association if retrieved directly from the pragma
--
-- N_Component_Association if retrieved from the corresponding aspect and
-- the argument appears in a named association form.
--
-- An arbitrary expression if retrieved from the corresponding aspect and
-- the argument appears in positional form.
--
-- Empty if there is no such argument
procedure Validate_Compile_Time_Warning_Errors;
-- This routine is called after calling the back end to validate pragmas
-- Compile_Time_Error and Compile_Time_Warning for size and alignment
-- appropriateness. The reason it is called that late is to take advantage
-- of any back-annotation of size and alignment performed by the back end.
end Sem_Prag;