+2015-05-12 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.adb Node32 is now used as Encapsulating_State.
+ Node37 is now used as Associated_Entity.
+ (Associated_Entity): New routine.
+ (Encapsulating_State): Update the assertion guard
+ to include constants.
+ (Set_Associated_Entity): New routine.
+ (Set_Encapsulating_State): Update the assertion guard to
+ include constants.
+ (Write_Field10_Name): Remove the output for Encapsulating_State.
+ (Write_Field32_Name): Add output for Encapsulating_State.
+ (Write_Field37_Name): Add output for Associated_Entity.
+ * einfo.ads New attribute Associated_Entity along with placement
+ in entities. Attribute Encapsulating_State now uses Node32.
+ (Associated_Entity): New routine along with pragma Inline.
+ (Set_Associated_Entity): New routine along with pragma Inline.
+ * inline.ads Code reformatting.
+ * sem_attr.adb (Analyze_Attribute): Correct the prefix of
+ attribute 'Result when the context is a generic instantiation.
+ (Analyze_Attribute_Old_Result): Pragmas Depends and
+ Refined_Depends are a valid context for attribute 'Result.
+ (Denote_Same_Function): Allow attribute 'Result to denote
+ generic functions.
+ * sem_ch3.adb Add with and use clauses for Sem_Ch12.
+ (Analyze_Declarations): Capture global references within the
+ contracts of packages, subprograms and their respective bodies.
+ * sem_ch6.adb (Analyze_Aspects_On_Body_Or_Stub): Removed.
+ (Analyze_Completion_Contract): Removed.
+ (Analyze_Generic_Subprogram_Body): Enchange the aspects after
+ creating the generic copy. Create a generic contract for the
+ template. Analyze the aspects of the generic body. Analyze the
+ contract of the generic body when it is a compilation unit and
+ capture global references.
+ (Analyze_Subprogram_Body_Contract): Code cleanup.
+ (Analyze_Subprogram_Contract): Do not save global references here.
+ (Save_Global_References_In_List): Removed.
+ * sem_ch7.adb (Analyze_Package_Body_Contract): Code cleanup.
+ (Analyze_Package_Body_Helper): Create a generic contract for
+ the template.
+ (Analyze_Package_Contract): Code cleanup.
+ * sem_ch10.adb Add with and use clauses for Sem_Ch12.
+ (Analyze_Compilation_Unit): Capture global references in a
+ generic subprogram declaration that acts as a compilation unit.
+ * sem_ch12.adb Add with and use clauses for Sem_Prag. Illustrate
+ the implementation of generic contracts. Alphabetize various
+ subprograms.
+ (Analyze_Generic_Package_Declaration):
+ Create a generic contract for the template.
+ (Analyze_Generic_Subprogram_Declaration): Create a generic
+ contract for the template.
+ (Analyze_Subprogram_Instantiation): Instantiate the contract of the
+ subprogram.
+ (Copy_Generic_Node): Link defining entities of the generic template
+ with the corresponding defining entities of the generic copy. Update
+ the processing of pragmas.
+ (Instantiate_Contract): Removed.
+ (Instantiate_Subprogram_Contract): New routine.
+ (Requires_Delayed_Save): New routine.
+ (Save_Global_References): Rename formal parameter N to Templ. Various
+ cleanups.
+ (Save_Global_References_In_Aspects): Moved from the spec.
+ (Save_Global_References_In_Contract): New routine.
+ (Save_References_In_Aggregate): New routine.
+ (Save_References_In_Char_Lit_Or_Op_Symbol): New routine.
+ (Save_References_In_Descendants): New routine.
+ (Save_References_In_Identifier): New routine.
+ (Save_References_In_Operator): New routine.
+ (Save_References_In_Pragma): New routine.
+ * sem_ch12.ads (Save_Global_References): Rename formal
+ parameter N to Templ. Update the comment on usage.
+ (Save_Global_References_In_Aspects): Moved to the body.
+ (Save_Global_References_In_Contract): New routine.
+ * sem_ch13.adb (Analyze_Aspect_Specifications_On_Body_Or_Stub):
+ New routine.
+ * sem_ch13.ads (Analyze_Aspect_Specifications_On_Body_Or_Stub):
+ New routine.
+ * sem_prag.adb (Add_Item_To_Name_Buffer): Add support for
+ generic parameters.
+ (Analyze_Contract_Cases_In_Decl_Part): Code cleanup.
+ (Analyze_Depends_Global): New routine.
+ (Analyze_Depends_In_Decl_Part): Code cleanup.
+ (Analyze_Global_In_Decl_Part): Code cleanup.
+ (Analyze_Global_Item): Constants are now valid global items. Do
+ not perform state-related checks in an instance. Change the way
+ renamings are handled. (Analyze_Initial_Condition_In_Decl_Part):
+ Code cleanup.
+ (Analyze_Initializes_In_Decl_Part): Code cleanup.
+ (Analyze_Input_Output): The analysis of attribute 'Result in
+ the context of pragmas Depends or Refined_Depends now reuses
+ the existing attribute analysis machinery. Constants and
+ generic parameters are now valid dependency items. Do not
+ perform state-related checks in an instance. Change the way
+ renamings are handled. (Analyze_Pragma): Add a "characteristics"
+ section for pragmas Abstract_State, Contract_Cases, Depends,
+ Extensions_Visible, Global, Initial_Condition, Initializes,
+ Post, Post_Class, Postcondition, Pre, Pre_Class, Precondition,
+ Refined_Depends, Refined_Global, Refined_Post, Refined_State, Test_Case.
+ (Analyze_Pre_Post_Condition): Do not create a generic
+ template here.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Code cleanup.
+ (Analyze_Refined_Depends_Global_Post): New routine.
+ (Analyze_Refined_Depends_In_Decl_Part): Code cleanup.
+ (Analyze_Refined_Global_In_Decl_Part): Code cleanup.
+ (Analyze_Refined_Pragma): Removed.
+ (Analyze_Refined_State_In_Decl_Part): Code cleanup.
+ (Analyze_Test_Case_In_Decl_Part): Code cleanup.
+ (Check_Dependency_Clause): Do not perform this check in an instance.
+ (Check_Function_Return): Add support for generic functions.
+ (Check_In_Out_States): Do not perform this check in an instance.
+ (Check_Input_States): Do not perform this check in an instance.
+ (Check_Mode_Restriction_In_Function): Add support for generic functions.
+ (Check_Output_States): Do not perform this check in an instance.
+ (Check_Postcondition_Use_In_Inlined_Subprogram): Rename
+ parameter Subp_Id to Spec_Id and update comment on usage.
+ (Check_Proof_In_States): Do not perform this check in an instance.
+ (Check_Refined_Global_Item): Add support for constants.
+ (Check_Refined_Global_List): Do not perform this check in an instance.
+ (Collect_Global_Items): Reimplemented.
+ (Collect_Subprogram_Inputs_Outputs): Add support for generic parameters.
+ (Create_Generic_Template): Removed.
+ (Find_Related_Package_Or_Body): Moved to spec.
+ (Find_Role): Add support for generic parameters and constants.
+ (Get_Argument): Moved to spec. Rename parameter Spec_Id to Context_Id.
+ (Match_Item): Add support for constants.
+ (Preanalyze_Test_Case_Arg): Reimplemented.
+ (Report_Extra_Clauses): Do not perform this check in an instance.
+ (Report_Extra_Constituents): Do not perform this check in an instance.
+ * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update
+ the comment on usage.
+ (Find_Related_Package_Or_Body): Moved from body.
+ (Get_Argument): Moved from body.
+ * sem_util.adb Add with and use clauses for Sem_Ch12.
+ (Corresponding_Spec_Of): Add support for packages and package bodies.
+ (Create_Generic_Contract): New routine.
+ (Is_Contract_Annotation): Reimplemented.
+ (Is_Generic_Declaration_Or_Body): New routine.
+ (Is_Package_Contract_Annotation): New routine.
+ (Is_Subprogram_Contract_Annotation): New routine.
+ * sem_util.ads (Corresponding_Spec_Of): Update the comment on usage.
+ (Create_Generic_Contract): New routine.
+ (Is_Generic_Declaration_Or_Body): New routine.
+ (Is_Package_Contract_Annotation): New routine.
+ (Is_Subprogram_Contract_Annotation): New routine.
+ * sinfo.adb (Is_Generic_Contract_Pragma): New routine.
+ (Set_Is_Generic_Contract_Pragma): New routine.
+ * sinfo.ads Add new attribute Is_Generic_Contract_Pragma along
+ with occurrences in nodes.
+ (Is_Generic_Contract_Pragma): New routine along with pragma Inline.
+ (Set_Is_Generic_Contract_Pragma): New routine along with pragma Inline.
+ * treepr.adb (Print_Entity_Info): Output fields 36 to 41.
+
+2015-05-12 Robert Dewar <dewar@adacore.com>
+
+ * a-taster.ads: Minor comment fix: fix bad header, this is a
+ pure RM unit.
+
2015-05-12 Robert Dewar <dewar@adacore.com>
* sem_intr.adb: (Check_Shift): Diagnose bad modulus value.
-- --
-- S p e c --
-- --
--- Copyright (C) 2005, Free Software Foundation, Inc. --
--- --
-- This specification is derived from the Ada Reference Manual for use with --
--- GNAT. The copyright notice above, and the license provisions that follow --
--- apply solely to the contents of the part following the private keyword. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- GNAT. In accordance with the copyright of that document, you can freely --
+-- copy and modify this specification, provided that if you redistribute a --
+-- modified version, any changes that you have made are clearly indicated. --
-- --
------------------------------------------------------------------------------
-- Homonym Node4
-- First_Rep_Item Node6
-- Freeze_Node Node7
+ -- Associated_Entity Node37
-- The usage of other fields (and the entity kinds to which it applies)
-- depends on the particular field (see Einfo spec for details).
-- Part_Of_Constituents Elist9
-- Renaming_Map Uint9
- -- Encapsulating_State Node10
-- Direct_Primitive_Operations Elist10
-- Discriminal_Link Node10
-- Float_Rep Uint10 (but returns Float_Rep_Kind)
-- Related_Expression Node24
-- Subps_Index Uint24
- -- Interface_Alias Node25
- -- Interfaces Elist25
-- Debug_Renaming_Link Node25
-- DT_Offset_To_Top_Func Node25
+ -- Interface_Alias Node25
+ -- Interfaces Elist25
-- PPC_Wrapper Node25
-- Related_Array_Object Node25
-- Static_Discrete_Predicate List25
-- Thunk_Entity Node31
-- Activation_Record_Component Node31
+ -- Encapsulating_State Node32
-- SPARK_Pragma Node32
-- No_Tagged_Streams_Pragma Node32
-- Import_Pragma Node35
-- (unused) Node36
- -- (unused) Node37
-- (unused) Node38
-- (unused) Node39
-- (unused) Node40
return Uint14 (Id);
end Alignment;
+ function Associated_Entity (Id : E) return E is
+ begin
+ return Node37 (Id);
+ end Associated_Entity;
+
function Associated_Formal_Package (Id : E) return E is
begin
pragma Assert (Ekind (Id) = E_Package);
function Encapsulating_State (Id : E) return N is
begin
- pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
- return Node10 (Id);
+ pragma Assert (Ekind_In (Id, E_Abstract_State, E_Constant, E_Variable));
+ return Node32 (Id);
end Encapsulating_State;
function Enclosing_Scope (Id : E) return E is
E_Package,
E_Package_Body,
E_Subprogram_Body,
- E_Variable)
+ E_Variable,
+ E_Void)
or else Is_Subprogram_Or_Generic_Subprogram (Id));
return Node34 (Id);
end Contract;
Set_Elist16 (Id, V);
end Set_Access_Disp_Table;
+ procedure Set_Associated_Entity (Id : E; V : E) is
+ begin
+ Set_Node37 (Id, V);
+ end Set_Associated_Entity;
+
procedure Set_Associated_Formal_Package (Id : E; V : E) is
begin
Set_Node12 (Id, V);
begin
pragma Assert
(Ekind_In (Id, E_Entry,
- E_Entry_Family,
- E_Generic_Package,
- E_Package,
- E_Package_Body,
- E_Subprogram_Body,
- E_Variable,
- E_Void)
+ E_Entry_Family,
+ E_Generic_Package,
+ E_Package,
+ E_Package_Body,
+ E_Subprogram_Body,
+ E_Variable,
+ E_Void)
or else Is_Subprogram_Or_Generic_Subprogram (Id));
Set_Node34 (Id, V);
end Set_Contract;
procedure Set_Encapsulating_State (Id : E; V : E) is
begin
- pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
- Set_Node10 (Id, V);
+ pragma Assert (Ekind_In (Id, E_Abstract_State, E_Constant, E_Variable));
+ Set_Node32 (Id, V);
end Set_Encapsulating_State;
procedure Set_Enclosing_Scope (Id : E; V : E) is
-----------------------
procedure Write_Field6_Name (Id : Entity_Id) is
- pragma Warnings (Off, Id);
+ pragma Unreferenced (Id);
begin
Write_Str ("First_Rep_Item");
end Write_Field6_Name;
-----------------------
procedure Write_Field7_Name (Id : Entity_Id) is
- pragma Warnings (Off, Id);
+ pragma Unreferenced (Id);
begin
Write_Str ("Freeze_Node");
end Write_Field7_Name;
procedure Write_Field10_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
- when E_Abstract_State |
- E_Variable =>
- Write_Str ("Encapsulating_State");
-
when Class_Wide_Kind |
Incomplete_Kind |
E_Record_Type |
Concurrent_Kind =>
Write_Str ("Direct_Primitive_Operations");
- when Float_Kind =>
- Write_Str ("Float_Rep");
-
when E_In_Parameter |
E_Constant =>
Write_Str ("Discriminal_Link");
+ when Float_Kind =>
+ Write_Str ("Float_Rep");
+
when E_Function |
E_Package |
E_Package_Body |
procedure Write_Field32_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Abstract_State |
+ E_Constant |
+ E_Variable =>
+ Write_Str ("Encapsulating_State");
+
when E_Function |
E_Generic_Function |
E_Generic_Package |
E_Package_Body |
E_Subprogram_Body |
E_Variable |
+ E_Void |
Generic_Subprogram_Kind |
Subprogram_Kind =>
Write_Str ("Contract");
------------------------
procedure Write_Field37_Name (Id : Entity_Id) is
+ pragma Unreferenced (Id);
begin
- case Ekind (Id) is
- when others =>
- Write_Str ("Field37??");
- end case;
+ Write_Str ("Associated_Entity");
end Write_Field37_Name;
------------------------
-- definition clause with an (obsolescent) mod clause is converted
-- into an attribute definition clause for this purpose.
+-- Associated_Entity (Node37)
+-- Defined in all entities. This field is similar to Associated_Node, but
+-- applied to entities. The attribute links an entity from the generic
+-- template with its corresponding entity in the analyzed generic copy.
+-- The global references mechanism relies on the Associated_Entity to
+-- infer the context.
+
-- Associated_Formal_Package (Node12)
-- Defined in packages that are the actuals of formal_packages. Points
-- to the entity in the declaration for the formal package.
-- primitives that come from source must be stored in this list in the
-- order of their occurrence in the sources. For incomplete types the
-- list is always empty.
---
-- When expansion is disabled the corresponding record type of a
-- synchronized type is not constructed. In that case, such types
-- carry this attribute directly, for ASIS use.
-- then if there is no other elaboration code, obviously there is no
-- need to set the flag.
--- Encapsulating_State (Node10)
--- Defined in abstract states and variables. Contains the entity of an
--- ancestor state whose refinement utilizes this item as a constituent.
+-- Encapsulating_State (Node32)
+-- Defined in abstract states, constants and variables. Contains the
+-- entity of an ancestor state whose refinement utilizes this item as
+-- a constituent.
-- Enclosing_Scope (Node18)
-- Defined in labels. Denotes the innermost enclosing construct that
-- 'COUNT when it applies to a family member.
-- Contract (Node34)
--- Defined in entry, entry family, package, package body, subprogram and
--- subprogram body entities as well as their respective generic forms. A
--- contract is also applicable to a variable. Points to the contract of
--- the entity, holding various assertion items and data classifiers.
+-- Defined in entry, entry family, [generic] package, package body,
+-- [generic] subprogram, subprogram body and variable entities. Points
+-- to the contract of the entity, holding various assertion items and
+-- data classifiers.
-- Entry_Parameters_Type (Node15)
-- Defined in entries. Points to the access-to-record type that is
-- Has_Inherited_Default_Init_Cond (Flag133)
-- Defined in type and subtype entities. Set if a derived type inherits
-- pragma Default_Initial_Condition from its parent type. This flag must
--- be mutually exclusive with Had_Default_Init_Cond.
+-- be mutually exclusive with Has_Default_Init_Cond.
-- Has_Initial_Value (Flag219)
-- Defined in entities for variables and out parameters. Set if there
-- Etype (Node5)
-- First_Rep_Item (Node6)
-- Freeze_Node (Node7)
+ -- Associated_Entity (Node37)
-- Address_Taken (Flag104)
-- Can_Never_Be_Null (Flag38)
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
-- Part_Of_Constituents (Elist9)
- -- Encapsulating_State (Node10)
-- Body_References (Elist16)
-- Non_Limited_View (Node19)
+ -- Encapsulating_State (Node32)
-- From_Limited_With (Flag159)
-- Has_Visible_Refinement (Flag263)
-- Has_Non_Limited_View (synth)
-- BIP_Initialization_Call (Node29)
-- Last_Aggregate_Assignment (Node30)
-- Activation_Record_Component (Node31)
+ -- Encapsulating_State (Node32) (constants only)
-- Linker_Section_Pragma (Node33)
-- Has_Alignment_Clause (Flag46)
-- Has_Atomic_Components (Flag86)
-- Alias (Node18)
-- Extra_Accessibility_Of_Result (Node19)
-- Last_Entity (Node20)
- -- Has_Nested_Subprogram (Flag282)
-- Subps_Index (Uint24)
-- Overridden_Operation (Node26)
-- Subprograms_For_Type (Node29)
-- Contract (Node34)
-- Import_Pragma (Node35)
-- Has_Invariants (Flag232)
+ -- Has_Nested_Subprogram (Flag282)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Pure (Flag44)
-- Is_Intrinsic_Subprogram (Flag64)
-- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
-- Finalizer (Node28) (non-generic case only)
- -- SPARK_Aux_Pragma (Node33)
-- SPARK_Pragma (Node32)
+ -- SPARK_Aux_Pragma (Node33)
-- Contract (Node34)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Finalizer (Node28) (non-generic case only)
- -- SPARK_Aux_Pragma (Node33)
-- SPARK_Pragma (Node32)
+ -- SPARK_Aux_Pragma (Node33)
-- Contract (Node34)
-- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
-- E_Variable
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
- -- Encapsulating_State (Node10)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
-- BIP_Initialization_Call (Node29)
-- Last_Aggregate_Assignment (Node30)
-- Activation_Record_Component (Node31)
+ -- Encapsulating_State (Node32)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Has_Alignment_Clause (Flag46)
function Address_Taken (Id : E) return B;
function Alias (Id : E) return E;
function Alignment (Id : E) return U;
+ function Associated_Entity (Id : E) return E;
function Associated_Formal_Package (Id : E) return E;
function Associated_Node_For_Itype (Id : E) return N;
function Associated_Storage_Pool (Id : E) return E;
procedure Set_Address_Taken (Id : E; V : B := True);
procedure Set_Alias (Id : E; V : E);
procedure Set_Alignment (Id : E; V : U);
+ procedure Set_Associated_Entity (Id : E; V : E);
procedure Set_Associated_Formal_Package (Id : E; V : E);
procedure Set_Associated_Node_For_Itype (Id : E; V : N);
procedure Set_Associated_Storage_Pool (Id : E; V : E);
pragma Inline (Address_Taken);
pragma Inline (Alias);
pragma Inline (Alignment);
+ pragma Inline (Associated_Entity);
pragma Inline (Associated_Formal_Package);
pragma Inline (Associated_Node_For_Itype);
pragma Inline (Associated_Storage_Pool);
pragma Inline (Set_Address_Taken);
pragma Inline (Set_Alias);
pragma Inline (Set_Alignment);
+ pragma Inline (Set_Associated_Entity);
pragma Inline (Set_Associated_Formal_Package);
pragma Inline (Set_Associated_Node_For_Itype);
pragma Inline (Set_Associated_Storage_Pool);
-- enabled and the subprogram contains a construct that cannot be inlined,
-- the problematic construct is flagged accordingly.
+ function Can_Be_Inlined_In_GNATprove_Mode
+ (Spec_Id : Entity_Id;
+ Body_Id : Entity_Id) return Boolean;
+ -- Returns True if the subprogram identified by Spec_Id and Body_Id can
+ -- be inlined in GNATprove mode. One but not both of Spec_Id and Body_Id
+ -- can be Empty. Body_Id is Empty when doing a partial check on a call
+ -- to a subprogram whose body has not been seen yet, to know whether this
+ -- subprogram could possibly be inlined. GNATprove relies on this to adapt
+ -- its treatment of the subprogram.
+
procedure Cannot_Inline
(Msg : String;
N : Node_Id;
-- If an instantiation appears in unreachable code, delete the pending
-- body instance.
- function Can_Be_Inlined_In_GNATprove_Mode
- (Spec_Id : Entity_Id;
- Body_Id : Entity_Id) return Boolean;
- -- Returns True if the subprogram identified by Spec_Id and Body_Id can
- -- be inlined in GNATprove mode. One but not both of Spec_Id and Body_Id
- -- can be Empty. Body_Id is Empty when doing a partial check on a call
- -- to a subprogram whose body has not been seen yet, to know whether this
- -- subprogram could possibly be inlined. GNATprove relies on this to adapt
- -- its treatment of the subprogram.
-
end Inline;
elsif Prag_Nam = Name_Contract_Cases then
Check_Placement_In_Contract_Cases (Prag);
+ -- Attribute 'Result is allowed to appear in aspect or pragma
+ -- [Refined_]Depends (SPARK RM 6.1.5(11)).
+
+ elsif Nam_In (Prag_Nam, Name_Depends, Name_Refined_Depends)
+ and then Aname = Name_Result
+ then
+ null;
+
elsif Nam_In (Prag_Nam, Name_Post,
Name_Post_Class,
Name_Postcondition,
elsif Nkind (Subp_Spec) = N_Function_Specification
and then Present (Generic_Parent (Subp_Spec))
- and then Ekind (Pref_Id) = E_Function
- and then Present (Alias (Pref_Id))
- and then Alias (Pref_Id) = Spec_Id
+ and then Ekind_In (Pref_Id, E_Generic_Function, E_Function)
then
- return True;
+ if Generic_Parent (Subp_Spec) = Pref_Id then
+ return True;
+
+ elsif Present (Alias (Pref_Id))
+ and then Alias (Pref_Id) = Spec_Id
+ then
+ return True;
+ end if;
+ end if;
-- Otherwise the prefix does not denote the related subprogram
- else
- return False;
- end if;
+ return False;
end Denote_Same_Function;
-- Local variables
if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then
if Denote_Same_Function (Pref_Id, Spec_Id) then
+
+ -- Correct the prefix of the attribute when the context
+ -- is a generic function.
+
+ if Pref_Id /= Spec_Id then
+ Rewrite (P, New_Occurrence_Of (Spec_Id, Loc));
+ Analyze (P);
+ end if;
+
Set_Etype (N, Etype (Spec_Id));
-- Otherwise the prefix denotes some unrelated function
with Sem_Ch6; use Sem_Ch6;
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch12; use Sem_Ch12;
with Sem_Dist; use Sem_Dist;
with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
N_Subprogram_Declaration)
then
Analyze_Subprogram_Contract (Defining_Entity (Unit_Node));
+
+ -- Capture all global references in a generic subprogram that acts as
+ -- a compilation unit now that the contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Unit_Node) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Unit_Node),
+ Gen_Id => Defining_Entity (Unit_Node));
+ end if;
end if;
-- Generate distribution stubs if requested and no error
with Sem_Elab; use Sem_Elab;
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
-- circularity is detected, and used to abandon compilation after the
-- messages have been posted.
+ -----------------------------------------
+ -- Implementation of Generic Contracts --
+ -----------------------------------------
+
+ -- A "contract" is a collection of aspects and pragmas that either verify a
+ -- property of a construct at runtime or classify the data flow to and from
+ -- the construct in some fashion.
+
+ -- Generic packages, subprograms and their respective bodies may be subject
+ -- to the following contract-related aspects or pragmas collectively known
+ -- as annotations:
+
+ -- package subprogram [body]
+ -- Abstract_State Contract_Cases
+ -- Initial_Condition Depends
+ -- Initializes Extensions_Visible
+ -- Global
+ -- package body Post
+ -- Refined_State Post_Class
+ -- Postcondition
+ -- Pre
+ -- Pre_Class
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Test_Case
+
+ -- Most package contract annotations utilize forward references to classify
+ -- data declared within the package [body]. Subprogram annotations then use
+ -- the classifications to further refine them. These inter dependencies are
+ -- problematic with respect to the implementation of generics because their
+ -- analysis, capture of global references and instantiation does not mesh
+ -- well with the existing mechanism.
+
+ -- 1) Analysis of generic contracts is carried out the same way non-generic
+ -- contracts are analyzed:
+
+ -- 1.1) General rule - a contract is analyzed after all related aspects
+ -- and pragmas are analyzed. This is done by routines
+
+ -- Analyze_Package_Body_Contract
+ -- Analyze_Package_Contract
+ -- Analyze_Subprogram_Body_Contract
+ -- Analyze_Subprogram_Contract
+
+ -- 1.2) Compilation unit - the contract is analyzed after Pragmas_After
+ -- are processed.
+
+ -- 1.3) Compilation unit body - the contract is analyzed at the end of
+ -- the body declaration list.
+
+ -- 1.4) Package - the contract is analyzed at the end of the private or
+ -- visible declarations, prior to analyzing the contracts of any nested
+ -- packages or subprograms.
+
+ -- 1.5) Package body - the contract is analyzed at the end of the body
+ -- declaration list, prior to analyzing the contracts of any nested
+ -- packages or subprograms.
+
+ -- 1.6) Subprogram - if the subprogram is declared inside a block, a
+ -- package or a subprogram, then its contract is analyzed at the end of
+ -- the enclosing declarations, otherwise the subprogram is a compilation
+ -- unit 1.2).
+
+ -- 1.7) Subprogram body - if the subprogram body is declared inside a
+ -- block, a package body or a subprogram body, then its contract is
+ -- analyzed at the end of the enclosing declarations, otherwise the
+ -- subprogram is a compilation unit 1.3).
+
+ -- 2) Capture of global references within contracts is done after capturing
+ -- global references within the generic template. There are two reasons for
+ -- this delay - pragma annotations are not part of the generic template in
+ -- the case of a generic subprogram declaration, and analysis of contracts
+ -- is delayed.
+
+ -- Contract-related source pragmas within generic templates are prepared
+ -- for delayed capture of global references by routine
+
+ -- Create_Generic_Contract
+
+ -- The routine associates these pragmas with the contract of the template.
+ -- In the case of a generic subprogram declaration, the routine creates
+ -- generic templates for the pragmas declared after the subprogram because
+ -- they are not part of the template.
+
+ -- generic -- template starts
+ -- procedure Gen_Proc (Input : Integer); -- template ends
+ -- pragma Precondition (Input > 0); -- requires own template
+
+ -- 2.1) The capture of global references with aspect specifications and
+ -- source pragmas that apply to a generic unit must be suppressed when
+ -- the generic template is being processed because the contracts have not
+ -- been analyzed yet. Any attempts to capture global references at that
+ -- point will destroy the Associated_Node linkages and leave the template
+ -- undecorated. This delay is controlled by routine
+
+ -- Requires_Delayed_Save
+
+ -- 2.2) The real capture of global references within a contract is done
+ -- after the contract has been analyzed, by routine
+
+ -- Save_Global_References_In_Contract
+
+ -- 3) The instantiation of a generic contract occurs as part of the
+ -- instantiation of the contract owner. Generic subprogram declarations
+ -- require additional processing when the contract is specified by pragmas
+ -- because the pragmas are not part of the generic template. This is done
+ -- by routine
+
+ -- Instantiate_Subprogram_Contract
+
Circularity_Detected : Boolean := False;
-- This should really be reset on encountering a new main unit, but in
-- practice we are not using multiple main units so it is not critical.
-- packages, and the prefix of the formal type may be needed to resolve
-- the ambiguity in the instance ???
+ procedure Freeze_Subprogram_Body
+ (Inst_Node : Node_Id;
+ Gen_Body : Node_Id;
+ Pack_Id : Entity_Id);
+ -- The generic body may appear textually after the instance, including
+ -- in the proper body of a stub, or within a different package instance.
+ -- Given that the instance can only be elaborated after the generic, we
+ -- place freeze_nodes for the instance and/or for packages that may enclose
+ -- the instance and the generic, so that the back-end can establish the
+ -- proper order of elaboration.
+
+ function Get_Associated_Node (N : Node_Id) return Node_Id;
+ -- In order to propagate semantic information back from the analyzed copy
+ -- to the original generic, we maintain links between selected nodes in the
+ -- generic and their corresponding copies. At the end of generic analysis,
+ -- the routine Save_Global_References traverses the generic tree, examines
+ -- the semantic information, and preserves the links to those nodes that
+ -- contain global information. At instantiation, the information from the
+ -- associated node is placed on the new copy, so that name resolution is
+ -- not repeated.
+ --
+ -- Three kinds of source nodes have associated nodes:
+ --
+ -- a) those that can reference (denote) entities, that is identifiers,
+ -- character literals, expanded_names, operator symbols, operators,
+ -- and attribute reference nodes. These nodes have an Entity field
+ -- and are the set of nodes that are in N_Has_Entity.
+ --
+ -- b) aggregates (N_Aggregate and N_Extension_Aggregate)
+ --
+ -- c) selected components (N_Selected_Component)
+ --
+ -- For the first class, the associated node preserves the entity if it is
+ -- global. If the generic contains nested instantiations, the associated
+ -- node itself has been recopied, and a chain of them must be followed.
+ --
+ -- For aggregates, the associated node allows retrieval of the type, which
+ -- may otherwise not appear in the generic. The view of this type may be
+ -- different between generic and instantiation, and the full view can be
+ -- installed before the instantiation is analyzed. For aggregates of type
+ -- extensions, the same view exchange may have to be performed for some of
+ -- the ancestor types, if their view is private at the point of
+ -- instantiation.
+ --
+ -- Nodes that are selected components in the parse tree may be rewritten
+ -- as expanded names after resolution, and must be treated as potential
+ -- entity holders, which is why they also have an Associated_Node.
+ --
+ -- Nodes that do not come from source, such as freeze nodes, do not appear
+ -- in the generic tree, and need not have an associated node.
+ --
+ -- The associated node is stored in the Associated_Node field. Note that
+ -- this field overlaps Entity, which is fine, because the whole point is
+ -- that we don't need or want the normal Entity field in this situation.
+
+ function Has_Been_Exchanged (E : Entity_Id) return Boolean;
+ -- Traverse the Exchanged_Views list to see if a type was private
+ -- and has already been flipped during this phase of instantiation.
+
+ procedure Hide_Current_Scope;
+ -- When instantiating a generic child unit, the parent context must be
+ -- present, but the instance and all entities that may be generated
+ -- must be inserted in the current scope. We leave the current scope
+ -- on the stack, but make its entities invisible to avoid visibility
+ -- problems. This is reversed at the end of the instantiation. This is
+ -- not done for the instantiation of the bodies, which only require the
+ -- instances of the generic parents to be in scope.
+
function In_Same_Declarative_Part
(F_Node : Node_Id;
Inst : Node_Id) return Boolean;
-- Used to determine whether its body should be elaborated to allow
-- front-end inlining.
- procedure Set_Instance_Env
- (Gen_Unit : Entity_Id;
- Act_Unit : Entity_Id);
- -- Save current instance on saved environment, to be used to determine
- -- the global status of entities in nested instances. Part of Save_Env.
- -- called after verifying that the generic unit is legal for the instance,
- -- The procedure also examines whether the generic unit is a predefined
- -- unit, in order to set configuration switches accordingly. As a result
- -- the procedure must be called after analyzing and freezing the actuals.
+ procedure Inherit_Context (Gen_Decl : Node_Id; Inst : Node_Id);
+ -- Add the context clause of the unit containing a generic unit to a
+ -- compilation unit that is, or contains, an instantiation.
- procedure Set_Instance_Of (A : Entity_Id; B : Entity_Id);
- -- Associate analyzed generic parameter with corresponding
- -- instance. Used for semantic checks at instantiation time.
+ procedure Init_Env;
+ -- Establish environment for subsequent instantiation. Separated from
+ -- Save_Env because data-structures for visibility handling must be
+ -- initialized before call to Check_Generic_Child_Unit.
- function Has_Been_Exchanged (E : Entity_Id) return Boolean;
- -- Traverse the Exchanged_Views list to see if a type was private
- -- and has already been flipped during this phase of instantiation.
+ procedure Inline_Instance_Body
+ (N : Node_Id;
+ Gen_Unit : Entity_Id;
+ Act_Decl : Node_Id);
+ -- If front-end inlining is requested, instantiate the package body,
+ -- and preserve the visibility of its compilation unit, to insure
+ -- that successive instantiations succeed.
- procedure Hide_Current_Scope;
- -- When instantiating a generic child unit, the parent context must be
- -- present, but the instance and all entities that may be generated
- -- must be inserted in the current scope. We leave the current scope
- -- on the stack, but make its entities invisible to avoid visibility
- -- problems. This is reversed at the end of the instantiation. This is
- -- not done for the instantiation of the bodies, which only require the
- -- instances of the generic parents to be in scope.
+ procedure Insert_Freeze_Node_For_Instance
+ (N : Node_Id;
+ F_Node : Node_Id);
+ -- N denotes a package or a subprogram instantiation and F_Node is the
+ -- associated freeze node. Insert the freeze node before the first source
+ -- body which follows immediately after N. If no such body is found, the
+ -- freeze node is inserted at the end of the declarative region which
+ -- contains N.
procedure Install_Body
(Act_Body : Node_Id;
-- of packages that are early instantiations are delayed, and their freeze
-- node appears after the generic body.
- procedure Insert_Freeze_Node_For_Instance
- (N : Node_Id;
- F_Node : Node_Id);
- -- N denotes a package or a subprogram instantiation and F_Node is the
- -- associated freeze node. Insert the freeze node before the first source
- -- body which follows immediately after N. If no such body is found, the
- -- freeze node is inserted at the end of the declarative region which
- -- contains N.
-
- procedure Freeze_Subprogram_Body
- (Inst_Node : Node_Id;
- Gen_Body : Node_Id;
- Pack_Id : Entity_Id);
- -- The generic body may appear textually after the instance, including
- -- in the proper body of a stub, or within a different package instance.
- -- Given that the instance can only be elaborated after the generic, we
- -- place freeze_nodes for the instance and/or for packages that may enclose
- -- the instance and the generic, so that the back-end can establish the
- -- proper order of elaboration.
-
- procedure Init_Env;
- -- Establish environment for subsequent instantiation. Separated from
- -- Save_Env because data-structures for visibility handling must be
- -- initialized before call to Check_Generic_Child_Unit.
-
procedure Install_Formal_Packages (Par : Entity_Id);
-- Install the visible part of any formal of the parent that is a formal
-- package. Note that for the case of a formal package with a box, this
-- includes the formal part of the formal package (12.7(10/2)).
- procedure Install_Parent (P : Entity_Id; In_Body : Boolean := False);
- -- When compiling an instance of a child unit the parent (which is
- -- itself an instance) is an enclosing scope that must be made
- -- immediately visible. This procedure is also used to install the non-
- -- generic parent of a generic child unit when compiling its body, so
- -- that full views of types in the parent are made visible.
-
- procedure Remove_Parent (In_Body : Boolean := False);
- -- Reverse effect after instantiation of child is complete
-
procedure Install_Hidden_Primitives
(Prims_List : in out Elist_Id;
Gen_T : Entity_Id;
-- visibility of primitives of Gen_T. The list of primitives to which
-- the suffix is removed is added to Prims_List to restore them later.
- procedure Restore_Hidden_Primitives (Prims_List : in out Elist_Id);
- -- Restore suffix 'P' to primitives of Prims_List and leave Prims_List
- -- set to No_Elist.
-
- procedure Inline_Instance_Body
- (N : Node_Id;
- Gen_Unit : Entity_Id;
- Act_Decl : Node_Id);
- -- If front-end inlining is requested, instantiate the package body,
- -- and preserve the visibility of its compilation unit, to insure
- -- that successive instantiations succeed.
+ procedure Install_Parent (P : Entity_Id; In_Body : Boolean := False);
+ -- When compiling an instance of a child unit the parent (which is
+ -- itself an instance) is an enclosing scope that must be made
+ -- immediately visible. This procedure is also used to install the non-
+ -- generic parent of a generic child unit when compiling its body, so
+ -- that full views of types in the parent are made visible.
-- The functions Instantiate_XXX perform various legality checks and build
-- the declarations for instantiated generic parameters. In all of these
-- instances in the current declarative part that precede the one being
-- loaded. In that case a missing body is acceptable.
- procedure Inherit_Context (Gen_Decl : Node_Id; Inst : Node_Id);
- -- Add the context clause of the unit containing a generic unit to a
- -- compilation unit that is, or contains, an instantiation.
-
- function Get_Associated_Node (N : Node_Id) return Node_Id;
- -- In order to propagate semantic information back from the analyzed copy
- -- to the original generic, we maintain links between selected nodes in the
- -- generic and their corresponding copies. At the end of generic analysis,
- -- the routine Save_Global_References traverses the generic tree, examines
- -- the semantic information, and preserves the links to those nodes that
- -- contain global information. At instantiation, the information from the
- -- associated node is placed on the new copy, so that name resolution is
- -- not repeated.
- --
- -- Three kinds of source nodes have associated nodes:
- --
- -- a) those that can reference (denote) entities, that is identifiers,
- -- character literals, expanded_names, operator symbols, operators,
- -- and attribute reference nodes. These nodes have an Entity field
- -- and are the set of nodes that are in N_Has_Entity.
- --
- -- b) aggregates (N_Aggregate and N_Extension_Aggregate)
- --
- -- c) selected components (N_Selected_Component)
- --
- -- For the first class, the associated node preserves the entity if it is
- -- global. If the generic contains nested instantiations, the associated
- -- node itself has been recopied, and a chain of them must be followed.
- --
- -- For aggregates, the associated node allows retrieval of the type, which
- -- may otherwise not appear in the generic. The view of this type may be
- -- different between generic and instantiation, and the full view can be
- -- installed before the instantiation is analyzed. For aggregates of type
- -- extensions, the same view exchange may have to be performed for some of
- -- the ancestor types, if their view is private at the point of
- -- instantiation.
- --
- -- Nodes that are selected components in the parse tree may be rewritten
- -- as expanded names after resolution, and must be treated as potential
- -- entity holders, which is why they also have an Associated_Node.
- --
- -- Nodes that do not come from source, such as freeze nodes, do not appear
- -- in the generic tree, and need not have an associated node.
- --
- -- The associated node is stored in the Associated_Node field. Note that
- -- this field overlaps Entity, which is fine, because the whole point is
- -- that we don't need or want the normal Entity field in this situation.
-
procedure Map_Formal_Package_Entities (Form : Entity_Id; Act : Entity_Id);
-- Within the generic part, entities in the formal package are
-- visible. To validate subsequent type declarations, indicate
-- before installing parents of generics, that are not visible for the
-- actuals themselves.
+ procedure Remove_Parent (In_Body : Boolean := False);
+ -- Reverse effect after instantiation of child is complete
+
+ procedure Restore_Hidden_Primitives (Prims_List : in out Elist_Id);
+ -- Restore suffix 'P' to primitives of Prims_List and leave Prims_List
+ -- set to No_Elist.
+
+ procedure Save_Global_References_In_Aspects (N : Node_Id);
+ -- Save all global references found within the expressions of all aspects
+ -- that appear on node N.
+
+ procedure Set_Instance_Env
+ (Gen_Unit : Entity_Id;
+ Act_Unit : Entity_Id);
+ -- Save current instance on saved environment, to be used to determine
+ -- the global status of entities in nested instances. Part of Save_Env.
+ -- called after verifying that the generic unit is legal for the instance,
+ -- The procedure also examines whether the generic unit is a predefined
+ -- unit, in order to set configuration switches accordingly. As a result
+ -- the procedure must be called after analyzing and freezing the actuals.
+
+ procedure Set_Instance_Of (A : Entity_Id; B : Entity_Id);
+ -- Associate analyzed generic parameter with corresponding instance. Used
+ -- for semantic checks at instantiation time.
+
function True_Parent (N : Node_Id) return Node_Id;
-- For a subunit, return parent of corresponding stub, else return
-- parent of node.
(Specification (Original_Node (Gen_Decl)),
Empty, Instantiating => True));
- Renaming := Make_Package_Renaming_Declaration (Loc,
+ Renaming :=
+ Make_Package_Renaming_Declaration (Loc,
Defining_Unit_Name =>
Make_Defining_Identifier (Loc, Chars (Gen_Unit)),
- Name => New_Occurrence_Of (Formal, Loc));
+ Name => New_Occurrence_Of (Formal, Loc));
if Nkind (Gen_Id) = N_Identifier
and then Chars (Gen_Id) = Chars (Pack_Id)
-- do the same for their respective aspect specifications.
Exchange_Aspects (N, New_N);
+
+ -- Collect all contract-related source pragmas found within the template
+ -- and attach them to the contract of the package spec. This contract is
+ -- used in the capture of global references within annotations.
+
+ Create_Generic_Contract (N);
+
Id := Defining_Entity (N);
Generate_Definition (Id);
Exchange_Aspects (N, New_N);
+ -- Collect all contract-related source pragmas found within the template
+ -- and attach them to the contract of the subprogram spec. This contract
+ -- is used in the capture of global references within annotations.
+
+ Create_Generic_Contract (N);
+
Spec := Specification (N);
Id := Defining_Entity (Spec);
Generate_Definition (Id);
-- aspects that appear in the generic. This renaming declaration is
-- inserted after the instance declaration which it renames.
- procedure Instantiate_Contract (Subp_Id : Entity_Id);
- -- Instantiate all source pragmas found in the contract of subprogram
- -- Subp_Id. The instantiated pragmas are added to list Renaming_List.
+ procedure Instantiate_Subprogram_Contract (Templ : Node_Id);
+ -- Instantiate all source pragmas found in the contract of the generic
+ -- subprogram declaration template denoted by Templ. The instantiated
+ -- pragmas are added to list Renaming_List.
------------------------------------
-- Analyze_Instance_And_Renamings --
end if;
end Build_Subprogram_Renaming;
- --------------------------
- -- Instantiate_Contract --
- --------------------------
+ -------------------------------------
+ -- Instantiate_Subprogram_Contract --
+ -------------------------------------
- procedure Instantiate_Contract (Subp_Id : Entity_Id) is
+ procedure Instantiate_Subprogram_Contract (Templ : Node_Id) is
procedure Instantiate_Pragmas (First_Prag : Node_Id);
-- Instantiate all contract-related source pragmas found in the list
-- starting with pragma First_Prag. Each instantiated pragma is added
begin
Prag := First_Prag;
while Present (Prag) loop
- if Comes_From_Source (Prag)
- and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases,
- Name_Depends,
- Name_Extensions_Visible,
- Name_Global,
- Name_Postcondition,
- Name_Precondition,
- Name_Test_Case)
- then
+ if Is_Generic_Contract_Pragma (Prag) then
Inst_Prag :=
- Copy_Generic_Node
- (Original_Node (Prag), Empty, Instantiating => True);
+ Copy_Generic_Node (Prag, Empty, Instantiating => True);
Set_Analyzed (Inst_Prag, False);
Append_To (Renaming_List, Inst_Prag);
-- Local variables
- Items : constant Node_Id := Contract (Subp_Id);
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
- -- Start of processing for Instantiate_Contract
+ -- Start of processing for Instantiate_Subprogram_Contract
begin
if Present (Items) then
Instantiate_Pragmas (Contract_Test_Cases (Items));
Instantiate_Pragmas (Classifications (Items));
end if;
- end Instantiate_Contract;
+ end Instantiate_Subprogram_Contract;
-- Local variables
end if;
Append (Act_Decl, Renaming_List);
- Instantiate_Contract (Gen_Unit);
+
+ -- Contract-related source pragmas that follow a generic subprogram
+ -- must be instantiated explicitly because they are not part of the
+ -- subprogram template.
+
+ Instantiate_Subprogram_Contract (Original_Node (Gen_Decl));
Build_Subprogram_Renaming;
Analyze_Instance_And_Renamings;
----------------------
procedure Copy_Descendants is
-
use Atree.Unchecked_Access;
-- This code section is part of the implementation of an untyped
-- tree traversal, so it needs direct access to node fields.
function In_Defining_Unit_Name (Nam : Node_Id) return Boolean is
begin
- return Present (Parent (Nam))
- and then (Nkind (Parent (Nam)) = N_Defining_Program_Unit_Name
- or else
- (Nkind (Parent (Nam)) = N_Expanded_Name
- and then In_Defining_Unit_Name (Parent (Nam))));
+ return
+ Present (Parent (Nam))
+ and then (Nkind (Parent (Nam)) = N_Defining_Program_Unit_Name
+ or else
+ (Nkind (Parent (Nam)) = N_Expanded_Name
+ and then In_Defining_Unit_Name (Parent (Nam))));
end In_Defining_Unit_Name;
-- Start of processing for Copy_Generic_Node
Set_Parent (New_N, Parent_Id);
end if;
- -- If defining identifier, then all fields have been copied already
-
- if Nkind (New_N) in N_Entity then
- null;
-
-- Special casing for identifiers and other entity names and operators
- elsif Nkind_In (New_N, N_Identifier,
- N_Character_Literal,
- N_Expanded_Name,
- N_Operator_Symbol)
+ if Nkind_In (New_N, N_Character_Literal,
+ N_Expanded_Name,
+ N_Identifier,
+ N_Operator_Symbol)
or else Nkind (New_N) in N_Op
then
if not Instantiating then
end if;
end if;
+ -- Establish a link between an entity from the generic template and the
+ -- corresponding entity in the generic copy to be analyzed.
+
+ elsif Nkind (N) in N_Entity then
+ if not Instantiating then
+ Set_Associated_Entity (N, New_N);
+ end if;
+
+ -- Clear any existing link the copy may inherit from the replicated
+ -- generic template entity.
+
+ Set_Associated_Entity (New_N, Empty);
+
-- Special casing for stubs
elsif Nkind (N) in N_Body_Stub then
S_Adjustment := Save_Adjustment;
end;
- -- Don't copy Ident or Comment pragmas, since the comment belongs to the
- -- generic unit, not to the instantiating unit.
-
elsif Nkind (N) = N_Pragma and then Instantiating then
- declare
- Prag_Id : constant Pragma_Id := Get_Pragma_Id (N);
- begin
- if Prag_Id = Pragma_Ident or else Prag_Id = Pragma_Comment then
- New_N := Make_Null_Statement (Sloc (N));
- else
- Copy_Descendants;
- end if;
- end;
+
+ -- Do not copy Comment or Ident pragmas their content is relevant to
+ -- the generic unit, not to the instantiating unit.
+
+ if Nam_In (Pragma_Name (N), Name_Comment, Name_Ident) then
+ New_N := Make_Null_Statement (Sloc (N));
+
+ -- Do not copy pragmas generated from aspects because the pragmas do
+ -- not carry any semantic information, plus they will be regenerated
+ -- in the instance.
+
+ elsif From_Aspect_Specification (N) then
+ New_N := Make_Null_Statement (Sloc (N));
+
+ else
+ Copy_Descendants;
+ end if;
elsif Nkind_In (N, N_Integer_Literal, N_Real_Literal) then
-- Save_Global_References --
----------------------------
- procedure Save_Global_References (N : Node_Id) is
+ procedure Save_Global_References (Templ : Node_Id) is
+
+ -- ??? it is horrible to use global variables in highly recursive code
+
+ E : Entity_Id;
+ -- The entity of the current associated node
+
Gen_Scope : Entity_Id;
- E : Entity_Id;
- N2 : Node_Id;
+ -- The scope of the generic for which references are being saved
+
+ N2 : Node_Id;
+ -- The current associated node
function Is_Global (E : Entity_Id) return Boolean;
-- Check whether entity is defined outside of generic unit. Examine the
-- nodes. N can also be a character literal, identifier, or operator
-- symbol node, but the call has no effect in these cases.
- procedure Save_Global_Defaults (N1, N2 : Node_Id);
+ procedure Save_Global_Defaults (N1 : Node_Id; N2 : Node_Id);
-- Default actuals in nested instances must be handled specially
-- because there is no link to them from the original tree. When an
-- actual subprogram is given by a default, we add an explicit generic
-- so that it can be properly resolved in a subsequent instantiation.
procedure Save_Global_Descendant (D : Union_Id);
- -- Apply Save_Global_References recursively to the descendents of the
- -- current node.
+ -- Apply Save_References recursively to the descendents of node D
procedure Save_References (N : Node_Id);
-- This is the recursive procedure that does the work, once the
------------------
procedure Reset_Entity (N : Node_Id) is
-
procedure Set_Global_Type (N : Node_Id; N2 : Node_Id);
-- If the type of N2 is global to the generic unit, save the type in
-- the generic node. Just as we perform name capture for explicit
begin
Set_Etype (N, Typ);
- if Entity (N) /= N2
- and then Has_Private_View (Entity (N))
- then
- -- If the entity of N is not the associated node, this is a
- -- nested generic and it has an associated node as well, whose
- -- type is already the full view (see below). Indicate that the
- -- original node has a private view.
+ -- If the entity of N is not the associated node, this is a
+ -- nested generic and it has an associated node as well, whose
+ -- type is already the full view (see below). Indicate that the
+ -- original node has a private view.
+ if Entity (N) /= N2 and then Has_Private_View (Entity (N)) then
Set_Has_Private_View (N);
end if;
begin
N2 := Get_Associated_Node (N);
- E := Entity (N2);
+ E := Entity (N2);
if Present (E) then
-- preserve in this case, since the expansion will be redone in
-- the instance.
- if not Nkind_In (E, N_Defining_Identifier,
- N_Defining_Character_Literal,
+ if not Nkind_In (E, N_Defining_Character_Literal,
+ N_Defining_Identifier,
N_Defining_Operator_Symbol)
then
Set_Associated_Node (N, Empty);
- Set_Etype (N, Empty);
+ Set_Etype (N, Empty);
return;
end if;
Set_Associated_Node (N, N2);
Set_Global_Type (N, N2);
- else
- -- Renaming is local, and will be resolved in instance
+ -- Renaming is local, and will be resolved in instance
+ else
Set_Associated_Node (N, Empty);
- Set_Etype (N, Empty);
+ Set_Etype (N, Empty);
end if;
else
and then Is_Generic_Type (Etype (N2))
and then (Base_Type (Etype (Right_Opnd (N2))) = Etype (N2)
or else
- Base_Type (Etype (Left_Opnd (N2))) = Etype (N2))
+ Base_Type (Etype (Left_Opnd (N2))) = Etype (N2))
and then Is_Intrinsic_Subprogram (E)
then
null;
- else
- -- Entity is local. Mark generic node as unresolved.
- -- Note that now it does not have an entity.
+ -- Entity is local. Mark generic node as unresolved. Note that now
+ -- it does not have an entity.
+ else
Set_Associated_Node (N, Empty);
- Set_Etype (N, Empty);
+ Set_Etype (N, Empty);
end if;
if Nkind (Parent (N)) in N_Generic_Instantiation
and then Parent (N) = Name (Parent (Parent (N)))
then
Save_Global_Defaults
- (Parent (Parent (N)), Parent (Parent ((N2))));
+ (Parent (Parent (N)), Parent (Parent (N2)));
end if;
-- A selected component may denote a static constant that has been
then
Rewrite (Parent (N), New_Copy (Parent (N2)));
Set_Analyzed (Parent (N), False);
-
- else
- null;
end if;
-- A selected component may be transformed into a parameterless
begin
case Nkind (N) is
when N_Binary_Op =>
- Save_Global_Descendant (Union_Id (Left_Opnd (N)));
+ Save_Global_Descendant (Union_Id (Left_Opnd (N)));
Save_Global_Descendant (Union_Id (Right_Opnd (N)));
when N_Unary_Op =>
Save_Global_Descendant (Union_Id (Right_Opnd (N)));
- when N_Expanded_Name | N_Selected_Component =>
+ when N_Expanded_Name |
+ N_Selected_Component =>
Save_Global_Descendant (Union_Id (Prefix (N)));
Save_Global_Descendant (Union_Id (Selector_Name (N)));
- when N_Identifier | N_Character_Literal | N_Operator_Symbol =>
+ when N_Identifier |
+ N_Character_Literal |
+ N_Operator_Symbol =>
null;
when others =>
-- Save_Global_Defaults --
--------------------------
- procedure Save_Global_Defaults (N1, N2 : Node_Id) is
+ procedure Save_Global_Defaults (N1 : Node_Id; N2 : Node_Id) is
Loc : constant Source_Ptr := Sloc (N1);
Assoc2 : constant List_Id := Generic_Associations (N2);
Gen_Id : constant Entity_Id := Get_Generic_Entity (N2);
if Is_Global (Actual) then
Ndec :=
Make_Generic_Association (Loc,
- Selector_Name => New_Occurrence_Of (Subp, Loc),
- Explicit_Generic_Actual_Parameter =>
- New_Occurrence_Of (Actual, Loc));
+ Selector_Name =>
+ New_Occurrence_Of (Subp, Loc),
+ Explicit_Generic_Actual_Parameter =>
+ New_Occurrence_Of (Actual, Loc));
Set_Associated_Node
(Explicit_Generic_Actual_Parameter (Ndec), Def);
elsif Present (Next (Act2)) then
Ndec :=
Make_Generic_Association (Loc,
- Selector_Name => New_Occurrence_Of (Subp, Loc),
- Explicit_Generic_Actual_Parameter => Empty);
+ Selector_Name =>
+ New_Occurrence_Of (Subp, Loc),
+ Explicit_Generic_Actual_Parameter => Empty);
Append (Ndec, Assoc1);
end if;
(Selector_Name (Name (N1)), Selector_Name (Name (N2)));
Set_Etype (Name (N1), Etype (Gen_Id));
end if;
-
end Save_Global_Defaults;
----------------------------
procedure Save_References (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
- begin
- if N = Empty then
- null;
+ function Requires_Delayed_Save (Nod : Node_Id) return Boolean;
+ -- Determine whether arbitrary node Nod requires delayed capture of
+ -- global references within its aspect specifications.
- elsif Nkind_In (N, N_Character_Literal, N_Operator_Symbol) then
- if Nkind (N) = Nkind (Get_Associated_Node (N)) then
- Reset_Entity (N);
+ procedure Save_References_In_Aggregate (N : Node_Id);
+ -- Save all global references in [extension] aggregate node N
- elsif Nkind (N) = N_Operator_Symbol
- and then Nkind (Get_Associated_Node (N)) = N_String_Literal
- then
- Change_Operator_Symbol_To_String_Literal (N);
- end if;
+ procedure Save_References_In_Char_Lit_Or_Op_Symbol (N : Node_Id);
+ -- Save all global references in a character literal or operator
+ -- symbol denoted by N.
- elsif Nkind (N) in N_Op then
- if Nkind (N) = Nkind (Get_Associated_Node (N)) then
- if Nkind (N) = N_Op_Concat then
- Set_Is_Component_Left_Opnd (N,
- Is_Component_Left_Opnd (Get_Associated_Node (N)));
+ procedure Save_References_In_Descendants (N : Node_Id);
+ -- Save all global references in all descendants of node N
- Set_Is_Component_Right_Opnd (N,
- Is_Component_Right_Opnd (Get_Associated_Node (N)));
- end if;
+ procedure Save_References_In_Identifier (N : Node_Id);
+ -- Save all global references in identifier node N
- Reset_Entity (N);
+ procedure Save_References_In_Operator (N : Node_Id);
+ -- Save all global references in operator node N
- else
- -- Node may be transformed into call to a user-defined operator
+ procedure Save_References_In_Pragma (Prag : Node_Id);
+ -- Save all global references found within the expression of pragma
+ -- Prag.
- N2 := Get_Associated_Node (N);
+ ---------------------------
+ -- Requires_Delayed_Save --
+ ---------------------------
- if Nkind (N2) = N_Function_Call then
- E := Entity (Name (N2));
+ function Requires_Delayed_Save (Nod : Node_Id) return Boolean is
+ begin
+ -- Generic packages and subprograms require delayed capture of
+ -- global references within their aspects due to the timing of
+ -- annotation analysis.
- if Present (E)
- and then Is_Global (E)
- then
- Set_Etype (N, Etype (N2));
- else
- Set_Associated_Node (N, Empty);
- Set_Etype (N, Empty);
- end if;
+ if Nkind_In (Nod, N_Generic_Package_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Package_Body,
+ N_Package_Body_Stub,
+ N_Subprogram_Body,
+ N_Subprogram_Body_Stub)
+ then
+ -- Since the capture of global references is done on the
+ -- unanalyzed generic template, there is no information around
+ -- to infer the context. Use the Associated_Entity linkages to
+ -- peek into the analyzed generic copy and determine what the
+ -- template corresponds to.
+
+ if Nod = Templ then
+ return
+ Is_Generic_Declaration_Or_Body
+ (Unit_Declaration_Node
+ (Associated_Entity (Defining_Entity (Nod))));
+
+ -- Otherwise the generic unit being processed is not the top
+ -- level template. It is safe to capture of global references
+ -- within the generic unit because at this point the top level
+ -- copy is fully analyzed.
- elsif Nkind_In (N2, N_Integer_Literal,
- N_Real_Literal,
- N_String_Literal)
- then
- if Present (Original_Node (N2))
- and then Nkind (Original_Node (N2)) = Nkind (N)
- then
+ else
+ return False;
+ end if;
- -- Operation was constant-folded. Whenever possible,
- -- recover semantic information from unfolded node,
- -- for ASIS use.
+ -- Otherwise capture the global references without interference
- Set_Associated_Node (N, Original_Node (N2));
+ else
+ return False;
+ end if;
+ end Requires_Delayed_Save;
- if Nkind (N) = N_Op_Concat then
- Set_Is_Component_Left_Opnd (N,
- Is_Component_Left_Opnd (Get_Associated_Node (N)));
- Set_Is_Component_Right_Opnd (N,
- Is_Component_Right_Opnd (Get_Associated_Node (N)));
- end if;
+ ----------------------------------
+ -- Save_References_In_Aggregate --
+ ----------------------------------
- Reset_Entity (N);
+ procedure Save_References_In_Aggregate (N : Node_Id) is
+ Nam : Node_Id;
+ Qual : Node_Id := Empty;
+ Typ : Entity_Id := Empty;
- else
- -- If original node is already modified, propagate
- -- constant-folding to template.
+ use Atree.Unchecked_Access;
+ -- This code section is part of implementing an untyped tree
+ -- traversal, so it needs direct access to node fields.
- Rewrite (N, New_Copy (N2));
- Set_Analyzed (N, False);
- end if;
+ begin
+ N2 := Get_Associated_Node (N);
- elsif Nkind (N2) = N_Identifier
- and then Ekind (Entity (N2)) = E_Enumeration_Literal
+ if Present (N2) then
+ Typ := Etype (N2);
+
+ -- In an instance within a generic, use the name of the actual
+ -- and not the original generic parameter. If the actual is
+ -- global in the current generic it must be preserved for its
+ -- instantiation.
+
+ if Nkind (Parent (Typ)) = N_Subtype_Declaration
+ and then Present (Generic_Parent_Type (Parent (Typ)))
then
- -- Same if call was folded into a literal, but in this case
- -- retain the entity to avoid spurious ambiguities if it is
- -- overloaded at the point of instantiation or inlining.
+ Typ := Base_Type (Typ);
+ Set_Etype (N2, Typ);
+ end if;
+ end if;
- Rewrite (N, New_Copy (N2));
- Set_Analyzed (N, False);
+ if No (N2) or else No (Typ) or else not Is_Global (Typ) then
+ Set_Associated_Node (N, Empty);
+
+ -- If the aggregate is an actual in a call, it has been
+ -- resolved in the current context, to some local type. The
+ -- enclosing call may have been disambiguated by the aggregate,
+ -- and this disambiguation might fail at instantiation time
+ -- because the type to which the aggregate did resolve is not
+ -- preserved. In order to preserve some of this information,
+ -- wrap the aggregate in a qualified expression, using the id
+ -- of its type. For further disambiguation we qualify the type
+ -- name with its scope (if visible) because both id's will have
+ -- corresponding entities in an instance. This resolves most of
+ -- the problems with missing type information on aggregates in
+ -- instances.
+
+ if Present (N2)
+ and then Nkind (N2) = Nkind (N)
+ and then Nkind (Parent (N2)) in N_Subprogram_Call
+ and then Present (Typ)
+ and then Comes_From_Source (Typ)
+ then
+ Nam := Make_Identifier (Loc, Chars (Typ));
+
+ if Is_Immediately_Visible (Scope (Typ)) then
+ Nam :=
+ Make_Selected_Component (Loc,
+ Prefix =>
+ Make_Identifier (Loc, Chars (Scope (Typ))),
+ Selector_Name => Nam);
+ end if;
+
+ Qual :=
+ Make_Qualified_Expression (Loc,
+ Subtype_Mark => Nam,
+ Expression => Relocate_Node (N));
end if;
end if;
- -- Complete operands check if node has not been constant-folded
+ Save_Global_Descendant (Field1 (N));
+ Save_Global_Descendant (Field2 (N));
+ Save_Global_Descendant (Field3 (N));
+ Save_Global_Descendant (Field5 (N));
- if Nkind (N) in N_Op then
- Save_Entity_Descendants (N);
+ if Present (Qual) then
+ Rewrite (N, Qual);
end if;
+ end Save_References_In_Aggregate;
+
+ ----------------------------------------------
+ -- Save_References_In_Char_Lit_Or_Op_Symbol --
+ ----------------------------------------------
+
+ procedure Save_References_In_Char_Lit_Or_Op_Symbol (N : Node_Id) is
+ begin
+ if Nkind (N) = Nkind (Get_Associated_Node (N)) then
+ Reset_Entity (N);
+
+ elsif Nkind (N) = N_Operator_Symbol
+ and then Nkind (Get_Associated_Node (N)) = N_String_Literal
+ then
+ Change_Operator_Symbol_To_String_Literal (N);
+ end if;
+ end Save_References_In_Char_Lit_Or_Op_Symbol;
+
+ ------------------------------------
+ -- Save_References_In_Descendants --
+ ------------------------------------
+
+ procedure Save_References_In_Descendants (N : Node_Id) is
+ use Atree.Unchecked_Access;
+ -- This code section is part of implementing an untyped tree
+ -- traversal, so it needs direct access to node fields.
+
+ begin
+ Save_Global_Descendant (Field1 (N));
+ Save_Global_Descendant (Field2 (N));
+ Save_Global_Descendant (Field3 (N));
+ Save_Global_Descendant (Field4 (N));
+ Save_Global_Descendant (Field5 (N));
+ end Save_References_In_Descendants;
+
+ -----------------------------------
+ -- Save_References_In_Identifier --
+ -----------------------------------
+
+ procedure Save_References_In_Identifier (N : Node_Id) is
+ begin
+ -- The node did not undergo a transformation
- elsif Nkind (N) = N_Identifier then
if Nkind (N) = Nkind (Get_Associated_Node (N)) then
-- If this is a discriminant reference, always save it. It is
(N, Original_Discriminant (Get_Associated_Node (N)));
Reset_Entity (N);
+ -- The analysis of the generic copy transformed the identifier
+ -- into another construct. Propagate the changes to the template.
+
else
N2 := Get_Associated_Node (N);
+ -- The identifier denotes a call to a parameterless function.
+ -- Mark the node as resolved when the function is external.
+
if Nkind (N2) = N_Function_Call then
E := Entity (Name (N2));
- -- Name resolves to a call to parameterless function. If
- -- original entity is global, mark node as resolved.
-
- if Present (E)
- and then Is_Global (E)
- then
+ if Present (E) and then Is_Global (E) then
Set_Etype (N, Etype (N2));
else
Set_Associated_Node (N, Empty);
Set_Etype (N, Empty);
end if;
+ -- The identifier denotes a named number that was constant
+ -- folded. Preserve the original name for ASIS and undo the
+ -- constant folding which will be repeated in the instance.
+
elsif Nkind_In (N2, N_Integer_Literal, N_Real_Literal)
and then Is_Entity_Name (Original_Node (N2))
then
- -- Name resolves to named number that is constant-folded,
- -- We must preserve the original name for ASIS use, and
- -- undo the constant-folding, which will be repeated in
- -- each instance.
-
Set_Associated_Node (N, Original_Node (N2));
Reset_Entity (N);
- elsif Nkind (N2) = N_String_Literal then
-
- -- Name resolves to string literal. Perform the same
- -- replacement in generic.
+ -- The identifier resolved to a string literal. Propagate this
+ -- information to the generic template.
+ elsif Nkind (N2) = N_String_Literal then
Rewrite (N, New_Copy (N2));
- elsif Nkind (N2) = N_Explicit_Dereference then
-
- -- An identifier is rewritten as a dereference if it is the
- -- prefix in an implicit dereference (call or attribute).
- -- The analysis of an instantiation will expand the node
- -- again, so we preserve the original tree but link it to
- -- the resolved entity in case it is global.
+ -- The identifier is rewritten as a dereference if it is the
+ -- prefix of an implicit dereference. Preserve the original
+ -- tree as the analysis of the instance will expand the node
+ -- again, but preserve the resolved entity if it is global.
+ elsif Nkind (N2) = N_Explicit_Dereference then
if Is_Entity_Name (Prefix (N2))
and then Present (Entity (Prefix (N2)))
and then Is_Global (Entity (Prefix (N2)))
Set_Associated_Node (N, Prefix (N2));
elsif Nkind (Prefix (N2)) = N_Function_Call
+ and then Present (Entity (Name (Prefix (N2))))
and then Is_Global (Entity (Name (Prefix (N2))))
then
Rewrite (N,
Make_Explicit_Dereference (Loc,
- Prefix => Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of
- (Entity (Name (Prefix (N2))), Loc))));
+ Prefix =>
+ Make_Function_Call (Loc,
+ Name =>
+ New_Occurrence_Of
+ (Entity (Name (Prefix (N2))), Loc))));
else
Set_Associated_Node (N, Empty);
then
Set_Associated_Node (N, Original_Node (N2));
Reset_Entity (N);
-
- else
- null;
end if;
end if;
+ end Save_References_In_Identifier;
- elsif Nkind (N) in N_Entity then
- null;
+ ---------------------------------
+ -- Save_References_In_Operator --
+ ---------------------------------
- else
- declare
- Qual : Node_Id := Empty;
- Typ : Entity_Id := Empty;
- Nam : Node_Id;
+ procedure Save_References_In_Operator (N : Node_Id) is
+ begin
+ -- The node did not undergo a transformation
- use Atree.Unchecked_Access;
- -- This code section is part of implementing an untyped tree
- -- traversal, so it needs direct access to node fields.
+ if Nkind (N) = Nkind (Get_Associated_Node (N)) then
+ if Nkind (N) = N_Op_Concat then
+ Set_Is_Component_Left_Opnd (N,
+ Is_Component_Left_Opnd (Get_Associated_Node (N)));
- begin
- if Nkind_In (N, N_Aggregate, N_Extension_Aggregate) then
- N2 := Get_Associated_Node (N);
+ Set_Is_Component_Right_Opnd (N,
+ Is_Component_Right_Opnd (Get_Associated_Node (N)));
+ end if;
- if No (N2) then
- Typ := Empty;
+ Reset_Entity (N);
- else
- Typ := Etype (N2);
+ -- The analysis of the generic copy transformed the operator into
+ -- some other construct. Propagate the changes to the template.
- -- In an instance within a generic, use the name of the
- -- actual and not the original generic parameter. If the
- -- actual is global in the current generic it must be
- -- preserved for its instantiation.
+ else
+ N2 := Get_Associated_Node (N);
- if Nkind (Parent (Typ)) = N_Subtype_Declaration
- and then
- Present (Generic_Parent_Type (Parent (Typ)))
- then
- Typ := Base_Type (Typ);
- Set_Etype (N2, Typ);
- end if;
- end if;
+ -- The operator resoved to a function call
- if No (N2) or else No (Typ) or else not Is_Global (Typ) then
+ if Nkind (N2) = N_Function_Call then
+ E := Entity (Name (N2));
+
+ if Present (E) and then Is_Global (E) then
+ Set_Etype (N, Etype (N2));
+ else
Set_Associated_Node (N, Empty);
+ Set_Etype (N, Empty);
+ end if;
- -- If the aggregate is an actual in a call, it has been
- -- resolved in the current context, to some local type.
- -- The enclosing call may have been disambiguated by the
- -- aggregate, and this disambiguation might fail at
- -- instantiation time because the type to which the
- -- aggregate did resolve is not preserved. In order to
- -- preserve some of this information, we wrap the
- -- aggregate in a qualified expression, using the id of
- -- its type. For further disambiguation we qualify the
- -- type name with its scope (if visible) because both
- -- id's will have corresponding entities in an instance.
- -- This resolves most of the problems with missing type
- -- information on aggregates in instances.
-
- if Nkind (N2) = Nkind (N)
- and then Nkind (Parent (N2)) in N_Subprogram_Call
- and then Comes_From_Source (Typ)
- then
- if Is_Immediately_Visible (Scope (Typ)) then
- Nam :=
- Make_Selected_Component (Loc,
- Prefix =>
- Make_Identifier (Loc, Chars (Scope (Typ))),
- Selector_Name =>
- Make_Identifier (Loc, Chars (Typ)));
- else
- Nam := Make_Identifier (Loc, Chars (Typ));
- end if;
+ -- The operator was folded into a literal
- Qual :=
- Make_Qualified_Expression (Loc,
- Subtype_Mark => Nam,
- Expression => Relocate_Node (N));
+ elsif Nkind_In (N2, N_Integer_Literal,
+ N_Real_Literal,
+ N_String_Literal)
+ then
+ if Present (Original_Node (N2))
+ and then Nkind (Original_Node (N2)) = Nkind (N)
+ then
+ -- Operation was constant-folded. Whenever possible,
+ -- recover semantic information from unfolded node,
+ -- for ASIS use.
+
+ Set_Associated_Node (N, Original_Node (N2));
+
+ if Nkind (N) = N_Op_Concat then
+ Set_Is_Component_Left_Opnd (N,
+ Is_Component_Left_Opnd (Get_Associated_Node (N)));
+ Set_Is_Component_Right_Opnd (N,
+ Is_Component_Right_Opnd (Get_Associated_Node (N)));
end if;
- end if;
- Save_Global_Descendant (Field1 (N));
- Save_Global_Descendant (Field2 (N));
- Save_Global_Descendant (Field3 (N));
- Save_Global_Descendant (Field5 (N));
+ Reset_Entity (N);
- if Present (Qual) then
- Rewrite (N, Qual);
+ -- Propagate the constant folding back to the template
+
+ else
+ Rewrite (N, New_Copy (N2));
+ Set_Analyzed (N, False);
end if;
- -- All other cases than aggregates
+ -- The operator was folded into an enumeration literal. Retain
+ -- the entity to avoid spurious ambiguities if it is overloaded
+ -- at the point of instantiation or inlining.
+
+ elsif Nkind (N2) = N_Identifier
+ and then Ekind (Entity (N2)) = E_Enumeration_Literal
+ then
+ Rewrite (N, New_Copy (N2));
+ Set_Analyzed (N, False);
+ end if;
+ end if;
+
+ -- Complete the operands check if node has not been constant
+ -- folded.
+
+ if Nkind (N) in N_Op then
+ Save_Entity_Descendants (N);
+ end if;
+ end Save_References_In_Operator;
+
+ -------------------------------
+ -- Save_References_In_Pragma --
+ -------------------------------
+
+ procedure Save_References_In_Pragma (Prag : Node_Id) is
+ Context : Node_Id;
+ Do_Save : Boolean := True;
+
+ use Atree.Unchecked_Access;
+ -- This code section is part of implementing an untyped tree
+ -- traversal, so it needs direct access to node fields.
+
+ begin
+ -- Do not save global references in pragmas generated from aspects
+ -- because the pragmas will be regenerated at instantiation time.
+
+ if From_Aspect_Specification (Prag) then
+ Do_Save := False;
+
+ -- The capture of global references within contract-related source
+ -- pragmas associated with generic packages, subprograms or their
+ -- respective bodies must be delayed due to timing of annotation
+ -- analysis. Global references are still captured in routine
+ -- Save_Global_References_In_Contract.
+
+ elsif Is_Generic_Contract_Pragma (Prag) and then Prag /= Templ then
+ if Is_Package_Contract_Annotation (Prag) then
+ Context := Find_Related_Package_Or_Body (Prag);
else
- Save_Global_Descendant (Field1 (N));
- Save_Global_Descendant (Field2 (N));
- Save_Global_Descendant (Field3 (N));
- Save_Global_Descendant (Field4 (N));
- Save_Global_Descendant (Field5 (N));
+ pragma Assert (Is_Subprogram_Contract_Annotation (Prag));
+ Context := Find_Related_Subprogram_Or_Body (Prag);
end if;
- end;
+
+ -- The use of Original_Node accounts for the case when the
+ -- related context is generic template.
+
+ if Requires_Delayed_Save (Original_Node (Context)) then
+ Do_Save := False;
+ end if;
+ end if;
+
+ -- For all other cases, save all global references within the
+ -- descendants, but skip the following semantic fields:
+
+ -- Field1 - Next_Pragma
+ -- Field3 - Corresponding_Aspect
+ -- Field5 - Next_Rep_Item
+
+ if Do_Save then
+ Save_Global_Descendant (Field2 (Prag));
+ Save_Global_Descendant (Field4 (Prag));
+ end if;
+ end Save_References_In_Pragma;
+
+ -- Start of processing for Save_References
+
+ begin
+ if N = Empty then
+ null;
+
+ -- Aggregates
+
+ elsif Nkind_In (N, N_Aggregate, N_Extension_Aggregate) then
+ Save_References_In_Aggregate (N);
+
+ -- Character literals, operator symbols
+
+ elsif Nkind_In (N, N_Character_Literal, N_Operator_Symbol) then
+ Save_References_In_Char_Lit_Or_Op_Symbol (N);
+
+ -- Defining identifiers
+
+ elsif Nkind (N) in N_Entity then
+ null;
+
+ -- Identifiers
+
+ elsif Nkind (N) = N_Identifier then
+ Save_References_In_Identifier (N);
+
+ -- Operators
+
+ elsif Nkind (N) in N_Op then
+ Save_References_In_Operator (N);
+
+ -- Pragmas
+
+ elsif Nkind (N) = N_Pragma then
+ Save_References_In_Pragma (N);
+
+ else
+ Save_References_In_Descendants (N);
end if;
- -- Save all global references found within the aspects of the related
- -- node. This is not done for generic subprograms because the aspects
- -- must be delayed and analyzed at the end of the declarative part.
- -- Only then can global references be saved. This action is performed
- -- by the analysis of the generic subprogram contract.
+ -- Save all global references found within the aspect specifications
+ -- of the related node.
- if Nkind (N) /= N_Generic_Subprogram_Declaration then
- Save_Global_References_In_Aspects (N);
+ if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
+
+ -- The capture of global references within aspects associated with
+ -- generic packages, subprograms or their bodies must be delayed
+ -- due to timing of annotation analysis. Global references are
+ -- still captured in routine Save_Global_References_In_Contract.
+
+ if Requires_Delayed_Save (N) then
+ null;
+
+ -- Otherwise save all global references within the aspects
+
+ else
+ Save_Global_References_In_Aspects (N);
+ end if;
end if;
end Save_References;
Gen_Scope := Scope (Gen_Scope);
end loop;
- Save_References (N);
+ Save_References (Templ);
end Save_Global_References;
---------------------------------------
Expr : Node_Id;
begin
- if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
- Asp := First (Aspect_Specifications (N));
- while Present (Asp) loop
- Expr := Expression (Asp);
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ Expr := Expression (Asp);
+
+ if Present (Expr) then
+ Save_Global_References (Expr);
+ end if;
- if Present (Expr) then
- Save_Global_References (Expr);
+ Next (Asp);
+ end loop;
+ end Save_Global_References_In_Aspects;
+
+ ----------------------------------------
+ -- Save_Global_References_In_Contract --
+ ----------------------------------------
+
+ procedure Save_Global_References_In_Contract
+ (Templ : Node_Id;
+ Gen_Id : Entity_Id)
+ is
+ procedure Save_Global_References_In_List (First_Prag : Node_Id);
+ -- Save all global references in contract-related source pragmas found
+ -- in the list starting with pragma First_Prag.
+
+ ------------------------------------
+ -- Save_Global_References_In_List --
+ ------------------------------------
+
+ procedure Save_Global_References_In_List (First_Prag : Node_Id) is
+ Prag : Node_Id;
+
+ begin
+ Prag := First_Prag;
+ while Present (Prag) loop
+ if Is_Generic_Contract_Pragma (Prag) then
+ Save_Global_References (Prag);
end if;
- Next (Asp);
+ Prag := Next_Pragma (Prag);
end loop;
+ end Save_Global_References_In_List;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
+
+ -- Start of processing for Save_Global_References_In_Contract
+
+ begin
+ -- The entity of the analyzed generic copy must be on the scope stack
+ -- to ensure proper detection of global references.
+
+ Push_Scope (Gen_Id);
+
+ if Permits_Aspect_Specifications (Templ)
+ and then Has_Aspects (Templ)
+ then
+ Save_Global_References_In_Aspects (Templ);
end if;
- end Save_Global_References_In_Aspects;
+
+ if Present (Items) then
+ Save_Global_References_In_List (Pre_Post_Conditions (Items));
+ Save_Global_References_In_List (Contract_Test_Cases (Items));
+ Save_Global_References_In_List (Classifications (Items));
+ end if;
+
+ Pop_Scope;
+ end Save_Global_References_In_Contract;
--------------------------------------
-- Set_Copied_Sloc_For_Inlined_Body --
-- pragma, or because a pragma appears for the instance in the scope.
-- of the instance.
- procedure Save_Global_References (N : Node_Id);
+ procedure Save_Global_References (Templ : Node_Id);
-- Traverse the original generic unit, and capture all references to
- -- entities that are defined outside of the generic in the analyzed
- -- tree for the template. These references are copied into the original
- -- tree, so that they appear automatically in every instantiation.
- -- A critical invariant in this approach is that if an id in the generic
- -- resolves to a local entity, the corresponding id in the instance
- -- will resolve to the homologous entity in the instance, even though
- -- the enclosing context for resolution is different, as long as the
- -- global references have been captured as described here.
+ -- entities that are defined outside of the generic in the analyzed tree
+ -- for the template. These references are copied into the original tree,
+ -- so that they appear automatically in every instantiation. A critical
+ -- invariant in this approach is that if an id in the generic resolves to
+ -- a local entity, the corresponding id in the instance will resolve to
+ -- the homologous entity in the instance, even though the enclosing context
+ -- for resolution is different, as long as the global references have been
+ -- captured as described here.
-- Because instantiations can be nested, the environment of the instance,
-- involving the actuals and other data-structures, must be saved and
-- restored in stack-like fashion. Front-end inlining also uses these
-- structures for the management of private/full views.
- procedure Save_Global_References_In_Aspects (N : Node_Id);
- -- Save all global references in the aspect specifications of node N
+ procedure Save_Global_References_In_Contract
+ (Templ : Node_Id;
+ Gen_Id : Entity_Id);
+ -- Save all global references found within the aspect specifications and
+ -- the contract-related source pragmas assocated with generic template
+ -- Templ. Gen_Id denotes the entity of the analyzed generic copy.
procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id);
-- This procedure is used when a subprogram body is inlined. This process
end if;
end Analyze_Aspect_Specifications;
+ ---------------------------------------------------
+ -- Analyze_Aspect_Specifications_On_Body_Or_Stub --
+ ---------------------------------------------------
+
+ procedure Analyze_Aspect_Specifications_On_Body_Or_Stub (N : Node_Id) is
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+
+ procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id);
+ -- Subprogram body [stub] N has aspects, but they are not properly
+ -- placed. Emit an error message depending on the aspects involved.
+ -- Spec_Id is the entity of the corresponding spec.
+
+ --------------------------------
+ -- Diagnose_Misplaced_Aspects --
+ --------------------------------
+
+ procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id) is
+ procedure Misplaced_Aspect_Error
+ (Asp : Node_Id;
+ Ref_Nam : Name_Id);
+ -- Emit an error message concerning misplaced aspect Asp. Ref_Nam is
+ -- the name of the refined version of the aspect.
+
+ ----------------------------
+ -- Misplaced_Aspect_Error --
+ ----------------------------
+
+ procedure Misplaced_Aspect_Error
+ (Asp : Node_Id;
+ Ref_Nam : Name_Id)
+ is
+ Asp_Nam : constant Name_Id := Chars (Identifier (Asp));
+ Asp_Id : constant Aspect_Id := Get_Aspect_Id (Asp_Nam);
+
+ begin
+ -- The corresponding spec already contains the aspect in question
+ -- and the one appearing on the body must be the refined form:
+
+ -- procedure P with Global ...;
+ -- procedure P with Global ... is ... end P;
+ -- ^
+ -- Refined_Global
+
+ if Has_Aspect (Spec_Id, Asp_Id) then
+ Error_Msg_Name_1 := Asp_Nam;
+
+ -- Subunits cannot carry aspects that apply to a subprogram
+ -- declaration.
+
+ if Nkind (Parent (N)) = N_Subunit then
+ Error_Msg_N ("aspect % cannot apply to a subunit", Asp);
+
+ -- Otherwise suggest the refined form
+
+ else
+ Error_Msg_Name_2 := Ref_Nam;
+ Error_Msg_N ("aspect % should be %", Asp);
+ end if;
+
+ -- Otherwise the aspect must appear on the spec, not on the body
+
+ -- procedure P;
+ -- procedure P with Global ... is ... end P;
+
+ else
+ Error_Msg_N
+ ("aspect specification must appear in subprogram declaration",
+ Asp);
+ end if;
+ end Misplaced_Aspect_Error;
+
+ -- Local variables
+
+ Asp : Node_Id;
+ Asp_Nam : Name_Id;
+
+ -- Start of processing for Diagnose_Misplaced_Aspects
+
+ begin
+ -- Iterate over the aspect specifications and emit specific errors
+ -- where applicable.
+
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ Asp_Nam := Chars (Identifier (Asp));
+
+ -- Do not emit errors on aspects that can appear on a subprogram
+ -- body. This scenario occurs when the aspect specification list
+ -- contains both misplaced and properly placed aspects.
+
+ if Aspect_On_Body_Or_Stub_OK (Get_Aspect_Id (Asp_Nam)) then
+ null;
+
+ -- Special diagnostics for SPARK aspects
+
+ elsif Asp_Nam = Name_Depends then
+ Misplaced_Aspect_Error (Asp, Name_Refined_Depends);
+
+ elsif Asp_Nam = Name_Global then
+ Misplaced_Aspect_Error (Asp, Name_Refined_Global);
+
+ elsif Asp_Nam = Name_Post then
+ Misplaced_Aspect_Error (Asp, Name_Refined_Post);
+
+ -- Otherwise a language-defined aspect is misplaced
+
+ else
+ Error_Msg_N
+ ("aspect specification must appear in subprogram declaration",
+ Asp);
+ end if;
+
+ Next (Asp);
+ end loop;
+ end Diagnose_Misplaced_Aspects;
+
+ -- Local variables
+
+ Spec_Id : Entity_Id;
+
+ -- Start of processing for Analyze_Aspects_On_Body_Or_Stub
+
+ begin
+ if Nkind (N) = N_Subprogram_Body_Stub then
+ Spec_Id := Corresponding_Spec_Of_Stub (N);
+ else
+ Spec_Id := Corresponding_Spec (N);
+ end if;
+
+ -- Language-defined aspects cannot be associated with a subprogram body
+ -- [stub] if the subprogram has a spec. Certain implementation defined
+ -- aspects are allowed to break this rule (for all applicable cases, see
+ -- table Aspects.Aspect_On_Body_Or_Stub_OK).
+
+ if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then
+ Diagnose_Misplaced_Aspects (Spec_Id);
+ else
+ Analyze_Aspect_Specifications (N, Body_Id);
+ end if;
+ end Analyze_Aspect_Specifications_On_Body_Or_Stub;
+
-----------------------
-- Analyze_At_Clause --
-----------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- is the corresponding entity declared by the declaration node N. Callers
-- should check that Has_Aspects (N) is True before calling this routine.
+ procedure Analyze_Aspect_Specifications_On_Body_Or_Stub (N : Node_Id);
+ -- Analyze the aspect specifications of [generic] subprogram body or stub
+ -- N. Callers should check that Has_Aspects (N) is True before calling the
+ -- routine. This routine diagnoses misplaced aspects that should appear on
+ -- the initial declaration of N and offers suggestions for replacements.
+
procedure Adjust_Record_For_Reverse_Bit_Order (R : Entity_Id);
-- Called from Freeze where R is a record entity for which reverse bit
-- order is specified and there is at least one component clause. Adjusts
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch10; use Sem_Ch10;
+with Sem_Ch12; use Sem_Ch12;
with Sem_Ch13; use Sem_Ch13;
with Sem_Dim; use Sem_Dim;
with Sem_Disp; use Sem_Disp;
-- Local variables
- Context : Node_Id;
+ Context : Node_Id := Empty;
Freeze_From : Entity_Id := Empty;
Next_Decl : Node_Id;
- Spec_Id : Entity_Id;
+ Pack_Decl : Node_Id := Empty;
Body_Seen : Boolean := False;
-- Flag set when the first body [stub] is encountered
- In_Package_Body : Boolean := False;
- -- Flag set when the current declaration list belongs to a package body
-
-- Start of processing for Analyze_Declarations
begin
Context := Parent (L);
if Nkind (Context) = N_Package_Specification then
+ Pack_Decl := Parent (Context);
-- When a package has private declarations, its contract must be
-- analyzed at the end of the said declarations. This way both the
end if;
elsif Nkind (Context) = N_Package_Body then
- In_Package_Body := True;
- Spec_Id := Corresponding_Spec (Context);
-
+ Pack_Decl := Context;
Analyze_Package_Body_Contract (Defining_Entity (Context));
end if;
- end if;
- -- Analyze the contracts of subprogram declarations, subprogram bodies
- -- and variables now due to the delayed visibility requirements of their
- -- aspects.
+ -- Analyze the contracts of all subprogram declarations, subprogram
+ -- bodies and variables now due to the delayed visibility needs of
+ -- of their aspects and pragmas. Capture global references in generic
+ -- subprograms or bodies.
- Decl := First (L);
- while Present (Decl) loop
- if Nkind (Decl) = N_Object_Declaration then
- Analyze_Object_Contract (Defining_Entity (Decl));
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Object_Declaration then
+ Analyze_Object_Contract (Defining_Entity (Decl));
- elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration)
- then
- Analyze_Subprogram_Contract (Defining_Entity (Decl));
+ elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Analyze_Subprogram_Contract (Defining_Entity (Decl));
- elsif Nkind (Decl) = N_Subprogram_Body then
- Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
+ elsif Nkind (Decl) = N_Subprogram_Body then
+ Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
- elsif Nkind (Decl) = N_Subprogram_Body_Stub then
- Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
- end if;
+ elsif Nkind (Decl) = N_Subprogram_Body_Stub then
+ Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
+ end if;
- Next (Decl);
- end loop;
+ -- Capture all global references in a generic subprogram or a body
+ -- [stub] now that the contract has been analyzed.
+
+ if Nkind_In (Decl, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Body_Stub)
+ and then Is_Generic_Declaration_Or_Body (Decl)
+ then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Decl),
+ Gen_Id => Corresponding_Spec_Of (Decl));
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ -- The owner of the declarations is a package [body]
+
+ if Present (Pack_Decl) then
- -- State refinements are visible upto the end the of the package body
- -- declarations. Hide the refinements from visibility to restore the
- -- original state conditions.
+ -- Capture all global references in a generic package or a body
+ -- after all nested generic subprograms and bodies were subjected
+ -- to the same processing.
- if In_Package_Body then
- Remove_Visible_Refinements (Spec_Id);
+ if Is_Generic_Declaration_Or_Body (Pack_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Pack_Decl),
+ Gen_Id => Corresponding_Spec_Of (Pack_Decl));
+ end if;
+
+ -- State refinements are visible upto the end the of the package
+ -- body declarations. Hide the state refinements from visibility
+ -- to restore the original state conditions.
+
+ if Nkind (Pack_Decl) = N_Package_Body then
+ Remove_Visible_Refinements (Corresponding_Spec (Pack_Decl));
+ end if;
+ end if;
end if;
end Analyze_Declarations;
if Nkind (N) /= N_Subprogram_Body_Stub then
New_N := Copy_Generic_Node (N, Empty, Instantiating => False);
Rewrite (N, New_N);
+
+ -- Once the contents of the generic copy and the template are
+ -- swapped, do the same for their respective aspect specifications.
+
+ Exchange_Aspects (N, New_N);
+
+ -- Collect all contract-related source pragmas found within the
+ -- template and attach them to the contract of the subprogram body.
+ -- This contract is used in the capture of global references within
+ -- annotations.
+
+ Create_Generic_Contract (N);
+
Start_Generic;
end if;
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
+ -- Analyze any aspect specifications that appear on the generic
+ -- subprogram body.
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
+ end if;
+
Analyze_Declarations (Declarations (N));
Check_Completion;
- Analyze (Handled_Statement_Sequence (N));
+ -- When a generic subprogram body appears inside a package, its
+ -- contract is analyzed at the end of the package body declarations.
+ -- This is due to the delay with respect of the package contract upon
+ -- which the body contract may depend. When the generic subprogram
+ -- body is a compilation unit, this delay is not necessary.
+
+ if Nkind (Parent (N)) = N_Compilation_Unit then
+ Analyze_Subprogram_Body_Contract (Body_Id);
+
+ -- Capture all global references in a generic subprogram body
+ -- that acts as a compilation unit now that the contract has
+ -- been analyzed.
+
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (N),
+ Gen_Id => Gen_Id);
+ end if;
+
+ Analyze (Handled_Statement_Sequence (N));
Save_Global_References (Original_Node (N));
-- Prior to exiting the scope, include generic formals again (if any
--------------------------------------
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
- Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
+ Items : constant Node_Id := Contract (Body_Id);
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+ Ref_Depends : Node_Id := Empty;
+ Ref_Global : Node_Id := Empty;
- procedure Analyze_Completion_Contract (Spec_Id : Entity_Id);
- -- Analyze all delayed pragmas chained on the contract of subprogram
- -- body Body_Id as if they appeared at the end of a declarative region.
- -- Spec_Id denotes the corresponding spec. The aspects in question are:
- -- Refined_Depends
- -- Refined_Global
- -- Note that pragma Refined_Post is analyzed immediately
+ begin
+ -- When a subprogram body declaration is illegal, its defining entity is
+ -- left unanalyzed. There is nothing left to do in this case because the
+ -- body lacks a contract, or even a proper Ekind.
- ---------------------------------
- -- Analyze_Completion_Contract --
- ---------------------------------
+ if Ekind (Body_Id) = E_Void then
+ return;
+ end if;
- procedure Analyze_Completion_Contract (Spec_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Body_Id);
- Prag : Node_Id;
- Prag_Nam : Name_Id;
- Ref_Depends : Node_Id := Empty;
- Ref_Global : Node_Id := Empty;
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related subprogram body.
- begin
- -- All subprograms carry a contract, but for some it is not
- -- significant and should not be processed.
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
- if not Has_Significant_Contract (Spec_Id) then
- return;
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed.
- elsif Present (Items) then
+ if not Has_Significant_Contract (Body_Id) then
+ null;
- -- Locate and store pragmas Refined_Depends and Refined_Global
- -- since their order of analysis matters.
+ -- The subprogram body is a completion, analyze all delayed pragmas that
+ -- apply. Note that when the body is stand alone, the pragmas are always
+ -- analyzed on the spot.
- Prag := Classifications (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
+ elsif Present (Items) then
- if Prag_Nam = Name_Refined_Depends then
- Ref_Depends := Prag;
+ -- Locate and store pragmas Refined_Depends and Refined_Global since
+ -- their order of analysis matters.
- elsif Prag_Nam = Name_Refined_Global then
- Ref_Global := Prag;
- end if;
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
+ if Prag_Nam = Name_Refined_Depends then
+ Ref_Depends := Prag;
+
+ elsif Prag_Nam = Name_Refined_Global then
+ Ref_Global := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
-- Analyze Refined_Global first as Refined_Depends may mention items
-- classified in the global refinement.
if Present (Ref_Depends) then
Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
end if;
- end Analyze_Completion_Contract;
-
- -- Local variables
-
- Mode : SPARK_Mode_Type;
- Spec_Id : Entity_Id;
-
- -- Start of processing for Analyze_Subprogram_Body_Contract
-
- begin
- -- When a subprogram body declaration is illegal, its defining entity is
- -- left unanalyzed. There is nothing left to do in this case because the
- -- body lacks a contract, or even a proper Ekind.
-
- if Ekind (Body_Id) = E_Void then
- return;
- end if;
-
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related subprogram body.
-
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
-
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
- else
- Spec_Id := Corresponding_Spec (Body_Decl);
- end if;
-
- -- The subprogram body is a completion, analyze all delayed pragmas that
- -- apply. Note that when the body is stand alone, the pragmas are always
- -- analyzed on the spot.
-
- if Present (Spec_Id) then
- Analyze_Completion_Contract (Spec_Id);
end if;
-- Ensure that the contract cases or postconditions mention 'Result or
-- chained beyond that point. It is initialized to Empty to deal with
-- the case where there is no separate spec.
- procedure Analyze_Aspects_On_Body_Or_Stub;
- -- Analyze the aspect specifications of a subprogram body [stub]. It is
- -- assumed that N has aspects.
-
function Body_Has_Contract return Boolean;
-- Check whether unanalyzed body has an aspect or pragma that may
-- generate a SPARK contract.
-- indicator, check that it is consistent with the known status of the
-- entity.
- -------------------------------------
- -- Analyze_Aspects_On_Body_Or_Stub --
- -------------------------------------
-
- procedure Analyze_Aspects_On_Body_Or_Stub is
- procedure Diagnose_Misplaced_Aspects;
- -- Subprogram body [stub] N has aspects, but they are not properly
- -- placed. Provide precise diagnostics depending on the aspects
- -- involved.
-
- --------------------------------
- -- Diagnose_Misplaced_Aspects --
- --------------------------------
-
- procedure Diagnose_Misplaced_Aspects is
- Asp : Node_Id;
- Asp_Nam : Name_Id;
- Asp_Id : Aspect_Id;
- -- The current aspect along with its name and id
-
- procedure SPARK_Aspect_Error (Ref_Nam : Name_Id);
- -- Emit an error message concerning SPARK aspect Asp. Ref_Nam is
- -- the name of the refined version of the aspect.
-
- ------------------------
- -- SPARK_Aspect_Error --
- ------------------------
-
- procedure SPARK_Aspect_Error (Ref_Nam : Name_Id) is
- begin
- -- The corresponding spec already contains the aspect in
- -- question and the one appearing on the body must be the
- -- refined form:
-
- -- procedure P with Global ...;
- -- procedure P with Global ... is ... end P;
- -- ^
- -- Refined_Global
-
- if Has_Aspect (Spec_Id, Asp_Id) then
- Error_Msg_Name_1 := Asp_Nam;
-
- -- Subunits cannot carry aspects that apply to a subprogram
- -- declaration.
-
- if Nkind (Parent (N)) = N_Subunit then
- Error_Msg_N ("aspect % cannot apply to a subunit", Asp);
-
- else
- Error_Msg_Name_2 := Ref_Nam;
- Error_Msg_N ("aspect % should be %", Asp);
- end if;
-
- -- Otherwise the aspect must appear in the spec, not in the
- -- body:
-
- -- procedure P;
- -- procedure P with Global ... is ... end P;
-
- else
- Error_Msg_N
- ("aspect specification must appear in subprogram "
- & "declaration", Asp);
- end if;
- end SPARK_Aspect_Error;
-
- -- Start of processing for Diagnose_Misplaced_Aspects
-
- begin
- -- Iterate over the aspect specifications and emit specific errors
- -- where applicable.
-
- Asp := First (Aspect_Specifications (N));
- while Present (Asp) loop
- Asp_Nam := Chars (Identifier (Asp));
- Asp_Id := Get_Aspect_Id (Asp_Nam);
-
- -- Do not emit errors on aspects that can appear on a
- -- subprogram body. This scenario occurs when the aspect
- -- specification list contains both misplaced and properly
- -- placed aspects.
-
- if Aspect_On_Body_Or_Stub_OK (Asp_Id) then
- null;
-
- -- Special diagnostics for SPARK aspects
-
- elsif Asp_Nam = Name_Depends then
- SPARK_Aspect_Error (Name_Refined_Depends);
-
- elsif Asp_Nam = Name_Global then
- SPARK_Aspect_Error (Name_Refined_Global);
-
- elsif Asp_Nam = Name_Post then
- SPARK_Aspect_Error (Name_Refined_Post);
-
- else
- Error_Msg_N
- ("aspect specification must appear in subprogram "
- & "declaration", Asp);
- end if;
-
- Next (Asp);
- end loop;
- end Diagnose_Misplaced_Aspects;
-
- -- Start of processing for Analyze_Aspects_On_Body_Or_Stub
-
- begin
- -- Language-defined aspects cannot be associated with a subprogram
- -- body [stub] if the subprogram has a spec. Certain implementation
- -- defined aspects are allowed to break this rule (for list, see
- -- table Aspect_On_Body_Or_Stub_OK).
-
- if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then
- Diagnose_Misplaced_Aspects;
- else
- Analyze_Aspect_Specifications (N, Body_Id);
- end if;
- end Analyze_Aspects_On_Body_Or_Stub;
-
-----------------------
-- Body_Has_Contract --
-----------------------
Set_Has_Completion (Body_Id);
Check_Eliminated (Body_Id);
- if Nkind (N) = N_Subprogram_Body_Stub then
-
- -- Analyze any aspect specifications that appear on the subprogram
- -- body stub.
+ -- Analyze any aspect specifications that appear on the subprogram body
+ -- stub. Stop the analysis now as the stub does not have a declarative
+ -- or a statement part, and it cannot be inlined.
+ if Nkind (N) = N_Subprogram_Body_Stub then
if Has_Aspects (N) then
- Analyze_Aspects_On_Body_Or_Stub;
+ Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- -- Stop the analysis now as the stub cannot be inlined, plus it does
- -- not have declarative or statement lists.
-
return;
end if;
-- Analyze any aspect specifications that appear on the subprogram body
if Has_Aspects (N) then
- Analyze_Aspects_On_Body_Or_Stub;
+ Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
Analyze_Declarations (Declarations (N));
---------------------------------
procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
- procedure Save_Global_References_In_List (First_Prag : Node_Id);
- -- Save all global references in contract-related source pragma found in
- -- the list starting from pragma First_Prag.
-
- ------------------------------------
- -- Save_Global_References_In_List --
- ------------------------------------
-
- procedure Save_Global_References_In_List (First_Prag : Node_Id) is
- Prag : Node_Id;
-
- begin
- Prag := First_Prag;
- while Present (Prag) loop
- if Comes_From_Source (Prag)
- and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases,
- Name_Depends,
- Name_Extensions_Visible,
- Name_Global,
- Name_Postcondition,
- Name_Precondition,
- Name_Test_Case)
- then
- Save_Global_References (Original_Node (Prag));
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end Save_Global_References_In_List;
-
- -- Local variables
-
- Items : constant Node_Id := Contract (Subp_Id);
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- Depends : Node_Id := Empty;
- Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Prag_Nam : Name_Id;
- Restore_Scope : Boolean := False;
-
- -- Start of processing for Analyze_Subprogram_Contract
+ Items : constant Node_Id := Contract (Subp_Id);
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
begin
- -- All subprograms carry a contract, but for some it is not significant
- -- and should not be processed.
-
- if not Has_Significant_Contract (Subp_Id) then
- return;
- end if;
-
-- Due to the timing of contract analysis, delayed pragmas may be
-- subject to the wrong SPARK_Mode, usually that of the enclosing
-- context. To remedy this, restore the original SPARK_Mode of the
Save_SPARK_Mode_And_Set (Subp_Id, Mode);
- -- Ensure that the formal parameters are visible when analyzing all
- -- contract items.
-
- if not In_Open_Scopes (Subp_Id) then
- Restore_Scope := True;
- Push_Scope (Subp_Id);
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed.
- if Is_Generic_Subprogram (Subp_Id) then
- Install_Generic_Formals (Subp_Id);
- else
- Install_Formals (Subp_Id);
- end if;
- end if;
+ if not Has_Significant_Contract (Subp_Id) then
+ null;
- if Present (Items) then
+ elsif Present (Items) then
-- Analyze pre- and postconditions
Check_Result_And_Post_State (Subp_Id);
end if;
- -- The aspects and contract-related source pragmas associated with a
- -- generic subprogram are treated separately from the declaration as
- -- they need to be analyzed when the subprogram contract is analyzed.
- -- Once this is done, global references can be successfully saved.
-
- if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
-
- -- Save all global references found in the aspect specifications of
- -- the parameter profile of the generic subprogram.
-
- Save_Global_References_In_Aspects (Original_Node (Subp_Decl));
-
- -- Save all global references found in contract-related source
- -- pragmas. These pragmas usually appear after the declaration of
- -- the generic subprogram, either in the same declarative part or
- -- in the Pragmas_After list when the generic subprogram is a
- -- compilation unit.
-
- if Present (Items) then
- Save_Global_References_In_List (Pre_Post_Conditions (Items));
- Save_Global_References_In_List (Contract_Test_Cases (Items));
- Save_Global_References_In_List (Classifications (Items));
- end if;
- end if;
-
- if Restore_Scope then
- End_Scope;
- end if;
-
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
-----------------------------------
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
- Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
+ Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
+ Mode : SPARK_Mode_Type;
+ Ref_State : Node_Id;
begin
-- Due to the timing of contract analysis, delayed pragmas may be
Save_SPARK_Mode_And_Set (Body_Id, Mode);
- Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
+ Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
-- The analysis of pragma Refined_State detects whether the spec has
-- abstract states available for refinement.
- if Present (Prag) then
- Analyze_Refined_State_In_Decl_Part (Prag);
+ if Present (Ref_State) then
+ Analyze_Refined_State_In_Decl_Part (Ref_State);
-- State refinement is required when the package declaration defines at
-- least one abstract state. Null states are not considered. Refinement
Exchange_Aspects (N, New_N);
+ -- Collect all contract-related source pragmas found within the
+ -- template and attach them to the contract of the package body.
+ -- This contract is used in the capture of global references within
+ -- annotations.
+
+ Create_Generic_Contract (N);
+
-- Update Body_Id to point to the copied node for the remainder of
-- the processing.
------------------------------
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
+ Items : constant Node_Id := Contract (Pack_Id);
+ Init : Node_Id := Empty;
+ Init_Cond : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
begin
-- Due to the timing of contract analysis, delayed pragmas may be
Save_SPARK_Mode_And_Set (Pack_Id, Mode);
- -- Analyze the initialization related pragmas. Initializes must come
- -- before Initial_Condition due to item dependencies.
+ if Present (Items) then
- Prag := Get_Pragma (Pack_Id, Pragma_Initializes);
+ -- Locate and store pragmas Initial_Condition and Initializes since
+ -- their order of analysis matters.
- if Present (Prag) then
- Analyze_Initializes_In_Decl_Part (Prag);
- end if;
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
- Prag := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
+ if Prag_Nam = Name_Initial_Condition then
+ Init_Cond := Prag;
- if Present (Prag) then
- Analyze_Initial_Condition_In_Decl_Part (Prag);
+ elsif Prag_Nam = Name_Initializes then
+ Init := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze the initialization related pragmas. Initializes must come
+ -- before Initial_Condition due to item dependencies.
+
+ if Present (Init) then
+ Analyze_Initializes_In_Decl_Part (Init);
+ end if;
+
+ if Present (Init_Cond) then
+ Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
+ end if;
end if;
-- Check whether the lack of indicator Part_Of agrees with the placement
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
- Subp_Id : Entity_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 Subp_Id subject to Inline_Always.
+ -- Prag is associated with subprogram Spec_Id subject to Inline_Always.
procedure Check_State_And_Constituent_Use
(States : Elist_Id;
-- Find_Related_Subprogram_Or_Body. Emit an error on pragma Prag that
-- duplicates previous pragma Prev.
- function Find_Related_Package_Or_Body
- (Prag : Node_Id;
- Do_Checks : Boolean := False) return Node_Id;
- -- Subsidiary to the analysis of pragmas Abstract_State, Initial_Condition,
- -- Initializes and Refined_State. Find the declaration of the related
- -- package [body] subject to pragma Prag. The return value is either
- -- N_Package_Declaration, N_Package_Body or Empty if the placement of
- -- the pragma is illegal. If flag Do_Checks is set, the routine reports
- -- duplicate pragmas.
-
- function Get_Argument
- (Prag : Node_Id;
- Spec_Id : Entity_Id := Empty) return Node_Id;
- -- Obtain the argument of pragma Prag depending on context and the nature
- -- of the pragma. The argument is extracted in the following manner:
- --
- -- When the pragma is generated from an aspect, return the corresponding
- -- aspect for ASIS or when Spec_Id denotes a generic subprogram.
- --
- -- Otherwise return the first argument of Prag
- --
- -- Spec_Id denotes the entity of the subprogram spec where Prag resides
-
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
-- original one, following the renaming chain) is returned. Otherwise the
-- Local variables
- All_Cases : Node_Id;
- CCase : Node_Id;
- Spec_Id : Entity_Id;
- Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
+ Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ CCase : Node_Id;
Restore_Scope : Boolean := False;
- -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
begin
Set_Analyzed (N);
- Subp_Decl := Find_Related_Subprogram_Or_Body (N);
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
- Subp_Id := Defining_Entity (Subp_Decl);
- All_Cases := Expression (Get_Argument (N, Subp_Id));
-
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser of the analysis of the
-- pragma failed to produce an aggregate.
- pragma Assert (Nkind (All_Cases) = N_Aggregate);
+ pragma Assert (Nkind (CCases) = N_Aggregate);
- if Present (Component_Associations (All_Cases)) then
+ if Present (Component_Associations (CCases)) then
-- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining
- -- to subprogram declarations. Skip the installation for subprogram
- -- bodies because the formals are already visible.
+ -- to subprogram declarations.
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
end if;
end if;
- CCase := First (Component_Associations (All_Cases));
+ 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);
- if Restore_Scope then
- End_Scope;
- end if;
+ -- Otherwise the pragma is illegal
+
else
Error_Msg_N ("wrong syntax for constract cases", N);
end if;
----------------------------------
procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
+ Loc : constant Source_Ptr := Sloc (N);
+ Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
All_Inputs_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the inputs processed so far.
Result_Seen : Boolean := False;
-- A flag set when Subp_Id'Result is processed
- Spec_Id : Entity_Id;
- -- The entity of the subprogram subject to pragma [Refined_]Depends
-
States_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all states processed so far. It
-- helps in detecting illegal usage of a state and a corresponding
-- constituent in pragma [Refined_]Depends.
- Subp_Id : Entity_Id;
- -- The entity of the subprogram [body or stub] subject to pragma
- -- [Refined_]Depends.
-
Subp_Inputs : Elist_Id := No_Elist;
Subp_Outputs : Elist_Id := No_Elist;
-- Two lists containing the full set of inputs and output of the related
procedure Add_Item_To_Name_Buffer (Item_Id : Entity_Id);
-- Subsidiary routine to Check_Role and Check_Usage. Add the item kind
-- to the name buffer. The individual kinds are as follows:
- -- E_Abstract_State - "state"
- -- E_In_Parameter - "parameter"
- -- E_In_Out_Parameter - "parameter"
- -- E_Out_Parameter - "parameter"
- -- E_Variable - "global"
+ -- E_Abstract_State - "state"
+ -- E_Constant - "constant"
+ -- E_Generic_In_Out_Parameter - "generic parameter"
+ -- E_Generic_Out_Parameter - "generic parameter"
+ -- E_In_Parameter - "parameter"
+ -- E_In_Out_Parameter - "parameter"
+ -- E_Out_Parameter - "parameter"
+ -- E_Variable - "global"
procedure Analyze_Dependency_Clause
(Clause : Node_Id;
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 Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
+ E_Generic_In_Parameter)
+ then
+ Add_Str_To_Name_Buffer ("generic parameter");
+
elsif Is_Formal (Item_Id) then
Add_Str_To_Name_Buffer ("parameter");
-- denotes an output. Flag Self_Ref should be set when the item is an
-- output and the dependency clause has a "+". Flag Top_Level should
-- be set whenever Item appears immediately within an input or output
- -- list. Seen is a collection of all abstract states, variables and
+ -- 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.
Error_Msg_N ("malformed dependency list", Item);
end if;
- -- Process Function'Result in the context of a dependency clause
+ -- Process attribute 'Result in the context of a dependency clause
elsif Is_Attribute_Result (Item) then
Non_Null_Seen := True;
- -- It is sufficent to analyze the prefix of 'Result in order to
- -- establish legality of the attribute.
-
- Analyze (Prefix (Item));
-
- -- The prefix of 'Result must denote the function for which
- -- pragma Depends applies (SPARK RM 6.1.5(11)).
+ Analyze (Item);
- if not Is_Entity_Name (Prefix (Item))
- or else Ekind (Spec_Id) /= E_Function
- or else Entity (Prefix (Item)) /= Spec_Id
- then
- Error_Msg_Name_1 := Name_Result;
- SPARK_Msg_N
- ("prefix of attribute % must denote the enclosing "
- & "function", Item);
+ -- Attribute 'Result is allowed to appear on the output side of
+ -- a dependency clause (SPARK RM 6.1.5(6)).
- -- Function'Result is allowed to appear on the output side of a
- -- dependency clause (SPARK RM 6.1.5(6)).
-
- elsif Is_Input then
+ if Is_Input then
SPARK_Msg_N ("function result cannot act as input", Item);
elsif Null_Seen then
if Present (Item_Id) then
if Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Generic_In_Out_Parameter,
+ E_Generic_In_Parameter,
E_In_Parameter,
E_In_Out_Parameter,
E_Out_Parameter,
-- State related checks (SPARK RM 6.1.5(3))
if Ekind (Item_Id) = E_Abstract_State then
- if Has_Visible_Refinement (Item_Id) 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 Is_Generic_Instance (Spec_Id) 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 global refinement",
+ ("cannot mention state & in dependence relation",
Item, Item_Id);
SPARK_Msg_N ("\use its constituents instead", Item);
return;
-- When the item renames an entire object, replace the
-- item with a reference to the object.
- if Present (Renamed_Object (Entity (Item))) then
+ if Entity (Item) /= Item_Id then
Rewrite (Item,
New_Occurrence_Of (Item_Id, Sloc (Item)));
Analyze (Item);
Add_Item (Item_Id, States_Seen);
end if;
- if Ekind_In (Item_Id, E_Abstract_State, E_Variable)
+ if Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
and then Present (Encapsulating_State (Item_Id))
then
Add_Item (Item_Id, Constits_Seen);
procedure Check_Function_Return is
begin
- if Ekind (Spec_Id) = E_Function and then not Result_Seen then
+ if Ekind_In (Spec_Id, 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);
Item_Is_Output := True;
end if;
+ -- Generic parameter cases
+
+ elsif Ekind (Item_Id) = E_Generic_In_Parameter then
+ Item_Is_Input := True;
+
+ elsif Ekind (Item_Id) = E_Generic_In_Out_Parameter then
+ Item_Is_Input := True;
+ Item_Is_Output := True;
+
-- Parameter cases
elsif Ekind (Item_Id) = E_In_Parameter then
Item_Is_Output := True;
end if;
- -- Variable cases
+ -- Object cases
- else pragma Assert (Ekind (Item_Id) = E_Variable);
+ else pragma Assert (Ekind_In (Item_Id, E_Constant, E_Variable));
- -- When pragma Global is present, the mode of the variable may
+ -- When pragma Global is present, the mode of the object may
-- be further constrained by setting a more restrictive mode.
if Global_Seen then
- -- A variable has mode IN when its type is unconstrained or
+ -- An object has mode IN when its type is unconstrained or
-- tagged because array bounds, discriminants or tags can be
-- read.
Item_Is_Output := True;
end if;
- -- Otherwise the variable has a default IN OUT mode
+ -- Otherwise the object has a default IN OUT mode
else
Item_Is_Input := True;
Error_Msg := Name_Find;
SPARK_Msg_NE (Get_Name_String (Error_Msg), Item, Item_Id);
- Error_Msg_Name_1 := Chars (Subp_Id);
+ Error_Msg_Name_1 := Chars (Spec_Id);
SPARK_Msg_NE
("\& is not part of the input or output set of subprogram %",
Item, Item_Id);
if Is_Formal (Item_Id) then
Usage_Error (Item, Item_Id);
- -- States and global variables are not used properly only when
+ -- States and global objects are not used properly only when
-- the subprogram is subject to pragma Global.
elsif Global_Seen then
(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.
+ -- list. Output denotes a self-referencial output item. Inputs
+ -- is the input list of a clause.
----------------------
-- Propagate_Output --
end if;
-- When performing the transformation in place, simply add the
- -- output to the list of inputs (if not already there). This case
- -- arises when dealing with the last output of an output list -
- -- we perform the normalization in place to avoid generating a
- -- malformed tree.
+ -- 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);
Expression => New_Copy_Tree (Inputs));
-- The new clause contains replicated content that has already
- -- been analyzed. There is not need to reanalyze it or
- -- renormalize it again.
+ -- been analyzed. There is not need to reanalyze or renormalize
+ -- it again.
Set_Analyzed (New_Clause);
-- Local variables
- Clause : Node_Id;
- Deps : Node_Id;
- Errors : Nat;
- Last_Clause : Node_Id;
- Subp_Decl : Node_Id;
+ 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;
- -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
-- Start of processing for Analyze_Depends_In_Decl_Part
begin
Set_Analyzed (N);
- Subp_Decl := Find_Related_Subprogram_Or_Body (N);
- Subp_Id := Defining_Entity (Subp_Decl);
- Deps := Expression (Get_Argument (N, Subp_Id));
-
- -- The logic in this routine is used to analyze both pragma Depends and
- -- pragma Refined_Depends since they have the same syntax and base
- -- semantics. Find the entity of the corresponding spec when analyzing
- -- Refined_Depends.
-
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-
-- Empty dependency list
if Nkind (Deps) = N_Null then
- -- Gather all states, variables and formal parameters that the
+ -- 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).
if Present (Component_Associations (Deps)) then
Last_Clause := Last (Component_Associations (Deps));
- -- Gather all states, variables and formal parameters that the
+ -- 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).
-- Ensure that the formal parameters are visible when analyzing
-- all clauses. This falls out of the general rule of aspects
- -- pertaining to subprogram declarations. Skip the installation
- -- for subprogram bodies because the formals are already visible.
+ -- pertaining to subprogram declarations.
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
while Present (Clause) loop
Errors := Serious_Errors_Detected;
- -- Normalization may create extra clauses that contain
- -- replicated input and output names. There is no need to
- -- reanalyze them.
+ -- 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);
---------------------------------
procedure Analyze_Global_In_Decl_Part (N : Node_Id) is
+ Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of (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
-- A list containing the entities of all the items processed so far. It
-- plays a role in detecting distinct entities.
- Spec_Id : Entity_Id;
- -- The entity of the subprogram subject to pragma [Refined_]Global
-
States_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all states processed so far. It
-- helps in detecting illegal usage of a state and a corresponding
-- constituent in pragma [Refined_]Global.
- Subp_Id : Entity_Id;
- -- The entity of the subprogram [body or stub] subject to pragma
- -- [Refined_]Global.
-
In_Out_Seen : Boolean := False;
Input_Seen : Boolean := False;
Output_Seen : Boolean := False;
procedure Analyze_Global_Item
(Item : Node_Id;
Global_Mode : Name_Id);
- -- Verify the legality of a single global item declaration.
- -- Global_Mode denotes the current mode in effect.
+ -- 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;
if Is_Formal (Item_Id) then
if Scope (Item_Id) = Spec_Id then
SPARK_Msg_NE
- ("global item cannot reference parameter of subprogram",
- Item, Spec_Id);
+ ("global item cannot reference parameter of "
+ & "subprogram &", Item, Spec_Id);
return;
end if;
- -- A constant cannot act as a global item (SPARK RM 6.1.4(7)).
- -- Do this check first to provide a better error diagnostic.
-
- elsif Ekind (Item_Id) = E_Constant then
- SPARK_Msg_N ("global item cannot denote a constant", Item);
-
-- A formal object may act as a global item inside a generic
elsif Is_Formal_Object (Item_Id) then
null;
-- The only legal references are those to abstract states and
- -- variables (SPARK RM 6.1.4(4)).
+ -- objects (SPARK RM 6.1.4(4)).
- elsif not Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+ elsif not Ekind_In (Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
+ then
SPARK_Msg_N
- ("global item must denote variable or state", Item);
+ ("global item must denote object or state", Item);
return;
end if;
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 Is_Generic_Instance (Spec_Id) 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(8)).
+ -- some of its constituents (SPARK RM 6.1.4(7)).
- if Has_Visible_Refinement (Item_Id) then
+ elsif Has_Visible_Refinement (Item_Id) then
SPARK_Msg_NE
("cannot mention state & in global refinement",
Item, Item_Id);
-- rules.
elsif SPARK_Mode = On
+ and then Ekind (Item_Id) = E_Variable
and then Is_Effectively_Volatile (Item_Id)
then
-- An effectively volatile object cannot appear as a global
-- An effectively volatile object with external property
-- Effective_Reads set to True must have mode Output or
- -- In_Out.
+ -- In_Out (SPARK RM 7.1.3(11)).
elsif Effective_Reads_Enabled (Item_Id)
and then Global_Mode = Name_Input
then
Error_Msg_NE
("volatile object & with property Effective_Reads must "
- & "have mode In_Out or Output (SPARK RM 7.1.3(11))",
- Item, Item_Id);
+ & "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 Present (Renamed_Object (Entity (Item))) then
+ if Entity (Item) /= Item_Id then
Rewrite (Item, New_Occurrence_Of (Item_Id, Sloc (Item)));
Analyze (Item);
end if;
-- (SPARK RM 6.1.4(4)).
else
- Error_Msg_N ("global item must denote variable or state", Item);
+ Error_Msg_N ("global item must denote object or state", Item);
return;
end if;
-- The same entity might be referenced through various way.
-- Check the entity of the item rather than the item itself
- -- (SPARK RM 6.1.4(11)).
+ -- (SPARK RM 6.1.4(10)).
if Contains (Seen, Item_Id) then
SPARK_Msg_N ("duplicate global item", Item);
Add_Item (Item_Id, States_Seen);
end if;
- if Ekind_In (Item_Id, E_Abstract_State, E_Variable)
+ if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
and then Present (Encapsulating_State (Item_Id))
then
Add_Item (Item_Id, Constits_Seen);
Global_Seen => Dummy);
-- The item is classified as In_Out or Output but appears as
- -- an Input in an enclosing subprogram (SPARK RM 6.1.4(12)).
+ -- an Input in an enclosing subprogram (SPARK RM 6.1.4(11)).
if Appears_In (Inputs, Item_Id)
and then not Appears_In (Outputs, Item_Id)
procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is
begin
- if Ekind (Spec_Id) = E_Function then
+ if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
SPARK_Msg_N
("global mode & is not applicable to functions", Mode);
end if;
Item := First (Expressions (List));
while Present (Item) loop
Analyze_Global_Item (Item, Global_Mode);
-
Next (Item);
end loop;
-- Local variables
- Items : Node_Id;
- Subp_Decl : Node_Id;
+ Items : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Restore_Scope : Boolean := False;
- -- Set True if we do a Push_Scope requiring a Pop_Scope on exit
-- Start of processing for Analyze_Global_In_Decl_Part
begin
Set_Analyzed (N);
- Subp_Decl := Find_Related_Subprogram_Or_Body (N);
- Subp_Id := Defining_Entity (Subp_Decl);
- Items := Expression (Get_Argument (N, Subp_Id));
-
- -- The logic in this routine is used to analyze both pragma Global and
- -- pragma Refined_Global since they have the same syntax and base
- -- semantics. Find the entity of the corresponding spec when analyzing
- -- Refined_Global.
-
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-
-- There is nothing to be done for a null global list
if Nkind (Items) = N_Null then
--------------------------------------------
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
- Expr : constant Node_Id := Expression (Get_Argument (N));
+ 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));
begin
Set_Analyzed (N);
--------------------------------------
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id) is
- Pack_Spec : constant Node_Id := Parent (N);
- Pack_Id : constant Entity_Id := Defining_Entity (Parent (Pack_Spec));
+ 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.
----------------------------------
procedure Collect_States_And_Variables is
- Decl : Node_Id;
+ Pack_Spec : constant Node_Id := Specification (Pack_Decl);
+ Decl : Node_Id;
begin
-- Collect the abstract states defined in the package (if any)
-- Local variables
- Inits : constant Node_Id := Expression (Get_Argument (N));
+ Inits : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
Init : Node_Id;
-- Start of processing for Analyze_Initializes_In_Decl_Part
-- 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;
+ -- Subsidiary to the analysis of pragma Depends and Global
+
procedure Analyze_Part_Of
(Item_Id : Entity_Id;
State : Node_Id;
procedure Analyze_Pre_Post_Condition;
-- Subsidiary to the analysis of pragmas Precondition and Postcondition
- procedure Analyze_Refined_Pragma
+ procedure Analyze_Refined_Depends_Global_Post
(Spec_Id : out Entity_Id;
Body_Id : out Entity_Id;
Legal : out Boolean);
-- presence of at least one component. UU_Typ is the related Unchecked_
-- Union type.
- procedure Create_Generic_Template
- (Prag : Node_Id;
- Subp_Id : Entity_Id);
- -- Subsidiary routine to the processing of pragmas Contract_Cases,
- -- Depends, Global, Postcondition, Precondition and Test_Case. Create
- -- a generic template for pragma Prag when Prag is a source construct
- -- and the related context denoted by Subp_Id is a generic subprogram.
-
procedure Ensure_Aggregate_Form (Arg : Node_Id);
-- Subsidiary routine to the processing of pragmas Abstract_State,
-- Contract_Cases, Depends, Global, Initializes, Refined_Depends,
end if;
end Ada_2012_Pragma;
+ ----------------------------
+ -- Analyze_Depends_Global --
+ ----------------------------
+
+ procedure Analyze_Depends_Global is
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
+
+ begin
+ GNAT_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Depends/Global must be
+ -- associated with a subprogram declaration or a body that acts as a
+ -- spec.
+
+ Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+
+ -- Generic subprogram
+
+ if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ null;
+
+ -- Body acts as spec
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ and then No (Corresponding_Spec (Subp_Decl))
+ then
+ null;
+
+ -- Body stub acts as spec
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ null;
+
+ -- Subprogram declaration
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ null;
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+
+ Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
+
+ -- Fully analyze the pragma when it appears inside a subprogram body
+ -- because it cannot benefit from forward references.
+
+ if Nkind (Subp_Decl) = N_Subprogram_Body then
+ if Pragma_Name (N) = Name_Depends then
+ Analyze_Depends_In_Decl_Part (N);
+
+ else pragma Assert (Pname = Name_Global);
+ Analyze_Global_In_Decl_Part (N);
+ end if;
+ end if;
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Depends_In_Decl_Part/Analyze_Global_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+ end Analyze_Depends_Global;
+
---------------------
-- Analyze_Part_Of --
---------------------
procedure Analyze_Pre_Post_Condition is
Prag_Iden : constant Node_Id := Pragma_Identifier (N);
Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
Duplicates_OK : Boolean := False;
-- Flag set when a pre/postcondition allows multiple pragmas of the
return;
end if;
- Subp_Id := Defining_Entity (Subp_Decl);
-
- -- Construct a generic template for the pragma when the context is a
- -- generic subprogram and the pragma is a source construct.
-
- Create_Generic_Template (N, Subp_Id);
-
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
Analyze_Pre_Post_Condition_In_Decl_Part (N);
end if;
- -- Chain the pragma on the contract for further processing
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Pre_Post_Condition_In_Decl_Part.
- Add_Contract_Item (N, Subp_Id);
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
end Analyze_Pre_Post_Condition;
- ----------------------------
- -- Analyze_Refined_Pragma --
- ----------------------------
+ -----------------------------------------
+ -- Analyze_Refined_Depends_Global_Post --
+ -----------------------------------------
- procedure Analyze_Refined_Pragma
+ procedure Analyze_Refined_Depends_Global_Post
(Spec_Id : out Entity_Id;
Body_Id : out Entity_Id;
Legal : out Boolean)
Name_Refined_Global,
Name_Refined_State)
then
- Ensure_Aggregate_Form (Get_Argument (N));
+ Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
end if;
Legal := True;
- end Analyze_Refined_Pragma;
+ end Analyze_Refined_Depends_Global_Post;
--------------------------
-- Check_Ada_83_Warning --
end loop;
end Check_Variant;
- -----------------------------
- -- Create_Generic_Template --
- -----------------------------
-
- procedure Create_Generic_Template
- (Prag : Node_Id;
- Subp_Id : Entity_Id)
- is
- begin
- if Comes_From_Source (Prag)
- and then Is_Generic_Subprogram (Subp_Id)
- then
- Rewrite
- (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
- end if;
- end Create_Generic_Template;
-
---------------------------
-- Ensure_Aggregate_Form --
---------------------------
-- ABSTRACT_STATE ::= name
+ -- Characteristics:
+
+ -- * Analysis - The annotation is fully analyzed immediately upon
+ -- elaboration as it cannot forward reference entities.
+
+ -- * Expansion - None.
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related package declaration.
+
+ -- * Globals - The annotation cannot reference global entities.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic package is instantiated.
+
when Pragma_Abstract_State => Abstract_State : declare
Missing_Parentheses : Boolean := False;
-- Flag set when a state declaration with options is not properly
-- as a component association.
if Nkind (State) = N_Component_Association then
- Error_Msg_N ("\\use WITH to specify simple option", State);
+ Error_Msg_N ("\use WITH to specify simple option", State);
end if;
end Malformed_State_Error;
return;
end if;
- Ensure_Aggregate_Form (Get_Argument (N));
Pack_Id := Defining_Entity (Pack_Decl);
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
+
-- Mark the associated package as Ghost if it is subject to aspect
-- or pragma Ghost as this affects the declaration of an abstract
-- state.
Set_Is_Ghost_Entity (Pack_Id);
end if;
- States := Expression (Get_Argument (N));
+ States := Expression (Get_Argument (N, Pack_Id));
-- Multiple non-null abstract states appear as an aggregate
Analyze_Abstract_State (States, Pack_Id);
end if;
- -- Save the pragma for retrieval by other tools
-
- Add_Contract_Item (N, Pack_Id);
-
-- Verify the declaration order of pragmas Abstract_State and
-- Initializes.
Check_Declaration_Order
(First => N,
Second => Get_Pragma (Pack_Id, Pragma_Initializes));
+
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Pack_Id);
end Abstract_State;
------------
end if;
-- Chain the pragma on the contract for further processing
+ -- by Analyze_External_Property_In_Decl_Part.
Add_Contract_Item (N, Obj_Id);
end if;
-- CONSEQUENCE ::= boolean_EXPRESSION
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expressions in:
+
+ -- Analyze_Contract_Cases_In_Decl_Part
+
+ -- * Expansion - The annotation is expanded during the expansion of
+ -- the related subprogram [body] contract as performed in:
+
+ -- Expand_Subprogram_Contract
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
+
+ -- aspect on subprogram declaration
+ -- aspect on stand alone subprogram body
+ -- pragma on stand alone subprogram body
+
+ -- The annotation must prepare its own template when it is:
+
+ -- pragma on subprogram declaration
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
+
when Pragma_Contract_Cases => Contract_Cases : declare
+ Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
begin
GNAT_Pragma;
return;
end if;
- Subp_Id := Defining_Entity (Subp_Decl);
-
- Ensure_Aggregate_Form (Get_Argument (N, Subp_Id));
-
- -- Construct a generic template for the pragma when the context is
- -- a generic subprogram and the pragma is a source construct.
+ Spec_Id := Corresponding_Spec_Of (Subp_Decl);
- Create_Generic_Template (N, Subp_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
Analyze_Contract_Cases_In_Decl_Part (N);
end if;
- -- Chain the pragma on the contract for further processing
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Contract_Cases_In_Decl_Part.
- Add_Contract_Item (N, Subp_Id);
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
end Contract_Cases;
----------------
-- where FUNCTION_RESULT is a function Result attribute_reference
- when Pragma_Depends => Depends : declare
- Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
-
- begin
- GNAT_Pragma;
- Check_Arg_Count (1);
-
- -- Ensure the proper placement of the pragma. Depends must be
- -- associated with a subprogram declaration or a body that acts
- -- as a spec.
-
- Subp_Decl :=
- Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
-
- -- Body acts as spec
-
- if Nkind (Subp_Decl) = N_Subprogram_Body
- and then No (Corresponding_Spec (Subp_Decl))
- then
- null;
-
- -- Body stub acts as spec
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
- and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
- then
- null;
-
- -- Subprogram declaration
+ -- Characteristics:
- elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
- null;
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks fully analyze
+ -- the dependency clauses in:
- else
- Pragma_Misplaced;
- return;
- end if;
+ -- Analyze_Depends_In_Decl_Part
- Subp_Id := Defining_Entity (Subp_Decl);
+ -- * Expansion - None.
- Ensure_Aggregate_Form (Get_Argument (N, Subp_Id));
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
- -- Construct a generic template for the pragma when the context is
- -- a generic subprogram and the pragma is a source construct.
+ -- aspect on subprogram declaration
+ -- aspect on stand alone subprogram body
+ -- pragma on stand alone subprogram body
- Create_Generic_Template (N, Subp_Id);
+ -- The annotation must prepare its own template when it is:
- -- When the pragma appears on a subprogram body, perform the full
- -- analysis now.
+ -- pragma on subprogram declaration
- if Nkind (Subp_Decl) = N_Subprogram_Body then
- Analyze_Depends_In_Decl_Part (N);
- end if;
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
- -- Chain the pragma on the contract for further processing
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
- Add_Contract_Item (N, Subp_Id);
- end Depends;
+ when Pragma_Depends =>
+ Analyze_Depends_Global;
---------------------
-- Detect_Blocking --
-- pragma Extensions_Visible [ (boolean_EXPRESSION) ];
+ -- Characteristics:
+
+ -- * Analysis - The annotation is fully analyzed immediately upon
+ -- elaboration as its expression must be static.
+
+ -- * Expansion - None.
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
+
+ -- aspect on subprogram declaration
+ -- aspect on stand alone subprogram body
+ -- pragma on stand alone subprogram body
+
+ -- The annotation must prepare its own template when it is:
+
+ -- pragma on subprogram declaration
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
+
when Pragma_Extensions_Visible => Extensions_Visible : declare
Expr : Node_Id;
Formal : Entity_Id;
Has_OK_Formal : Boolean := False;
Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
begin
GNAT_Pragma;
end if;
Spec_Id := Corresponding_Spec_Of (Subp_Decl);
- Subp_Id := Defining_Entity (Subp_Decl);
-- Examine the formals of the related subprogram
return;
end if;
- -- Construct a generic template for the pragma when the context is
- -- a generic subprogram and the pragma is a source construct.
-
- Create_Generic_Template (N, Subp_Id);
-
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
- Expr := Expression (Get_Argument (N));
+ Expr := Expression (Get_Argument (N, Spec_Id));
Analyze_And_Resolve (Expr, Standard_Boolean);
end if;
end if;
- -- Chain the pragma on the contract for further processing
+ -- Chain the pragma on the contract for completeness
- Add_Contract_Item (N, Subp_Id);
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
end Extensions_Visible;
--------------
-- GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
-- GLOBAL_ITEM ::= NAME
- when Pragma_Global => Global : declare
- Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
-
- begin
- GNAT_Pragma;
- Check_Arg_Count (1);
-
- -- Ensure the proper placement of the pragma. Global must be
- -- associated with a subprogram declaration or a body that acts
- -- as a spec.
-
- Subp_Decl :=
- Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
-
- -- Body acts as spec
-
- if Nkind (Subp_Decl) = N_Subprogram_Body
- and then No (Corresponding_Spec (Subp_Decl))
- then
- null;
-
- -- Body stub acts as spec
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
- and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
- then
- null;
-
- -- Subprogram declaration
+ -- Characteristics:
- elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
- null;
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks fully analyze
+ -- the dependency clauses in:
- else
- Pragma_Misplaced;
- return;
- end if;
+ -- Analyze_Global_In_Decl_Part
- Subp_Id := Defining_Entity (Subp_Decl);
+ -- * Expansion - None.
- Ensure_Aggregate_Form (Get_Argument (N, Subp_Id));
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
- -- Construct a generic template for the pragma when the context is
- -- a generic subprogram and the pragma is a source construct.
+ -- aspect on subprogram declaration
+ -- aspect on stand alone subprogram body
+ -- pragma on stand alone subprogram body
- Create_Generic_Template (N, Subp_Id);
+ -- The annotation must prepare its own template when it is:
- -- When the pragma appears on a subprogram body, perform the full
- -- analysis now.
+ -- pragma on subprogram declaration
- if Nkind (Subp_Decl) = N_Subprogram_Body then
- Analyze_Global_In_Decl_Part (N);
- end if;
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
- -- Chain the pragma on the contract for further processing
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
- Add_Contract_Item (N, Subp_Id);
- end Global;
+ when Pragma_Global =>
+ Analyze_Depends_Global;
-----------
-- Ident --
-- pragma Initial_Condition (boolean_EXPRESSION);
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expression in:
+
+ -- Analyze_Initial_Condition_In_Decl_Part
+
+ -- * Expansion - The annotation is expanded during the expansion of
+ -- the package body whose declaration is subject to the annotation
+ -- as done in:
+
+ -- Expand_Pragma_Initial_Condition
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related package declaration.
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic package is instantiated.
+
when Pragma_Initial_Condition => Initial_Condition : declare
Pack_Decl : Node_Id;
Pack_Id : Entity_Id;
-- the contract of the package.
Pack_Id := Defining_Entity (Pack_Decl);
- Add_Contract_Item (N, Pack_Id);
-- Verify the declaration order of pragma Initial_Condition with
-- respect to pragmas Abstract_State and Initializes when SPARK
(First => Get_Pragma (Pack_Id, Pragma_Initializes),
Second => N);
end if;
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Initial_Condition_In_Decl_Part.
+
+ Add_Contract_Item (N, Pack_Id);
end Initial_Condition;
------------------------
-- INPUT ::= name
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expression in:
+
+ -- Analyze_Initializes_In_Decl_Part
+
+ -- * Expansion - None.
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related package declaration.
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic package is instantiated.
+
when Pragma_Initializes => Initializes : declare
Pack_Decl : Node_Id;
Pack_Id : Entity_Id;
return;
end if;
- Ensure_Aggregate_Form (Get_Argument (N));
-
- -- The pragma must be analyzed at the end of the visible
- -- declarations of the related package. Save the pragma for later
- -- (see Analyze_Initializes_In_Decl_Part) by adding it to the
- -- contract of the package.
-
Pack_Id := Defining_Entity (Pack_Decl);
- Add_Contract_Item (N, Pack_Id);
+
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-- Verify the declaration order of pragmas Abstract_State and
-- Initializes when SPARK checks are enabled.
(First => Get_Pragma (Pack_Id, Pragma_Abstract_State),
Second => N);
end if;
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Initializes_In_Decl_Part.
+
+ Add_Contract_Item (N, Pack_Id);
end Initializes;
------------
if not Comes_From_Source (Item_Id) then
null;
- -- The Part_Of indicator turns an abstract state or
+ -- The Part_Of indicator turns an abstract state or a
-- variable into a constituent of the encapsulating
-- state.
Stmt := Prev (Stmt);
end loop;
- -- When the context is an object declaration, ensure that we are
- -- dealing with a variable.
+ -- When the context is an object declaration, ensure that it is a
+ -- variable.
if Nkind (Stmt) = N_Object_Declaration
and then Ekind (Defining_Entity (Stmt)) /= E_Variable
if Legal then
State_Id := Entity (State);
- -- Add the pragma to the contract of the item. This aids with
- -- the detection of a missing but required Part_Of indicator.
-
- Add_Contract_Item (N, Item_Id);
-
-- The Part_Of indicator turns a variable into a constituent
-- of the encapsulating state.
State_Id => State_Id,
Instance => Stmt);
end if;
+
+ -- Add the pragma to the contract of the item. This aids with
+ -- the detection of a missing but required Part_Of indicator.
+
+ Add_Contract_Item (N, Item_Id);
end if;
end Part_Of;
-- pragma Postcondition ([Check =>] Boolean_EXPRESSION
-- [,[Message =>] String_EXPRESSION]);
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expression in:
+
+ -- Analyze_Pre_Post_Condition_In_Decl_Part
+
+ -- * Expansion - The annotation is expanded during the expansion of
+ -- the related subprogram [body] contract as performed in:
+
+ -- Expand_Subprogram_Contract
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
+
+ -- aspect on subprogram declaration
+ -- aspect on stand alone subprogram body
+ -- pragma on stand alone subprogram body
+
+ -- The annotation must prepare its own template when it is:
+
+ -- pragma on subprogram declaration
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
+
when Pragma_Post |
Pragma_Post_Class |
Pragma_Postcondition =>
-- pragma Precondition ([Check =>] Boolean_EXPRESSION
-- [,[Message =>] String_EXPRESSION]);
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expression in:
+
+ -- Analyze_Pre_Post_Condition_In_Decl_Part
+
+ -- * Expansion - The annotation is expanded during the expansion of
+ -- the related subprogram [body] contract as performed in:
+
+ -- Expand_Subprogram_Contract
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
+
+ -- aspect on subprogram declaration
+ -- aspect on stand alone subprogram body
+ -- pragma on stand alone subprogram body
+
+ -- The annotation must prepare its own template when it is:
+
+ -- pragma on subprogram declaration
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
+
when Pragma_Pre |
Pragma_Pre_Class |
Pragma_Precondition =>
-- GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
-- GLOBAL_ITEM ::= NAME
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks fully analyze
+ -- the dependency clauses/global list in:
+
+ -- Analyze_Refined_Depends_In_Decl_Part
+ -- Analyze_Refined_Global_In_Decl_Part
+
+ -- * Expansion - None.
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram body.
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram body is instantiated.
+
when Pragma_Refined_Depends |
Pragma_Refined_Global => Refined_Depends_Global :
declare
Spec_Id : Entity_Id;
begin
- Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
+ Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal);
- -- Save the pragma in the contract of the subprogram body. The
- -- remaining analysis is performed at the end of the enclosing
- -- declarations.
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Refined_[Depends|Global]_In_Decl_Part.
if Legal then
Add_Contract_Item (N, Body_Id);
-- pragma Refined_Post (boolean_EXPRESSION);
+ -- Characteristics:
+
+ -- * Analysis - The annotation is fully analyzed immediately upon
+ -- elaboration as it cannot forward reference entities.
+
+ -- * Expansion - The annotation is expanded during the expansion of
+ -- the related subprogram body contract as performed in:
+
+ -- Expand_Subprogram_Contract
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram body.
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram body is instantiated.
+
when Pragma_Refined_Post => Refined_Post : declare
Body_Id : Entity_Id;
Legal : Boolean;
Spec_Id : Entity_Id;
begin
- Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
+ Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal);
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
- -- Chain the pragma on the contract for easy retrieval
+ -- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Body_Id);
end if;
-- CONSTITUENT ::= object_NAME | state_NAME
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- refinement clauses in:
+
+ -- Analyze_Refined_State_In_Decl_Part
+
+ -- * Expansion - None.
+
+ -- * Template - The annotation utilizes the template of the related
+ -- package body.
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic package body is instantiated.
+
when Pragma_Refined_State => Refined_State : declare
Pack_Decl : Node_Id;
Spec_Id : Entity_Id;
return;
end if;
- -- The pragma must be analyzed at the end of the declarations as
- -- it has visibility over the whole declarative region. Save the
- -- pragma for later (see Analyze_Refined_State_In_Decl_Part) by
- -- adding it to the contract of the package body.
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Refined_State_In_Decl_Part.
Add_Contract_Item (N, Defining_Entity (Pack_Decl));
end Refined_State;
-- MODE_TYPE ::= Nominal | Robustness
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expressions in:
+
+ -- Analyze_Test_Case_In_Decl_Part
+
+ -- * Expansion - None.
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram when it is:
+
+ -- aspect on subprogram declaration
+
+ -- The annotation must prepare its own template when it is:
+
+ -- pragma on subprogram declaration
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram is instantiated except for the
+ -- "pragma on subprogram declaration" case. In that scenario the
+ -- annotation must instantiate itself.
+
when Pragma_Test_Case => Test_Case : declare
procedure Check_Distinct_Name (Subp_Id : Entity_Id);
-- Ensure that the contract of subprogram Subp_Id does not contain
Check_Distinct_Name (Subp_Id);
- -- Construct a generic template for the pragma when the context is
- -- a generic subprogram and the pragma is a source construct.
-
- Create_Generic_Template (N, Subp_Id);
-
-- Fully analyze the pragma when it appears inside a subprogram
-- body because it cannot benefit from forward references.
Analyze_Test_Case_In_Decl_Part (N);
end if;
- -- Chain the pragma on the contract for further processing
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Test_Case_In_Decl_Part.
Add_Contract_Item (N, Subp_Id);
end Test_Case;
-- Local variables
Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
- Expr : constant Node_Id :=
- Expression (Get_Argument (N, Defining_Entity (Subp_Decl)));
Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+ Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Restore_Scope : Boolean := False;
- -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl);
end if;
+ 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);
-
- -- Remove the subprogram from the scope stack now that the pre-analysis
- -- of the precondition/postcondition is done.
-
- if Restore_Scope then
- End_Scope;
- end if;
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
if Is_Entity_Name (Ref_Item) then
Ref_Item_Id := Entity_Of (Ref_Item);
- if Ekind_In (Ref_Item_Id, E_Abstract_State, E_Variable)
+ if Ekind_In (Ref_Item_Id, E_Abstract_State,
+ E_Constant,
+ E_Variable)
and then Present (Encapsulating_State (Ref_Item_Id))
and then Encapsulating_State (Ref_Item_Id) =
Dep_Item_Id
-- Start of processing for Check_Dependency_Clause
begin
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ return;
+ end if;
+
-- Examine all refinement clauses and compare them against the
-- dependence clause.
-- Start of processing for Check_Output_States
begin
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
-- Inspect the outputs of pragma Depends looking for a state with a
-- visible refinement.
- if Present (Spec_Outputs) then
+ elsif Present (Spec_Outputs) then
Item_Elmt := First_Elmt (Spec_Outputs);
while Present (Item_Elmt) loop
Item := Node (Item_Elmt);
Clause : Node_Id;
begin
- if Present (Refinements) then
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
+ elsif Present (Refinements) then
Clause := First (Refinements);
while Present (Clause) loop
-- Do not complain about a null input refinement, since a null
-- input legitimately matches anything.
- if Nkind (Clause) /= N_Component_Association
- or else Nkind (Expression (Clause)) /= N_Null
+ if Nkind (Clause) = N_Component_Association
+ and then Nkind (Expression (Clause)) = N_Null
then
+ null;
+
+ else
SPARK_Msg_N
("unmatched or extra clause in dependence refinement",
Clause);
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
Errors : constant Nat := Serious_Errors_Detected;
- Refs : constant Node_Id := Expression (Get_Argument (N));
Clause : Node_Id;
Deps : Node_Id;
Dummy : Boolean;
+ Refs : Node_Id;
-- Start of processing for Analyze_Refined_Depends_In_Decl_Part
return;
end if;
- Deps := Expression (Get_Argument (Depends));
+ Deps := Expression (Get_Argument (Depends, Spec_Id));
-- A null dependency relation renders the refinement useless because it
-- cannot possibly mention abstract states with visible refinement. Note
Dependencies := New_Copy_List_Tree (Component_Associations (Deps));
Normalize_Clauses (Dependencies);
+ Refs := Expression (Get_Argument (N, Spec_Id));
+
if Nkind (Refs) = N_Null then
Refinements := No_List;
-- These list contain the entities of all Input, In_Out, Output and
-- Proof_In items defined in the corresponding Global pragma.
+ Spec_Id : Entity_Id;
+ -- The entity of the subprogram subject to pragma Refined_Global
+
procedure Check_In_Out_States;
-- Determine whether the corresponding Global pragma mentions In_Out
-- states with visible refinement and if so, ensure that one of the
-- Verify the legality of a single global list declaration. Global_Mode
-- denotes the current mode in effect.
- procedure Collect_Global_Items (Prag : Node_Id);
- -- Gather all input, in out, output and Proof_In items of pragma Prag
- -- in lists In_Items, In_Out_Items, Out_Items and Proof_In_Items. Flags
- -- Has_In_State, Has_In_Out_State, Has_Out_State and Has_Proof_In_State
- -- are set when there is at least one abstract state with visible
- -- refinement available in the corresponding mode. Flag Has_Null_State
- -- is set when at least state has a null refinement.
+ procedure Collect_Global_Items
+ (List : Node_Id;
+ Mode : Name_Id := Name_Input);
+ -- Gather all input, in out, output and Proof_In items from node List
+ -- and separate them in lists In_Items, In_Out_Items, Out_Items and
+ -- Proof_In_Items. Flags Has_In_State, Has_In_Out_State, Has_Out_State
+ -- and Has_Proof_In_State are set when there is at least one abstract
+ -- state with visible refinement available in the corresponding mode.
+ -- Flag Has_Null_State is set when at least state has a null refinement.
+ -- Mode enotes the current global mode in effect.
function Present_Then_Remove
(List : Elist_Id;
Error_Msg_Name_1 := Chars (State_Id);
SPARK_Msg_NE
("constituent & of state % must have mode Input, In_Out "
- & "or Output in global refinement",
- N, Constit_Id);
+ & "or Output in global refinement", N, Constit_Id);
else
Has_Missing := True;
-- Start of processing for Check_In_Out_States
begin
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
-- Inspect the In_Out items of the corresponding Global pragma
-- looking for a state with a visible refinement.
- if Has_In_Out_State and then Present (In_Out_Items) then
+ elsif Has_In_Out_State and then Present (In_Out_Items) then
Item_Elmt := First_Elmt (In_Out_Items);
while Present (Item_Elmt) loop
Item_Id := Node (Item_Elmt);
-- Start of processing for Check_Input_States
begin
- -- Inspect the Input items of the corresponding Global pragma
- -- looking for a state with a visible refinement.
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
+ -- Inspect the Input items of the corresponding Global pragma looking
+ -- for a state with a visible refinement.
- if Has_In_State and then Present (In_Items) then
+ elsif Has_In_State and then Present (In_Items) then
Item_Elmt := First_Elmt (In_Items);
while Present (Item_Elmt) loop
Item_Id := Node (Item_Elmt);
-- Start of processing for Check_Output_States
begin
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
-- Inspect the Output items of the corresponding Global pragma
-- looking for a state with a visible refinement.
- if Has_Out_State and then Present (Out_Items) then
+ elsif Has_Out_State and then Present (Out_Items) then
Item_Elmt := First_Elmt (Out_Items);
while Present (Item_Elmt) loop
Item_Id := Node (Item_Elmt);
-- Start of processing for Check_Proof_In_States
begin
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
-- Inspect the Proof_In items of the corresponding Global pragma
-- looking for a state with a visible refinement.
- if Has_Proof_In_State and then Present (Proof_In_Items) then
+ elsif Has_Proof_In_State and then Present (Proof_In_Items) then
Item_Elmt := First_Elmt (Proof_In_Items);
while Present (Item_Elmt) loop
Item_Id := Node (Item_Elmt);
-- Start of processing for Check_Refined_Global_Item
begin
- -- When the state or variable acts as a constituent of another
+ -- When the state or object acts as a constituent of another
-- state with a visible refinement, collect it for the state
-- completeness checks performed later on.
- if Present (Encapsulating_State (Item_Id))
+ if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
+ and then Present (Encapsulating_State (Item_Id))
and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
then
if Global_Mode = Name_Input then
-- Start of processing for Check_Refined_Global_List
begin
- if Nkind (List) = N_Null then
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
+ elsif Nkind (List) = N_Null then
null;
-- Single global item declaration
-- Collect_Global_Items --
--------------------------
- procedure Collect_Global_Items (Prag : Node_Id) is
- procedure Process_Global_List
- (List : Node_Id;
- Mode : Name_Id := Name_Input);
- -- Collect all items housed in a global list. Formal Mode denotes the
+ procedure Collect_Global_Items
+ (List : Node_Id;
+ Mode : Name_Id := Name_Input)
+ is
+ procedure Collect_Global_Item
+ (Item : Node_Id;
+ Item_Mode : Name_Id);
+ -- Add a single item to the appropriate list. Item_Mode denotes the
-- current mode in effect.
-------------------------
- -- Process_Global_List --
+ -- Collect_Global_Item --
-------------------------
- procedure Process_Global_List
- (List : Node_Id;
- Mode : Name_Id := Name_Input)
+ procedure Collect_Global_Item
+ (Item : Node_Id;
+ Item_Mode : Name_Id)
is
- procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id);
- -- Add a single item to the appropriate list. Formal Mode denotes
- -- the current mode in effect.
-
- -------------------------
- -- Process_Global_Item --
- -------------------------
-
- procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is
- Item_Id : constant Entity_Id :=
- Available_View (Entity_Of (Item));
- -- The above handles abstract views of variables and states
- -- built for limited with clauses.
+ Item_Id : constant Entity_Id := Available_View (Entity_Of (Item));
+ -- The above handles abstract views of variables and states built
+ -- for limited with clauses.
- begin
- -- Signal that the global list contains at least one abstract
- -- state with a visible refinement. Note that the refinement
- -- may be null in which case there are no constituents.
-
- if Ekind (Item_Id) = E_Abstract_State then
- if Has_Null_Refinement (Item_Id) then
- Has_Null_State := True;
+ begin
+ -- Signal that the global list contains at least one abstract
+ -- state with a visible refinement. Note that the refinement may
+ -- be null in which case there are no constituents.
- elsif Has_Non_Null_Refinement (Item_Id) then
- if Mode = Name_Input then
- Has_In_State := True;
- elsif Mode = Name_In_Out then
- Has_In_Out_State := True;
- elsif Mode = Name_Output then
- Has_Out_State := True;
- elsif Mode = Name_Proof_In then
- Has_Proof_In_State := True;
- end if;
+ if Ekind (Item_Id) = E_Abstract_State then
+ if Has_Null_Refinement (Item_Id) then
+ Has_Null_State := True;
+
+ elsif Has_Non_Null_Refinement (Item_Id) then
+ if Item_Mode = Name_Input then
+ Has_In_State := True;
+ elsif Item_Mode = Name_In_Out then
+ Has_In_Out_State := True;
+ elsif Item_Mode = Name_Output then
+ Has_Out_State := True;
+ elsif Item_Mode = Name_Proof_In then
+ Has_Proof_In_State := True;
end if;
end if;
+ end if;
- -- Add the item to the proper list
-
- if Mode = Name_Input then
- Add_Item (Item_Id, In_Items);
- elsif Mode = Name_In_Out then
- Add_Item (Item_Id, In_Out_Items);
- elsif Mode = Name_Output then
- Add_Item (Item_Id, Out_Items);
- elsif Mode = Name_Proof_In then
- Add_Item (Item_Id, Proof_In_Items);
- end if;
- end Process_Global_Item;
-
- -- Local variables
+ -- Add the item to the proper list
- Item : Node_Id;
+ if Item_Mode = Name_Input then
+ Add_Item (Item_Id, In_Items);
+ elsif Item_Mode = Name_In_Out then
+ Add_Item (Item_Id, In_Out_Items);
+ elsif Item_Mode = Name_Output then
+ Add_Item (Item_Id, Out_Items);
+ elsif Item_Mode = Name_Proof_In then
+ Add_Item (Item_Id, Proof_In_Items);
+ end if;
+ end Collect_Global_Item;
- -- Start of processing for Process_Global_List
+ -- Local variables
- begin
- if Nkind (List) = N_Null then
- null;
+ Item : Node_Id;
- -- Single global item declaration
+ -- Start of processing for Collect_Global_Items
- elsif Nkind_In (List, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
- then
- Process_Global_Item (List, Mode);
+ begin
+ if Nkind (List) = N_Null then
+ null;
- -- Single global list or moded global list declaration
+ -- Single global item declaration
- elsif Nkind (List) = N_Aggregate then
+ elsif Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ Collect_Global_Item (List, Mode);
- -- The declaration of a simple global list appear as a
- -- collection of expressions.
+ -- Single global list or moded global list declaration
- if Present (Expressions (List)) then
- Item := First (Expressions (List));
- while Present (Item) loop
- Process_Global_Item (Item, Mode);
- Next (Item);
- end loop;
+ elsif Nkind (List) = N_Aggregate then
- -- The declaration of a moded global list appears as a
- -- collection of component associations where individual
- -- choices denote mode.
+ -- The declaration of a simple global list appear as a collection
+ -- of expressions.
- elsif Present (Component_Associations (List)) then
- Item := First (Component_Associations (List));
- while Present (Item) loop
- Process_Global_List
- (List => Expression (Item),
- Mode => Chars (First (Choices (Item))));
+ if Present (Expressions (List)) then
+ Item := First (Expressions (List));
+ while Present (Item) loop
+ Collect_Global_Item (Item, Mode);
+ Next (Item);
+ end loop;
- Next (Item);
- end loop;
+ -- The declaration of a moded global list appears as a collection
+ -- of component associations where individual choices denote mode.
- -- Invalid tree
+ elsif Present (Component_Associations (List)) then
+ Item := First (Component_Associations (List));
+ while Present (Item) loop
+ Collect_Global_Items
+ (List => Expression (Item),
+ Mode => Chars (First (Choices (Item))));
- else
- raise Program_Error;
- end if;
+ Next (Item);
+ end loop;
- -- To accomodate partial decoration of disabled SPARK features,
- -- this routine may be called with illegal input. If this is the
- -- case, do not raise Program_Error.
+ -- Invalid tree
else
- null;
+ raise Program_Error;
end if;
- end Process_Global_List;
- -- Start of processing for Collect_Global_Items
+ -- To accomodate partial decoration of disabled SPARK features, this
+ -- routine may be called with illegal input. If this is the case, do
+ -- not raise Program_Error.
- begin
- Process_Global_List (Expression (Get_Argument (Prag)));
+ else
+ null;
+ end if;
end Collect_Global_Items;
-------------------------
-- Start of processing for Report_Extra_Constituents
begin
- Report_Extra_Constituents_In_List (In_Constits);
- Report_Extra_Constituents_In_List (In_Out_Constits);
- Report_Extra_Constituents_In_List (Out_Constits);
- Report_Extra_Constituents_In_List (Proof_In_Constits);
+ -- Do not perform this check in an instance because it was already
+ -- performed successfully in the generic template.
+
+ if Is_Generic_Instance (Spec_Id) then
+ null;
+
+ else
+ Report_Extra_Constituents_In_List (In_Constits);
+ Report_Extra_Constituents_In_List (In_Out_Constits);
+ Report_Extra_Constituents_In_List (Out_Constits);
+ Report_Extra_Constituents_In_List (Proof_In_Constits);
+ end if;
end Report_Extra_Constituents;
-- Local variables
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Errors : constant Nat := Serious_Errors_Detected;
- Items : constant Node_Id := Expression (Get_Argument (N));
- Spec_Id : Entity_Id;
+ Items : Node_Id;
-- Start of processing for Analyze_Refined_Global_In_Decl_Part
end if;
Global := Get_Pragma (Spec_Id, Pragma_Global);
+ Items := Expression (Get_Argument (N, Spec_Id));
-- The subprogram declaration lacks pragma Global. This renders
-- Refined_Global useless as there is nothing to refine.
-- Extract all relevant items from the corresponding Global pragma
- Collect_Global_Items (Global);
+ Collect_Global_Items (Expression (Get_Argument (Global, Spec_Id)));
- -- Corresponding Global pragma must mention at least one state witha
- -- visible refinement at the point Refined_Global is processed. States
- -- with null refinements need Refined_Global pragma (SPARK RM 7.2.4(2)).
+ -- 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 not Has_In_State
- and then not Has_In_Out_State
- and then not Has_Out_State
- and then not Has_Proof_In_State
- and then not Has_Null_State
- then
- SPARK_Msg_NE
- ("useless refinement, subprogram & does not depend on abstract "
- & "state with visible refinement", N, Spec_Id);
- return;
- end if;
+ if Is_Generic_Instance (Spec_Id) then
+ null;
- -- The global refinement of inputs and outputs cannot be null when the
- -- corresponding Global pragma contains at least one item except in the
- -- case where we have states with null refinements.
+ -- Non-instance case
- if Nkind (Items) = N_Null
- and then
- (Present (In_Items)
- or else Present (In_Out_Items)
- or else Present (Out_Items)
- or else Present (Proof_In_Items))
- and then not Has_Null_State
- then
- SPARK_Msg_NE
- ("refinement cannot be null, subprogram & has global items",
- N, Spec_Id);
- return;
+ else
+ -- The corresponding Global pragma must mention at least one state
+ -- witha visible refinement at the point Refined_Global is processed.
+ -- States with null refinements need Refined_Global pragma
+ -- (SPARK RM 7.2.4(2)).
+
+ if not Has_In_State
+ and then not Has_In_Out_State
+ and then not Has_Out_State
+ and then not Has_Proof_In_State
+ and then not Has_Null_State
+ then
+ SPARK_Msg_NE
+ ("useless refinement, subprogram & does not depend on abstract "
+ & "state with visible refinement", N, Spec_Id);
+ return;
+
+ -- The global refinement of inputs and outputs cannot be null when
+ -- the corresponding Global pragma contains at least one item except
+ -- in the case where we have states with null refinements.
+
+ elsif Nkind (Items) = N_Null
+ and then
+ (Present (In_Items)
+ or else Present (In_Out_Items)
+ or else Present (Out_Items)
+ or else Present (Proof_In_Items))
+ and then not Has_Null_State
+ then
+ SPARK_Msg_NE
+ ("refinement cannot be null, subprogram & has global items",
+ N, Spec_Id);
+ return;
+ end if;
end if;
-- Analyze Refined_Global as if it behaved as a regular pragma Global.
----------------------------------------
procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is
+ Body_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
+ Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
+
Available_States : Elist_Id := No_Elist;
-- A list of all abstract states defined in the package declaration that
-- are available for refinement. The list is used to report unrefined
-- states.
- Body_Id : Entity_Id;
- -- The body entity of the package subject to pragma Refined_State
-
Body_States : Elist_Id := No_Elist;
-- A list of all hidden states that appear in the body of the related
-- package. The list is used to report unused hidden states.
-- A list that contains all refined states processed so far. The list is
-- used to detect duplicate refinements.
- Spec_Id : Entity_Id;
- -- The spec entity of the package subject to pragma Refined_State
-
procedure Analyze_Refinement_Clause (Clause : Node_Id);
-- Perform full analysis of a single refinement clause
Resolve_State (Constit);
-- Ensure that the constituent denotes a valid state or a
- -- whole variable.
+ -- whole object (SPARK RM 7.2.2(5)).
if Is_Entity_Name (Constit) then
Constit_Id := Entity_Of (Constit);
else
SPARK_Msg_NE
- ("constituent & must denote a variable or state (SPARK "
- & "RM 7.2.2(5))", Constit, Constit_Id);
+ ("constituent & must denote object or state",
+ Constit, Constit_Id);
end if;
-- The constituent is illegal
-- state ... has unused Part_Of constituents
-- abstract state ... defined at ...
+ -- constant ... defined at ...
-- variable ... defined at ...
if not Posted then
SPARK_Msg_NE
("\abstract state & defined #", State, Constit_Id);
else
- SPARK_Msg_NE
- ("\variable & defined #", State, Constit_Id);
+ SPARK_Msg_NE ("\variable & defined #", State, Constit_Id);
end if;
Next_Elmt (Constit_Elmt);
Constit := First (Expressions (Constit));
while Present (Constit) loop
Analyze_Constituent (Constit);
-
Next (Constit);
end loop;
end if;
-- A list containing all body states of Pack_Id
procedure Collect_Visible_States (Pack_Id : Entity_Id);
- -- Gather the entities of all abstract states and variables declared
- -- in the visible state space of package Pack_Id.
+ -- Gather the entities of all abstract states and objects declared in
+ -- the visible state space of package Pack_Id.
----------------------------
-- Collect_Visible_States --
-- Start of processing for Collect_Body_States
begin
- -- Inspect the declarations of the body looking for source variables,
+ -- Inspect the declarations of the body looking for source objects,
-- packages and package instantiations.
Decl := First (Declarations (Pack_Body));
if Nkind (Decl) = N_Object_Declaration then
Item_Id := Defining_Entity (Decl);
- -- Capture source variables only as internally generated
- -- temporaries cannot be named and participate in refinement.
+ -- Capture source variables as internally generated temporaries
+ -- cannot be named and participate in refinement.
if Ekind (Item_Id) = E_Variable
and then Comes_From_Source (Item_Id)
elsif Nkind (Decl) = N_Package_Declaration then
Item_Id := Defining_Entity (Decl);
- -- Capture the visible abstract states and variables of a
+ -- Capture the visible abstract states and objects of a
-- source package [instantiation].
if Comes_From_Source (Item_Id) then
-- body of package ... has unused hidden states
-- abstract state ... defined at ...
+ -- constant ... defined at ...
-- variable ... defined at ...
if not Posted then
SPARK_Msg_NE
("\abstract state & defined #", Body_Id, State_Id);
else
- SPARK_Msg_NE
- ("\variable & defined #", Body_Id, State_Id);
+ SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
end if;
Next_Elmt (State_Elmt);
-- Local declarations
- Body_Decl : constant Node_Id := Parent (N);
- Clauses : constant Node_Id := Expression (Get_Argument (N));
- Clause : Node_Id;
+ Clauses : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ Clause : Node_Id;
-- Start of processing for Analyze_Refined_State_In_Decl_Part
begin
Set_Analyzed (N);
- Body_Id := Defining_Entity (Body_Decl);
- Spec_Id := Corresponding_Spec (Body_Decl);
-
-- Replicate the abstract states declared by the package because the
-- matching algorithm will consume states.
------------------------------------
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is
- procedure Preanalyze_Test_Case_Arg
- (Arg_Nam : Name_Id;
- Spec_Id : Entity_Id);
+ Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+
+ procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id);
-- Preanalyze one of the optional arguments "Requires" or "Ensures"
- -- denoted by Arg_Nam. Spec_Id is the entity of the subprogram spec
- -- subject to pragma Test_Case.
+ -- denoted by Arg_Nam.
------------------------------
-- Preanalyze_Test_Case_Arg --
------------------------------
- procedure Preanalyze_Test_Case_Arg
- (Arg_Nam : Name_Id;
- Spec_Id : Entity_Id)
- is
+ procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id) is
Arg : Node_Id;
begin
-- Local variables
- Spec_Id : Entity_Id;
- Subp_Decl : Node_Id;
-
Restore_Scope : Boolean := False;
- -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
-- Start of processing for Analyze_Test_Case_In_Decl_Part
begin
- Subp_Decl := Find_Related_Subprogram_Or_Body (N);
- Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-
-- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining
-- to subprogram declarations.
end if;
end if;
- Preanalyze_Test_Case_Arg (Name_Requires, Spec_Id);
- Preanalyze_Test_Case_Arg (Name_Ensures, Spec_Id);
+ Preanalyze_Test_Case_Arg (Name_Requires);
+ Preanalyze_Test_Case_Arg (Name_Ensures);
+
+ 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);
-
- if Restore_Scope then
- End_Scope;
- end if;
end Analyze_Test_Case_In_Decl_Part;
----------------
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
- Subp_Id : Entity_Id)
+ Spec_Id : Entity_Id)
is
begin
if Warn_On_Redundant_Constructs
- and then Has_Pragma_Inline_Always (Subp_Id)
+ and then Has_Pragma_Inline_Always (Spec_Id)
then
Error_Msg_Name_1 := Original_Aspect_Pragma_Name (Prag);
if From_Aspect_Specification (Prag) then
Error_Msg_NE
("aspect % not enforced on inlined subprogram &?r?",
- Corresponding_Aspect (Prag), Subp_Id);
+ Corresponding_Aspect (Prag), Spec_Id);
else
Error_Msg_NE
("pragma % not enforced on inlined subprogram &?r?",
- Prag, Subp_Id);
+ Prag, Spec_Id);
end if;
end if;
end Check_Postcondition_Use_In_Inlined_Subprogram;
elsif Nkind (Clause) = N_Component_Association then
Collect_Dependency_Item
- (Expression (Clause), Is_Input => True);
+ (Item => Expression (Clause),
+ Is_Input => True);
+
Collect_Dependency_Item
- (First (Choices (Clause)), Is_Input => False);
+ (Item => First (Choices (Clause)),
+ Is_Input => False);
-- To accomodate partial decoration of disabled SPARK features, this
-- routine may be called with illegal input. If this is the case, do
begin
Global_Seen := False;
- -- Process all formal parameters
+ -- Process all [generic] formal parameters
- Formal := First_Formal (Spec_Id);
+ Formal := First_Entity (Spec_Id);
while Present (Formal) loop
- if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
+ if Ekind_In (Formal, E_Generic_In_Parameter,
+ E_In_Out_Parameter,
+ E_In_Parameter)
+ then
Add_Item (Formal, Subp_Inputs);
end if;
- if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+ if Ekind_In (Formal, E_Generic_In_Out_Parameter,
+ E_In_Out_Parameter,
+ E_Out_Parameter)
+ then
Add_Item (Formal, Subp_Outputs);
-- Out parameters can act as inputs when the related type is
end if;
end if;
- Next_Formal (Formal);
+ Next_Entity (Formal);
end loop;
-- When processing a subprogram body, look for pragmas Refined_Depends
Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends);
Global := Get_Pragma (Subp_Id, Pragma_Refined_Global);
- -- Subprogram declaration case, look for pragmas Depends and Global
+ -- Subprogram declaration or stand alone body case, look for pragmas
+ -- Depends and Global
else
Depends := Get_Pragma (Spec_Id, Pragma_Depends);
------------------
function Get_Argument
- (Prag : Node_Id;
- Spec_Id : Entity_Id := Empty) return Node_Id
+ (Prag : Node_Id;
+ Context_Id : Entity_Id := Empty) return Node_Id
is
Args : constant List_Id := Pragma_Argument_Associations (Prag);
begin
- -- Use the expression of the original aspect if possible when compiling
- -- for ASIS or when analyzing the template of a generic subprogram. In
- -- both cases the aspect's tree must be decorated to allow for ASIS
- -- queries or to save all global references in the generic context.
+ -- Use the expression of the original aspect when compiling for ASIS or
+ -- when analyzing the template of a generic unit. In both cases the
+ -- aspect's tree must be decorated to allow for ASIS queries or to save
+ -- the global references in the generic context.
if From_Aspect_Specification (Prag)
- and then
- (ASIS_Mode or else (Present (Spec_Id)
- and then Is_Generic_Subprogram (Spec_Id)))
+ and then (ASIS_Mode or else (Present (Context_Id)
+ and then Is_Generic_Unit (Context_Id)))
then
return Corresponding_Aspect (Prag);
-- 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 items of pragma [Refined_]Global
+ -- 2) The generic formal parameters of the generic subprogram
+ -- 3) The items of pragma [Refined_]Global
-- or
- -- 3) The items of pragma [Refined_]Depends if there is no pragma
+ -- 4) 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
-- 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 and Refined_State. Find the declaration of the related
+ -- package [body] subject to pragma Prag. The return value is either
+ -- N_Package_Declaration, N_Package_Body or Empty if the placement of
+ -- the pragma is illegal. If flag Do_Checks is set, the routine reports
+ -- duplicate pragmas.
+
function Find_Related_Subprogram_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
-- illegal.
+ function Get_Argument
+ (Prag : Node_Id;
+ Context_Id : Node_Id := Empty) return Node_Id;
+ -- Obtain the argument of pragma Prag depending on context and the nature
+ -- of the pragma. The argument is extracted in the following manner:
+ --
+ -- When the pragma is generated from an aspect, return the corresponding
+ -- aspect for ASIS or when 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_Pragma (N : Node_Id) return SPARK_Mode_Type;
-- Given a pragma SPARK_Mode node, return corresponding mode id
with Sem_Attr; use Sem_Attr;
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_Eval; use Sem_Eval;
-- Corresponding_Spec_Of --
---------------------------
- function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id is
+ function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id is
begin
- if Nkind (Subp_Decl) = N_Subprogram_Body
- and then Present (Corresponding_Spec (Subp_Decl))
+ if Nkind_In (Decl, N_Package_Body, N_Subprogram_Body)
+ and then Present (Corresponding_Spec (Decl))
then
- return Corresponding_Spec (Subp_Decl);
+ return Corresponding_Spec (Decl);
- elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
- and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+ elsif Nkind_In (Decl, N_Package_Body_Stub, N_Subprogram_Body_Stub)
+ and then Present (Corresponding_Spec_Of_Stub (Decl))
then
- return Corresponding_Spec_Of_Stub (Subp_Decl);
+ return Corresponding_Spec_Of_Stub (Decl);
else
- return Defining_Entity (Subp_Decl);
+ return Defining_Entity (Decl);
end if;
end Corresponding_Spec_Of;
+ -----------------------------
+ -- Create_Generic_Contract --
+ -----------------------------
+
+ procedure Create_Generic_Contract (Unit : Node_Id) is
+ Templ : constant Node_Id := Original_Node (Unit);
+ Templ_Id : constant Entity_Id := Defining_Entity (Templ);
+
+ procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
+ -- Add a single contract-related source pragma Prag to the contract of
+ -- generic template Templ_Id.
+
+ ---------------------------------
+ -- Add_Generic_Contract_Pragma --
+ ---------------------------------
+
+ procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
+ Prag_Templ : Node_Id;
+
+ begin
+ -- Mark the pragma to prevent the premature capture of global
+ -- references when capturing global references of the context
+ -- (see Save_References_In_Pragma).
+
+ Set_Is_Generic_Contract_Pragma (Prag);
+
+ -- Pragmas that apply to a generic subprogram declaration are not
+ -- part of the semantic structure of the generic template:
+
+ -- generic
+ -- procedure Example (Formal : Integer);
+ -- pragma Precondition (Formal > 0);
+
+ -- Create a generic template for such pragmas and link the template
+ -- of the pragma with the generic template.
+
+ if Nkind (Templ) = N_Generic_Subprogram_Declaration then
+ Rewrite
+ (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
+ Prag_Templ := Original_Node (Prag);
+
+ Set_Is_Generic_Contract_Pragma (Prag_Templ);
+ Add_Contract_Item (Prag_Templ, Templ_Id);
+
+ -- Otherwise link the pragma with the generic template
+
+ else
+ Add_Contract_Item (Prag, Templ_Id);
+ end if;
+ end Add_Generic_Contract_Pragma;
+
+ -- Local variables
+
+ Context : constant Node_Id := Parent (Unit);
+ Decl : Node_Id := Empty;
+
+ -- Start of processing for Create_Generic_Contract
+
+ begin
+ -- A generic package declaration carries contract-related source pragmas
+ -- in its visible declarations.
+
+ if Nkind (Templ) = N_Generic_Package_Declaration then
+ Set_Ekind (Templ_Id, E_Generic_Package);
+
+ if Present (Visible_Declarations (Specification (Templ))) then
+ Decl := First (Visible_Declarations (Specification (Templ)));
+ end if;
+
+ -- A generic package body carries contract-related source pragmas in its
+ -- declarations.
+
+ elsif Nkind (Templ) = N_Package_Body then
+ Set_Ekind (Templ_Id, E_Package_Body);
+
+ if Present (Declarations (Templ)) then
+ Decl := First (Declarations (Templ));
+ end if;
+
+ -- Generic subprogram declaration
+
+ elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
+ if Nkind (Specification (Templ)) = N_Function_Specification then
+ Set_Ekind (Templ_Id, E_Generic_Function);
+ else
+ Set_Ekind (Templ_Id, E_Generic_Procedure);
+ end if;
+
+ -- When the generic subprogram acts as a compilation unit, inspect
+ -- the Pragmas_After list for contract-related source pragmas.
+
+ if Nkind (Context) = N_Compilation_Unit then
+ if Present (Aux_Decls_Node (Context))
+ and then Present (Pragmas_After (Aux_Decls_Node (Context)))
+ then
+ Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
+ end if;
+
+ -- Otherwise inspect the successive declarations for contract-related
+ -- source pragmas.
+
+ else
+ Decl := Next (Unit);
+ end if;
+
+ -- A generic subprogram body carries contract-related source pragmas in
+ -- its declarations.
+
+ elsif Nkind (Templ) = N_Subprogram_Body then
+ Set_Ekind (Templ_Id, E_Subprogram_Body);
+
+ if Present (Declarations (Templ)) then
+ Decl := First (Declarations (Templ));
+ end if;
+ end if;
+
+ -- Inspect the relevant declarations looking for contract-related source
+ -- pragmas and add them to the contract of the generic unit.
+
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ if Nkind (Decl) = N_Pragma then
+
+ -- The source pragma is a contract annotation
+
+ if Is_Contract_Annotation (Decl) then
+ Add_Generic_Contract_Pragma (Decl);
+ end if;
+
+ -- The region where a contract-related source pragma may appear
+ -- ends with the first source non-pragma declaration or statement.
+
+ else
+ exit;
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Create_Generic_Contract;
+
--------------------
-- Current_Entity --
--------------------
----------------------------
function Is_Contract_Annotation (Item : Node_Id) return Boolean is
- Nam : Name_Id;
-
begin
- if Nkind (Item) = N_Aspect_Specification then
- Nam := Chars (Identifier (Item));
-
- else pragma Assert (Nkind (Item) = N_Pragma);
- Nam := Pragma_Name (Item);
- end if;
-
- return Nam = Name_Abstract_State
- or else Nam = Name_Contract_Cases
- or else Nam = Name_Depends
- or else Nam = Name_Extensions_Visible
- or else Nam = Name_Global
- or else Nam = Name_Initial_Condition
- or else Nam = Name_Initializes
- or else Nam = Name_Post
- or else Nam = Name_Post_Class
- or else Nam = Name_Postcondition
- or else Nam = Name_Pre
- or else Nam = Name_Pre_Class
- or else Nam = Name_Precondition
- or else Nam = Name_Refined_Depends
- or else Nam = Name_Refined_Global
- or else Nam = Name_Refined_State
- or else Nam = Name_Test_Case;
+ return Is_Package_Contract_Annotation (Item)
+ or else
+ Is_Subprogram_Contract_Annotation (Item);
end Is_Contract_Annotation;
--------------------------------------
end if;
end Is_Fully_Initialized_Variant;
+ ------------------------------------
+ -- Is_Generic_Declaration_Or_Body --
+ ------------------------------------
+
+ function Is_Generic_Declaration_Or_Body (Decl : Node_Id) return Boolean is
+ Spec_Decl : Node_Id;
+
+ begin
+ -- Package/subprogram body
+
+ if Nkind_In (Decl, N_Package_Body, N_Subprogram_Body)
+ and then Present (Corresponding_Spec (Decl))
+ then
+ Spec_Decl := Unit_Declaration_Node (Corresponding_Spec (Decl));
+
+ -- Package/subprogram body stub
+
+ elsif Nkind_In (Decl, N_Package_Body_Stub, N_Subprogram_Body_Stub)
+ and then Present (Corresponding_Spec_Of_Stub (Decl))
+ then
+ Spec_Decl :=
+ Unit_Declaration_Node (Corresponding_Spec_Of_Stub (Decl));
+
+ -- All other cases
+
+ else
+ Spec_Decl := Decl;
+ end if;
+
+ -- Rather than inspecting the defining entity of the spec declaration,
+ -- look at its Nkind. This takes care of the case where the analysis of
+ -- a generic body modifies the Ekind of its spec to allow for recursive
+ -- calls.
+
+ return
+ Nkind_In (Spec_Decl, N_Generic_Package_Declaration,
+ N_Generic_Subprogram_Declaration);
+ end Is_Generic_Declaration_Or_Body;
+
----------------------------
-- Is_Inherited_Operation --
----------------------------
end if;
end Is_OK_Variable_For_Out_Formal;
+ ------------------------------------
+ -- Is_Package_Contract_Annotation --
+ ------------------------------------
+
+ function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean is
+ Nam : Name_Id;
+
+ begin
+ if Nkind (Item) = N_Aspect_Specification then
+ Nam := Chars (Identifier (Item));
+
+ else pragma Assert (Nkind (Item) = N_Pragma);
+ Nam := Pragma_Name (Item);
+ end if;
+
+ return Nam = Name_Abstract_State
+ or else Nam = Name_Initial_Condition
+ or else Nam = Name_Initializes
+ or else Nam = Name_Refined_State;
+ end Is_Package_Contract_Annotation;
+
-----------------------------------
-- Is_Partially_Initialized_Type --
-----------------------------------
or else Nkind (N) = N_Procedure_Call_Statement;
end Is_Statement;
+ ---------------------------------------
+ -- Is_Subprogram_Contract_Annotation --
+ ---------------------------------------
+
+ function Is_Subprogram_Contract_Annotation
+ (Item : Node_Id) return Boolean
+ is
+ Nam : Name_Id;
+
+ begin
+ if Nkind (Item) = N_Aspect_Specification then
+ Nam := Chars (Identifier (Item));
+
+ else pragma Assert (Nkind (Item) = N_Pragma);
+ Nam := Pragma_Name (Item);
+ end if;
+
+ return Nam = Name_Contract_Cases
+ or else Nam = Name_Depends
+ or else Nam = Name_Extensions_Visible
+ or else Nam = Name_Global
+ or else Nam = Name_Post
+ or else Nam = Name_Post_Class
+ or else Nam = Name_Postcondition
+ or else Nam = Name_Pre
+ or else Nam = Name_Pre_Class
+ or else Nam = Name_Precondition
+ or else Nam = Name_Refined_Depends
+ or else Nam = Name_Refined_Global
+ or else Nam = Name_Refined_Post
+ or else Nam = Name_Test_Case;
+ end Is_Subprogram_Contract_Annotation;
+
--------------------------------------------------
-- Is_Subprogram_Stub_Without_Prior_Declaration --
--------------------------------------------------
-- Add pragma Prag to the contract of an entry, a package [body], a
-- subprogram [body] or variable denoted by Id. The following are valid
-- pragmas:
- -- Abstract_States
+ -- Abstract_State
-- Async_Readers
-- Async_Writers
-- Contract_Cases
-- attribute, except in the case of formal private and derived types.
-- Possible optimization???
- function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id;
- -- Return the corresponding spec of Subp_Decl when it denotes a body [stub]
- -- or the defining entity of subprogram declaration Subp_Decl in all other
- -- cases.
+ function Corresponding_Spec_Of (Decl : Node_Id) return Entity_Id;
+ -- Return the corresponding spec of Decl when it denotes a package or a
+ -- subprogram [stub], or the defining entity of Decl.
+
+ procedure Create_Generic_Contract (Unit : Node_Id);
+ -- Create a contract node for a generic package, generic subprogram or a
+ -- generic body denoted by Unit by collecting all source contract-related
+ -- pragmas in the contract of the unit.
function Current_Entity (N : Node_Id) return Entity_Id;
pragma Inline (Current_Entity);
-- means that the result returned is not crucial, but should err on the
-- side of thinking things are fully initialized if it does not know.
+ function Is_Generic_Declaration_Or_Body (Decl : Node_Id) return Boolean;
+ -- Determine whether arbitrary declaration Decl denotes a generic package,
+ -- a generic subprogram or a generic body.
+
function Is_Inherited_Operation (E : Entity_Id) return Boolean;
-- E is a subprogram. Return True is E is an implicit operation inherited
-- by a derived type declaration.
-- the Is_Variable sense) with an untagged type target are considered view
-- conversions and hence variables.
+ function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean;
+ -- Determine whether aspect specification or pragma Item is one of the
+ -- following package contract annotations:
+ -- Abstract_State
+ -- Initial_Condition
+ -- Initializes
+ -- Refined_State
+
function Is_Partially_Initialized_Type
(Typ : Entity_Id;
Include_Implicit : Boolean := True) return Boolean;
-- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo).
-- Note that a label is *not* a statement, and will return False.
+ function Is_Subprogram_Contract_Annotation (Item : Node_Id) return Boolean;
+ -- Determine whether aspect specification or pragma Item is one of the
+ -- following subprogram contract annotations:
+ -- Contract_Cases
+ -- Depends
+ -- Extensions_Visible
+ -- Global
+ -- Post
+ -- Post_Class
+ -- Postcondition
+ -- Pre
+ -- Pre_Class
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Test_Case
+
function Is_Subprogram_Stub_Without_Prior_Declaration
(N : Node_Id) return Boolean;
-- Return True if N is a subprogram stub with no prior subprogram
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
return Flag4 (N);
end Is_Folded_In_Parser;
+ function Is_Generic_Contract_Pragma
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ return Flag2 (N);
+ end Is_Generic_Contract_Pragma;
+
function Is_Ignored
(N : Node_Id) return Boolean is
begin
Set_Flag4 (N, Val);
end Set_Is_Folded_In_Parser;
+ procedure Set_Is_Generic_Contract_Pragma
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ Set_Flag2 (N, Val);
+ end Set_Is_Generic_Contract_Pragma;
+
procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True) is
begin
-- operand is of the component type of the result. Used in resolving
-- concatenation nodes in instances.
+ -- Is_Controlling_Actual (Flag16-Sem)
+ -- This flag is set on in an expression that is a controlling argument in
+ -- a dispatching call. It is off in all other cases. See Sem_Disp for
+ -- details of its use.
+
-- Is_Delayed_Aspect (Flag14-Sem)
-- Present in N_Pragma and N_Attribute_Definition_Clause nodes which
-- come from aspect specifications, where the evaluation of the aspect
-- must be delayed to the freeze point. This flag is also set True in
-- the corresponding N_Aspect_Specification node.
- -- Is_Controlling_Actual (Flag16-Sem)
- -- This flag is set on in an expression that is a controlling argument in
- -- a dispatching call. It is off in all other cases. See Sem_Disp for
- -- details of its use.
-
-- Is_Disabled (Flag15-Sem)
-- A flag set in an N_Aspect_Specification or N_Pragma node if there was
-- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
-- objects. The wrapper prevents interference between exception handlers
-- and At_End handlers.
+ -- Is_Generic_Contract_Pragma (Flag2-Sem)
+ -- This flag is present in N_Pragma nodes. It is set when the pragma is
+ -- a source construct, applies to a generic unit or its body and denotes
+ -- one of the following contract-related annotations:
+ -- Abstract_State
+ -- Contract_Cases
+ -- Depends
+ -- Extensions_Visible
+ -- Global
+ -- Initial_Condition
+ -- Initializes
+ -- Post
+ -- Post_Class
+ -- Postcondition
+ -- Pre
+ -- Pre_Class
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Refined_State
+ -- Test_Case
+
-- Is_Ignored (Flag9-Sem)
-- A flag set in an N_Aspect_Specification or N_Pragma node if there was
-- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
-- Is_Checked (Flag11-Sem)
-- Is_Delayed_Aspect (Flag14-Sem)
-- Is_Disabled (Flag15-Sem)
+ -- Is_Generic_Contract_Pragma (Flag2-Sem)
-- Is_Ignored (Flag9-Sem)
-- Is_Inherited (Flag4-Sem)
-- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
-- N_Contract
-- Sloc points to the subprogram's name
- -- Pre_Post_Conditions (Node1) (set to Empty if none)
- -- Contract_Test_Cases (Node2) (set to Empty if none)
- -- Classifications (Node3) (set to Empty if none)
+ -- Pre_Post_Conditions (Node1-Sem) (set to Empty if none)
+ -- Contract_Test_Cases (Node2-Sem) (set to Empty if none)
+ -- Classifications (Node3-Sem) (set to Empty if none)
-- Pre_Post_Conditions contains a collection of pragmas that correspond
-- to pre- and postconditions associated with an entry or a subprogram
subtype N_Unit_Body is Node_Kind range
N_Package_Body ..
- N_Subprogram_Body;
+ N_Subprogram_Body;
---------------------------
-- Node Access Functions --
function Is_Folded_In_Parser
(N : Node_Id) return Boolean; -- Flag4
+ function Is_Generic_Contract_Pragma
+ (N : Node_Id) return Boolean; -- Flag2
+
function Is_Ignored
(N : Node_Id) return Boolean; -- Flag9
procedure Set_Is_Disabled
(N : Node_Id; Val : Boolean := True); -- Flag15
- procedure Set_Is_Ignored
- (N : Node_Id; Val : Boolean := True); -- Flag9
-
procedure Set_Is_Dynamic_Coextension
(N : Node_Id; Val : Boolean := True); -- Flag18
procedure Set_Is_Folded_In_Parser
(N : Node_Id; Val : Boolean := True); -- Flag4
+ procedure Set_Is_Generic_Contract_Pragma
+ (N : Node_Id; Val : Boolean := True); -- Flag2
+
+ procedure Set_Is_Ignored
+ (N : Node_Id; Val : Boolean := True); -- Flag9
+
procedure Set_Is_In_Discriminant_Check
(N : Node_Id; Val : Boolean := True); -- Flag11
N_Pragma =>
(1 => False, -- Next_Pragma (Node1-Sem)
2 => True, -- Pragma_Argument_Associations (List2)
- 3 => False, -- unused
+ 3 => False, -- Corresponding_Aspect (Node3-Sem)
4 => True, -- Pragma_Identifier (Node4)
5 => False), -- Next_Rep_Item (Node5-Sem)
5 => False), -- unused
N_Contract =>
- (1 => False, -- Pre_Post_Conditions (Node1)
- 2 => False, -- Contract_Test_Cases (Node2)
- 3 => False, -- Classifications (Node3)
+ (1 => False, -- Pre_Post_Conditions (Node1-Sem)
+ 2 => False, -- Contract_Test_Cases (Node2-Sem)
+ 3 => False, -- Classifications (Node3-Sem)
4 => False, -- unused
5 => False), -- unused
pragma Inline (Is_Expanded_Build_In_Place_Call);
pragma Inline (Is_Finalization_Wrapper);
pragma Inline (Is_Folded_In_Parser);
+ pragma Inline (Is_Generic_Contract_Pragma);
pragma Inline (Is_Ignored);
pragma Inline (Is_In_Discriminant_Check);
pragma Inline (Is_Inherited);
pragma Inline (Set_Is_Expanded_Build_In_Place_Call);
pragma Inline (Set_Is_Finalization_Wrapper);
pragma Inline (Set_Is_Folded_In_Parser);
+ pragma Inline (Set_Is_Generic_Contract_Pragma);
pragma Inline (Set_Is_Ignored);
pragma Inline (Set_Is_In_Discriminant_Check);
pragma Inline (Set_Is_Inherited);
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Print_Eol;
end if;
+ if Field_Present (Field36 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field36_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field36 (Ent));
+ Print_Eol;
+ end if;
+
+ if Field_Present (Field37 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field37_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field37 (Ent));
+ Print_Eol;
+ end if;
+
+ if Field_Present (Field38 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field38_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field38 (Ent));
+ Print_Eol;
+ end if;
+
+ if Field_Present (Field39 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field39_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field39 (Ent));
+ Print_Eol;
+ end if;
+
+ if Field_Present (Field40 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field40_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field40 (Ent));
+ Print_Eol;
+ end if;
+
+ if Field_Present (Field41 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field41_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field41 (Ent));
+ Print_Eol;
+ end if;
+
Write_Entity_Flags (Ent, Prefix);
end Print_Entity_Info;
projects / gcc.git / commitdiff