+2013-10-14 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb: Add an entry in table Canonical_Aspect for
+ Initializes.
+ * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
+ Aspect_Names and Aspect_Delay for Initializes.
+ * atree.ads, atree.adb (Ekind_In): New seven argument versions of the
+ routines.
+ * einfo.adb: Remove Refined_State_Pragma from the list of node
+ usage. Finalizer is now at position 28.
+ (Contract): Package
+ and package bodies now have a contract.
+ (Finalizer): Update
+ the assertion and node usage.
+ (Get_Pragma): Update the Is_CDG
+ flag to include Abstract_State, Initializes and Refined_State.
+ (Refined_State_Pragma): Removed.
+ (Set_Contract): Package and
+ package bodies now have a contract.
+ (Set_Finalizer): Update the
+ assertion and node usage.
+ (Set_Refined_State_Pragma): Removed.
+ (Write_Field8_Name): Remove the output for Refined_State_Pragma.
+ (Write_Field24_Name): Remove the output for Finalizer. Package
+ and package bodies now have a contract.
+ (Write_Field28_Name):
+ Add output for Finalizer.
+ * einfo.ads: Update the documentation and usage in entities
+ of attribute Contract. Update the node position and usage in
+ entities of attribute Finalizer. Remove the documentation
+ and usage in entities for attribute Refined_State_Pragma.
+ (Refined_State_Pragma): Removed along with pragma Inline.
+ (Set_Refined_State_Pragma): Removed along with pragma Inline.
+ * par-prag.adb: Add Initializes to the pragmas that do not
+ require special processing by the parser.
+ * sem_ch3.adb (Analyze_Declarations): Add local variable
+ Prag. Update the retrieval of pragma Refined_State. Analyze
+ aspect/pragma Initializes at the end of the visible declarations
+ of the related package.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Contract):
+ Add local variables Ref_Depends and Ref_Global. Analyze
+ pragmas Refined_Global and Refined_Depends in that order.
+ (Analyze_Subprogram_Contract): Add local variables Depends and
+ Global. Analyze pragmas Global and Depends in that order.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Package
+ bodies now have a contract. Move the analysis of the aspect
+ specifications after the defining entity has been decorated.
+ (Analyze_Package_Declaration): Packages now have a contract. Move
+ the analysis of the aspect specifications after the defining
+ entity has been decorated.
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration): Packages
+ now have contracts.
+ * sem_ch13.adb (Analyze_Pragma): Code cleanup for aspect
+ Abstract_State. Add processing for aspect Initializes.
+ (Check_Aspect_At_Freeze_Point): Add an entry for Initializes.
+ * sem_prag.adb: Use Get_Pragma_Arg to extract the expression
+ of a pragma argument. Add an entry in table Sig_Flags for
+ Initializes.
+ (Analyze_Initializes_In_Decl_Part): New routine.
+ (Analyze_Pragma): Check the declaration order of pragmas
+ Abstract_State and Initializes. Abstract_State is now part of
+ the package contract. Analyze pragma Initializes. Check for
+ duplicate Refined_State pragma. Refined_State is now part of
+ the package contract.
+ (Check_Declaration_Order): New routine.
+ (Check_Test_Case): Alphabetized.
+ * sem_prag.ads (Analyze_Initializes_In_Decl_Part): New routine.
+ * sem_util.adb (Add_Contract_Item): Rename formal Subp_Id
+ to Id. This routine can now support contracts on packages and
+ package bodies.
+ * sem_util.ads (Add_Contract_Item): Rename formal Subp_Id to
+ Id. Update comment on usage.
+ * sinfo.ads: Update the usage of N_Contract nodes.
+ * snames.ads-tmpl: Add predefined name Initializes. Add new
+ pragma id for Initializes.
+
2013-10-13 Nicolas Roche <roche@adacore.com>
Eric Botcazou <ebotcazou@adacore.com>
Aspect_Independent_Components => Aspect_Independent_Components,
Aspect_Inline => Aspect_Inline,
Aspect_Inline_Always => Aspect_Inline,
+ Aspect_Initializes => Aspect_Initializes,
Aspect_Input => Aspect_Input,
Aspect_Interrupt_Handler => Aspect_Interrupt_Handler,
Aspect_Interrupt_Priority => Aspect_Priority,
Aspect_External_Tag,
Aspect_Global, -- GNAT
Aspect_Implicit_Dereference,
+ Aspect_Initializes, -- GNAT
Aspect_Input,
Aspect_Interrupt_Priority,
Aspect_Invariant, -- GNAT
Aspect_External_Tag => Expression,
Aspect_Global => Expression,
Aspect_Implicit_Dereference => Name,
+ Aspect_Initializes => Expression,
Aspect_Input => Name,
Aspect_Interrupt_Priority => Expression,
Aspect_Invariant => Expression,
Aspect_Independent_Components => Name_Independent_Components,
Aspect_Inline => Name_Inline,
Aspect_Inline_Always => Name_Inline_Always,
+ Aspect_Initializes => Name_Initializes,
Aspect_Input => Name_Input,
Aspect_Interrupt_Handler => Name_Interrupt_Handler,
Aspect_Interrupt_Priority => Name_Interrupt_Priority,
Aspect_Independent_Components => Always_Delay,
Aspect_Inline => Always_Delay,
Aspect_Inline_Always => Always_Delay,
+ Aspect_Initializes => Always_Delay,
Aspect_Input => Always_Delay,
Aspect_Interrupt_Handler => Always_Delay,
Aspect_Interrupt_Priority => Always_Delay,
end Ekind_In;
function Ekind_In
+ (T : Entity_Kind;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind) return Boolean
+ is
+ begin
+ return T = V1 or else
+ T = V2 or else
+ T = V3 or else
+ T = V4 or else
+ T = V5 or else
+ T = V6 or else
+ T = V7;
+ end Ekind_In;
+
+ function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
V2 : Entity_Kind) return Boolean
return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6);
end Ekind_In;
+ function Ekind_In
+ (E : Entity_Id;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind) return Boolean
+ is
+ begin
+ return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7);
+ end Ekind_In;
+
------------------------
-- Set_Reporting_Proc --
------------------------
V6 : Entity_Kind) return Boolean;
function Ekind_In
+ (E : Entity_Id;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind) return Boolean;
+
+ function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
V2 : Entity_Kind) return Boolean;
V5 : Entity_Kind;
V6 : Entity_Kind) return Boolean;
+ function Ekind_In
+ (T : Entity_Kind;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind) return Boolean;
+
pragma Inline (Ekind_In);
-- Inline all above functions
-- Mechanism Uint8 (but returns Mechanism_Type)
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
- -- Refined_State_Pragma Node8
-- Refinement_Constituents Elist8
-- Return_Applies_To Node8
-- First_Exit_Statement Node8
-- Protection_Object Node23
-- Stored_Constraint Elist23
- -- Finalizer Node24
-- Related_Expression Node24
-- Contract Node24
-- Wrapped_Entity Node27
-- Extra_Formals Node28
+ -- Finalizer Node28
-- Initialization_Statements Node28
-- Underlying_Record_View Node28
function Contract (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body)
- or else Is_Subprogram (Id)
- or else Is_Generic_Subprogram (Id));
+ (Ekind_In (Id, E_Entry,
+ E_Entry_Family,
+ E_Generic_Package,
+ E_Package,
+ E_Package_Body,
+ E_Subprogram_Body)
+ or else Is_Generic_Subprogram (Id)
+ or else Is_Subprogram (Id));
return Node24 (Id);
end Contract;
function Finalizer (Id : E) return E is
begin
- pragma Assert
- (Ekind (Id) = E_Package
- or else Ekind (Id) = E_Package_Body);
- return Node24 (Id);
+ pragma Assert (Ekind_In (Id, E_Package, E_Package_Body));
+ return Node28 (Id);
end Finalizer;
function First_Entity (Id : E) return E is
return Node10 (Id);
end Refined_State;
- function Refined_State_Pragma (Id : E) return N is
- begin
- pragma Assert (Ekind (Id) = E_Package_Body);
- return Node8 (Id);
- end Refined_State_Pragma;
-
function Refinement_Constituents (Id : E) return L is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
procedure Set_Contract (Id : E; V : N) is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body, E_Void)
- or else Is_Subprogram (Id)
- or else Is_Generic_Subprogram (Id));
+ (Ekind_In (Id, E_Entry,
+ E_Entry_Family,
+ E_Generic_Package,
+ E_Package,
+ E_Package_Body,
+ E_Subprogram_Body,
+ E_Void)
+ or else Is_Generic_Subprogram (Id)
+ or else Is_Subprogram (Id));
Set_Node24 (Id, V);
end Set_Contract;
procedure Set_Finalizer (Id : E; V : E) is
begin
- pragma Assert
- (Ekind (Id) = E_Package
- or else Ekind (Id) = E_Package_Body);
- Set_Node24 (Id, V);
+ pragma Assert (Ekind_In (Id, E_Package, E_Package_Body));
+ Set_Node28 (Id, V);
end Set_Finalizer;
procedure Set_First_Entity (Id : E; V : E) is
Set_Node10 (Id, V);
end Set_Refined_State;
- procedure Set_Refined_State_Pragma (Id : E; V : N) is
- begin
- pragma Assert (Ekind (Id) = E_Package_Body);
- Set_Node8 (Id, V);
- end Set_Refined_State_Pragma;
-
procedure Set_Refinement_Constituents (Id : E; V : L) is
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
Is_CDG : constant Boolean :=
+ Id = Pragma_Abstract_State or else
Id = Pragma_Depends or else
Id = Pragma_Global or else
+ Id = Pragma_Initializes or else
Id = Pragma_Refined_Depends or else
- Id = Pragma_Refined_Global;
+ Id = Pragma_Refined_Global or else
+ Id = Pragma_Refined_State;
Is_CTC : constant Boolean :=
Id = Pragma_Contract_Cases or else
Id = Pragma_Test_Case;
Is_PPC : constant Boolean :=
- Id = Pragma_Precondition or else
+ Id = Pragma_Precondition or else
Id = Pragma_Postcondition;
In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
when E_Procedure =>
Write_Str ("Postcondition_Proc");
- when E_Package_Body =>
- Write_Str ("Refined_State_Pragma");
-
when E_Abstract_State =>
Write_Str ("Refinement_Constituents");
procedure Write_Field24_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
- when E_Package |
- E_Package_Body =>
- Write_Str ("Finalizer");
-
when E_Constant |
E_Variable |
Type_Kind =>
when E_Entry |
E_Entry_Family |
+ E_Generic_Package |
+ E_Package |
+ E_Package_Body |
E_Subprogram_Body |
- Subprogram_Kind |
- Generic_Subprogram_Kind =>
+ Generic_Subprogram_Kind |
+ Subprogram_Kind =>
Write_Str ("Contract");
when others =>
E_Subprogram_Type =>
Write_Str ("Extra_Formals");
- when E_Constant | E_Variable =>
+ when E_Package |
+ E_Package_Body =>
+ Write_Str ("Finalizer");
+
+ when E_Constant |
+ E_Variable =>
Write_Str ("Initialization_Statements");
when E_Record_Type =>
-- 'COUNT when it applies to a family member.
-- Contract (Node24)
--- Defined in entry and entry family entities, subprogram body entities,
--- subprograms, and generic subprograms. Points to the contract of the
--- entity, holding both preconditions, postconditions, and test cases.
+-- Defined in entry, entry family, package, package body, subprogram and
+-- subprogram body entities as well as their respective generic forms.
+-- 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
-- the Finalize_Storage_Only pragma is required at each level of
-- derivation.
--- Finalizer (Node24)
+-- Finalizer (Node28)
-- Applies to package declarations and bodies. Contains the entity of the
-- library-level program which finalizes all package-level controlled
-- objects.
-- Defined in abstract states and variables. Contains the entity of an
-- ancestor state whose refinement mentions this item.
--- Refined_State_Pragma (Node8)
--- Defined in [generic] package bodies. Contains the pragma that refines
--- all abstract states defined in the corresponding package declaration.
-
-- Refinement_Constituents (Elist8)
-- Present in abstract state entities. Contains all the constituents that
-- refine the state, in other words, all the hidden states that appear in
-- Generic_Renamings (Elist23) (for an instance)
-- Inner_Instances (Elist23) (generic case only)
-- Limited_View (Node23) (non-generic/instance)
- -- Finalizer (Node24) (non-generic case only)
+ -- Contract (Node24)
-- Abstract_States (Elist25)
-- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
+ -- Finalizer (Node28) (non-generic case only)
-- SPARK_Mode_Pragmas (Node32)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Scope_Depth (synth)
-- E_Package_Body
- -- Refined_State_Pragma (Node8)
-- Handler_Records (List10) (non-generic case only)
-- Related_Instance (Node15) (non-generic case only)
-- First_Entity (Node17)
-- Spec_Entity (Node19)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
- -- Finalizer (Node24) (non-generic case only)
+ -- Contract (Node24)
+ -- Finalizer (Node28) (non-generic case only)
-- SPARK_Mode_Pragmas (Node32)
-- Delay_Subprogram_Descriptors (Flag50)
-- Has_Anonymous_Master (Flag253)
function Referenced_As_LHS (Id : E) return B;
function Referenced_As_Out_Parameter (Id : E) return B;
function Refined_State (Id : E) return E;
- function Refined_State_Pragma (Id : E) return E;
function Refinement_Constituents (Id : E) return L;
function Register_Exception_Call (Id : E) return N;
function Related_Array_Object (Id : E) return E;
procedure Set_Referenced_As_LHS (Id : E; V : B := True);
procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True);
procedure Set_Refined_State (Id : E; V : E);
- procedure Set_Refined_State_Pragma (Id : E; V : N);
procedure Set_Refinement_Constituents (Id : E; V : L);
procedure Set_Register_Exception_Call (Id : E; V : N);
procedure Set_Related_Array_Object (Id : E; V : E);
pragma Inline (Referenced_As_LHS);
pragma Inline (Referenced_As_Out_Parameter);
pragma Inline (Refined_State);
- pragma Inline (Refined_State_Pragma);
pragma Inline (Refinement_Constituents);
pragma Inline (Register_Exception_Call);
pragma Inline (Related_Array_Object);
pragma Inline (Set_Referenced_As_LHS);
pragma Inline (Set_Referenced_As_Out_Parameter);
pragma Inline (Set_Refined_State);
- pragma Inline (Set_Refined_State_Pragma);
pragma Inline (Set_Refinement_Constituents);
pragma Inline (Set_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);
Pragma_Independent |
Pragma_Independent_Components |
Pragma_Initialize_Scalars |
+ Pragma_Initializes |
Pragma_Inline |
Pragma_Inline_Always |
Pragma_Inline_Generic |
Id := Defining_Entity (N);
Generate_Definition (Id);
+ -- Expansion is not applied to generic units
+
+ Start_Generic;
+
+ Enter_Name (Id);
+ Set_Ekind (Id, E_Generic_Package);
+ Set_Etype (Id, Standard_Void_Type);
+ Set_Contract (Id, Make_Contract (Sloc (Id)));
+
-- Analyze aspects now, so that generated pragmas appear in the
-- declarations before building and analyzing the generic copy.
Analyze_Aspect_Specifications (N, Id);
end if;
- -- Expansion is not applied to generic units
-
- Start_Generic;
-
- Enter_Name (Id);
- Set_Ekind (Id, E_Generic_Package);
- Set_Etype (Id, Standard_Void_Type);
Push_Scope (Id);
Enter_Generic_Scope (Id);
Set_Inner_Instances (Id, New_Elmt_List);
Aspects : constant List_Id := Aspect_Specifications (N);
begin
Set_Has_Aspects (N, False);
- Move_Aspects (New_N, N);
+ Move_Aspects (New_N, To => N);
Set_Has_Aspects (Original_Node (N), False);
Set_Aspect_Specifications (Original_Node (N), Aspects);
end;
-- pre/postconditions on the instance are analyzed below, in a
-- separate step.
- Move_Aspects (Act_Tree, Act_Decl);
+ Move_Aspects (Act_Tree, To => Act_Decl);
Set_Categorization_From_Pragmas (Act_Decl);
if Parent_Installed then
-- Abstract_State
+ -- Aspect Abstract_State introduces implicit declarations for
+ -- all state abstraction entities it defines. To emulate this
+ -- behavior, insert the pragma at the beginning of the visible
+ -- declarations of the related package so that it is analyzed
+ -- immediately.
+
when Aspect_Abstract_State => Abstract_State : declare
Decls : List_Id;
- Spec : Node_Id;
begin
- -- Aspect Abstract_State introduces implicit declarations
- -- for all state abstraction entities it defines. To emulate
- -- this behavior, insert the pragma at the beginning of the
- -- visible declarations of the related package so that it is
- -- analyzed immediately.
-
if Nkind_In (N, N_Generic_Package_Declaration,
N_Package_Declaration)
then
- Spec := Specification (N);
- Decls := Visible_Declarations (Spec);
+ Decls := Visible_Declarations (Specification (N));
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Insert_Delayed_Pragma (Aitem);
goto Continue;
+ -- Initializes
+
+ -- Aspect Initializes coverts the visible declarations of a
+ -- package. As such, it must be evaluated at the end of the
+ -- said declarations.
+
+ when Aspect_Initializes => Initializes : declare
+ Decls : List_Id;
+
+ begin
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Decls := Visible_Declarations (Specification (N));
+
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Initializes);
+ Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (N, Decls);
+ end if;
+
+ Prepend_To (Decls, Aitem);
+
+ else
+ Error_Msg_NE
+ ("aspect & must apply to a package declaration",
+ Aspect, Id);
+ end if;
+
+ goto Continue;
+ end Initializes;
+
-- SPARK_Mode
when Aspect_SPARK_Mode =>
Aspect_Dimension |
Aspect_Dimension_System |
Aspect_Implicit_Dereference |
+ Aspect_Initializes |
Aspect_Post |
Aspect_Postcondition |
Aspect_Pre |
Context : Node_Id;
Freeze_From : Entity_Id := Empty;
Next_Decl : Node_Id;
+ Prag : Node_Id;
Spec_Id : Entity_Id;
-- Start of processing for Analyze_Declarations
Decl := Next_Decl;
end loop;
- -- Analyze the state refinements within a package body now, after all
- -- hidden states have been encountered and freely visible. Refinements
- -- must be processed before pragmas Refined_Depends and Refined_Global
- -- because the last two may mention constituents.
-
if Present (L) then
Context := Parent (L);
- if Nkind (Context) = N_Package_Body then
+ -- Analyze aspect/pragma Initializes of a package at the end of the
+ -- visible declarations as the aspect/pragma has visibility over the
+ -- said region.
+
+ if Nkind (Context) = N_Package_Specification
+ and then L = Visible_Declarations (Context)
+ then
+ Spec_Id := Defining_Entity (Parent (Context));
+ Prag := Get_Pragma (Spec_Id, Pragma_Initializes);
+
+ if Present (Prag) then
+ Analyze_Initializes_In_Decl_Part (Prag);
+ end if;
+
+ -- Analyze the state refinements within a package body now, after
+ -- all hidden states have been encountered and freely visible.
+ -- Refinements must be processed before pragmas Refined_Depends and
+ -- Refined_Global because the last two may mention constituents.
+
+ elsif Nkind (Context) = N_Package_Body then
Body_Id := Defining_Entity (Context);
Spec_Id := Corresponding_Spec (Context);
+ Prag := 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 (Refined_State_Pragma (Body_Id)) then
- Analyze_Refined_State_In_Decl_Part
- (Refined_State_Pragma (Body_Id));
+ if Present (Prag) then
+ Analyze_Refined_State_In_Decl_Part (Prag);
-- State refinement is required when the package declaration has
-- abstract states. Null states are not considered.
--------------------------------------
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
- Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
- Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
- Prag : Node_Id;
-
- Has_Refined_Global : Boolean := False;
+ Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
+ Prag : Node_Id;
+ Ref_Depends : Node_Id := Empty;
+ Ref_Global : Node_Id := Empty;
begin
-- When a subprogram body declaration is erroneous, its defining entity
return;
end if;
+ -- Locate and store pragmas Refined_Depends and Refined_Global since
+ -- their order of analysis matters.
+
Prag := Classifications (Contract (Body_Id));
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Refined_Depends then
- Analyze_Refined_Depends_In_Decl_Part (Prag);
+ Ref_Depends := Prag;
elsif Pragma_Name (Prag) = Name_Refined_Global then
- Has_Refined_Global := True;
- Analyze_Refined_Global_In_Decl_Part (Prag);
+ 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_Global) then
+ Analyze_Refined_Global_In_Decl_Part (Ref_Global);
+
-- When the corresponding Global aspect/pragma references a state with
-- visible refinement, the body requires Refined_Global.
- if not Has_Refined_Global and then Present (Spec_Id) then
+ elsif Present (Spec_Id) then
Prag := Get_Pragma (Spec_Id, Pragma_Global);
if Present (Prag) and then Contains_Refined_State (Prag) then
Body_Decl, Spec_Id);
end if;
end if;
+
+ -- Refined_Depends must be analyzed after Refined_Global in order to see
+ -- the modes of all global refinements.
+
+ if Present (Ref_Depends) then
+ Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
+ end if;
end Analyze_Subprogram_Body_Contract;
------------------------------------
-- Local variables
Items : constant Node_Id := Contract (Subp);
- Error_CCase : Node_Id;
- Error_Post : Node_Id;
+ Depends : Node_Id := Empty;
+ Error_CCase : Node_Id := Empty;
+ Error_Post : Node_Id := Empty;
+ Global : Node_Id := Empty;
Nam : Name_Id;
Prag : Node_Id;
-- Start of processing for Analyze_Subprogram_Contract
begin
- Error_CCase := Empty;
- Error_Post := Empty;
-
if Present (Items) then
-- Analyze pre- and postconditions
Nam := Pragma_Name (Prag);
if Nam = Name_Depends then
- Analyze_Depends_In_Decl_Part (Prag);
- else
- pragma Assert (Nam = Name_Global);
- Analyze_Global_In_Decl_Part (Prag);
+ Depends := Prag;
+ else pragma Assert (Nam = Name_Global);
+ Global := Prag;
end if;
Prag := Next_Pragma (Prag);
end loop;
+
+ -- Analyze Global first as Depends may mention items classified in
+ -- the global categorization.
+
+ if Present (Global) then
+ Analyze_Global_In_Decl_Part (Global);
+ end if;
+
+ -- Depends must be analyzed after Global in order to see the modes of
+ -- all global items.
+
+ if Present (Depends) then
+ Analyze_Depends_In_Decl_Part (Depends);
+ end if;
end if;
-- Emit an error when none of the postconditions or contract-cases
Body_Id := Defining_Entity (N);
- if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Body_Id);
- end if;
+ -- Body is body of package instantiation. Corresponding spec has already
+ -- been set.
if Present (Corresponding_Spec (N)) then
-
- -- Body is body of package instantiation. Corresponding spec has
- -- already been set.
-
Spec_Id := Corresponding_Spec (N);
Pack_Decl := Unit_Declaration_Node (Spec_Id);
Set_Ekind (Body_Id, E_Package_Body);
Set_Body_Entity (Spec_Id, Body_Id);
Set_Spec_Entity (Body_Id, Spec_Id);
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
-- Defining name for the package body is not a visible entity: Only the
-- defining name for the declaration is visible.
Set_Has_Completion (Spec_Id);
Last_Spec_Entity := Last_Entity (Spec_Id);
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Body_Id);
+ end if;
+
Push_Scope (Spec_Id);
Set_Categorization_From_Pragmas (N);
-- True when this package declaration is not a nested declaration
begin
+ if Debug_Flag_C then
+ Write_Str ("==> package spec ");
+ Write_Name (Chars (Id));
+ Write_Str (" from ");
+ Write_Location (Sloc (N));
+ Write_Eol;
+ Indent;
+ end if;
+
+ Generate_Definition (Id);
+ Enter_Name (Id);
+ Set_Ekind (Id, E_Package);
+ Set_Etype (Id, Standard_Void_Type);
+ Set_Contract (Id, Make_Contract (Sloc (Id)));
+
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
return;
end if;
- if Debug_Flag_C then
- Write_Str ("==> package spec ");
- Write_Name (Chars (Id));
- Write_Str (" from ");
- Write_Location (Sloc (N));
- Write_Eol;
- Indent;
- end if;
-
- Generate_Definition (Id);
- Enter_Name (Id);
- Set_Ekind (Id, E_Package);
- Set_Etype (Id, Standard_Void_Type);
-
Push_Scope (Id);
PF := Is_Pure (Enclosing_Lib_Unit_Entity);
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- All_Cases := Expression (First (Pragma_Argument_Associations (N)));
+ All_Cases := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
-- Multiple contract cases appear in aggregate form
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- Clause := Expression (First (Pragma_Argument_Associations (N)));
+ Clause := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
-- Empty dependency list
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- List := Expression (First (Pragma_Argument_Associations (N)));
+ List := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
-- There is nothing to be done for a null global list
end if;
end Analyze_Global_In_Decl_Part;
+ --------------------------------------
+ -- Analyze_Initializes_In_Decl_Part --
+ --------------------------------------
+
+ procedure Analyze_Initializes_In_Decl_Part (N : Node_Id) is
+ Pack_Spec : constant Node_Id := Parent (N);
+ Pack_Id : constant Entity_Id := Defining_Entity (Parent (Pack_Spec));
+
+ Items_Seen : Elist_Id := No_Elist;
+ -- A list of all initialization items processed so far. This list is
+ -- used to detect duplicate items.
+
+ Non_Null_Seen : Boolean := False;
+ Null_Seen : Boolean := False;
+ -- Flags used to check the legality of a null initialization list
+
+ States_And_Vars : Elist_Id := No_Elist;
+ -- A list of all abstract states and variables declared in the visible
+ -- declarations of the related package. This list is used to detect the
+ -- legality of initialization items.
+
+ procedure Analyze_Initialization_Item (Item : Node_Id);
+ -- Verify the legality of a single initialization item
+
+ procedure Analyze_Initialization_Item_With_Inputs (Item : Node_Id);
+ -- Verify the legality of a single initialization item followed by a
+ -- list of input items.
+
+ procedure Collect_States_And_Variables;
+ -- Inspect the visible declarations of the related package and gather
+ -- the entities of all abstract states and variables in States_And_Vars.
+
+ ---------------------------------
+ -- Analyze_Initialization_Item --
+ ---------------------------------
+
+ procedure Analyze_Initialization_Item (Item : Node_Id) is
+ Item_Id : Entity_Id;
+
+ begin
+ -- A package with null initialization list is not allowed to have
+ -- additional initializations.
+
+ if Null_Seen then
+ Error_Msg_NE ("package & has null initialization", Item, Pack_Id);
+
+ -- Null initialization list
+
+ elsif Nkind (Item) = N_Null then
+
+ -- Catch a case where a null initialization item appears in a list
+ -- of non-null items.
+
+ if Non_Null_Seen then
+ Error_Msg_NE
+ ("package & has non-null initialization", Item, Pack_Id);
+ else
+ Null_Seen := True;
+ end if;
+
+ -- Initialization item
+
+ else
+ Non_Null_Seen := True;
+
+ Analyze (Item);
+
+ if Is_Entity_Name (Item) then
+ Item_Id := Entity (Item);
+
+ if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+
+ -- The state or variable must be declared in the visible
+ -- declarations of the package.
+
+ if not Contains (States_And_Vars, Item_Id) then
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ Error_Msg_NE
+ ("initialization item & must appear in the visible "
+ & "declarations of package %", Item, Item_Id);
+
+ -- Detect a duplicate use of the same initialization item
+
+ elsif Contains (Items_Seen, Item_Id) then
+ Error_Msg_N ("duplicate initialization item", Item);
+
+ -- The item is legal, add it to the list of processed states
+ -- and variables.
+
+ else
+ Add_Item (Item_Id, Items_Seen);
+ end if;
+
+ -- The item references something that is not a state or a
+ -- variable.
+
+ else
+ Error_Msg_N
+ ("initialization item must denote variable or state",
+ Item);
+ end if;
+
+ -- Some form of illegal construct masquerading as a name
+
+ else
+ Error_Msg_N
+ ("initialization item must denote variable or state", Item);
+ end if;
+ end if;
+ end Analyze_Initialization_Item;
+
+ ---------------------------------------------
+ -- Analyze_Initialization_Item_With_Inputs --
+ ---------------------------------------------
+
+ procedure Analyze_Initialization_Item_With_Inputs (Item : Node_Id) is
+ Inputs_Seen : Elist_Id := No_Elist;
+ -- A list of all inputs processed so far. This list is used to detect
+ -- duplicate uses of an input.
+
+ Non_Null_Seen : Boolean := False;
+ Null_Seen : Boolean := False;
+ -- Flags used to check the legality of an input list
+
+ procedure Analyze_Input_Item (Input : Node_Id);
+ -- Verify the legality of a single input item
+
+ ------------------------
+ -- Analyze_Input_Item --
+ ------------------------
+
+ procedure Analyze_Input_Item (Input : Node_Id) is
+ Input_Id : Entity_Id;
+
+ begin
+ -- An initialization item with null inputs is not allowed to have
+ -- assitional inputs.
+
+ if Null_Seen then
+ Error_Msg_N ("item has null input list", Item);
+
+ -- Null input list
+
+ elsif Nkind (Input) = N_Null then
+
+ -- Catch a case where a null input appears in a list of non-
+ -- null inpits.
+
+ if Non_Null_Seen then
+ Error_Msg_N ("item has non-null input list", Item);
+ else
+ Null_Seen := True;
+ end if;
+
+ -- Input item
+
+ else
+ Non_Null_Seen := True;
+
+ Analyze (Input);
+
+ if Is_Entity_Name (Input) then
+ Input_Id := Entity (Input);
+
+ if Ekind_In (Input_Id, E_Abstract_State, E_Variable) then
+
+ -- The input cannot denote states or variables declared
+ -- within the visible declarations of the package.
+
+ if Contains (States_And_Vars, Input_Id) then
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ Error_Msg_NE
+ ("input item & cannot denote a visible variable or "
+ & "state of package %", Input, Input_Id);
+
+ -- Detect a duplicate use of the same input item
+
+ elsif Contains (Inputs_Seen, Input_Id) then
+ Error_Msg_N ("duplicate input item", Input);
+
+ -- The input is legal, add it to the list of processed
+ -- inputs.
+
+ else
+ Add_Item (Input_Id, Inputs_Seen);
+ end if;
+
+ -- The input references something that is not a state or a
+ -- variable.
+
+ else
+ Error_Msg_N
+ ("input item must denote variable or state", Input);
+ end if;
+
+ -- Some form of illegal construct masquerading as a name
+
+ else
+ Error_Msg_N
+ ("input item must denote variable or state", Input);
+ end if;
+ end if;
+ end Analyze_Input_Item;
+
+ -- Local variables
+
+ Inputs : constant Node_Id := Expression (Item);
+ Elmt : Node_Id;
+ Input : Node_Id;
+
+ Name_Seen : Boolean := False;
+ -- A flag used to detect multiple item names
+
+ -- Start of processing for Analyze_Initialization_Item_With_Inputs
+
+ begin
+ -- Inspect the name of an item with inputs
+
+ Elmt := First (Choices (Item));
+ while Present (Elmt) loop
+ if Name_Seen then
+ Error_Msg_N ("only one item allowed in initialization", Elmt);
+
+ else
+ Name_Seen := True;
+ Analyze_Initialization_Item (Elmt);
+ end if;
+
+ Next (Elmt);
+ end loop;
+
+ -- Multiple input items appear as an aggregate
+
+ if Nkind (Inputs) = N_Aggregate then
+ if Present (Expressions (Inputs)) then
+ Input := First (Expressions (Inputs));
+ while Present (Input) loop
+ Analyze_Input_Item (Input);
+
+ Next (Input);
+ end loop;
+ end if;
+
+ if Present (Component_Associations (Inputs)) then
+ Error_Msg_N
+ ("inputs must appear in named association form", Inputs);
+ end if;
+
+ -- Single input item
+
+ else
+ Analyze_Input_Item (Inputs);
+ end if;
+ end Analyze_Initialization_Item_With_Inputs;
+
+ ----------------------------------
+ -- Collect_States_And_Variables --
+ ----------------------------------
+
+ procedure Collect_States_And_Variables is
+ Decl : Node_Id;
+
+ begin
+ -- Collect the abstract states defined in the package (if any)
+
+ if Present (Abstract_States (Pack_Id)) then
+ States_And_Vars := New_Copy_Elist (Abstract_States (Pack_Id));
+ end if;
+
+ -- Collect all variables the appear in the visible declarations of
+ -- the related package.
+
+ if Present (Visible_Declarations (Pack_Spec)) then
+ Decl := First (Visible_Declarations (Pack_Spec));
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Object_Declaration
+ and then Ekind (Defining_Entity (Decl)) = E_Variable
+ and then Comes_From_Source (Decl)
+ then
+ Add_Item (Defining_Entity (Decl), States_And_Vars);
+ end if;
+
+ Next (Decl);
+ end loop;
+ end if;
+ end Collect_States_And_Variables;
+
+ -- Local variables
+
+ Inits : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Init : Node_Id;
+
+ -- Start of processing for Analyze_Initializes_In_Decl_Part
+
+ begin
+ Set_Analyzed (N);
+
+ -- Initialize the various lists used during analysis
+
+ Collect_States_And_Variables;
+
+ -- Multiple initialization clauses appear as an aggregate
+
+ if Nkind (Inits) = N_Aggregate then
+ if Present (Expressions (Inits)) then
+ Init := First (Expressions (Inits));
+ while Present (Init) loop
+ Analyze_Initialization_Item (Init);
+
+ Next (Init);
+ end loop;
+ end if;
+
+ if Present (Component_Associations (Inits)) then
+ Init := First (Component_Associations (Inits));
+ while Present (Init) loop
+ Analyze_Initialization_Item_With_Inputs (Init);
+
+ Next (Init);
+ end loop;
+ end if;
+
+ -- Various forms of a single initialization clause. Note that these may
+ -- include malformed initializations.
+
+ else
+ Analyze_Initialization_Item (Inits);
+ end if;
+ end Analyze_Initializes_In_Decl_Part;
+
--------------------
-- Analyze_Pragma --
--------------------
-- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part
-- should be set when Comp comes from a record variant.
- procedure Check_Test_Case;
- -- Called to process a test-case pragma. It starts with checking pragma
- -- arguments, and the rest of the treatment is similar to the one for
- -- pre- and postcondition in Check_Precondition_Postcondition, except
- -- the placement rules for the test-case pragma are stricter. These
- -- pragmas may only occur after a subprogram spec declared directly
- -- in a package spec unit. In this case, the pragma is chained to the
- -- subprogram in question (using Contract_Test_Cases and Next_Pragma)
- -- and analysis of the pragma is delayed till the end of the spec. In
- -- all other cases, an error message for bad placement is given.
+ procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id);
+ -- Subsidiary routine to the analysis of pragmas Abstract_State and
+ -- Initializes. Determine whether aspect/pragma Abstract_State denoted
+ -- by States is defined earlier than aspect/pragma Initializes denoted
+ -- by Inits.
procedure Check_Duplicate_Pragma (E : Entity_Id);
-- Check if a rep item of the same name as the current pragma is already
-- that the constraint is static as required by the restrictions for
-- Unchecked_Union.
+ procedure Check_Test_Case;
+ -- Called to process a test-case pragma. It starts with checking pragma
+ -- arguments, and the rest of the treatment is similar to the one for
+ -- pre- and postcondition in Check_Precondition_Postcondition, except
+ -- the placement rules for the test-case pragma are stricter. These
+ -- pragmas may only occur after a subprogram spec declared directly
+ -- in a package spec unit. In this case, the pragma is chained to the
+ -- subprogram in question (using Contract_Test_Cases and Next_Pragma)
+ -- and analysis of the pragma is delayed till the end of the spec. In
+ -- all other cases, an error message for bad placement is given.
+
procedure Check_Valid_Configuration_Pragma;
-- Legality checks for placement of a configuration pragma
end if;
end Check_Component;
+ -----------------------------
+ -- Check_Declaration_Order --
+ -----------------------------
+
+ procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id) is
+ procedure Check_Aspect_Specification_Order;
+ -- Inspect the aspect specifications of the context to determine the
+ -- proper order.
+
+ --------------------------------------
+ -- Check_Aspect_Specification_Order --
+ --------------------------------------
+
+ procedure Check_Aspect_Specification_Order is
+ Asp_I : constant Node_Id := Corresponding_Aspect (Inits);
+ Asp_S : constant Node_Id := Corresponding_Aspect (States);
+ Asp : Node_Id;
+
+ States_Seen : Boolean := False;
+
+ begin
+ -- Both aspects must be part of the same aspect specification list
+
+ pragma Assert (List_Containing (Asp_I) = List_Containing (Asp_S));
+
+ Asp := First (List_Containing (Asp_I));
+ while Present (Asp) loop
+ if Get_Aspect_Id (Asp) = Aspect_Abstract_State then
+ States_Seen := True;
+
+ elsif Get_Aspect_Id (Asp) = Aspect_Initializes then
+ if not States_Seen then
+ Error_Msg_N
+ ("aspect % must come before aspect %", States);
+ end if;
+
+ exit;
+ end if;
+
+ Next (Asp);
+ end loop;
+ end Check_Aspect_Specification_Order;
+
+ -- Local variables
+
+ Stmt : Node_Id;
+
+ -- Start of processing for Check_Declaration_Order
+
+ begin
+ -- Cannot check the order if one of the pragmas is missing
+
+ if No (States) or else No (Inits) then
+ return;
+ end if;
+
+ -- Set up the error names in case the order is incorrect
+
+ Error_Msg_Name_1 := Name_Abstract_State;
+ Error_Msg_Name_2 := Name_Initializes;
+
+ if From_Aspect_Specification (States) then
+
+ -- Both pragmas are actually aspects, check their declaration
+ -- order in the associated aspect specification list. Otherwise
+ -- States is an aspect and Inits a source pragma.
+
+ if From_Aspect_Specification (Inits) then
+ Check_Aspect_Specification_Order;
+ end if;
+
+ -- Abstract_States is a source pragma
+
+ else
+ if From_Aspect_Specification (Inits) then
+ Error_Msg_N ("pragma % cannot come after aspect %", States);
+
+ -- Both pragmas are source constructs. Try to reach States from
+ -- Inits by traversing the declarations backwards.
+
+ else
+ Stmt := Prev (Inits);
+ while Present (Stmt) loop
+
+ -- The order is ok, Abstract_States is first followed by
+ -- Initializes.
+
+ if Nkind (Stmt) = N_Pragma
+ and then Pragma_Name (Stmt) = Name_Abstract_State
+ then
+ return;
+ end if;
+
+ Prev (Stmt);
+ end loop;
+
+ -- If we get here, then the pragmas are out of order
+
+ Error_Msg_N ("pragma % cannot come after pragma %", States);
+ end if;
+ end if;
+ end Check_Declaration_Order;
+
----------------------------
-- Check_Duplicate_Pragma --
----------------------------
end if;
Pack_Id := Defining_Entity (Context);
- State := Expression (Arg1);
+ Add_Contract_Item (N, Pack_Id);
+
+ -- Verify the declaration order of aspects/pragmas Abstract_State
+ -- and Initializes.
+
+ Check_Declaration_Order
+ (States => N,
+ Inits => Get_Pragma (Pack_Id, Pragma_Initializes));
+
+ State := Expression (Arg1);
-- Multiple abstract states appear as an aggregate
Initialize_Scalars := True;
end if;
+ -----------------
+ -- Initializes --
+ -----------------
+
+ -- pragma Initializes (INITIALIZATION_SPEC);
+
+ -- INITIALIZATION_SPEC ::= null | INITIALIZATION_LIST
+
+ -- INITIALIZATION_LIST ::=
+ -- INITIALIZATION_ITEM
+ -- | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM})
+
+ -- INITIALIZATION_ITEM ::= name [=> INPUT_LIST]
+
+ -- INPUT_LIST ::=
+ -- null
+ -- | INPUT
+ -- | (INPUT {, INPUT})
+
+ -- INPUT ::= name
+
+ when Pragma_Initializes => Initializes : declare
+ Context : constant Node_Id := Parent (Parent (N));
+ Pack_Id : Entity_Id;
+ Stmt : Node_Id;
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Initializes must be
+ -- associated with a package declaration.
+
+ if not Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Stmt := Prev (N);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Pragma_Name (Stmt) = Pname then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Stmt);
+ Error_Msg_N ("pragma % duplicates pragma declared #", N);
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Stmt := Prev (Stmt);
+ end loop;
+
+ -- 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 (Context);
+ Add_Contract_Item (N, Pack_Id);
+
+ -- Verify the declaration order of aspects/pragmas Abstract_State
+ -- and Initializes.
+
+ Check_Declaration_Order
+ (States => Get_Pragma (Pack_Id, Pragma_Abstract_State),
+ Inits => N);
+ end Initializes;
+
------------
-- Inline --
------------
when Pragma_Refined_State => Refined_State : declare
Context : constant Node_Id := Parent (N);
Spec_Id : Entity_Id;
+ Stmt : Node_Id;
begin
GNAT_Pragma;
return;
end if;
+ Stmt := Prev (N);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Pragma_Name (Stmt) = Pname then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Stmt);
+ Error_Msg_N ("pragma % duplicates pragma declared #", N);
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Stmt := Prev (Stmt);
+ end loop;
+
-- State refinement is allowed only when the corresponding package
-- declaration has a non-null aspect/pragma Abstract_State.
-- 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_Depends_In_Decl_Part).
+ -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part) by
+ -- adding it to the contract of the package body.
- Set_Refined_State_Pragma (Defining_Entity (Context), N);
+ Add_Contract_Item (N, Defining_Entity (Context));
end Refined_State;
-----------------------
procedure Analyze_Refinement_Clause (Clause : Node_Id);
-- Perform full analysis of a single refinement clause
- function Collect_Hidden_States return Elist_Id;
+ procedure Collect_Hidden_States;
-- Gather the entities of all hidden states that appear in the spec and
- -- body of the related package.
+ -- body of the related package in Hidden_States.
procedure Report_Unrefined_States;
-- Emit errors for all abstract states that have not been refined by
-- Collect_Hidden_States --
---------------------------
- function Collect_Hidden_States return Elist_Id is
- Result : Elist_Id := No_Elist;
-
+ procedure Collect_Hidden_States is
procedure Collect_Hidden_States_In_Decls (Decls : List_Id);
-- Find all hidden states that appear in declarative list Decls and
-- append their entities to Result.
begin
State_Elmt := First_Elmt (States);
while Present (State_Elmt) loop
- Add_Item (Node (State_Elmt), Result);
+ Add_Item (Node (State_Elmt), Hidden_States);
Next_Elmt (State_Elmt);
end loop;
and then Ekind (Defining_Entity (Decl)) = E_Variable
and then Comes_From_Source (Decl)
then
- Add_Item (Defining_Entity (Decl), Result);
+ Add_Item (Defining_Entity (Decl), Hidden_States);
-- Gather the abstract states of a package along with all
-- hidden states in its visible declarations.
Collect_Hidden_States_In_Decls (Private_Declarations (Pack_Spec));
Collect_Hidden_States_In_Decls (Declarations (Pack_Body));
-
- return Result;
end Collect_Hidden_States;
-----------------------------
-- Local declarations
Clauses : constant Node_Id :=
- Expression (First (Pragma_Argument_Associations (N)));
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
Clause : Node_Id;
-- Start of processing for Analyze_Refined_State_In_Decl_Part
-- Initialize the various lists used during analysis
- Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id));
- Hidden_States := Collect_Hidden_States;
+ Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id));
+ Collect_Hidden_States;
-- Multiple state refinements appear as an aggregate
Pragma_Independent => 0,
Pragma_Independent_Components => 0,
Pragma_Initialize_Scalars => -1,
+ Pragma_Initializes => -1,
Pragma_Inline => 0,
Pragma_Inline_Always => 0,
Pragma_Inline_Generic => 0,
procedure Analyze_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Global
+ procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Initializes
+
procedure Analyze_Pre_Post_Condition_In_Decl_Part
(Prag : Node_Id;
Subp_Id : Entity_Id);
-- Add_Contract_Item --
-----------------------
- procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Subp_Id);
+ procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Id);
Nam : Name_Id;
N : Node_Id;
begin
- -- The related subprogram [body] must have a contract and the item to be
- -- added must be a pragma.
+ -- The related context must have a contract and the item to be added
+ -- must be a pragma.
pragma Assert (Present (Items));
pragma Assert (Nkind (Prag) = N_Pragma);
Nam := Original_Aspect_Name (Prag);
- -- Contract items related to subprogram bodies
+ -- Contract items related to [generic] packages. The applicable pragmas
+ -- are:
+ -- Abstract_States
+ -- Initializes
- if Ekind (Subp_Id) = E_Subprogram_Body then
- if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
+ if Ekind_In (Id, E_Generic_Package, E_Package) then
+ if Nam_In (Nam, Name_Abstract_State, Name_Initializes) then
Set_Next_Pragma (Prag, Classifications (Items));
Set_Classifications (Items, Prag);
raise Program_Error;
end if;
- -- Contract items related to subprogram declarations
+ -- Contract items related to package bodies. The applicable pragmas are:
+ -- Refined_States
- else
+ elsif Ekind (Id) = E_Package_Body then
+ if Nam = Name_Refined_State then
+ Set_Next_Pragma (Prag, Classifications (Items));
+ Set_Classifications (Items, Prag);
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to subprogram or entry declarations. The
+ -- applicable pragmas are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Post
+ -- Postcondition
+ -- Pre
+ -- Precondition
+ -- Test_Case
+
+ elsif Ekind_In (Id, E_Entry, E_Entry_Family)
+ or else Is_Generic_Subprogram (Id)
+ or else Is_Subprogram (Id)
+ then
if Nam_In (Nam, Name_Precondition,
Name_Postcondition,
Name_Pre,
then
-- Before we add a precondition or postcondition to the list,
-- make sure we do not have a disallowed duplicate, which can
- -- happen if we use a pragma for Pre{_Class] or Post[_Class]
+ -- happen if we use a pragma for Pre[_Class] or Post[_Class]
-- instead of the corresponding aspect.
if not From_Aspect_Specification (Prag)
then
Error_Msg_Sloc := Sloc (N);
Error_Msg_NE
- ("duplication of aspect for & given#", Prag, Subp_Id);
+ ("duplication of aspect for & given#", Prag, Id);
return;
else
N := Next_Pragma (N);
else
raise Program_Error;
end if;
+
+ -- Contract items related to subprogram bodies. The applicable pragmas
+ -- are:
+ -- Refined_Depends
+ -- Refined_Global
+
+ elsif Ekind (Id) = E_Subprogram_Body then
+ if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
+ Set_Next_Pragma (Prag, Classifications (Items));
+ Set_Classifications (Items, Prag);
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
end if;
end Add_Contract_Item;
-- Add A to the list of access types to process when expanding the
-- freeze node of E.
- procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id);
- -- Add one of the following contract item to the contract of a subprogram.
- -- Prag denotes a pragma and Subp_Id is the related subprogram [body].
+ procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
+ -- Add pragma Prag to the contract of an entry, a package [body] or a
+ -- subprogram [body] denoted by Id. The following are valid pragmas:
+ -- Abstract_States
-- Contract_Cases
-- Depends
-- Global
+ -- Initializes
-- Postcondition
-- Precondition
-- Refined_Depends
-- Refined_Global
+ -- Refined_States
-- Test_Case
procedure Add_Global_Declaration (N : Node_Id);
-- Contract --
--------------
- -- This node is used to hold the various parts of an entry or subprogram
- -- [body] contract, consisting of precondition, postconditions, contract
- -- cases, test cases and global dependencies.
+ -- This node is used to hold the various parts of an entry, subprogram
+ -- [body] or package [body] contract, in particular:
+ -- Abstract states declared by a package declaration
+ -- Contract cases that apply to a subprogram
+ -- Dependency relations of inputs and output of a subprogram
+ -- Global annotations classifying data as input or output
+ -- Initialization sequences for a package declaration
+ -- Pre- and postconditions that apply to a subprogram
-- The node appears in an entry and [generic] subprogram [body] entity.
-- Pre_Post_Conditions contains a collection of pragmas that correspond
-- to pre- and postconditions associated with an entry or a subprogram
-- [body or stub]. The pragmas can either come from source or be the
- -- byproduct of aspect expansion. The ordering in the list is in LIFO
- -- fashion.
+ -- byproduct of aspect expansion. Currently the following pragmas appear
+ -- in this list:
+ -- Post
+ -- Postcondition
+ -- Pre
+ -- Precondition
+ -- The ordering in the list is in LIFO fashion.
-- Note that there might be multiple preconditions or postconditions
-- in this list, either because they come from separate pragmas in the
-- to aspects/pragmas Contract_Cases and Test_Case. The ordering in the
-- list is in LIFO fashion.
- -- Classifications contains pragmas that either categorize subprogram
- -- inputs and outputs or establish dependencies between them. Currently
- -- pragmas Depends, Global, Refined_Depends and Refined_Global are
- -- stored in this list. The ordering is in LIFO fashion.
+ -- Classifications contains pragmas that either declare, categorize or
+ -- establish dependencies between subprogram or package inputs and
+ -- outputs. Currently the following pragmas appear in this list:
+ -- Abstract_States
+ -- Depends
+ -- Global
+ -- Initializes
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_States
+ -- The ordering is in LIFO fashion.
-------------------
-- Expanded_Name --
Name_Import_Valued_Procedure : constant Name_Id := N + $; -- GNAT
Name_Independent : constant Name_Id := N + $; -- Ada 12
Name_Independent_Components : constant Name_Id := N + $; -- Ada 12
+ Name_Initializes : constant Name_Id := N + $; -- GNAT
Name_Inline : constant Name_Id := N + $;
Name_Inline_Always : constant Name_Id := N + $; -- GNAT
Name_Inline_Generic : constant Name_Id := N + $; -- GNAT
Name_Refined_Global : constant Name_Id := N + $; -- GNAT
Name_Refined_Post : constant Name_Id := N + $; -- GNAT
Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
-
- -- Kirchev
-
Name_Refined_State : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT
Pragma_Import_Valued_Procedure,
Pragma_Independent,
Pragma_Independent_Components,
+ Pragma_Initializes,
Pragma_Inline,
Pragma_Inline_Always,
Pragma_Inline_Generic,
projects / platform / upstream / linaro-gcc.git / commitdiff