This patch implements pragmas [Refined_]Depends and [Refined_]Global on
protected entries and task units. As a prerequisite, the patch implements
aspect specifications on entry bodies as specified in Ada 2012 (AI12-0169):
ENTRY_BODY ::=
entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART
[ASPECT_SPECIFICATIONS] ENTRY_BARRIER
is
DECLARATIVE_PART
begin
HANDLED_SEQUENCE_OF_STATEMENTS
end [entry_IDENTIFIER];
------------
-- Source --
------------
-- synchronized_contracts.ads
package Synchronized_Contracts
with SPARK_Mode,
Abstract_State => State
is
Var : Integer := 1;
protected type Prot_Typ_1 is
entry Prot_Ent (Formal : out Integer)
with Global => (Input => (State, Var)),
Depends => (Formal => (State, Var));
end Prot_Typ_1;
protected Prot_Typ_2 is
entry Prot_Ent (Formal : out Integer);
pragma Global ((Input => State));
pragma Depends ((Formal => State));
end Prot_Typ_2;
task type Task_Typ_1
with Global => (Input => State, Output => Var),
Depends => (Var => State);
task Task_Typ_2;
pragma Global ((Output => (State, Var)));
pragma Depends (((State, Var) => null));
end Synchronized_Contracts;
-- synchronized_contracts.adb
package body Synchronized_Contracts
with SPARK_Mode,
Refined_State => (State => Constit)
is
Constit : Integer := 2;
protected body Prot_Typ_1 is
entry Prot_Ent (Formal : out Integer) when True is
pragma Refined_Global ((Input => (Constit, Var)));
pragma Refined_Depends ((Formal => (Constit, Var)));
begin
Formal := Constit + Var;
end Prot_Ent;
end Prot_Typ_1;
protected body Prot_Typ_2 is
entry Prot_Ent (Formal : out Integer)
with Refined_Global => (Input => Constit),
Refined_Depends => (Formal => Constit)
when True is
begin
Formal := Constit + 1;
end Prot_Ent;
end Prot_Typ_2;
task body Task_Typ_1 is
pragma Refined_Global ((Input => Constit, Output => Var));
pragma Refined_Depends ((Var => Constit));
begin
null;
end Task_Typ_1;
task body Task_Typ_2
with Refined_Global => (Output => (Constit, Var)),
Refined_Depends => ((Constit, Var) => null)
is
begin
null;
end Task_Typ_2;
end Synchronized_Contracts;
-----------------
-- Compilation --
-----------------
$ gcc -c synchronized_contracts.adb
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-10-26 Hristian Kirtchev <kirtc...@adacore.com>
* aspects.adb Add an entry for entry bodies in table
Has_Aspect_Specifications_Flag.
(Aspects_On_Body_Or_Stub_OK): Entry bodies now allow for certain
aspects.
* contracts.adb (Add_Contract_Items): Code cleanup. Add
processing for entry bodies, entry declarations and task units.
(Analyze_Subprogram_Body_Contract): Renamed
to Analyze_Entry_Or_Subprogram_Body_Contract. Do not
analyze the contract of an entry body unless annotating the
original tree.
(Analyze_Subprogram_Contract): Renamed to
Analyze_Entry_Or_Subprogram_Contract. Do not analyze the contract
of an entry declaration unless annotating the original tree.
(Analyze_Task_Contract): New routine.
* contracts.ads (Add_Contract_Item): Update the comment on usage.
(Analyze_Package_Body_Contract): Update comment on usage.
(Analyze_Package_Contract): Update the comment on usage.
(Analyze_Subprogram_Body_Contract): Renamed to
Analyze_Entry_Or_Subprogram_Body_Contract.
(Analyze_Subprogram_Body_Stub_Contract): Update the comment on usage.
(Analyze_Subprogram_Contract): Renamed to
Analyze_Entry_Or_Subprogram_Contract.
(Analyze_Task_Contract): New routine.
* einfo.adb (Contract): Restructure the assertion to include
entries and task units.
(SPARK_Pragma): This attribute now applies to operators.
(SPARK_Pragma_Inherited): This flag now applies to operators.
(Set_Contract): Restructure the assertion to include entries and task
units.
(Set_SPARK_Pragma): This attribute now applies to operators.
(Set_SPARK_Pragma_Inherited): This flag now applies to operators.
(Write_Field34_Name): Write out all Ekinds that have a contract.
(Write_Field40_Name): SPARK_Pragma now applies to operators.
* einfo.ads: Update the documentation of attribute Contract along
with usage in nodes. Update the documentation of attributes
SPARK_Pragma and SPARK_Pragma_Inherited.
* exp_ch6.adb (Freeze_Subprogram): Update the call to
Analyze_Subprogram_Contract.
* par-ch9.adb (P_Entry_Barrier): Do not parse keyword "is" as it
is not part of the entry barrier production.
(P_Entry_Body): Parse the optional aspect specifications. Diagnose
misplaced aspects.
* sem_attr.adb (Analyze_Attribute_Old_Result): Update the call
to Find_Related_Subprogram_Or_Body.
* sem_aux.adb (Unit_Declaration_Node) Add an entry for entry
declarations and bodies.
* sem_ch3.adb (Analyze_Declarations): Analyze the contracts of
entry declarations, entry bodies and task units.
* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
Update the call to Analyze_Subprogram_Body_Contract.
(Analyze_Subprogram_Body_Helper): Update the call to
Analyze_Subprogram_Body_Contract.
* sem_ch9.adb (Analyze_Entry_Body): Analyze the aspect
specifications and the contract.
* sem_ch10.adb (Analyze_Compilation_Unit): Update the call to
Analyze_Subprogram_Contract.
* sem_ch12.adb (Save_References_In_Pragma): Update the call to
Find_Related_Subprogram_Or_Body.
* sem_ch13.adb (Analyze_Aspects_On_Body_Or_Stub): Use
Unique_Defining_Entity rather than rummaging around in nodes.
(Diagnose_Misplaced_Aspects): Update comment on usage. Update the
error messages to accomondate the increasing number of contexts.
* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
Update the call to Find_Related_Subprogram_Or_Body.
(Analyze_Depends_Global): Update the call to
Find_Related_Subprogram_Or_Body. Add processing for entry
declarations.
(Analyze_Depends_In_Decl_Part): Update the call
to Find_Related_Subprogram_Or_Body. Task units have no formal
parameters to install. (Analyze_Global_In_Decl_Part): Update
the call to Find_Related_Subprogram_Or_Body. Task units have no
formal parameters to install.
(Analyze_Global_Item): Use Fix_Msg to handle the increasing number of
contexts.
(Analyze_Pragma): Update the call to Find_Related_Subprogram_Or_Body.
Perform full analysis when various pragmas appear in an entry body.
(Analyze_Pre_Post_Condition): Update the call to
Find_Related_Subprogram_Or_Body. Perform full analysis when the pragma
appears in an entry body.
(Analyze_Pre_Post_Condition_In_Decl_Part): Update the call to
Find_Related_Subprogram_Or_Body.
(Analyze_Refined_Depends_Global_Post): Update
the call to Find_Related_Subprogram_Or_Body. Use
Fix_Msg to handle the increasing number of contexts.
(Analyze_Refined_Depends_In_Decl_Part): Update
the call to Find_Related_Subprogram_Or_Body. Use
Unique_Defining_Entity to obtain the entity of the
spec. Use Fix_Msg to handle the increasing number of contexts.
(Analyze_Refined_Global_In_Decl_Part): Update the call to
Find_Related_Subprogram_Or_Body. Use Unique_Defining_Entity to obtain
the entity of the spec. Use Fix_Msg to handle the increasing number of
contexts.
(Analyze_Test_Case_In_Decl_Part): Update the call to
Find_Related_Subprogram_Or_Body.
(Check_Dependency_Clause): Use Fix_Msg to handle the increasing number
of contexts.
(Check_Mode_Restriction_In_Enclosing_Context): Use
Fix_Msg to handle the increasing number of contexts.
(Collect_Subprogram_Inputs_Outputs): Use the refined
versions of the pragmas when the context is an entry body or
a task body.
(Find_Related_Subprogram_Or_Body): Renamed to
Find_Related_Declaration_Or_Body. Add processing for entries
and task units.
(Fix_Msg): New routine.
(Role_Error): Use Fix_Msg to handle the increasing number of contexts.
* sem_prag.ads (Find_Related_Subprogram_Or_Body): Renamed to
Find_Related_Declaration_Or_Body. Update the comment on usage.
* sem_util.adb (Is_Entry_Body): New routine.
(Is_Entry_Declaration): New routine.
* sem_util.ads (Is_Entry_Body): New routine.
(Is_Entry_Declaration): New routine.
Index: par-ch9.adb
===================================================================
--- par-ch9.adb (revision 229313)
+++ par-ch9.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -1089,7 +1089,6 @@
Resync_Past_Semicolon;
Pop_Scope_Stack; -- discard unused entry
return Error;
-
end P_Accept_Statement;
------------------------
@@ -1098,12 +1097,45 @@
-- Parsed by P_Expression (4.4)
+ --------------------------
+ -- 9.5.2 Entry Barrier --
+ --------------------------
+
+ -- ENTRY_BARRIER ::= when CONDITION
+
+ -- Error_Recovery: cannot raise Error_Resync
+
+ function P_Entry_Barrier return Node_Id is
+ Bnode : Node_Id;
+
+ begin
+ if Token = Tok_When then
+ Scan; -- past WHEN;
+ Bnode := P_Expression_No_Right_Paren;
+
+ if Token = Tok_Colon_Equal then
+ Error_Msg_SC -- CODEFIX
+ ("|"":="" should be ""=""");
+ Scan;
+ Bnode := P_Expression_No_Right_Paren;
+ end if;
+
+ else
+ T_When; -- to give error message
+ Bnode := Error;
+ end if;
+
+ return Bnode;
+ end P_Entry_Barrier;
+
-----------------------
-- 9.5.2 Entry Body --
-----------------------
-- ENTRY_BODY ::=
- -- entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART ENTRY_BARRIER is
+ -- entry DEFINING_IDENTIFIER ENTRY_BODY_FORMAL_PART
+ -- [ASPECT_SPECIFICATIONS] ENTRY_BARRIER
+ -- is
-- DECLARATIVE_PART
-- begin
-- HANDLED_SEQUENCE_OF_STATEMENTS
@@ -1114,6 +1146,7 @@
-- Error_Recovery: cannot raise Error_Resync
function P_Entry_Body return Node_Id is
+ Dummy_Node : Node_Id;
Entry_Node : Node_Id;
Formal_Part_Node : Node_Id;
Name_Node : Node_Id;
@@ -1135,8 +1168,34 @@
Formal_Part_Node := P_Entry_Body_Formal_Part;
Set_Entry_Body_Formal_Part (Entry_Node, Formal_Part_Node);
+ -- Ada 2012 (AI12-0169): Aspect specifications may appear on an entry
+ -- body immediately after the formal part. Do not parse the aspect
+ -- specifications directly because the "when" of the entry barrier may
+ -- be interpreted as a misused "with".
+
+ if Token = Tok_With then
+ P_Aspect_Specifications (Entry_Node, Semicolon => False);
+ end if;
+
Set_Condition (Formal_Part_Node, P_Entry_Barrier);
+
+ -- Detect an illegal placement of aspect specifications following the
+ -- entry barrier.
+
+ -- entry E ... when Barrier with Aspect is
+
+ if Token = Tok_With then
+ Error_Msg_SC ("aspect specifications must come before entry barrier");
+
+ -- Consume the illegal aspects to allow for parsing to continue
+
+ Dummy_Node := New_Node (N_Entry_Body, Sloc (Entry_Node));
+ P_Aspect_Specifications (Dummy_Node, Semicolon => False);
+ end if;
+
+ TF_Is;
Parse_Decls_Begin_End (Entry_Node);
+
return Entry_Node;
end P_Entry_Body;
@@ -1185,38 +1244,6 @@
return Fpart_Node;
end P_Entry_Body_Formal_Part;
- --------------------------
- -- 9.5.2 Entry Barrier --
- --------------------------
-
- -- ENTRY_BARRIER ::= when CONDITION
-
- -- Error_Recovery: cannot raise Error_Resync
-
- function P_Entry_Barrier return Node_Id is
- Bnode : Node_Id;
-
- begin
- if Token = Tok_When then
- Scan; -- past WHEN;
- Bnode := P_Expression_No_Right_Paren;
-
- if Token = Tok_Colon_Equal then
- Error_Msg_SC -- CODEFIX
- ("|"":="" should be ""=""");
- Scan;
- Bnode := P_Expression_No_Right_Paren;
- end if;
-
- else
- T_When; -- to give error message
- Bnode := Error;
- end if;
-
- TF_Is;
- return Bnode;
- end P_Entry_Barrier;
-
--------------------------------------
-- 9.5.2 Entry Index Specification --
--------------------------------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 229320)
+++ sem_ch3.adb (working copy)
@@ -2505,16 +2505,23 @@
Analyze_Object_Contract (Defining_Entity (Decl));
elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Entry_Declaration,
N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
- Analyze_Subprogram_Contract (Defining_Entity (Decl));
+ Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
- elsif Nkind (Decl) = N_Subprogram_Body then
- Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
+ elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
+ Analyze_Entry_Or_Subprogram_Body_Contract
+ (Defining_Entity (Decl));
elsif Nkind (Decl) = N_Subprogram_Body_Stub then
Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
+
+ elsif Nkind_In (Decl, N_Single_Task_Declaration,
+ N_Task_Type_Declaration)
+ then
+ Analyze_Task_Contract (Defining_Entity (Decl));
end if;
Next (Decl);
Index: sem_aux.adb
===================================================================
--- sem_aux.adb (revision 229328)
+++ sem_aux.adb (working copy)
@@ -819,8 +819,8 @@
-- Generic subprogram body
elsif Is_Subprogram (S)
- and then Nkind (Unit_Declaration_Node (S))
- = N_Generic_Subprogram_Declaration
+ and then Nkind (Unit_Declaration_Node (S)) =
+ N_Generic_Subprogram_Declaration
then
return True;
end if;
@@ -1649,6 +1649,8 @@
-- Isn't there some better way to express the following ???
while Nkind (N) /= N_Abstract_Subprogram_Declaration
+ and then Nkind (N) /= N_Entry_Body
+ and then Nkind (N) /= N_Entry_Declaration
and then Nkind (N) /= N_Formal_Package_Declaration
and then Nkind (N) /= N_Function_Instantiation
and then Nkind (N) /= N_Generic_Package_Declaration
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb (revision 229328)
+++ sem_ch9.adb (working copy)
@@ -1213,8 +1213,8 @@
Set_Ekind (Id, E_Entry);
end if;
+ Set_Etype (Id, Standard_Void_Type);
Set_Scope (Id, Current_Scope);
- Set_Etype (Id, Standard_Void_Type);
Set_Accept_Address (Id, New_Elmt_List);
-- Set the SPARK_Mode from the current context (may be overwritten later
@@ -1223,6 +1223,12 @@
Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Id);
+ -- Analyze any aspect specifications that appear on the entry body
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
+ end if;
+
E := First_Entity (P_Type);
while Present (E) loop
if Chars (E) = Chars (Id)
@@ -1352,6 +1358,12 @@
Inspect_Deferred_Constant_Completion (Decls);
end if;
+ -- Process the contract of the subprogram body after all declarations
+ -- have been analyzed. This ensures that any contract-related pragmas
+ -- are available through the N_Contract node of the body.
+
+ Analyze_Entry_Or_Subprogram_Body_Contract (Id);
+
if Present (Stats) then
Analyze (Stats);
end if;
Index: sem_ch10.adb
===================================================================
--- sem_ch10.adb (revision 229328)
+++ sem_ch10.adb (working copy)
@@ -939,7 +939,7 @@
if Nkind_In (Unit_Node, N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
- Analyze_Subprogram_Contract (Defining_Entity (Unit_Node));
+ Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Unit_Node));
end if;
-- Generate distribution stubs if requested and no error
Index: einfo.adb
===================================================================
--- einfo.adb (revision 229328)
+++ einfo.adb (working copy)
@@ -1205,16 +1205,25 @@
function Contract (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Constant,
- E_Entry,
+ (Ekind_In (Id, E_Constant, -- object variants
+ E_Variable)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
- E_Generic_Package,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Operator,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body,
- E_Subprogram_Body,
- E_Variable,
- E_Void)
- or else Is_Subprogram_Or_Generic_Subprogram (Id));
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Task_Body, -- synchronized variants
+ E_Task_Type,
+ E_Void)); -- special purpose
return Node34 (Id);
end Contract;
@@ -3139,6 +3148,7 @@
E_Function,
E_Generic_Function,
E_Generic_Procedure,
+ E_Operator,
E_Procedure,
E_Subprogram_Body)
or else
@@ -3161,6 +3171,7 @@
E_Function,
E_Generic_Function,
E_Generic_Procedure,
+ E_Operator,
E_Procedure,
E_Subprogram_Body)
or else
@@ -3834,16 +3845,25 @@
procedure Set_Contract (Id : E; V : N) is
begin
pragma Assert
- (Ekind_In (Id, E_Constant,
- E_Entry,
+ (Ekind_In (Id, E_Constant, -- object variants
+ E_Variable)
+ or else
+ Ekind_In (Id, E_Entry, -- overloadable variants
E_Entry_Family,
- E_Generic_Package,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Operator,
+ E_Procedure,
+ E_Subprogram_Body)
+ or else
+ Ekind_In (Id, E_Generic_Package, -- package variants
E_Package,
- E_Package_Body,
- E_Subprogram_Body,
- E_Variable,
- E_Void)
- or else Is_Subprogram_Or_Generic_Subprogram (Id));
+ E_Package_Body)
+ or else
+ Ekind_In (Id, E_Task_Body, -- synchronized variants
+ E_Task_Type,
+ E_Void)); -- special purpose
Set_Node34 (Id, V);
end Set_Contract;
@@ -6170,6 +6190,7 @@
E_Function,
E_Generic_Function,
E_Generic_Procedure,
+ E_Operator,
E_Procedure,
E_Subprogram_Body)
or else
@@ -6192,6 +6213,7 @@
E_Function,
E_Generic_Function,
E_Generic_Procedure,
+ E_Operator,
E_Procedure,
E_Subprogram_Body)
or else
@@ -10212,14 +10234,19 @@
when E_Constant |
E_Entry |
E_Entry_Family |
+ E_Function |
+ E_Generic_Function |
E_Generic_Package |
+ E_Generic_Procedure |
+ E_Operator |
E_Package |
E_Package_Body |
+ E_Procedure |
E_Subprogram_Body |
+ E_Task_Body |
+ E_Task_Type |
E_Variable |
- E_Void |
- Generic_Subprogram_Kind |
- Subprogram_Kind =>
+ E_Void =>
Write_Str ("Contract");
when others =>
@@ -10317,6 +10344,7 @@
E_Generic_Function |
E_Generic_Package |
E_Generic_Procedure |
+ E_Operator |
E_Package |
E_Package_Body |
E_Procedure |
Index: einfo.ads
===================================================================
--- einfo.ads (revision 229328)
+++ einfo.ads (working copy)
@@ -705,10 +705,10 @@
-- of declaration, procedure call, assignment statement or pragma.
-- Contract (Node34)
--- Defined in constant, entry, entry family, [generic] package, package
--- body, [generic] subprogram, subprogram body, and variable entities.
--- Points to the contract of the entity, holding various assertion items
--- and data classifiers.
+-- Defined in constant, entry, entry family, operator, [generic] package,
+-- package body, [generic] subprogram, subprogram body, variable and task
+-- type entities. Points to the contract of the entity, holding various
+-- assertion items and data classifiers.
-- Corresponding_Concurrent_Type (Node18)
-- Defined in record types that are constructed by the expander to
@@ -4087,19 +4087,20 @@
-- inherited, rather than a local one.
-- SPARK_Pragma (Node40)
--- Present in entries, [generic] package specs, package bodies, [generic]
--- subprogram specs, subprogram bodies and synchronized types. Points to
--- the N_Pragma node that applies to the spec or body. This is either set
--- by a local SPARK_Mode pragma or is inherited from the context (from an
--- outer scope for the spec case or from the spec for the body case). In
--- the case where it is inherited the flag SPARK_Pragma_Inherited is set.
--- Empty if no SPARK_Mode pragma is applicable.
+-- Present in entries, operators, [generic] packages, package bodies,
+-- [generic] subprograms, subprogram bodies and synchronized types.
+-- Points to the N_Pragma node that applies to the spec or body. This
+-- is either set by a local SPARK_Mode pragma or is inherited from the
+-- context (from an outer scope for the spec case or from the spec for
+-- the body case). In the case where it is inherited the flag
+-- SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma is
+-- applicable.
-- SPARK_Pragma_Inherited (Flag265)
--- Present in entries, [generic] package specs, package bodies, [generic]
--- subprogram specs, subprogram bodies and synchronized types. Set if the
--- SPARK_Pragma attribute points to a pragma that is inherited, rather
--- than a local one.
+-- Present in entries, operators, [generic] packages, package bodies,
+-- [generic] subprograms, subprogram bodies and synchronized types. Set
+-- if the SPARK_Pragma attribute points to a pragma that is inherited,
+-- rather than a local one.
-- Spec_Entity (Node19)
-- Defined in package body entities. Points to corresponding package
@@ -6041,13 +6042,15 @@
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Import_Pragma (Node35)
+ -- SPARK_Pragma (Node40)
+ -- Default_Expressions_Processed (Flag108)
-- Has_Invariants (Flag232)
-- Has_Nested_Subprogram (Flag282)
+ -- Is_Intrinsic_Subprogram (Flag64)
-- Is_Machine_Code_Subprogram (Flag137)
+ -- Is_Primitive (Flag218)
-- Is_Pure (Flag44)
- -- Is_Intrinsic_Subprogram (Flag64)
- -- Is_Primitive (Flag218)
- -- Default_Expressions_Processed (Flag108)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Aren't there more flags and fields? seems like this list should be
-- more similar to the E_Function list, which is much longer ???
@@ -6378,6 +6381,7 @@
-- (plus type attributes)
-- E_Task_Body
+ -- Contract (Node34)
-- SPARK_Pragma (Node40)
-- SPARK_Pragma_Inherited (Flag265)
-- (any others??? First/Last Entity, Scope_Depth???)
@@ -6396,6 +6400,7 @@
-- Task_Body_Procedure (Node25)
-- Storage_Size_Variable (Node26) (base type only)
-- Relative_Deadline_Variable (Node28) (base type only)
+ -- Contract (Node34)
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
-- Delay_Cleanups (Flag114)
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 229331)
+++ sem_prag.adb (working copy)
@@ -209,6 +209,12 @@
-- Do_Checks is set, the routine reports duplicate pragmas. The routine
-- returns Empty when reaching the start of the node chain.
+ function Fix_Msg (Id : Entity_Id; Msg : String) return String;
+ -- Replace all occurrences of "subprogram" in string Msg with a specific
+ -- word depending on the Ekind of Id as follows:
+ -- * When Id is an entry [family], replace with "entry"
+ -- * When Id is a task type, replace with "task unit"
+
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
-- original one, following the renaming chain) is returned. Otherwise the
@@ -386,7 +392,7 @@
-- Local variables
- Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
@@ -465,7 +471,7 @@
procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
- Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
All_Inputs_Seen : Elist_Id := No_Elist;
@@ -1144,8 +1150,8 @@
Error_Msg_Name_1 := Chars (Spec_Id);
SPARK_Msg_NE
- ("\& is not part of the input or output set of subprogram %",
- Item, Item_Id);
+ (Fix_Msg (Spec_Id, "\& is not part of the input or output "
+ & "set of subprogram %"), Item, Item_Id);
-- The mode of the item and its role in pragma [Refined_]Depends
-- are in conflict. Construct a detailed message explaining the
@@ -1638,7 +1644,9 @@
Restore_Scope := True;
Push_Scope (Spec_Id);
- if Is_Generic_Subprogram (Spec_Id) then
+ if Ekind (Spec_Id) = E_Task_Type then
+ null;
+ elsif Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
else
Install_Formals (Spec_Id);
@@ -1772,7 +1780,7 @@
---------------------------------
procedure Analyze_Global_In_Decl_Part (N : Node_Id) is
- Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Subp_Id : constant Entity_Id := Defining_Entity (Subp_Decl);
@@ -1876,8 +1884,8 @@
if Is_Formal (Item_Id) then
if Scope (Item_Id) = Spec_Id then
SPARK_Msg_NE
- ("global item cannot reference parameter of "
- & "subprogram &", Item, Spec_Id);
+ (Fix_Msg (Spec_Id, "global item cannot reference "
+ & "parameter of subprogram &"), Item, Spec_Id);
return;
end if;
@@ -2096,9 +2104,10 @@
SPARK_Msg_NE
("global item & cannot have mode In_Out or Output",
Item, Item_Id);
+
SPARK_Msg_NE
- ("\item already appears as input of subprogram &",
- Item, Context);
+ (Fix_Msg (Subp_Id, "\item already appears as input of "
+ & "subprogram &"), Item, Context);
-- Stop the traversal once an error has been detected
@@ -2257,7 +2266,9 @@
Restore_Scope := True;
Push_Scope (Spec_Id);
- if Is_Generic_Subprogram (Spec_Id) then
+ if Ekind (Spec_Id) = E_Task_Type then
+ null;
+ elsif Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
else
Install_Formals (Spec_Id);
@@ -3351,21 +3362,26 @@
-- associated with a subprogram declaration or a body that acts as a
-- spec.
- Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+ Subp_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
+ -- Entry
+
+ if Nkind (Subp_Decl) = N_Entry_Declaration then
+ null;
+
-- Generic subprogram
- if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
- -- Body acts as spec
+ -- Subprogram body acts as spec
elsif Nkind (Subp_Decl) = N_Subprogram_Body
and then No (Corresponding_Spec (Subp_Decl))
then
null;
- -- Body stub acts as spec
+ -- Subprogram body stub acts as spec
elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
@@ -3377,6 +3393,11 @@
elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
null;
+ -- Task unit
+
+ elsif Nkind (Subp_Decl) = N_Task_Type_Declaration then
+ null;
+
else
Pragma_Misplaced;
return;
@@ -3387,6 +3408,16 @@
Legal := True;
Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ -- When the related context is an entry, it must be a protected entry
+ -- (SPARK RM 6.1.4(6)).
+
+ if Is_Entry_Declaration (Spec_Id)
+ and then Ekind (Scope (Spec_Id)) /= E_Protected_Type
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
@@ -3686,7 +3717,8 @@
-- Ensure the proper placement of the pragma
Subp_Decl :=
- Find_Related_Subprogram_Or_Body (N, Do_Checks => not Duplicates_OK);
+ Find_Related_Declaration_Or_Body
+ (N, Do_Checks => not Duplicates_OK);
-- When a pre/postcondition pragma applies to an abstract subprogram,
-- its original form must be an aspect with 'Class.
@@ -3759,10 +3791,11 @@
Mark_Pragma_As_Ghost (N, Subp_Id);
- -- Fully analyze the pragma when it appears inside a subprogram
- -- body because it cannot benefit from forward references.
+ -- Fully analyze the pragma when it appears inside an entry or
+ -- subprogram body because it cannot benefit from forward references.
- if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ if Nkind_In (Subp_Decl, N_Entry_Body,
+ N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
-- The legality checks of pragmas Precondition and Postcondition
@@ -3801,23 +3834,36 @@
-- Verify the placement of the pragma and check for duplicates. The
-- pragma must apply to a subprogram body [stub].
- Body_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+ Body_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
- -- Extract the entities of the spec and body
+ -- Entry body
- if Nkind (Body_Decl) = N_Subprogram_Body then
- Body_Id := Defining_Entity (Body_Decl);
- Spec_Id := Corresponding_Spec (Body_Decl);
+ if Nkind (Body_Decl) = N_Entry_Body then
+ null;
+ -- Subprogram body
+
+ elsif Nkind (Body_Decl) = N_Subprogram_Body then
+ null;
+
+ -- Subprogram body stub
+
elsif Nkind (Body_Decl) = N_Subprogram_Body_Stub then
- Body_Id := Defining_Entity (Body_Decl);
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+ null;
+ -- Task body
+
+ elsif Nkind (Body_Decl) = N_Task_Body then
+ null;
+
else
Pragma_Misplaced;
return;
end if;
+ Body_Id := Defining_Entity (Body_Decl);
+ Spec_Id := Unique_Defining_Entity (Body_Decl);
+
-- The pragma must apply to the second declaration of a subprogram.
-- In other words, the body [stub] cannot acts as a spec.
@@ -3839,10 +3885,17 @@
Spec_Decl := Unit_Declaration_Node (Spec_Id);
+ -- The proper context of a entry declaration is the declaration of
+ -- the enclosing synchronized type.
+
+ if Nkind (Spec_Decl) = N_Entry_Declaration then
+ Spec_Decl := Parent (Parent (Spec_Decl));
+ end if;
+
if Nkind (Parent (Spec_Decl)) /= N_Package_Specification then
Error_Pragma
- ("pragma % must apply to the body of a subprogram declared in a "
- & "package specification");
+ (Fix_Msg (Spec_Id, "pragma % must apply to the body of "
+ & "subprogram declared in a package specification"));
return;
end if;
@@ -12275,7 +12328,7 @@
-- as a spec.
Subp_Decl :=
- Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+ Find_Related_Declaration_Or_Body (N, Do_Checks => True);
-- Generic subprogram
@@ -12319,10 +12372,12 @@
Mark_Pragma_As_Ghost (N, Spec_Id);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
- -- Fully analyze the pragma when it appears inside a subprogram
- -- body because it cannot benefit from forward references.
+ -- Fully analyze the pragma when it appears inside an entry
+ -- or subprogram body because it cannot benefit from forward
+ -- references.
- if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ if Nkind_In (Subp_Decl, N_Entry_Body,
+ N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
-- The legality checks of pragma Contract_Cases are affected by
@@ -13046,10 +13101,12 @@
Add_Contract_Item (N, Spec_Id);
- -- Fully analyze the pragma when it appears inside a subprogram
- -- body because it cannot benefit from forward references.
+ -- Fully analyze the pragma when it appears inside an entry
+ -- or subprogram body because it cannot benefit from forward
+ -- references.
- if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ if Nkind_In (Subp_Decl, N_Entry_Body,
+ N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
-- The legality checks of pragmas Depends and Global are
@@ -13993,7 +14050,7 @@
Check_At_Most_N_Arguments (1);
Subp_Decl :=
- Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+ Find_Related_Declaration_Or_Body (N, Do_Checks => True);
-- Generic subprogram declaration
@@ -14564,10 +14621,12 @@
Add_Contract_Item (N, Spec_Id);
- -- Fully analyze the pragma when it appears inside a subprogram
- -- body because it cannot benefit from forward references.
+ -- Fully analyze the pragma when it appears inside an entry
+ -- or subprogram body because it cannot benefit from forward
+ -- references.
- if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ if Nkind_In (Subp_Decl, N_Entry_Body,
+ N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
-- The legality checks of pragmas Depends and Global are
@@ -20991,7 +21050,7 @@
return;
end if;
- Subp_Decl := Find_Related_Subprogram_Or_Body (N);
+ Subp_Decl := Find_Related_Declaration_Or_Body (N);
-- Find the enclosing context
@@ -21067,10 +21126,12 @@
Check_Distinct_Name (Subp_Id);
- -- Fully analyze the pragma when it appears inside a subprogram
- -- body because it cannot benefit from forward references.
+ -- Fully analyze the pragma when it appears inside an entry
+ -- or subprogram body because it cannot benefit from forward
+ -- references.
- if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ if Nkind_In (Subp_Decl, N_Entry_Body,
+ N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
-- The legality checks of pragma Test_Case are affected by the
@@ -21910,7 +21971,7 @@
Check_At_Most_N_Arguments (1);
Subp_Decl :=
- Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+ Find_Related_Declaration_Or_Body (N, Do_Checks => True);
-- Generic subprogram
@@ -22575,7 +22636,7 @@
-- Local variables
- Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
@@ -22773,9 +22834,9 @@
Item_Id := Available_View (Entity_Of (Item));
- return Ekind (Item_Id) = E_Abstract_State
- and then Has_Null_Refinement (Item_Id);
-
+ return
+ Ekind (Item_Id) = E_Abstract_State
+ and then Has_Null_Refinement (Item_Id);
else
return False;
end if;
@@ -23059,8 +23120,8 @@
if not Clause_Matched then
SPARK_Msg_NE
- ("dependence clause of subprogram & has no matching refinement "
- & "in body", Dep_Clause, Spec_Id);
+ (Fix_Msg (Spec_Id, "dependence clause of subprogram & has no "
+ & "matching refinement in body"), Dep_Clause, Spec_Id);
end if;
end Check_Dependency_Clause;
@@ -23377,7 +23438,7 @@
-- Local variables
- Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Body_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
Errors : constant Nat := Serious_Errors_Detected;
Clause : Node_Id;
@@ -23394,12 +23455,7 @@
return;
end if;
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
- else
- Spec_Id := Corresponding_Spec (Body_Decl);
- end if;
-
+ Spec_Id := Unique_Defining_Entity (Body_Decl);
Depends := Get_Pragma (Spec_Id, Pragma_Depends);
-- Subprogram declarations lacks pragma Depends. Refined_Depends is
@@ -23407,8 +23463,8 @@
if No (Depends) then
SPARK_Msg_NE
- ("useless refinement, declaration of subprogram & lacks aspect or "
- & "pragma Depends", N, Spec_Id);
+ (Fix_Msg (Spec_Id, "useless refinement, declaration of subprogram "
+ & "& lacks aspect or pragma Depends"), N, Spec_Id);
goto Leave;
end if;
@@ -23421,8 +23477,8 @@
if Nkind (Deps) = N_Null then
SPARK_Msg_NE
- ("useless refinement, subprogram & does not depend on abstract "
- & "state with visible refinement", N, Spec_Id);
+ (Fix_Msg (Spec_Id, "useless refinement, subprogram & does not "
+ & "depend on abstract state with visible refinement"), N, Spec_Id);
goto Leave;
end if;
@@ -24355,7 +24411,7 @@
-- Local variables
- Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Body_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Errors : constant Nat := Serious_Errors_Detected;
Items : Node_Id;
@@ -24368,22 +24424,17 @@
return;
end if;
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
- else
- Spec_Id := Corresponding_Spec (Body_Decl);
- end if;
+ Spec_Id := Unique_Defining_Entity (Body_Decl);
+ Global := Get_Pragma (Spec_Id, Pragma_Global);
+ Items := Expression (Get_Argument (N, Spec_Id));
- Global := Get_Pragma (Spec_Id, Pragma_Global);
- Items := Expression (Get_Argument (N, Spec_Id));
-
-- The subprogram declaration lacks pragma Global. This renders
-- Refined_Global useless as there is nothing to refine.
if No (Global) then
SPARK_Msg_NE
- ("useless refinement, declaration of subprogram & lacks aspect or "
- & "pragma Global", N, Spec_Id);
+ (Fix_Msg (Spec_Id, "useless refinement, declaration of subprogram "
+ & "& lacks aspect or pragma Global"), N, Spec_Id);
goto Leave;
end if;
@@ -24415,8 +24466,9 @@
and then not Has_Null_State
then
SPARK_Msg_NE
- ("useless refinement, subprogram & does not depend on abstract "
- & "state with visible refinement", N, Spec_Id);
+ (Fix_Msg (Spec_Id, "useless refinement, subprogram & does not "
+ & "depend on abstract state with visible refinement"),
+ N, Spec_Id);
goto Leave;
-- The global refinement of inputs and outputs cannot be null when
@@ -24432,8 +24484,8 @@
and then not Has_Null_State
then
SPARK_Msg_NE
- ("refinement cannot be null, subprogram & has global items",
- N, Spec_Id);
+ (Fix_Msg (Spec_Id, "refinement cannot be null, subprogram & has "
+ & "global items"), N, Spec_Id);
goto Leave;
end if;
end if;
@@ -25292,7 +25344,7 @@
------------------------------------
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is
- Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
procedure Preanalyze_Test_Case_Arg (Arg_Nam : Name_Id);
@@ -26326,10 +26378,13 @@
Next_Entity (Formal);
end loop;
- -- When processing a subprogram body, look for pragmas Refined_Depends
- -- and Refined_Global as they specify the inputs and outputs.
+ -- When processing an entry, subprogram or task body, look for pragmas
+ -- Refined_Depends and Refined_Global as they specify the inputs and
+ -- outputs.
- if Ekind (Subp_Id) = E_Subprogram_Body then
+ if Is_Entry_Body (Subp_Id)
+ or else Ekind_In (Subp_Id, E_Subprogram_Body, E_Task_Body)
+ then
Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends);
Global := Get_Pragma (Subp_Id, Pragma_Refined_Global);
@@ -26469,102 +26524,14 @@
return Empty;
end Find_Related_Context;
- ----------------------------------
- -- Find_Related_Package_Or_Body --
- ----------------------------------
+ --------------------------------------
+ -- Find_Related_Declaration_Or_Body --
+ --------------------------------------
- function Find_Related_Package_Or_Body
+ function Find_Related_Declaration_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id
is
- Context : constant Node_Id := Parent (Prag);
- Prag_Nam : constant Name_Id := Pragma_Name (Prag);
- Stmt : Node_Id;
-
- begin
- Stmt := Prev (Prag);
- while Present (Stmt) loop
-
- -- Skip prior pragmas, but check for duplicates
-
- if Nkind (Stmt) = N_Pragma then
- if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then
- Duplication_Error
- (Prag => Prag,
- Prev => Stmt);
- end if;
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- if Nkind (Stmt) = N_Subprogram_Declaration then
-
- -- The subprogram declaration is an internally generated spec
- -- for an expression function.
-
- if Nkind (Original_Node (Stmt)) = N_Expression_Function then
- return Stmt;
-
- -- The subprogram is actually an instance housed within an
- -- anonymous wrapper package.
-
- elsif Present (Generic_Parent (Specification (Stmt))) then
- return Stmt;
- end if;
- end if;
-
- -- Return the current source construct which is illegal
-
- else
- return Stmt;
- end if;
-
- Prev (Stmt);
- end loop;
-
- -- If we fall through, then the pragma was either the first declaration
- -- or it was preceded by other pragmas and no source constructs.
-
- -- The pragma is associated with a package. The immediate context in
- -- this case is the specification of the package.
-
- if Nkind (Context) = N_Package_Specification then
- return Parent (Context);
-
- -- The pragma appears in the declarations of a package body
-
- elsif Nkind (Context) = N_Package_Body then
- return Context;
-
- -- The pragma appears in the statements of a package body
-
- elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
- and then Nkind (Parent (Context)) = N_Package_Body
- then
- return Parent (Context);
-
- -- The pragma is a byproduct of aspect expansion, return the related
- -- context of the original aspect. This case has a lower priority as
- -- the above circuitry pinpoints precisely the related context.
-
- elsif Present (Corresponding_Aspect (Prag)) then
- return Parent (Corresponding_Aspect (Prag));
-
- -- No candidate packge [body] found
-
- else
- return Empty;
- end if;
- end Find_Related_Package_Or_Body;
-
- -------------------------------------
- -- Find_Related_Subprogram_Or_Body --
- -------------------------------------
-
- function Find_Related_Subprogram_Or_Body
- (Prag : Node_Id;
- Do_Checks : Boolean := False) return Node_Id
- is
Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
procedure Expression_Function_Error;
@@ -26604,7 +26571,7 @@
Name_Refined_Post);
-- Refinement pragmas must be associated with a subprogram body [stub]
- -- Start of processing for Find_Related_Subprogram_Or_Body
+ -- Start of processing for Find_Related_Declaration_Or_Body
begin
Stmt := Prev (Prag);
@@ -26660,6 +26627,14 @@
elsif Present (Generic_Parent (Specification (Stmt))) then
return Stmt;
end if;
+
+ -- The pragma applies to a single task declaration rewritten as a
+ -- task type.
+
+ elsif Nkind (Stmt) = N_Task_Type_Declaration
+ and then Nkind (Original_Node (Stmt)) = N_Single_Task_Declaration
+ then
+ return Stmt;
end if;
-- Return the current construct which is either a subprogram body,
@@ -26680,6 +26655,11 @@
if Nkind (Context) = N_Compilation_Unit_Aux then
return Unit (Parent (Context));
+ -- The pragma appears inside the declarations of an entry body
+
+ elsif Nkind (Context) = N_Entry_Body then
+ return Context;
+
-- The pragma appears inside the statements of a subprogram body. This
-- placement is the result of subprogram contract expansion.
@@ -26691,6 +26671,11 @@
elsif Nkind (Context) = N_Subprogram_Body then
return Context;
+ -- The pragma appears inside the declarative part of a task body
+
+ elsif Nkind (Context) = N_Task_Body then
+ return Context;
+
-- The pragma is a byproduct of aspect expansion, return the related
-- context of the original aspect. This case has a lower priority as
-- the above circuitry pinpoints precisely the related context.
@@ -26703,8 +26688,146 @@
else
return Empty;
end if;
- end Find_Related_Subprogram_Or_Body;
+ end Find_Related_Declaration_Or_Body;
+ ----------------------------------
+ -- Find_Related_Package_Or_Body --
+ ----------------------------------
+
+ function Find_Related_Package_Or_Body
+ (Prag : Node_Id;
+ Do_Checks : Boolean := False) return Node_Id
+ is
+ Context : constant Node_Id := Parent (Prag);
+ Prag_Nam : constant Name_Id := Pragma_Name (Prag);
+ Stmt : Node_Id;
+
+ begin
+ Stmt := Prev (Prag);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then
+ Duplication_Error
+ (Prag => Prag,
+ Prev => Stmt);
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ if Nkind (Stmt) = N_Subprogram_Declaration then
+
+ -- The subprogram declaration is an internally generated spec
+ -- for an expression function.
+
+ if Nkind (Original_Node (Stmt)) = N_Expression_Function then
+ return Stmt;
+
+ -- The subprogram is actually an instance housed within an
+ -- anonymous wrapper package.
+
+ elsif Present (Generic_Parent (Specification (Stmt))) then
+ return Stmt;
+ end if;
+ end if;
+
+ -- Return the current source construct which is illegal
+
+ else
+ return Stmt;
+ end if;
+
+ Prev (Stmt);
+ end loop;
+
+ -- If we fall through, then the pragma was either the first declaration
+ -- or it was preceded by other pragmas and no source constructs.
+
+ -- The pragma is associated with a package. The immediate context in
+ -- this case is the specification of the package.
+
+ if Nkind (Context) = N_Package_Specification then
+ return Parent (Context);
+
+ -- The pragma appears in the declarations of a package body
+
+ elsif Nkind (Context) = N_Package_Body then
+ return Context;
+
+ -- The pragma appears in the statements of a package body
+
+ elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
+ and then Nkind (Parent (Context)) = N_Package_Body
+ then
+ return Parent (Context);
+
+ -- The pragma is a byproduct of aspect expansion, return the related
+ -- context of the original aspect. This case has a lower priority as
+ -- the above circuitry pinpoints precisely the related context.
+
+ elsif Present (Corresponding_Aspect (Prag)) then
+ return Parent (Corresponding_Aspect (Prag));
+
+ -- No candidate packge [body] found
+
+ else
+ return Empty;
+ end if;
+ end Find_Related_Package_Or_Body;
+
+ -------------
+ -- Fix_Msg --
+ -------------
+
+ function Fix_Msg (Id : Entity_Id; Msg : String) return String is
+ Msg_Last : constant Natural := Msg'Last;
+ Msg_Index : Natural;
+ Res : String (Msg'Range) := (others => ' ');
+ Res_Index : Natural;
+
+ begin
+ -- Copy all characters from the input message Msg to result Res with
+ -- suitable replacements.
+
+ Msg_Index := Msg'First;
+ Res_Index := Res'First;
+ while Msg_Index <= Msg_Last loop
+
+ -- Replace "subprogram" with a different word
+
+ if Msg_Index <= Msg_Last - 10
+ and then Msg (Msg_Index .. Msg_Index + 9) = "subprogram"
+ then
+ if Ekind_In (Id, E_Entry, E_Entry_Family) then
+ Res (Res_Index .. Res_Index + 4) := "entry";
+ Res_Index := Res_Index + 5;
+
+ elsif Ekind_In (Id, E_Task_Body, E_Task_Type) then
+ Res (Res_Index .. Res_Index + 8) := "task unit";
+ Res_Index := Res_Index + 9;
+
+ else
+ Res (Res_Index .. Res_Index + 9) := "subprogram";
+ Res_Index := Res_Index + 10;
+ end if;
+
+ Msg_Index := Msg_Index + 10;
+
+ -- Otherwise copy the character
+
+ else
+ Res (Res_Index) := Msg (Msg_Index);
+ Msg_Index := Msg_Index + 1;
+ Res_Index := Res_Index + 1;
+ end if;
+ end loop;
+
+ return Res (Res'First .. Res_Index - 1);
+ end Fix_Msg;
+
------------------
-- Get_Argument --
------------------
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 229313)
+++ sem_prag.ads (working copy)
@@ -327,22 +327,29 @@
-- the pragma is illegal. If flag Do_Checks is set, the routine reports
-- duplicate pragmas.
- function Find_Related_Subprogram_Or_Body
+ function Find_Related_Declaration_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
- -- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global,
- -- Refined_Depends, Refined_Global and Refined_Post and attribute 'Result.
- -- Find the declaration of the related subprogram [body or stub] subject
- -- to pragma Prag. If flag Do_Checks is set, the routine reports duplicate
- -- pragmas and detects improper use of refinement pragmas in stand alone
- -- expression functions. The returned value depends on the related pragma
- -- as follows:
- -- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding
- -- N_Subprogram_Declaration node or if the pragma applies to a stand
- -- alone body, the N_Subprogram_Body node or Empty if illegal.
- -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield
- -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
- -- illegal.
+ -- Subsidiary to the analysis of pragmas
+ -- Contract_Cases
+ -- Depends
+ -- Extensions_Visible
+ -- Global
+ -- Post
+ -- Post_Class
+ -- Postcondition
+ -- Pre
+ -- Pre_Class
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Test_Case
+ -- as well as attributes 'Old and 'Result. Find the declaration of the
+ -- related entry, subprogram or task type [body] subject to pragma Prag.
+ -- If flag Do_Checks is set, the routine reports duplicate pragmas and
+ -- detects improper use of refinement pragmas in stand alone expression
+ -- functions.
function Get_Argument
(Prag : Node_Id;
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 229331)
+++ sem_ch12.adb (working copy)
@@ -14796,10 +14796,9 @@
elsif Is_Generic_Contract_Pragma (Prag) and then Prag /= Templ then
if Is_Package_Contract_Annotation (Prag) then
Context := Find_Related_Package_Or_Body (Prag);
-
else
pragma Assert (Is_Subprogram_Contract_Annotation (Prag));
- Context := Find_Related_Subprogram_Or_Body (Prag);
+ Context := Find_Related_Declaration_Or_Body (Prag);
end if;
-- The use of Original_Node accounts for the case when the
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 229329)
+++ sem_util.adb (working copy)
@@ -11444,6 +11444,28 @@
end if;
end Is_Effectively_Volatile_Object;
+ -------------------
+ -- Is_Entry_Body --
+ -------------------
+
+ function Is_Entry_Body (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind_In (Id, E_Entry, E_Entry_Family)
+ and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Body;
+ end Is_Entry_Body;
+
+ --------------------------
+ -- Is_Entry_Declaration --
+ --------------------------
+
+ function Is_Entry_Declaration (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind_In (Id, E_Entry, E_Entry_Family)
+ and then Nkind (Unit_Declaration_Node (Id)) = N_Entry_Declaration;
+ end Is_Entry_Declaration;
+
----------------------------
-- Is_Expression_Function --
----------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 229332)
+++ sem_util.ads (working copy)
@@ -1283,6 +1283,12 @@
-- Determine whether an arbitrary node denotes an effectively volatile
-- object (SPARK RM 7.1.2).
+ function Is_Entry_Body (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id is the body entity of an entry [family]
+
+ function Is_Entry_Declaration (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id is the spec entity of an entry [family]
+
function Is_Expression_Function (Subp : Entity_Id) return Boolean;
-- Predicate to determine whether a scope entity comes from a rewritten
-- expression function call, and should be inlined unconditionally. Also
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 229328)
+++ sem_attr.adb (working copy)
@@ -1330,7 +1330,7 @@
if Nkind (Prag) = N_Aspect_Specification then
Subp_Decl := Parent (Prag);
else
- Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
+ Subp_Decl := Find_Related_Declaration_Or_Body (Prag);
end if;
-- The aspect or pragma where the attribute resides should be
Index: contracts.adb
===================================================================
--- contracts.adb (revision 229330)
+++ contracts.adb (working copy)
@@ -121,7 +121,7 @@
Set_Contract (Id, Items);
end if;
- -- Contract items related to constants. Applicable pragmas are:
+ -- Constants, the applicable pragmas are:
-- Part_Of
if Ekind (Id) = E_Constant then
@@ -134,46 +134,25 @@
raise Program_Error;
end if;
- -- Contract items related to [generic] packages or instantiations. The
- -- applicable pragmas are:
- -- Abstract_States
- -- Initial_Condition
- -- Initializes
- -- Part_Of (instantiation only)
+ -- Entry bodies, the applicable pragmas are:
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
- elsif Ekind_In (Id, E_Generic_Package, E_Package) then
- if Nam_In (Prag_Nam, Name_Abstract_State,
- Name_Initial_Condition,
- Name_Initializes)
- then
+ elsif Is_Entry_Body (Id) then
+ if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
Add_Classification;
- -- Indicator Part_Of must be associated with a package instantiation
+ elsif Prag_Nam = Name_Refined_Post then
+ Add_Pre_Post_Condition;
- elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
- Add_Classification;
-
-- The pragma is not a proper contract item
else
raise Program_Error;
end if;
- -- Contract items related to package bodies. The applicable pragmas are:
- -- Refined_States
-
- elsif Ekind (Id) = E_Package_Body then
- if Prag_Nam = Name_Refined_State then
- Add_Classification;
-
- -- 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:
+ -- Entry or subprogram declarations, the applicable pragmas are:
-- Contract_Cases
-- Depends
-- Extensions_Visible
@@ -183,9 +162,11 @@
-- Test_Case
-- Volatile_Function
- elsif Ekind_In (Id, E_Entry, E_Entry_Family)
- or else Is_Generic_Subprogram (Id)
- or else Is_Subprogram (Id)
+ elsif Is_Entry_Declaration (Id)
+ or else Ekind_In (Id, E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Procedure)
then
if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
Add_Pre_Post_Condition;
@@ -210,7 +191,44 @@
raise Program_Error;
end if;
- -- Contract items related to subprogram bodies. Applicable pragmas are:
+ -- Packages or instantiations, the applicable pragmas are:
+ -- Abstract_States
+ -- Initial_Condition
+ -- Initializes
+ -- Part_Of (instantiation only)
+
+ elsif Ekind_In (Id, E_Generic_Package, E_Package) then
+ if Nam_In (Prag_Nam, Name_Abstract_State,
+ Name_Initial_Condition,
+ Name_Initializes)
+ then
+ Add_Classification;
+
+ -- Indicator Part_Of must be associated with a package instantiation
+
+ elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Package bodies, the applicable pragmas are:
+ -- Refined_States
+
+ elsif Ekind (Id) = E_Package_Body then
+ if Prag_Nam = Name_Refined_State then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Subprogram bodies, the applicable pragmas are:
-- Postcondition
-- Precondition
-- Refined_Depends
@@ -233,7 +251,35 @@
raise Program_Error;
end if;
- -- Contract items related to variables. Applicable pragmas are:
+ -- Task bodies, the applicable pragmas are:
+ -- Refined_Depends
+ -- Refined_Global
+
+ elsif Ekind (Id) = E_Task_Body then
+ if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Task units, the applicable pragmas are:
+ -- Depends
+ -- Global
+
+ elsif Ekind (Id) = E_Task_Type then
+ if Nam_In (Prag_Nam, Name_Depends, Name_Global) then
+ Add_Classification;
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Variables, the applicable pragmas are:
-- Async_Readers
-- Async_Writers
-- Constant_After_Elaboration
@@ -284,6 +330,231 @@
end loop;
end Analyze_Enclosing_Package_Body_Contract;
+ -----------------------------------------------
+ -- Analyze_Entry_Or_Subprogram_Body_Contract --
+ -----------------------------------------------
+
+ procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id) is
+ Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
+ Items : constant Node_Id := Contract (Body_Id);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
+ Mode : SPARK_Mode_Type;
+
+ begin
+ -- When a subprogram body declaration is illegal, its defining entity is
+ -- left unanalyzed. There is nothing left to do in this case because the
+ -- body lacks a contract, or even a proper Ekind.
+
+ if Ekind (Body_Id) = E_Void then
+ return;
+
+ -- Do not analyze the contract of an entry body unless annotating the
+ -- original tree. It is preferable to analyze the contract after the
+ -- entry body has been transformed into a subprogram body to properly
+ -- handle references to unpacked formals.
+
+ elsif Ekind_In (Body_Id, E_Entry, E_Entry_Family)
+ and then not ASIS_Mode
+ and then not GNATprove_Mode
+ then
+ return;
+
+ -- Do not analyze a contract multiple times
+
+ elsif Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ Set_Analyzed (Items);
+ end if;
+ end if;
+
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related subprogram body.
+
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
+ -- Ensure that the contract cases or postconditions mention 'Result or
+ -- define a post-state.
+
+ Check_Result_And_Post_State (Body_Id);
+
+ -- A stand-alone nonvolatile function body cannot have an effectively
+ -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
+ -- check is relevant only when SPARK_Mode is on, as it is not a standard
+ -- legality rule. The check is performed here because Volatile_Function
+ -- is processed after the analysis of the related subprogram body.
+
+ if SPARK_Mode = On
+ and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Body_Id)
+ then
+ Check_Nonvolatile_Function_Profile (Body_Id);
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+
+ -- Capture all global references in a generic subprogram body now that
+ -- the contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Body_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Body_Decl),
+ Gen_Id => Spec_Id);
+ end if;
+
+ -- Deal with preconditions, [refined] postconditions, Contract_Cases,
+ -- invariants and predicates associated with body and its spec. Do not
+ -- expand the contract of subprogram body stubs.
+
+ if Nkind (Body_Decl) = N_Subprogram_Body then
+ Expand_Subprogram_Contract (Body_Id);
+ end if;
+ end Analyze_Entry_Or_Subprogram_Body_Contract;
+
+ ------------------------------------------
+ -- Analyze_Entry_Or_Subprogram_Contract --
+ ------------------------------------------
+
+ procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+
+ begin
+ -- Do not analyze the contract of an entry declaration unless annotating
+ -- the original tree. It is preferable to analyze the contract after the
+ -- entry declaration has been transformed into a subprogram declaration
+ -- to properly handle references to unpacked formals.
+
+ if Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
+ and then not ASIS_Mode
+ and then not GNATprove_Mode
+ then
+ return;
+
+ -- Do not analyze a contract multiple times
+
+ elsif Present (Items) then
+ if Analyzed (Items) then
+ return;
+ else
+ Set_Analyzed (Items);
+ end if;
+ end if;
+
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related subprogram body.
+
+ Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed.
+
+ if not Has_Significant_Contract (Subp_Id) then
+ null;
+
+ elsif Present (Items) then
+
+ -- Analyze pre- and postconditions
+
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze contract-cases and test-cases
+
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
+
+ if Prag_Nam = Name_Contract_Cases then
+ Analyze_Contract_Cases_In_Decl_Part (Prag);
+ else
+ pragma Assert (Prag_Nam = Name_Test_Case);
+ Analyze_Test_Case_In_Decl_Part (Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze classification pragmas
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
+
+ if Prag_Nam = Name_Depends then
+ Depends := Prag;
+
+ elsif Prag_Nam = Name_Global then
+ 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;
+
+ -- Ensure that the contract cases or postconditions mention 'Result
+ -- or define a post-state.
+
+ Check_Result_And_Post_State (Subp_Id);
+ end if;
+
+ -- A nonvolatile function cannot have an effectively volatile formal
+ -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
+ -- only when SPARK_Mode is on, as it is not a standard legality rule.
+ -- The check is performed here because pragma Volatile_Function is
+ -- processed after the analysis of the related subprogram declaration.
+
+ if SPARK_Mode = On
+ and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Subp_Id)
+ then
+ Check_Nonvolatile_Function_Profile (Subp_Id);
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+
+ -- Capture all global references in a generic subprogram now that the
+ -- contract has been analyzed.
+
+ if Is_Generic_Declaration_Or_Body (Subp_Decl) then
+ Save_Global_References_In_Contract
+ (Templ => Original_Node (Subp_Decl),
+ Gen_Id => Subp_Id);
+ end if;
+ end Analyze_Entry_Or_Subprogram_Contract;
+
-----------------------------
-- Analyze_Object_Contract --
-----------------------------
@@ -617,95 +888,48 @@
end if;
end Analyze_Package_Contract;
- --------------------------------------
- -- Analyze_Subprogram_Body_Contract --
- --------------------------------------
+ -------------------------------------------
+ -- Analyze_Subprogram_Body_Stub_Contract --
+ -------------------------------------------
- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
- Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
- Items : constant Node_Id := Contract (Body_Id);
- Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
- Mode : SPARK_Mode_Type;
+ procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
+ Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
begin
- -- When a subprogram body declaration is illegal, its defining entity is
- -- left unanalyzed. There is nothing left to do in this case because the
- -- body lacks a contract, or even a proper Ekind.
+ -- A subprogram body stub may act as its own spec or as the completion
+ -- of a previous declaration. Depending on the context, the contract of
+ -- the stub may contain two sets of pragmas.
- if Ekind (Body_Id) = E_Void then
- return;
+ -- The stub is a completion, the applicable pragmas are:
+ -- Refined_Depends
+ -- Refined_Global
- -- Do not analyze a contract multiple times
+ if Present (Spec_Id) then
+ Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
- elsif Present (Items) then
- if Analyzed (Items) then
- return;
- else
- Set_Analyzed (Items);
- end if;
- end if;
+ -- The stub acts as its own spec, the applicable pragmas are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related subprogram body.
-
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
-
- -- Ensure that the contract cases or postconditions mention 'Result or
- -- define a post-state.
-
- Check_Result_And_Post_State (Body_Id);
-
- -- A stand-alone nonvolatile function body cannot have an effectively
- -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
- -- check is relevant only when SPARK_Mode is on, as it is not a standard
- -- legality rule. The check is performed here because Volatile_Function
- -- is processed after the analysis of the related subprogram body.
-
- if SPARK_Mode = On
- and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
- and then not Is_Volatile_Function (Body_Id)
- then
- Check_Nonvolatile_Function_Profile (Body_Id);
+ else
+ Analyze_Entry_Or_Subprogram_Contract (Stub_Id);
end if;
+ end Analyze_Subprogram_Body_Stub_Contract;
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
+ ---------------------------
+ -- Analyze_Task_Contract --
+ ---------------------------
- Restore_SPARK_Mode (Mode);
+ procedure Analyze_Task_Contract (Task_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Task_Id);
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
- -- Capture all global references in a generic subprogram body now that
- -- the contract has been analyzed.
-
- if Is_Generic_Declaration_Or_Body (Body_Decl) then
- Save_Global_References_In_Contract
- (Templ => Original_Node (Body_Decl),
- Gen_Id => Spec_Id);
- end if;
-
- -- Deal with preconditions, [refined] postconditions, Contract_Cases,
- -- invariants and predicates associated with body and its spec. Do not
- -- expand the contract of subprogram body stubs.
-
- if Nkind (Body_Decl) = N_Subprogram_Body then
- Expand_Subprogram_Contract (Body_Id);
- end if;
- end Analyze_Subprogram_Body_Contract;
-
- ---------------------------------
- -- Analyze_Subprogram_Contract --
- ---------------------------------
-
- procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
- Items : constant Node_Id := Contract (Subp_Id);
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- Depends : Node_Id := Empty;
- Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Prag_Nam : Name_Id;
-
begin
-- Do not analyze a contract multiple times
@@ -722,137 +946,32 @@
-- context. To remedy this, restore the original SPARK_Mode of the
-- related subprogram body.
- Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+ Save_SPARK_Mode_And_Set (Task_Id, Mode);
- -- All subprograms carry a contract, but for some it is not significant
- -- and should not be processed.
+ -- Analyze Global first, as Depends may mention items classified in the
+ -- global categorization.
- if not Has_Significant_Contract (Subp_Id) then
- null;
+ Prag := Get_Pragma (Task_Id, Pragma_Global);
- elsif Present (Items) then
+ if Present (Prag) then
+ Analyze_Global_In_Decl_Part (Prag);
+ end if;
- -- Analyze pre- and postconditions
+ -- Depends must be analyzed after Global in order to see the modes of
+ -- all global items.
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
- Prag := Next_Pragma (Prag);
- end loop;
+ Prag := Get_Pragma (Task_Id, Pragma_Depends);
- -- Analyze contract-cases and test-cases
-
- Prag := Contract_Test_Cases (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
-
- if Prag_Nam = Name_Contract_Cases then
- Analyze_Contract_Cases_In_Decl_Part (Prag);
- else
- pragma Assert (Prag_Nam = Name_Test_Case);
- Analyze_Test_Case_In_Decl_Part (Prag);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Analyze classification pragmas
-
- Prag := Classifications (Items);
- while Present (Prag) loop
- Prag_Nam := Pragma_Name (Prag);
-
- if Prag_Nam = Name_Depends then
- Depends := Prag;
-
- elsif Prag_Nam = Name_Global then
- 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;
-
- -- Ensure that the contract cases or postconditions mention 'Result
- -- or define a post-state.
-
- Check_Result_And_Post_State (Subp_Id);
+ if Present (Prag) then
+ Analyze_Depends_In_Decl_Part (Prag);
end if;
- -- A nonvolatile function cannot have an effectively volatile formal
- -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
- -- only when SPARK_Mode is on, as it is not a standard legality rule.
- -- The check is performed here because pragma Volatile_Function is
- -- processed after the analysis of the related subprogram declaration.
-
- if SPARK_Mode = On
- and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
- and then not Is_Volatile_Function (Subp_Id)
- then
- Check_Nonvolatile_Function_Profile (Subp_Id);
- end if;
-
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
Restore_SPARK_Mode (Mode);
+ end Analyze_Task_Contract;
- -- Capture all global references in a generic subprogram now that the
- -- contract has been analyzed.
-
- if Is_Generic_Declaration_Or_Body (Subp_Decl) then
- Save_Global_References_In_Contract
- (Templ => Original_Node (Subp_Decl),
- Gen_Id => Subp_Id);
- end if;
- end Analyze_Subprogram_Contract;
-
- -------------------------------------------
- -- Analyze_Subprogram_Body_Stub_Contract --
- -------------------------------------------
-
- procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
- Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
-
- begin
- -- A subprogram body stub may act as its own spec or as the completion
- -- of a previous declaration. Depending on the context, the contract of
- -- the stub may contain two sets of pragmas.
-
- -- The stub is a completion, the applicable pragmas are:
- -- Refined_Depends
- -- Refined_Global
-
- if Present (Spec_Id) then
- Analyze_Subprogram_Body_Contract (Stub_Id);
-
- -- The stub acts as its own spec, the applicable pragmas are:
- -- Contract_Cases
- -- Depends
- -- Global
- -- Postcondition
- -- Precondition
- -- Test_Case
-
- else
- Analyze_Subprogram_Contract (Stub_Id);
- end if;
- end Analyze_Subprogram_Body_Stub_Contract;
-
-----------------------------
-- Create_Generic_Contract --
-----------------------------
Index: contracts.ads
===================================================================
--- contracts.ads (revision 229314)
+++ contracts.ads (working copy)
@@ -31,9 +31,9 @@
package Contracts is
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
- -- Add pragma Prag to the contract of a constant, entry, package [body],
- -- subprogram [body], or variable denoted by Id. The following are valid
- -- pragmas:
+ -- Add pragma Prag to the contract of a constant, entry, entry family,
+ -- [generic] package, package body, [generic] subprogram, subprogram body,
+ -- variable or task unit denoted by Id. The following are valid pragmas:
-- Abstract_State
-- Async_Readers
-- Async_Writers
@@ -60,6 +60,31 @@
-- Analyze the contract of the nearest package body (if any) enclosing
-- package or subprogram body Body_Decl.
+ procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of entry or
+ -- subprogram body Body_Id as if they appeared at the end of a declarative
+ -- region. Pragmas in question are:
+ -- Contract_Cases (stand alone subprogram body)
+ -- Depends (stand alone subprogram body)
+ -- Global (stand alone subprogram body)
+ -- Postcondition (stand alone subprogram body)
+ -- Precondition (stand alone subprogram body)
+ -- Refined_Depends
+ -- Refined_Global
+ -- Refined_Post
+ -- Test_Case (stand alone subprogram body)
+
+ procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of entry or
+ -- subprogram Subp_Id as if they appeared at the end of a declarative
+ -- region. The pragmas in question are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
+
procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of object Obj_Id as
-- if they appeared at the end of the declarative region. The pragmas to be
@@ -73,51 +98,26 @@
procedure Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty);
- -- Analyze all delayed aspects chained on the contract of package body
+ -- Analyze all delayed pragmas chained on the contract of package body
-- Body_Id as if they appeared at the end of a declarative region. The
- -- aspects that are considered are:
+ -- pragmas that are considered are:
-- Refined_State
--
-- Freeze_Id is the entity of a [generic] package body or a [generic]
-- subprogram body which "freezes" the contract of Body_Id.
procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of package Pack_Id
- -- as if they appeared at the end of a declarative region. The aspects
+ -- Analyze all delayed pragmas chained on the contract of package Pack_Id
+ -- as if they appeared at the end of a declarative region. The pragmas
-- that are considered are:
-- Initial_Condition
-- Initializes
-- Part_Of
- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of subprogram body
- -- Body_Id as if they appeared at the end of a declarative region. Aspects
- -- in question are:
- -- Contract_Cases (stand alone body)
- -- Depends (stand alone body)
- -- Global (stand alone body)
- -- Postcondition (stand alone body)
- -- Precondition (stand alone body)
- -- Refined_Depends
- -- Refined_Global
- -- Refined_Post
- -- Test_Case (stand alone body)
-
- procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of subprogram
- -- Subp_Id as if they appeared at the end of a declarative region. The
- -- aspects in question are:
- -- Contract_Cases
- -- Depends
- -- Global
- -- Postcondition
- -- Precondition
- -- Test_Case
-
procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of a subprogram body
+ -- Analyze all delayed pragmas chained on the contract of a subprogram body
-- stub Stub_Id as if they appeared at the end of a declarative region. The
- -- aspects in question are:
+ -- pragmas in question are:
-- Contract_Cases
-- Depends
-- Global
@@ -128,6 +128,13 @@
-- Refined_Post
-- Test_Case
+ procedure Analyze_Task_Contract (Task_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of a task unit
+ -- Task_Id as if they appeared at the end of a declarative region. The
+ -- pragmas in question are:
+ -- Depends
+ -- Global
+
procedure Create_Generic_Contract (Unit : Node_Id);
-- Create a contract node for a generic package, generic subprogram, or a
-- generic body denoted by Unit by collecting all source contract-related
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 229314)
+++ exp_ch6.adb (working copy)
@@ -7105,7 +7105,7 @@
if Nkind (Parent (Subp)) = N_Procedure_Specification
and then Null_Present (Parent (Subp))
then
- Analyze_Subprogram_Contract (Subp);
+ Analyze_Entry_Or_Subprogram_Contract (Subp);
end if;
end Freeze_Subprogram;
Index: aspects.adb
===================================================================
--- aspects.adb (revision 229313)
+++ aspects.adb (working copy)
@@ -154,7 +154,8 @@
pragma Assert (Has_Aspects (N));
pragma Assert (Nkind (N) in N_Body_Stub
- or else Nkind_In (N, N_Package_Body,
+ or else Nkind_In (N, N_Entry_Body,
+ N_Package_Body,
N_Protected_Body,
N_Subprogram_Body,
N_Task_Body));
@@ -427,6 +428,7 @@
Has_Aspect_Specifications_Flag : constant array (Node_Kind) of Boolean :=
(N_Abstract_Subprogram_Declaration => True,
N_Component_Declaration => True,
+ N_Entry_Body => True,
N_Entry_Declaration => True,
N_Exception_Declaration => True,
N_Exception_Renaming_Declaration => True,
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 229330)
+++ sem_ch6.adb (working copy)
@@ -1385,7 +1385,7 @@
-- have been analyzed. This ensures that any contract-related pragmas
-- are available through the N_Contract node of the body.
- Analyze_Subprogram_Body_Contract (Body_Id);
+ Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
Analyze (Handled_Statement_Sequence (N));
Save_Global_References (Original_Node (N));
@@ -3789,7 +3789,7 @@
-- after the declarations of the body have been processed as pragmas
-- are now chained on the contract of the subprogram body.
- Analyze_Subprogram_Body_Contract (Body_Id);
+ Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
-- If SPARK_Mode for body is not On, disable frontend inlining for this
-- subprogram in GNATprove mode, as its body should not be analyzed.
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 229331)
+++ sem_ch13.adb (working copy)
@@ -3474,9 +3474,9 @@
Body_Id : constant Entity_Id := Defining_Entity (N);
procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id);
- -- Subprogram body [stub] N has aspects, but they are not properly
- -- placed. Emit an error message depending on the aspects involved.
- -- Spec_Id is the entity of the corresponding spec.
+ -- Body [stub] N has aspects, but they are not properly placed. Emit an
+ -- error message depending on the aspects involved. Spec_Id denotes the
+ -- entity of the corresponding spec.
--------------------------------
-- Diagnose_Misplaced_Aspects --
@@ -3532,7 +3532,7 @@
else
Error_Msg_N
- ("aspect specification must appear in subprogram declaration",
+ ("aspect specification must appear on initial declaration",
Asp);
end if;
end Misplaced_Aspect_Error;
@@ -3574,7 +3574,7 @@
else
Error_Msg_N
- ("aspect specification must appear in subprogram declaration",
+ ("aspect specification must appear on initial declaration",
Asp);
end if;
@@ -3584,23 +3584,17 @@
-- Local variables
- Spec_Id : Entity_Id;
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (N);
-- Start of processing for Analyze_Aspects_On_Body_Or_Stub
begin
- if Nkind (N) = N_Subprogram_Body_Stub then
- Spec_Id := Corresponding_Spec_Of_Stub (N);
- else
- Spec_Id := Corresponding_Spec (N);
- end if;
-
-- Language-defined aspects cannot be associated with a subprogram body
-- [stub] if the subprogram has a spec. Certain implementation defined
-- aspects are allowed to break this rule (for all applicable cases, see
-- table Aspects.Aspect_On_Body_Or_Stub_OK).
- if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then
+ if Spec_Id /= Body_Id and then not Aspects_On_Body_Or_Stub_OK (N) then
Diagnose_Misplaced_Aspects (Spec_Id);
else
Analyze_Aspect_Specifications (N, Body_Id);
