git
/
gcc
mirror of git://gcc.gnu.org/git/gcc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

aspects.adb: Add an entry in table Canonical_Aspect for Initializes. 

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.

From-SVN: r203522
This commit is contained in:
Hristian Kirtchev 2013-10-14 12:34:33 +00:00 committed by Arnaud Charlet
parent 83fd5d110e
commit 54e28df21a
19 changed files with 1013 additions and 175 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
gcc/ada/ChangeLog
View File

@ -1,3 +1,79 @@
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>

1
gcc/ada/aspects.adb
View File

@ -440,6 +440,7 @@ package body Aspects is
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,

4
gcc/ada/aspects.ads
View File

@ -96,6 +96,7 @@ package Aspects is
Aspect_External_Tag,
Aspect_Global, -- GNAT
Aspect_Implicit_Dereference,
Aspect_Initializes, -- GNAT
Aspect_Input,
Aspect_Interrupt_Priority,
Aspect_Invariant, -- GNAT
@ -309,6 +310,7 @@ package Aspects is
Aspect_External_Tag => Expression,
Aspect_Global => Expression,
Aspect_Implicit_Dereference => Name,
Aspect_Initializes => Expression,
Aspect_Input => Name,
Aspect_Interrupt_Priority => Expression,
Aspect_Invariant => Expression,
@ -398,6 +400,7 @@ package Aspects is
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,
@ -597,6 +600,7 @@ package Aspects is
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,

34
gcc/ada/atree.adb
View File

@ -978,6 +978,26 @@ package body Atree is
T = V6;
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;
@ -1033,6 +1053,20 @@ package body Atree is
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 --
------------------------

20
gcc/ada/atree.ads
View File

@ -735,6 +735,16 @@ package Atree is
V5 : Entity_Kind;
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;
@ -770,6 +780,16 @@ package Atree is
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

78
gcc/ada/einfo.adb
View File

@ -80,7 +80,6 @@ package body Einfo is
-- 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
@ -213,7 +212,6 @@ package body Einfo is
-- Protection_Object Node23
-- Stored_Constraint Elist23
-- Finalizer Node24
-- Related_Expression Node24
-- Contract Node24
@ -238,6 +236,7 @@ package body Einfo is
-- Wrapped_Entity Node27
-- Extra_Formals Node28
-- Finalizer Node28
-- Initialization_Statements Node28
-- Underlying_Record_View Node28
@ -1068,9 +1067,14 @@ package body Einfo is
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;
@ -1180,10 +1184,8 @@ package body Einfo is
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
@ -2656,12 +2658,6 @@ package body Einfo 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);
@ -3666,9 +3662,15 @@ package body Einfo is
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;
@ -3779,10 +3781,8 @@ package body Einfo is
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
@ -5328,12 +5328,6 @@ package body Einfo 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);
@ -6293,15 +6287,18 @@ package body Einfo is
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;
@ -8339,9 +8336,6 @@ package body Einfo is
when E_Procedure =>
Write_Str ("Postcondition_Proc");
when E_Package_Body =>
Write_Str ("Refined_State_Pragma");
when E_Abstract_State =>
Write_Str ("Refinement_Constituents");
@ -9055,10 +9049,6 @@ package body Einfo is
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 =>
@ -9066,9 +9056,12 @@ package body Einfo is
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 =>
@ -9202,7 +9195,12 @@ package body Einfo is
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 =>

24
gcc/ada/einfo.ads
View File

@ -1022,9 +1022,10 @@ package Einfo is
-- '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
@ -1181,7 +1182,7 @@ package Einfo 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.
@ -3541,10 +3542,6 @@ package Einfo is
-- 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
@ -5626,10 +5623,11 @@ package Einfo is
-- 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)
@ -5655,14 +5653,14 @@ package Einfo is
-- 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)
@ -6553,7 +6551,6 @@ package Einfo is
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;
@ -7173,7 +7170,6 @@ package Einfo is
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);
@ -7931,7 +7927,6 @@ package Einfo is
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);
@ -8349,7 +8344,6 @@ package Einfo is
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);

1
gcc/ada/par-prag.adb
View File

@ -1186,6 +1186,7 @@ begin
Pragma_Independent |
Pragma_Independent_Components |
Pragma_Initialize_Scalars |
Pragma_Initializes |
Pragma_Inline |
Pragma_Inline_Always |
Pragma_Inline_Generic |

20
gcc/ada/sem_ch12.adb
View File

@ -3022,6 +3022,15 @@ package body Sem_Ch12 is
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.
@ -3029,13 +3038,6 @@ package body Sem_Ch12 is
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);
@ -3124,7 +3126,7 @@ package body Sem_Ch12 is
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;
@ -4756,7 +4758,7 @@ package body Sem_Ch12 is
-- 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

55
gcc/ada/sem_ch13.adb
View File

