This patch implements the following rules from SPARK RM 6.1.4:
For purposes of the rules concerning the Global, Depends, Refined_Global,
and Refined_Depends aspects, when any of these aspects are specified for a
task unit the task unit's body is considered to be the body of a procedure
and the current instance of the task unit is considered to be a formal
parameter (of that notional procedure) of mode IN OUT.
Similarly, for purposes of the rules concerning the Global, Refined_Global,
Depends, and Refined_Depends aspects as they apply to protected operations,
the current instance of the enclosing protected unit is considered to be a
formal parameter (of mode IN for a protected function, of mode IN OUT
otherwise) and a protected entry is considered to be a protected procedure.
The patch also introduces the concept of a body "freezing" the contract of its
initial declaration.
------------
-- 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 => ((Prot_Typ_1, Formal) => (State, Var, Prot_Typ_1));
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, Task_Typ_1) => (State, Task_Typ_1));
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 (((Prot_Typ_1, Formal) =>
(Constit, Var, Prot_Typ_1)));
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, Task_Typ_1) => (Constit, Task_Typ_1)));
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>
* atree.ads, atree.adb (Ekind_In): New 10 and 11 parameter versions.
* contracts.ads, contracts.adb (Analyze_Initial_Declaration_Contract):
New routine.
* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
Analyze the contract of the initial declaration.
(Analyze_Subprogram_Body_Helper): Analyze the contract of the
initial declaration.
* sem_ch7.adb (Analyze_Package_Body_Helper): Analyze the contract
of the initial declaration.
* sem_ch9.adb (Analyze_Entry_Body): Analyze the contract of
the initial declaration.
(Analyze_Protected_Body): Analyze
the contract of the initial declaration.
(Analyze_Task_Body): Analyze the contract of the initial declaration.
* sem_prag.adb (Add_Entity_To_Name_Buffer): Use "type" rather
than "unit" as it makes the error messages sound better.
(Add_Item_To_Name_Buffer): Update comment on usage. The routine
now supports discriminants and current instances of concurrent
types.
(Analyze_Depends_In_Decl_Part): Install the discriminants
of a task type.
(Analyze_Global_In_Decl_Part): Install the discriminants of a task type.
(Analyze_Global_Item): Add processing for current instances of
concurrent types and include discriminants as valid global items.
(Analyze_Input_Output): Discriminants and current instances of
concurrent types are now valid items. Update various error messages.
(Check_Usage): Current instances of protected and task types behaves
as formal parameters.
(Collect_Subprogram_Inputs_Outputs): There is
no longer need to manually analyze [Refined_]Global thanks to
freezing of initial declaration contracts. Add processing for
the current instance of a concurrent type.
(Find_Role): Add categorizations for discriminants, protected and task
types.
(Is_CCT_Instance): New routine.
(Match_Items): Update the comment on usage. Update internal comments.
* sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update the
comment on usage.
* sem_util.adb (Entity_Of): Ensure that the entity is an object
when traversing a potential renaming chain.
(Fix_Msg): Use "type" rather than "unit" as it makes the error messages
sound better.
* sem_util.ads (Fix_Msg): Update the comment on usage.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 229328)
+++ sem_ch7.adb (working copy)
@@ -763,6 +763,14 @@
Declare_Inherited_Private_Subprograms (Spec_Id);
end if;
+ -- A package body "freezes" the contract of its initial declaration.
+ -- This analysis depends on attribute Corresponding_Spec being set. Only
+ -- bodies coming from source shuld cause this type of "freezing".
+
+ if Comes_From_Source (N) then
+ Analyze_Initial_Declaration_Contract (N);
+ end if;
+
if Present (Declarations (N)) then
Analyze_Declarations (Declarations (N));
Inspect_Deferred_Constant_Completion (Declarations (N));
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb (revision 229357)
+++ sem_ch9.adb (working copy)
@@ -1354,6 +1354,11 @@
(Sloc (N), Entry_Name, P_Type, N, Decls);
end if;
+ -- An entry body "freezes" the contract of its initial declaration. This
+ -- analysis depends on attribute Corresponding_Body being set.
+
+ Analyze_Initial_Declaration_Contract (N);
+
if Present (Decls) then
Analyze_Declarations (Decls);
Inspect_Deferred_Constant_Completion (Decls);
@@ -1811,11 +1816,14 @@
Set_Corresponding_Body (Parent (Spec_Id), Body_Id);
Set_Has_Completion (Spec_Id);
Install_Declarations (Spec_Id);
-
Expand_Protected_Body_Declarations (N, Spec_Id);
-
Last_E := Last_Entity (Spec_Id);
+ -- A protected body "freezes" the contract of its initial declaration.
+ -- This analysis depends on attribute Corresponding_Spec being set.
+
+ Analyze_Initial_Declaration_Contract (N);
+
Analyze_Declarations (Declarations (N));
-- For visibility purposes, all entities in the body are private. Set
@@ -2818,9 +2826,9 @@
begin
-- A task body "freezes" the contract of the nearest enclosing package
- -- body. This ensures that any annotations referenced by the contract
- -- of an entry or subprogram body declared within the current protected
- -- body are available.
+ -- body. This ensures that annotations referenced by the contract of an
+ -- entry or subprogram body declared within the current protected body
+ -- are available.
Analyze_Enclosing_Package_Body_Contract (N);
@@ -2884,6 +2892,11 @@
Install_Declarations (Spec_Id);
Last_E := Last_Entity (Spec_Id);
+ -- A task body "freezes" the contract of its initial declaration. This
+ -- analysis depends on attribute Corresponding_Spec being set.
+
+ Analyze_Initial_Declaration_Contract (N);
+
Analyze_Declarations (Decls);
Inspect_Deferred_Constant_Completion (Decls);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 229362)
+++ sem_prag.adb (working copy)
@@ -237,6 +237,11 @@
-- Determine whether dependency clause Clause is surrounded by extra
-- parentheses. If this is the case, issue an error message.
+ function Is_CCT_Instance (Ref : Node_Id) return Boolean;
+ -- Subsidiary to the analysis of pragmas [Refined_]Depends and [Refined_]
+ -- Global. Determine whether reference Ref denotes the current instance of
+ -- a concurrent type.
+
function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean;
-- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of
-- pragma Depends. Determine whether the type of dependency item Item is
@@ -520,11 +525,14 @@
-- to the name buffer. The individual kinds are as follows:
-- E_Abstract_State - "state"
-- E_Constant - "constant"
+ -- E_Discriminant - "discriminant"
-- E_Generic_In_Out_Parameter - "generic parameter"
-- E_Generic_Out_Parameter - "generic parameter"
-- E_In_Parameter - "parameter"
-- E_In_Out_Parameter - "parameter"
-- E_Out_Parameter - "parameter"
+ -- E_Protected_Type - "current instance of protected type"
+ -- E_Task_Type - "current instance of task type"
-- E_Variable - "global"
procedure Analyze_Dependency_Clause
@@ -571,6 +579,9 @@
elsif Ekind (Item_Id) = E_Constant then
Add_Str_To_Name_Buffer ("constant");
+ elsif Ekind (Item_Id) = E_Discriminant then
+ Add_Str_To_Name_Buffer ("discriminant");
+
elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
E_Generic_In_Parameter)
then
@@ -579,6 +590,12 @@
elsif Is_Formal (Item_Id) then
Add_Str_To_Name_Buffer ("parameter");
+ elsif Ekind (Item_Id) = E_Protected_Type then
+ Add_Str_To_Name_Buffer ("current instance of protected type");
+
+ elsif Ekind (Item_Id) = E_Task_Type then
+ Add_Str_To_Name_Buffer ("current instance of task type");
+
elsif Ekind (Item_Id) = E_Variable then
Add_Str_To_Name_Buffer ("global");
@@ -811,13 +828,27 @@
if Present (Item_Id) then
if Ekind_In (Item_Id, E_Abstract_State,
E_Constant,
+ E_Discriminant,
E_Generic_In_Out_Parameter,
E_Generic_In_Parameter,
E_In_Parameter,
E_In_Out_Parameter,
E_Out_Parameter,
+ E_Protected_Type,
+ E_Task_Type,
E_Variable)
then
+ -- The item denotes a concurrent type, but it is not the
+ -- current instance of an enclosing concurrent type.
+
+ if Ekind_In (Item_Id, E_Protected_Type, E_Task_Type)
+ and then not Is_CCT_Instance (Item)
+ then
+ SPARK_Msg_N
+ ("invalid use of subtype mark in dependency "
+ & "relation", Item);
+ end if;
+
-- Ensure that the item fulfils its role as input and/or
-- output as specified by pragma Global or the enclosing
-- context.
@@ -923,8 +954,8 @@
else
SPARK_Msg_N
- ("item must denote parameter, variable, or state",
- Item);
+ ("item must denote parameter, variable, state or "
+ & "current instance of concurren type", Item);
end if;
-- All other input/output items are illegal
@@ -932,7 +963,8 @@
else
Error_Msg_N
- ("item must denote parameter, variable, or state", Item);
+ ("item must denote parameter, variable, state or current "
+ & "instance of concurrent type", Item);
end if;
end if;
end Analyze_Input_Output;
@@ -1059,6 +1091,9 @@
elsif Ekind (Item_Id) = E_Constant then
Item_Is_Input := True;
+ elsif Ekind (Item_Id) = E_Discriminant then
+ Item_Is_Input := True;
+
-- Generic parameter cases
elsif Ekind (Item_Id) = E_Generic_In_Parameter then
@@ -1098,6 +1133,29 @@
Item_Is_Output := True;
end if;
+ -- Protected types
+
+ elsif Ekind (Item_Id) = E_Protected_Type then
+
+ -- A protected type acts as a formal parameter of mode IN when
+ -- it applies to a protected function.
+
+ if Ekind (Spec_Id) = E_Function then
+ Item_Is_Input := True;
+
+ -- Otherwise the protected type acts as a formal of mode IN OUT
+
+ else
+ Item_Is_Input := True;
+ Item_Is_Output := True;
+ end if;
+
+ -- Task types
+
+ elsif Ekind (Item_Id) = E_Task_Type then
+ Item_Is_Input := True;
+ Item_Is_Output := True;
+
-- Variable case
else pragma Assert (Ekind (Item_Id) = E_Variable);
@@ -1303,7 +1361,12 @@
if Present (Item_Id)
and then not Contains (Used_Items, Item_Id)
then
- if Is_Formal (Item_Id) then
+ -- The current instance of a concurrent type behaves as a
+ -- formal parameter (SPARK RM 6.1.4).
+
+ if Is_Formal (Item_Id)
+ or else Ekind_In (Item_Id, E_Protected_Type, E_Task_Type)
+ then
Usage_Error (Item_Id);
-- States and global objects are not used properly only when
@@ -1658,9 +1721,13 @@
Push_Scope (Spec_Id);
if Ekind (Spec_Id) = E_Task_Type then
- null;
+ if Has_Discriminants (Spec_Id) then
+ Install_Discriminants (Spec_Id);
+ end if;
+
elsif Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
+
else
Install_Formals (Spec_Id);
end if;
@@ -1902,20 +1969,68 @@
return;
end if;
+ -- A global item may denote a concurrent type as long as it is
+ -- the current instance of an enclosing concurrent type
+ -- (SPARK RM 6.1.4).
+
+ elsif Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) then
+ if Is_CCT_Instance (Item) then
+
+ -- Pragma [Refined_]Global associated with a protected
+ -- subprogram cannot mention the current instance of a
+ -- protected type because the instance behaves as a
+ -- formal parameter.
+
+ if Ekind (Item_Id) = E_Protected_Type
+ and then Scope (Spec_Id) = Item_Id
+ then
+ Error_Msg_Name_1 := Chars (Item_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Spec_Id, "global item of subprogram & "
+ & "cannot reference current instance of protected "
+ & "type %"), Item, Spec_Id);
+ return;
+
+ -- Pragma [Refined_]Global associated with a task type
+ -- cannot mention the current instance of a task type
+ -- because the instance behaves as a formal parameter.
+
+ elsif Ekind (Item_Id) = E_Task_Type
+ and then Spec_Id = Item_Id
+ then
+ Error_Msg_Name_1 := Chars (Item_Id);
+ SPARK_Msg_NE
+ (Fix_Msg (Spec_Id, "global item of subprogram & "
+ & "cannot reference current instance of task type "
+ & "%"), Item, Spec_Id);
+ return;
+ end if;
+
+ -- Otherwise the global item denotes a subtype mark that is
+ -- not a current instance.
+
+ else
+ SPARK_Msg_N
+ ("invalid use of subtype mark in global list", Item);
+ return;
+ end if;
+
-- A formal object may act as a global item inside a generic
elsif Is_Formal_Object (Item_Id) then
null;
- -- The only legal references are those to abstract states and
- -- objects (SPARK RM 6.1.4(4)).
+ -- The only legal references are those to abstract states,
+ -- discriminants and objects (SPARK RM 6.1.4(4)).
elsif not Ekind_In (Item_Id, E_Abstract_State,
E_Constant,
+ E_Discriminant,
E_Variable)
then
SPARK_Msg_N
- ("global item must denote object or state", Item);
+ ("global item must denote object, state or current "
+ & "instance of concurrent type", Item);
return;
end if;
@@ -1971,8 +2086,8 @@
elsif Ekind (Item_Id) = E_Constant then
- -- A constant is read-only item, therefore it cannot act as
- -- an output.
+ -- A constant is a read-only item, therefore it cannot act
+ -- as an output.
if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
SPARK_Msg_NE
@@ -1980,6 +2095,19 @@
return;
end if;
+ -- Discriminant related checks
+
+ elsif Ekind (Item_Id) = E_Discriminant then
+
+ -- A discriminant is a read-only item, therefore it cannot
+ -- act as an output.
+
+ if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+ SPARK_Msg_NE
+ ("discriminant & cannot act as output", Item, Item_Id);
+ return;
+ end if;
+
-- Variable related checks. These are only relevant when
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
@@ -2025,7 +2153,9 @@
-- (SPARK RM 6.1.4(4)).
else
- Error_Msg_N ("global item must denote object or state", Item);
+ Error_Msg_N
+ ("global item must denote object, state or current instance "
+ & "of concurrent type", Item);
return;
end if;
@@ -2286,9 +2416,13 @@
Push_Scope (Spec_Id);
if Ekind (Spec_Id) = E_Task_Type then
- null;
+ if Has_Discriminants (Spec_Id) then
+ Install_Discriminants (Spec_Id);
+ end if;
+
elsif Is_Generic_Subprogram (Spec_Id) then
Install_Generic_Formals (Spec_Id);
+
else
Install_Formals (Spec_Id);
end if;
@@ -20040,7 +20174,7 @@
Add_Str_To_Name_Buffer ("package");
elsif Ekind_In (E, E_Protected_Body, E_Protected_Type) then
- Add_Str_To_Name_Buffer ("protected unit");
+ Add_Str_To_Name_Buffer ("protected type");
elsif Ekind_In (E, E_Function,
E_Generic_Function,
@@ -20052,7 +20186,7 @@
else
pragma Assert (Ekind_In (E, E_Task_Body, E_Task_Type));
- Add_Str_To_Name_Buffer ("task unit");
+ Add_Str_To_Name_Buffer ("task type");
end if;
end Add_Entity_To_Name_Buffer;
@@ -23030,17 +23164,19 @@
-- 1) Both items denote null
-- 2) Dep_Item denotes null and Ref_Item is Empty (special case)
-- 3) Both items denote attribute 'Result
- -- 4) Both items denote the same formal parameter
- -- 5) Both items denote the same object
- -- 6) Dep_Item is an abstract state with visible null refinement
+ -- 4) Both items denote the same object
+ -- 5) Both items denote the same formal parameter
+ -- 6) Both items denote the same current instance of a type
+ -- 7) Both items denote the same discriminant
+ -- 8) Dep_Item is an abstract state with visible null refinement
-- and Ref_Item denotes null.
- -- 7) Dep_Item is an abstract state with visible null refinement
+ -- 9) Dep_Item is an abstract state with visible null refinement
-- and Ref_Item is Empty (special case).
- -- 8) Dep_Item is an abstract state with visible non-null
+ -- 10) Dep_Item is an abstract state with visible non-null
-- refinement and Ref_Item denotes one of its constituents.
- -- 9) Dep_Item is an abstract state without a visible refinement
+ -- 11) Dep_Item is an abstract state without a visible refinement
-- and Ref_Item denotes the same state.
- -- When scenario 8 is in effect, the entity of the abstract state
+ -- When scenario 10 is in effect, the entity of the abstract state
-- denoted by Dep_Item is added to list Refined_States.
procedure Record_Item (Item_Id : Entity_Id);
@@ -23127,7 +23263,8 @@
then
Matched := True;
- -- Abstract states, formal parameters and objects
+ -- Abstract states, current instances of concurrent types,
+ -- discriminants, formal parameters and objects.
elsif Is_Entity_Name (Dep_Item) then
@@ -23175,7 +23312,8 @@
Matched := True;
end if;
- -- A formal parameter or an object matches itself
+ -- A current instance of a concurrent type, discriminant,
+ -- formal parameter or an object matches itself.
elsif Is_Entity_Name (Ref_Item)
and then Entity_Of (Ref_Item) = Dep_Item_Id
@@ -26364,7 +26502,7 @@
Depends : Node_Id;
Formal : Entity_Id;
Global : Node_Id;
- List : Node_Id;
+ Typ : Entity_Id;
-- Start of processing for Collect_Subprogram_Inputs_Outputs
@@ -26425,22 +26563,8 @@
if Present (Global) then
Global_Seen := True;
- List := Expression (Get_Argument (Global, Spec_Id));
+ Collect_Global_List (Expression (Get_Argument (Global, Spec_Id)));
- -- The pragma may not have been analyzed because of the arbitrary
- -- declaration order of aspects. Make sure that it is analyzed for
- -- the purposes of item extraction.
-
- if not Analyzed (List) then
- if Pragma_Name (Global) = Name_Refined_Global then
- Analyze_Refined_Global_In_Decl_Part (Global);
- else
- Analyze_Global_In_Decl_Part (Global);
- end if;
- end if;
-
- Collect_Global_List (List);
-
-- When the related subprogram lacks pragma [Refined_]Global, fall back
-- to [Refined_]Depends if the caller requests this behavior. Synthesize
-- the inputs and outputs from [Refined_]Depends.
@@ -26463,6 +26587,45 @@
Collect_Dependency_Clause (Clauses);
end if;
end if;
+
+ if Ekind (Scope (Spec_Id)) = E_Protected_Type then
+ Typ := Scope (Spec_Id);
+
+ -- A single protected type declaration does not have a current
+ -- instance because the type is technically an object.
+
+ if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then
+ null;
+
+ -- Otherwise the current instance of the protected type acts as a
+ -- formal parameter of mode IN for functions and IN OUT for entries
+ -- and procedures (SPARK RM 6.1.4).
+
+ else
+ Append_New_Elmt (Typ, Subp_Inputs);
+
+ if Ekind_In (Spec_Id, E_Entry, E_Entry_Family, E_Procedure) then
+ Append_New_Elmt (Typ, Subp_Outputs);
+ end if;
+ end if;
+
+ elsif Ekind (Spec_Id) = E_Task_Type then
+ Typ := Spec_Id;
+
+ -- A single task type declaration does not have a current instance
+ -- because the type is technically an object.
+
+ if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then
+ null;
+
+ -- Otherwise the current instance of the task type acts as a formal
+ -- parameter of mode IN OUT (SPARK RM 6.1.4).
+
+ else
+ Append_New_Elmt (Typ, Subp_Inputs);
+ Append_New_Elmt (Typ, Subp_Outputs);
+ end if;
+ end if;
end Collect_Subprogram_Inputs_Outputs;
---------------------------------
@@ -27022,6 +27185,31 @@
return Add_Config_Static_String (Arg);
end Is_Config_Static_String;
+ ---------------------
+ -- Is_CCT_Instance --
+ ---------------------
+
+ function Is_CCT_Instance (Ref : Node_Id) return Boolean is
+ Ref_Id : constant Entity_Id := Entity (Ref);
+ S : Entity_Id;
+
+ begin
+ -- Climb the scope chain looking for an enclosing concurrent type that
+ -- matches the referenced entity.
+
+ S := Current_Scope;
+ while Present (S) and then S /= Standard_Standard loop
+ if Ekind_In (S, E_Protected_Type, E_Task_Type) and then S = Ref_Id
+ then
+ return True;
+ end if;
+
+ S := Scope (S);
+ end loop;
+
+ return False;
+ end Is_CCT_Instance;
+
-------------------------------
-- Is_Elaboration_SPARK_Mode --
-------------------------------
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 229362)
+++ sem_prag.ads (working copy)
@@ -300,9 +300,10 @@
-- and Subp_Outputs (outputs). The inputs and outputs are gathered from:
-- 1) The formal parameters of the subprogram
-- 2) The generic formal parameters of the generic subprogram
- -- 3) The items of pragma [Refined_]Global
+ -- 3) The current instance of a concurrent type
+ -- 4) The items of pragma [Refined_]Global
-- or
- -- 4) The items of pragma [Refined_]Depends if there is no pragma
+ -- 5) The items of pragma [Refined_]Depends if there is no pragma
-- [Refined_]Global present and flag Synthesize is set to True.
-- If the subprogram has no inputs and/or outputs, then the returned list
-- is No_Elist. Flag Global_Seen is set when the related subprogram has
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 229359)
+++ sem_util.adb (working copy)
@@ -6347,7 +6347,10 @@
-- Follow a possible chain of renamings to reach the root renamed
-- object.
- while Present (Id) and then Present (Renamed_Object (Id)) loop
+ while Present (Id)
+ and then Is_Object (Id)
+ and then Present (Renamed_Object (Id))
+ loop
if Is_Entity_Name (Renamed_Object (Id)) then
Id := Entity (Renamed_Object (Id));
else
@@ -7113,7 +7116,7 @@
Res_Index := Res_Index + 5;
elsif Is_Task then
- Res (Res_Index .. Res_Index + 8) := "task unit";
+ Res (Res_Index .. Res_Index + 8) := "task type";
Res_Index := Res_Index + 9;
else
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 229357)
+++ sem_util.ads (working copy)
@@ -770,7 +770,7 @@
-- the Ekind of Id as follows:
-- * Replace "subprogram" with
-- - "entry" when Id is an entry [family]
- -- - "task unit" when Id is a single task object, task type or task
+ -- - "task type" when Id is a single task object, task type or task
-- body.
-- * Replace "protected" with
-- - "task" when Id is a single task object, task type or task body
Index: contracts.adb
===================================================================
--- contracts.adb (revision 229357)
+++ contracts.adb (working copy)
@@ -578,6 +578,39 @@
end if;
end Analyze_Entry_Or_Subprogram_Contract;
+ ------------------------------------------
+ -- Analyze_Initial_Declaration_Contract --
+ ------------------------------------------
+
+ procedure Analyze_Initial_Declaration_Contract (Body_Decl : Node_Id) is
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
+
+ begin
+ -- Note that stubs are excluded because the compiler always analyzes the
+ -- proper body when a stub is encountered.
+
+ if Nkind (Body_Decl) = N_Entry_Body then
+ Analyze_Entry_Or_Subprogram_Contract (Spec_Id);
+
+ elsif Nkind (Body_Decl) = N_Package_Body then
+ Analyze_Package_Contract (Spec_Id);
+
+ elsif Nkind (Body_Decl) = N_Protected_Body then
+ Analyze_Protected_Contract (Spec_Id);
+
+ elsif Nkind (Body_Decl) = N_Subprogram_Body then
+ if Present (Corresponding_Spec (Body_Decl)) then
+ Analyze_Entry_Or_Subprogram_Contract (Spec_Id);
+ end if;
+
+ elsif Nkind (Body_Decl) = N_Task_Body then
+ Analyze_Task_Contract (Spec_Id);
+
+ else
+ raise Program_Error;
+ end if;
+ end Analyze_Initial_Declaration_Contract;
+
-----------------------------
-- Analyze_Object_Contract --
-----------------------------
Index: contracts.ads
===================================================================
--- contracts.ads (revision 229357)
+++ contracts.ads (working copy)
@@ -58,7 +58,7 @@
-- Volatile_Function
procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id);
- -- Analyze the contract of the nearest package body (if any) enclosing
+ -- Analyze the contract of the nearest package body (if any) which encloses
-- package or subprogram body Body_Decl.
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
@@ -86,6 +86,10 @@
-- Precondition
-- Test_Case
+ procedure Analyze_Initial_Declaration_Contract (Body_Decl : Node_Id);
+ -- Analyze the contract of the initial declaration of entry body, package
+ -- body, protected body, subprogram body or task body Body_Decl.
+
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
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 229343)
+++ sem_ch6.adb (working copy)
@@ -1378,6 +1378,15 @@
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
+ -- A generic subprogram body "freezes" the contract of its initial
+ -- declaration. This analysis depends on attribute Corresponding_Spec
+ -- being set. Only bodies coming from source should cause this type
+ -- of "freezing".
+
+ if Comes_From_Source (N) then
+ Analyze_Initial_Declaration_Contract (N);
+ end if;
+
Analyze_Declarations (Declarations (N));
Check_Completion;
@@ -3756,6 +3765,14 @@
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
+ -- A subprogram body "freezes" the contract of its initial declaration.
+ -- This analysis depends on attribute Corresponding_Spec being set. Only
+ -- bodies coming from source should cause this type of "freezing".
+
+ if Comes_From_Source (N) then
+ Analyze_Initial_Declaration_Contract (N);
+ end if;
+
Analyze_Declarations (Declarations (N));
-- Verify that the SPARK_Mode of the body agrees with that of its spec
Index: atree.adb
===================================================================
--- atree.adb (revision 229357)
+++ atree.adb (working copy)
@@ -1126,6 +1126,60 @@
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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : 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 or else
+ T = V8 or else
+ T = V9 or else
+ T = V10;
+ 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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : Entity_Kind;
+ V11 : 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 or else
+ T = V8 or else
+ T = V9 or else
+ T = V10 or else
+ T = V11;
+ end Ekind_In;
+
+ function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
V2 : Entity_Kind) return Boolean
@@ -1225,6 +1279,42 @@
return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9);
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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : Entity_Kind) return Boolean
+ is
+ begin
+ return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9, V10);
+ 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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : Entity_Kind;
+ V11 : Entity_Kind) return Boolean
+ is
+ begin
+ return
+ Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11);
+ end Ekind_In;
+
------------------------
-- Set_Reporting_Proc --
------------------------
Index: atree.ads
===================================================================
--- atree.ads (revision 229357)
+++ atree.ads (working copy)
@@ -803,6 +803,33 @@
V9 : 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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : 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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : Entity_Kind;
+ V11 : Entity_Kind) return Boolean;
+
+ function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
V2 : Entity_Kind) return Boolean;
@@ -870,6 +897,33 @@
V8 : Entity_Kind;
V9 : 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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : 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;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind;
+ V10 : Entity_Kind;
+ V11 : Entity_Kind) return Boolean;
+
pragma Inline (Ekind_In);
-- Inline all above functions