@ -1883,22 +1883,20 @@ package body Sem_Ch13 is
-- 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 (
@ -1959,6 +1957,44 @@ package body Sem_Ch13 is
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 =>
@ -7708,6 +7744,7 @@ package body Sem_Ch13 is
Aspect_Dimension |
Aspect_Dimension_System |
Aspect_Implicit_Dereference |
Aspect_Initializes |
Aspect_Post |
Aspect_Postcondition |
Aspect_Pre |

33
gcc/ada/sem_ch3.adb
View File

@ -2086,6 +2086,7 @@ package body Sem_Ch3 is
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
@ -2196,24 +2197,38 @@ package body Sem_Ch3 is
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.

63
gcc/ada/sem_ch6.adb
View File

@ -1976,11 +1976,11 @@ package body Sem_Ch6 is
--------------------------------------
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
@ -1991,22 +1991,30 @@ package body Sem_Ch6 is
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
@ -2015,6 +2023,13 @@ package body Sem_Ch6 is
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;
------------------------------------
@ -3570,17 +3585,16 @@ package body Sem_Ch6 is
-- 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
@ -3635,14 +3649,27 @@ package body Sem_Ch6 is
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

43
gcc/ada/sem_ch7.adb
View File

@ -224,15 +224,10 @@ package body Sem_Ch7 is
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);
@ -315,6 +310,7 @@ package body Sem_Ch7 is
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.
@ -338,6 +334,10 @@ package body Sem_Ch7 is
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);
@ -770,6 +770,21 @@ package body Sem_Ch7 is
-- 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.
@ -788,20 +803,6 @@ package body Sem_Ch7 is
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);

617
gcc/ada/sem_prag.adb
View File

@ -412,7 +412,7 @@ package body Sem_Prag is
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
@ -1243,7 +1243,7 @@ package body Sem_Prag is
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
@ -1701,7 +1701,7 @@ package body Sem_Prag is
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
@ -1731,6 +1731,337 @@ package body Sem_Prag is
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 --
--------------------
@ -1887,16 +2218,11 @@ package body Sem_Prag is
-- 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
@ -2013,6 +2339,17 @@ package body Sem_Prag is
-- 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
@ -2907,6 +3244,109 @@ package body Sem_Prag is
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 --
----------------------------
@ -8655,7 +9095,16 @@ package body Sem_Prag is
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
@ -12744,6 +13193,91 @@ package body Sem_Prag is
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 --
------------
@ -16177,6 +16711,7 @@ package body Sem_Prag is
when Pragma_Refined_State => Refined_State : declare
Context : constant Node_Id := Parent (N);
Spec_Id : Entity_Id;
Stmt : Node_Id;
begin
GNAT_Pragma;
@ -16191,6 +16726,34 @@ package body Sem_Prag is
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.
@ -16207,9 +16770,10 @@ package body Sem_Prag is
-- 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;
-----------------------
@ -19647,9 +20211,9 @@ package body Sem_Prag is
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
@ -19938,9 +20502,7 @@ package body Sem_Prag is
-- 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.
@ -19963,7 +20525,7 @@ package body Sem_Prag is
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;
@ -19985,7 +20547,7 @@ package body Sem_Prag is
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.
@ -20014,8 +20576,6 @@ package body Sem_Prag is
Collect_Hidden_States_In_Decls (Private_Declarations (Pack_Spec));
Collect_Hidden_States_In_Decls (Declarations (Pack_Body));
return Result;
end Collect_Hidden_States;
-----------------------------
@ -20080,7 +20640,7 @@ package body Sem_Prag is
-- 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
@ -20090,8 +20650,8 @@ package body Sem_Prag is
-- 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
@ -20814,6 +21374,7 @@ package body Sem_Prag is
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,

3
gcc/ada/sem_prag.ads
View File

@ -62,6 +62,9 @@ package Sem_Prag is
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);

67
gcc/ada/sem_util.adb
View File

@ -212,24 +212,27 @@ package body Sem_Util is
-- 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);
@ -239,9 +242,35 @@ package body Sem_Util is
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,
@ -251,7 +280,7 @@ package body Sem_Util is
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)
@ -269,7 +298,7 @@ package body Sem_Util is
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);
@ -290,6 +319,22 @@ package body Sem_Util is
-- The pragma is not a proper contract item
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;

9
gcc/ada/sem_util.ads
View File

@ -43,16 +43,19 @@ package Sem_Util is
-- 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);

35
gcc/ada/sinfo.ads
View File

@ -7151,9 +7151,14 @@ package Sinfo is
-- 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.
@ -7170,8 +7175,13 @@ package Sinfo is
-- 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
@ -7182,10 +7192,17 @@ package Sinfo is
-- 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 --

5
gcc/ada/snames.ads-tmpl
View File

@ -511,6 +511,7 @@ package Snames is
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
@ -587,9 +588,6 @@ package Snames is
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
@ -1831,6 +1829,7 @@ package Snames is
Pragma_Import_Valued_Procedure,
Pragma_Independent,
Pragma_Independent_Components,
Pragma_Initializes,
Pragma_Inline,
Pragma_Inline_Always,
Pragma_Inline_Generic,