===================================================================
@@ -2495,55 +2495,11 @@
Analyze_Package_Body_Contract (Defining_Entity (Context));
end if;
- -- Analyze the contracts of eligible constructs (see below) due to
- -- the delayed visibility needs of their aspects and pragmas.
+ -- Analyze the contracts of various constructs now due to the delayed
+ -- visibility needs of their aspects and pragmas.
- Decl := First (L);
- while Present (Decl) loop
+ Analyze_Contracts (L);
- -- Entry or subprogram declarations
-
- if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
- N_Entry_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration)
- then
- Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
-
- -- Entry or subprogram bodies
-
- elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
- Analyze_Entry_Or_Subprogram_Body_Contract
- (Defining_Entity (Decl));
-
- -- Objects
-
- elsif Nkind (Decl) = N_Object_Declaration then
- Analyze_Object_Contract (Defining_Entity (Decl));
-
- -- Protected untis
-
- elsif Nkind_In (Decl, N_Protected_Type_Declaration,
- N_Single_Protected_Declaration)
- then
- Analyze_Protected_Contract (Defining_Entity (Decl));
-
- -- Subprogram body stubs
-
- elsif Nkind (Decl) = N_Subprogram_Body_Stub then
- Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
-
- -- Task units
-
- elsif Nkind_In (Decl, N_Single_Task_Declaration,
- N_Task_Type_Declaration)
- then
- Analyze_Task_Contract (Defining_Entity (Decl));
- end if;
-
- Next (Decl);
- end loop;
-
if Nkind (Context) = N_Package_Body then
-- Ensure that all abstract states and objects declared in the
===================================================================
@@ -543,7 +543,8 @@
begin
-- A [generic] package body "freezes" the contract of the nearest
- -- enclosing package body:
+ -- enclosing package body and all other contracts encountered in the
+ -- same declarative part upto and excluding the package body:
-- package body Nearest_Enclosing_Package
-- with Refined_State => (State => Constit)
@@ -567,7 +568,7 @@
-- Only bodies coming from source should cause this type of "freezing"
if Comes_From_Source (N) then
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
end if;
-- Find corresponding package specification, and establish the current
@@ -767,10 +768,6 @@
-- 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));
===================================================================
@@ -1192,12 +1192,13 @@
Entry_Name : Entity_Id;
begin
- -- An entry 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.
+ -- An entry body "freezes" the contract of the nearest enclosing package
+ -- body and all other contracts encountered in the same declarative part
+ -- upto and excluding the entry body. This ensures that any 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);
+ Analyze_Previous_Contracts (N);
Tasking_Used := True;
@@ -1354,11 +1355,6 @@
(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);
@@ -1772,11 +1768,13 @@
begin
-- A protected 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.
+ -- package body and all other contracts encountered in the same
+ -- declarative part upto and excluding the protected body. This ensures
+ -- that any 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);
+ Analyze_Previous_Contracts (N);
Tasking_Used := True;
Set_Ekind (Body_Id, E_Protected_Body);
@@ -1819,11 +1817,6 @@
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
@@ -2816,11 +2809,12 @@
begin
-- A task body "freezes" the contract of the nearest enclosing package
- -- body. This ensures that annotations referenced by the contract of an
- -- entry or subprogram body declared within the current protected body
- -- are available.
+ -- body and all other contracts encountered in the same declarative part
+ -- upto and excluding the task 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);
+ Analyze_Previous_Contracts (N);
Tasking_Used := True;
Set_Scope (Body_Id, Current_Scope);
@@ -2882,11 +2876,6 @@
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);
===================================================================
@@ -208,6 +208,14 @@
-- corresponding constituent from list Constits (if any) appear in the same
-- context denoted by Context. If this is the case, emit an error.
+ procedure Contract_Freeze_Error
+ (Contract_Id : Entity_Id;
+ Freeze_Id : Entity_Id);
+ -- Subsidiary to the analysis of pragmas Contract_Cases, Part_Of, Post, and
+ -- Pre. Emit a freezing-related error message where Freeze_Id is the entity
+ -- of a body which caused contract "freezing" and Contract_Id denotes the
+ -- entity of the affected contstruct.
+
procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id);
-- Subsidiary to all Find_Related_xxx routines. Emit an error on pragma
-- Prag that duplicates previous pragma Prev.
@@ -341,8 +349,16 @@
-- Analyze_Contract_Cases_In_Decl_Part --
-----------------------------------------
- procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Contract_Cases_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
+
Others_Seen : Boolean := False;
+ -- This flag is set when an "others" choice is encountered. It is used
+ -- to detect multiple illegal occurences of "others".
procedure Analyze_Contract_Case (CCase : Node_Id);
-- Verify the legality of a single contract case
@@ -354,6 +370,7 @@
procedure Analyze_Contract_Case (CCase : Node_Id) is
Case_Guard : Node_Id;
Conseq : Node_Id;
+ Errors : Nat;
Extra_Guard : Node_Id;
begin
@@ -390,11 +407,35 @@
-- Preanalyze the case guard and consequence
if Nkind (Case_Guard) /= N_Others_Choice then
+ Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+
+ -- Emit a clarification message when the case guard contains
+ -- at leat one undefined reference, possibly due to contract
+ -- "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Case_Guard)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
end if;
+ Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
+ -- Emit a clarification message when the consequence contains
+ -- at leat one undefined reference, possibly due to contract
+ -- "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Conseq)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
+
-- The contract case is malformed
else
@@ -404,9 +445,7 @@
-- Local variables
- 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));
+ CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
@@ -594,10 +633,14 @@
elsif Ekind (Item_Id) = E_Loop_Parameter then
Add_Str_To_Name_Buffer ("loop parameter");
- elsif Ekind (Item_Id) = E_Protected_Type then
+ elsif Ekind (Item_Id) = E_Protected_Type
+ or else Is_Single_Protected_Object (Item_Id)
+ then
Add_Str_To_Name_Buffer ("current instance of protected type");
- elsif Ekind (Item_Id) = E_Task_Type then
+ elsif Ekind (Item_Id) = E_Task_Type
+ or else Is_Single_Task_Object (Item_Id)
+ then
Add_Str_To_Name_Buffer ("current instance of task type");
elsif Ekind (Item_Id) = E_Variable then
@@ -3162,7 +3205,13 @@
-- Analyze_Part_Of_In_Decl_Part --
----------------------------------
- procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Part_Of_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
+ Encap : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Errors : constant Nat := Serious_Errors_Detected;
Var_Decl : constant Node_Id := Find_Related_Context (N);
Var_Id : constant Entity_Id := Defining_Entity (Var_Decl);
Encap_Id : Entity_Id;
@@ -3176,7 +3225,7 @@
Analyze_Part_Of
(Indic => N,
Item_Id => Var_Id,
- Encap => Get_Pragma_Arg (First (Pragma_Argument_Associations (N))),
+ Encap => Encap,
Encap_Id => Encap_Id,
Legal => Legal);
@@ -3189,6 +3238,16 @@
Append_Elmt (Var_Id, Part_Of_Constituents (Encap_Id));
Set_Encapsulating_State (Var_Id, Encap_Id);
end if;
+
+ -- Emit a clarification message when the encapsulator is undefined,
+ -- possibly due to contract "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Encap)
+ then
+ Contract_Freeze_Error (Var_Id, Freeze_Id);
+ end if;
end Analyze_Part_Of_In_Decl_Part;
--------------------
@@ -20430,9 +20489,7 @@
-- Obj : Anon_Task_Typ;
-- pragma SPARK_Mode ...;
- if Is_Single_Concurrent_Object (Spec_Id)
- and then Ekind (Spec_Typ) = E_Task_Type
- then
+ if Is_Single_Task_Object (Spec_Id) then
Set_SPARK_Pragma (Spec_Typ, N);
Set_SPARK_Pragma_Inherited (Spec_Typ, False);
Set_SPARK_Aux_Pragma (Spec_Typ, N);
@@ -22980,7 +23037,10 @@
-- Analyze_Pre_Post_Condition_In_Decl_Part --
---------------------------------------------
- procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
procedure Process_Class_Wide_Condition
(Expr : Node_Id;
Spec_Id : Entity_Id;
@@ -23134,6 +23194,7 @@
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Errors : Nat;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
@@ -23166,8 +23227,19 @@
end if;
end if;
+ Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+ -- Emit a clarification message when the expression contains at leat one
+ -- undefined reference, possibly due to contract "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Expr)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
+
-- For a class-wide condition, a reference to a controlling formal must
-- be interpreted as having the class-wide type (or an access to such)
-- so that the inherited condition can be properly applied to any
@@ -25874,11 +25946,6 @@
Report_Unrefined_States (Available_States);
- -- Ensure that all abstract states and objects declared in the body
- -- state space of the related package are utilized as constituents.
-
- Report_Unused_Body_States (Body_Id, Body_States);
-
Set_Is_Analyzed_Pragma (N);
end Analyze_Refined_State_In_Decl_Part;
@@ -26631,13 +26698,13 @@
-- Local variables
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Clause : Node_Id;
Clauses : Node_Id;
Depends : Node_Id;
Formal : Entity_Id;
Global : Node_Id;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
Typ : Entity_Id;
-- Start of processing for Collect_Subprogram_Inputs_Outputs
@@ -26645,37 +26712,61 @@
begin
Global_Seen := False;
- -- Process all [generic] formal parameters
+ -- Process all formal parameters of entries, [generic] subprograms and
+ -- their bodies.
- Formal := First_Entity (Spec_Id);
- while Present (Formal) loop
- if Ekind_In (Formal, E_Generic_In_Parameter,
- E_In_Out_Parameter,
- E_In_Parameter)
- then
- Append_New_Elmt (Formal, Subp_Inputs);
- end if;
+ if Ekind_In (Subp_Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Procedure,
+ E_Subprogram_Body)
+ then
+ Subp_Decl := Unit_Declaration_Node (Subp_Id);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
- if Ekind_In (Formal, E_Generic_In_Out_Parameter,
- E_In_Out_Parameter,
- E_Out_Parameter)
- then
- Append_New_Elmt (Formal, Subp_Outputs);
+ -- Process all [generic] formal parameters
- -- Out parameters can act as inputs when the related type is
- -- tagged, unconstrained array, unconstrained record or record
- -- with unconstrained components.
-
- if Ekind (Formal) = E_Out_Parameter
- and then Is_Unconstrained_Or_Tagged_Item (Formal)
+ Formal := First_Entity (Spec_Id);
+ while Present (Formal) loop
+ if Ekind_In (Formal, E_Generic_In_Parameter,
+ E_In_Out_Parameter,
+ E_In_Parameter)
then
Append_New_Elmt (Formal, Subp_Inputs);
end if;
- end if;
- Next_Entity (Formal);
- end loop;
+ if Ekind_In (Formal, E_Generic_In_Out_Parameter,
+ E_In_Out_Parameter,
+ E_Out_Parameter)
+ then
+ Append_New_Elmt (Formal, Subp_Outputs);
+ -- Out parameters can act as inputs when the related type is
+ -- tagged, unconstrained array, unconstrained record or record
+ -- with unconstrained components.
+
+ if Ekind (Formal) = E_Out_Parameter
+ and then Is_Unconstrained_Or_Tagged_Item (Formal)
+ then
+ Append_New_Elmt (Formal, Subp_Inputs);
+ end if;
+ end if;
+
+ Next_Entity (Formal);
+ end loop;
+
+ -- Otherwise the input denotes a task type, a task body, or the
+ -- anonymous object created for a single task type.
+
+ elsif Ekind_In (Subp_Id, E_Task_Type, E_Task_Body)
+ or else Is_Single_Task_Object (Subp_Id)
+ then
+ Subp_Decl := Declaration_Node (Subp_Id);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ end if;
+
-- When processing an entry, subprogram or task body, look for pragmas
-- Refined_Depends and Refined_Global as they specify the inputs and
-- outputs.
@@ -26724,46 +26815,64 @@
end if;
end if;
+ -- The current instance of a protected type acts as a formal parameter
+ -- of mode IN for functions and IN OUT for entries and procedures
+ -- (SPARK RM 6.1.4).
+
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.
+ -- Use the anonymous object when the type is single protected
if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then
- null;
+ Typ := Anonymous_Object (Typ);
+ end if;
- -- 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).
+ Append_New_Elmt (Typ, Subp_Inputs);
- 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;
+ if Ekind_In (Spec_Id, E_Entry, E_Entry_Family, E_Procedure) then
+ Append_New_Elmt (Typ, Subp_Outputs);
end if;
+ -- The current instance of a task type acts as a formal parameter of
+ -- mode IN OUT (SPARK RM 6.1.4).
+
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.
+ -- Use the anonymous object when the type is single task
if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then
- null;
+ Typ := Anonymous_Object (Typ);
+ end if;
- -- Otherwise the current instance of the task type acts as a formal
- -- parameter of mode IN OUT (SPARK RM 6.1.4).
+ Append_New_Elmt (Typ, Subp_Inputs);
+ Append_New_Elmt (Typ, Subp_Outputs);
- else
- Append_New_Elmt (Typ, Subp_Inputs);
- Append_New_Elmt (Typ, Subp_Outputs);
- end if;
+ elsif Is_Single_Task_Object (Spec_Id) then
+ Append_New_Elmt (Spec_Id, Subp_Inputs);
+ Append_New_Elmt (Spec_Id, Subp_Outputs);
end if;
end Collect_Subprogram_Inputs_Outputs;
+ ---------------------------
+ -- Contract_Freeze_Error --
+ ---------------------------
+
+ procedure Contract_Freeze_Error
+ (Contract_Id : Entity_Id;
+ Freeze_Id : Entity_Id)
+ is
+ begin
+ Error_Msg_Name_1 := Chars (Contract_Id);
+ Error_Msg_Sloc := Sloc (Freeze_Id);
+
+ SPARK_Msg_NE
+ ("body & declared # freezes the contract of%", Contract_Id, Freeze_Id);
+ SPARK_Msg_N
+ ("\all contractual items must be declared before body #", Contract_Id);
+ end Contract_Freeze_Error;
+
---------------------------------
-- Delay_Config_Pragma_Analyze --
---------------------------------
===================================================================
@@ -181,8 +181,12 @@
procedure Analyze_Pragma (N : Node_Id);
-- Analyze procedure for pragma reference node N
- procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of delayed pragma Contract_Cases
+ procedure Analyze_Contract_Cases_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Contract_Cases. Freeze_Id is the
+ -- entity of [generic] package body or [generic] subprogram body which
+ -- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Depends. This routine is also
@@ -205,11 +209,20 @@
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
- procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of delayed pragma Part_Of
+ procedure Analyze_Part_Of_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Part_Of. Freeze_Id is the entity
+ -- of [generic] package body or [generic] subprogram body which caused the
+ -- "freezing" of the related contract where the pragma resides.
- procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of pragmas Precondition and Postcondition
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of pragmas Precondition and Postcondition.
+ -- Freeze_Id denotes the entity of [generic] package body or [generic]
+ -- subprogram body which caused "freezing" of the related contract where
+ -- the pragma resides.
procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
-- Preform full analysis of delayed pragma Refined_Depends. This routine
===================================================================
@@ -3717,17 +3717,15 @@
------------------------------
procedure Check_Unused_Body_States (Body_Id : Entity_Id) is
- Legal_Constits : Boolean := True;
- -- This flag designates whether all constituents of pragma Refined_State
- -- are legal. The flag is used to suppress the generation of potentially
- -- misleading error messages due to a malformed pragma.
-
procedure Process_Refinement_Clause
(Clause : Node_Id;
States : Elist_Id);
-- Inspect all constituents of refinement clause Clause and remove any
-- matches from body state list States.
+ procedure Report_Unused_Body_States (States : Elist_Id);
+ -- Emit errors for each abstract state or object found in list States
+
-------------------------------
-- Process_Refinement_Clause --
-------------------------------
@@ -3747,10 +3745,6 @@
Constit_Id : Entity_Id;
begin
- if Error_Posted (Constit) then
- Legal_Constits := False;
- end if;
-
-- Guard against illegal constituents. Only abstract states and
-- objects can appear on the right hand side of a refinement.
@@ -3794,10 +3788,63 @@
end if;
end Process_Refinement_Clause;
+ -------------------------------
+ -- Report_Unused_Body_States --
+ -------------------------------
+
+ procedure Report_Unused_Body_States (States : Elist_Id) is
+ Posted : Boolean := False;
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ if Present (States) then
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ -- Constants are part of the hidden state of a package, but the
+ -- compiler cannot determine whether they have variable input
+ -- (SPARK RM 7.1.1(2)) and cannot classify them properly as a
+ -- hidden state. Do not emit an error when a constant does not
+ -- participate in a state refinement, even though it acts as a
+ -- hidden state.
+
+ if Ekind (State_Id) = E_Constant then
+ null;
+
+ -- Generate an error message of the form:
+
+ -- body of package ... has unused hidden states
+ -- abstract state ... defined at ...
+ -- variable ... defined at ...
+
+ else
+ if not Posted then
+ Posted := True;
+ SPARK_Msg_N
+ ("body of package & has unused hidden states", Body_Id);
+ end if;
+
+ Error_Msg_Sloc := Sloc (State_Id);
+
+ if Ekind (State_Id) = E_Abstract_State then
+ SPARK_Msg_NE
+ ("\abstract state & defined #", Body_Id, State_Id);
+
+ else
+ SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
+ end if;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Report_Unused_Body_States;
+
-- Local variables
- Prag : constant Node_Id :=
- Get_Pragma (Body_Id, Pragma_Refined_State);
+ Prag : constant Node_Id := Get_Pragma (Body_Id, Pragma_Refined_State);
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
Clause : Node_Id;
States : Elist_Id;
@@ -3806,8 +3853,8 @@
begin
-- Inspect the clauses of pragma Refined_State and determine whether all
- -- visible states declared within the body of the package participate in
- -- the refinement.
+ -- visible states declared within the package body participate in the
+ -- refinement.
if Present (Prag) then
Clause := Expression (Get_Argument (Prag, Spec_Id));
@@ -3828,12 +3875,10 @@
Process_Refinement_Clause (Clause, States);
end if;
- -- Ensure that all abstract states and objects declared in the body
- -- state space of the related package are utilized as constituents.
+ -- Ensure that all abstract states and objects declared in the
+ -- package body state space are utilized as constituents.
- if Legal_Constits then
- Report_Unused_Body_States (Body_Id, States);
- end if;
+ Report_Unused_Body_States (States);
end if;
end Check_Unused_Body_States;
@@ -3842,6 +3887,10 @@
-------------------------
function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id is
+ function Is_Visible_Object (Obj_Id : Entity_Id) return Boolean;
+ -- Determine whether object Obj_Id is a suitable visible state of a
+ -- package body.
+
procedure Collect_Visible_States
(Pack_Id : Entity_Id;
States : in out Elist_Id);
@@ -3874,13 +3923,8 @@
elsif Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States);
- -- Do not consider objects that map generic formals to their
- -- actuals, as the formals cannot be named from the outside and
- -- participate in refinement.
-
elsif Ekind_In (Item_Id, E_Constant, E_Variable)
- and then No (Corresponding_Generic_Association
- (Declaration_Node (Item_Id)))
+ and then Is_Visible_Object (Item_Id)
then
Append_New_Elmt (Item_Id, States);
@@ -3894,6 +3938,34 @@
end loop;
end Collect_Visible_States;
+ -----------------------
+ -- Is_Visible_Object --
+ -----------------------
+
+ function Is_Visible_Object (Obj_Id : Entity_Id) return Boolean is
+ begin
+ -- Objects that map generic formals to their actuals are not visible
+ -- from outside the generic instantiation.
+
+ if Present (Corresponding_Generic_Association
+ (Declaration_Node (Obj_Id)))
+ then
+ return False;
+
+ -- Constituents of a single protected/task type act as components of
+ -- the type and are not visible from outside the type.
+
+ elsif Ekind (Obj_Id) = E_Variable
+ and then Present (Encapsulating_State (Obj_Id))
+ and then Is_Single_Concurrent_Object (Encapsulating_State (Obj_Id))
+ then
+ return False;
+
+ else
+ return True;
+ end if;
+ end Is_Visible_Object;
+
-- Local variables
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
@@ -3905,7 +3977,9 @@
begin
-- Inspect the declarations of the body looking for source objects,
- -- packages and package instantiations.
+ -- packages and package instantiations. Note that even though this
+ -- processing is very similar to Collect_Visible_States, a package
+ -- body does not have a First/Next_Entity list.
Decl := First (Declarations (Body_Decl));
while Present (Decl) loop
@@ -3916,7 +3990,9 @@
if Nkind (Decl) = N_Object_Declaration then
Item_Id := Defining_Entity (Decl);
- if Comes_From_Source (Item_Id) then
+ if Comes_From_Source (Item_Id)
+ and then Is_Visible_Object (Item_Id)
+ then
Append_New_Elmt (Item_Id, States);
end if;
@@ -7254,8 +7330,7 @@
function Fix_Msg (Id : Entity_Id; Msg : String) return String is
Is_Task : constant Boolean :=
Ekind_In (Id, E_Task_Body, E_Task_Type)
- or else (Is_Single_Concurrent_Object (Id)
- and then Ekind (Etype (Id)) = E_Task_Type);
+ or else Is_Single_Task_Object (Id);
Msg_Last : constant Natural := Msg'Last;
Msg_Index : Natural;
Res : String (Msg'Range) := (others => ' ');
@@ -9993,6 +10068,47 @@
end if;
end Has_Tagged_Component;
+ -----------------------------
+ -- Has_Undefined_Reference --
+ -----------------------------
+
+ function Has_Undefined_Reference (Expr : Node_Id) return Boolean is
+ Has_Undef_Ref : Boolean := False;
+ -- Flag set when expression Expr contains at least one undefined
+ -- reference.
+
+ function Is_Undefined_Reference (N : Node_Id) return Traverse_Result;
+ -- Determine whether N denotes a reference and if it does, whether it is
+ -- undefined.
+
+ ----------------------------
+ -- Is_Undefined_Reference --
+ ----------------------------
+
+ function Is_Undefined_Reference (N : Node_Id) return Traverse_Result is
+ begin
+ if Is_Entity_Name (N)
+ and then Present (Entity (N))
+ and then Entity (N) = Any_Id
+ then
+ Has_Undef_Ref := True;
+ return Abandon;
+ end if;
+
+ return OK;
+ end Is_Undefined_Reference;
+
+ procedure Find_Undefined_References is
+ new Traverse_Proc (Is_Undefined_Reference);
+
+ -- Start of processing for Has_Undefined_Reference
+
+ begin
+ Find_Undefined_References (Expr);
+
+ return Has_Undef_Ref;
+ end Has_Undefined_Reference;
+
----------------------------
-- Has_Volatile_Component --
----------------------------
@@ -13414,8 +13530,7 @@
function Is_Single_Concurrent_Object (Id : Entity_Id) return Boolean is
begin
return
- Ekind (Id) = E_Variable
- and then Is_Single_Concurrent_Type (Etype (Id));
+ Is_Single_Protected_Object (Id) or else Is_Single_Task_Object (Id);
end Is_Single_Concurrent_Object;
-------------------------------
@@ -13456,6 +13571,30 @@
and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_7);
end Is_Single_Precision_Floating_Point_Type;
+ --------------------------------
+ -- Is_Single_Protected_Object --
+ --------------------------------
+
+ function Is_Single_Protected_Object (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind (Id) = E_Variable
+ and then Ekind (Etype (Id)) = E_Protected_Type
+ and then Is_Single_Concurrent_Type (Etype (Id));
+ end Is_Single_Protected_Object;
+
+ ---------------------------
+ -- Is_Single_Task_Object --
+ ---------------------------
+
+ function Is_Single_Task_Object (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind (Id) = E_Variable
+ and then Ekind (Etype (Id)) = E_Task_Type
+ and then Is_Single_Concurrent_Type (Etype (Id));
+ end Is_Single_Task_Object;
+
-------------------------------------
-- Is_SPARK_05_Initialization_Expr --
-------------------------------------
@@ -17634,63 +17773,6 @@
(Boolean_Literals (not Range_Checks_Suppressed (E)), Loc);
end Rep_To_Pos_Flag;
- -------------------------------
- -- Report_Unused_Body_States --
- -------------------------------
-
- procedure Report_Unused_Body_States
- (Body_Id : Entity_Id;
- States : Elist_Id)
- is
- Posted : Boolean := False;
- State_Elmt : Elmt_Id;
- State_Id : Entity_Id;
-
- begin
- if Present (States) then
- State_Elmt := First_Elmt (States);
- while Present (State_Elmt) loop
- State_Id := Node (State_Elmt);
-
- -- Constants are part of the hidden state of a package, but the
- -- compiler cannot determine whether they have variable input
- -- (SPARK RM 7.1.1(2)) and cannot classify them properly as a
- -- hidden state. Do not emit an error when a constant does not
- -- participate in a state refinement, even though it acts as a
- -- hidden state.
-
- if Ekind (State_Id) = E_Constant then
- null;
-
- -- Generate an error message of the form:
-
- -- body of package ... has unused hidden states
- -- abstract state ... defined at ...
- -- variable ... defined at ...
-
- else
- if not Posted then
- Posted := True;
- SPARK_Msg_N
- ("body of package & has unused hidden states", Body_Id);
- end if;
-
- Error_Msg_Sloc := Sloc (State_Id);
-
- if Ekind (State_Id) = E_Abstract_State then
- SPARK_Msg_NE
- ("\abstract state & defined #", Body_Id, State_Id);
-
- else
- SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
- end if;
- end if;
-
- Next_Elmt (State_Elmt);
- end loop;
- end if;
- end Report_Unused_Body_States;
-
--------------------
-- Require_Entity --
--------------------
===================================================================
@@ -57,6 +57,9 @@
-- for the current unit. The declarations are added in the current scope,
-- so the caller should push a new scope as required before the call.
+ function Add_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
+ -- Returns the name of E adding Suffix
+
function Address_Integer_Convert_OK (T1, T2 : Entity_Id) return Boolean;
-- Given two types, returns True if we are in Allow_Integer_Address mode
-- and one of the types is (a descendent of) System.Address (and this type
@@ -327,14 +330,10 @@
-- and post-state.
procedure Check_Unused_Body_States (Body_Id : Entity_Id);
- -- Verify that all abstract states and object declared in the state space
- -- of a package body denoted by entity Body_Id are used as constituents.
- -- Emit an error if this is not the case.
+ -- Verify that all abstract states and objects declared in the state space
+ -- of package body Body_Id are used as constituents. Emit an error if this
+ -- is not the case.
- function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id;
- -- Gather the entities of all abstract states and objects declared in the
- -- body state space of package body Body_Id.
-
procedure Check_Unprotected_Access
(Context : Node_Id;
Expr : Node_Id);
@@ -342,6 +341,10 @@
-- and the context is external to the protected operation, to warn against
-- a possible unlocked access to data.
+ function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id;
+ -- Gather the entities of all abstract states and objects declared in the
+ -- body state space of package body Body_Id.
+
procedure Collect_Interfaces
(T : Entity_Id;
Ifaces_List : out Elist_Id;
@@ -1113,12 +1116,6 @@
function Has_Suffix (E : Entity_Id; Suffix : Character) return Boolean;
-- Returns true if the last character of E is Suffix. Used in Assertions.
- function Add_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
- -- Returns the name of E adding Suffix
-
- function Remove_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
- -- Returns the name of E without Suffix
-
function Has_Tagged_Component (Typ : Entity_Id) return Boolean;
-- Returns True if Typ is a composite type (array or record) which is
-- either itself a tagged type, or has a component (recursively) which is
@@ -1126,8 +1123,12 @@
-- component is present. This function is used to check if "=" has to be
-- expanded into a bunch component comparisons.
+ function Has_Undefined_Reference (Expr : Node_Id) return Boolean;
+ -- Given arbitrary expression Expr, determine whether it contains at
+ -- least one name whose entity is Any_Id.
+
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
- -- Given an arbitrary type, determine whether it contains at least one
+ -- Given arbitrary type Typ, determine whether it contains at least one
-- volatile component.
function Implementation_Kind (Subp : Entity_Id) return Name_Id;
@@ -1553,6 +1554,14 @@
-- . machine_emax = 2**7
-- . machine_emin = 3 - machine_emax
+ function Is_Single_Protected_Object (Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary entity Id denotes the anonymous object
+ -- created for a single protected type.
+
+ function Is_Single_Task_Object (Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary entity Id denotes the anonymous object
+ -- created for a single task type.
+
function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an initialization
-- expression in SPARK 2005, suitable for initializing an object in an
@@ -1950,6 +1959,9 @@
-- the removal performed by this routine does not affect the visibility of
-- existing homonyms.
+ function Remove_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
+ -- Returns the name of E without Suffix
+
function Rep_To_Pos_Flag (E : Entity_Id; Loc : Source_Ptr) return Node_Id;
-- This is used to construct the second argument in a call to Rep_To_Pos
-- which is Standard_True if range checks are enabled (E is an entity to
@@ -1963,13 +1975,6 @@
-- more there is at least one case in the generated code (the code for
-- array assignment in a loop) that depends on this suppression.
- procedure Report_Unused_Body_States
- (Body_Id : Entity_Id;
- States : Elist_Id);
- -- Emit errors for each abstract state or object found in list States that
- -- is declared in package body Body_Id, but is not used as constituent in a
- -- state refinement.
-
procedure Require_Entity (N : Node_Id);
-- N is a node which should have an entity value if it is an entity name.
-- If not, then check if there were previous errors. If so, just fill
===================================================================
@@ -50,6 +50,16 @@
package body Contracts is
+ procedure Analyze_Contracts
+ (L : List_Id;
+ Freeze_Nod : Node_Id;
+ Freeze_Id : Entity_Id);
+ -- Subsidiary to the one parameter version of Analyze_Contracts and routine
+ -- Analyze_Previous_Constracts. Analyze the contracts of all constructs in
+ -- the list L. If Freeze_Nod is set, then the analysis stops when the node
+ -- is reached. Freeze_Id is the entity of some related context which caused
+ -- freezing upto node Freeze_Nod.
+
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- any). This routine processes all [refined] pre- and postconditions as
@@ -330,30 +340,79 @@
end if;
end Add_Contract_Item;
- ---------------------------------------------
- -- Analyze_Enclosing_Package_Body_Contract --
- ---------------------------------------------
+ -----------------------
+ -- Analyze_Contracts --
+ -----------------------
- procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id) is
- Par : Node_Id;
+ procedure Analyze_Contracts (L : List_Id) is
+ begin
+ Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty);
+ end Analyze_Contracts;
+ procedure Analyze_Contracts
+ (L : List_Id;
+ Freeze_Nod : Node_Id;
+ Freeze_Id : Entity_Id)
+ is
+ Decl : Node_Id;
+
begin
- -- Climb the parent chain looking for an enclosing body. Do not use the
- -- scope stack, as a body uses the entity of its corresponding spec.
+ Decl := First (L);
+ while Present (Decl) loop
- Par := Parent (Body_Decl);
- while Present (Par) loop
- if Nkind (Par) = N_Package_Body then
- Analyze_Package_Body_Contract
- (Body_Id => Defining_Entity (Par),
- Freeze_Id => Defining_Entity (Body_Decl));
+ -- The caller requests that the traversal stops at a particular node
+ -- that causes contract "freezing".
- return;
+ if Present (Freeze_Nod) and then Decl = Freeze_Nod then
+ exit;
end if;
- Par := Parent (Par);
+ -- Entry or subprogram declarations
+
+ if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Entry_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id => Defining_Entity (Decl),
+ Freeze_Id => Freeze_Id);
+
+ -- Entry or subprogram bodies
+
+ elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
+ Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl));
+
+ -- Objects
+
+ elsif Nkind (Decl) = N_Object_Declaration then
+ Analyze_Object_Contract
+ (Obj_Id => Defining_Entity (Decl),
+ Freeze_Id => Freeze_Id);
+
+ -- Protected untis
+
+ elsif Nkind_In (Decl, N_Protected_Type_Declaration,
+ N_Single_Protected_Declaration)
+ then
+ Analyze_Protected_Contract (Defining_Entity (Decl));
+
+ -- Subprogram body stubs
+
+ elsif Nkind (Decl) = N_Subprogram_Body_Stub then
+ Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
+
+ -- Task units
+
+ elsif Nkind_In (Decl, N_Single_Task_Declaration,
+ N_Task_Type_Declaration)
+ then
+ Analyze_Task_Contract (Defining_Entity (Decl));
+ end if;
+
+ Next (Decl);
end loop;
- end Analyze_Enclosing_Package_Body_Contract;
+ end Analyze_Contracts;
-----------------------------------------------
-- Analyze_Entry_Or_Subprogram_Body_Contract --
@@ -435,7 +494,10 @@
-- Analyze_Entry_Or_Subprogram_Contract --
------------------------------------------
- procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is
+ procedure Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
Items : constant Node_Id := Contract (Subp_Id);
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
@@ -489,7 +551,7 @@
else
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
Prag := Next_Pragma (Prag);
end loop;
end if;
@@ -513,7 +575,7 @@
-- Otherwise analyze the contract cases
else
- Analyze_Contract_Cases_In_Decl_Part (Prag);
+ Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
end if;
else
pragma Assert (Prag_Nam = Name_Test_Case);
@@ -587,44 +649,14 @@
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 --
-----------------------------
- procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
+ procedure Analyze_Object_Contract
+ (Obj_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
AR_Val : Boolean := False;
AW_Val : Boolean := False;
@@ -769,7 +801,7 @@
-- Analyze indicator Part_Of
if Present (Prag) then
- Analyze_Part_Of_In_Decl_Part (Prag);
+ Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
-- The variable is a constituent of a single protected/task type
-- and behaves as a component of the type. Verify that references
@@ -1055,6 +1087,51 @@
end Analyze_Package_Contract;
--------------------------------
+ -- Analyze_Previous_Contracts --
+ --------------------------------
+
+ procedure Analyze_Previous_Contracts (Body_Decl : Node_Id) is
+ Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+ Par : Node_Id;
+
+ begin
+ -- A body that is in the process of being inlined appears from source,
+ -- but carries name _parent. Such a body does not cause "freezing" of
+ -- contracts.
+
+ if Chars (Body_Id) = Name_uParent then
+ return;
+ end if;
+
+ -- Climb the parent chain looking for an enclosing package body. Do not
+ -- use the scope stack, as a body uses the entity of its corresponding
+ -- spec.
+
+ Par := Parent (Body_Decl);
+ while Present (Par) loop
+ if Nkind (Par) = N_Package_Body then
+ Analyze_Package_Body_Contract
+ (Body_Id => Defining_Entity (Par),
+ Freeze_Id => Defining_Entity (Body_Decl));
+
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ -- Analyze the contracts of all eligible construct upto the body which
+ -- caused the "freezing".
+
+ if Is_List_Member (Body_Decl) then
+ Analyze_Contracts
+ (L => List_Containing (Body_Decl),
+ Freeze_Nod => Body_Decl,
+ Freeze_Id => Body_Id);
+ end if;
+ end Analyze_Previous_Contracts;
+
+ --------------------------------
-- Analyze_Protected_Contract --
--------------------------------
===================================================================
@@ -59,9 +59,8 @@
-- Test_Case
-- Volatile_Function
- procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id);
- -- Analyze the contract of the nearest package body (if any) which encloses
- -- package or subprogram body Body_Decl.
+ procedure Analyze_Contracts (L : List_Id);
+ -- Analyze the contracts of all eligible constructs found in list L
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of entry or
@@ -77,7 +76,9 @@
-- Refined_Post
-- Test_Case (stand alone subprogram body)
- procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id);
+ procedure Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty);
-- 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:
@@ -87,12 +88,13 @@
-- Postcondition
-- Precondition
-- Test_Case
+ --
+ -- Freeze_Id is the entity of a [generic] package body or a [generic]
+ -- subprogram body which "freezes" the contract of Subp_Id.
- 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);
+ procedure Analyze_Object_Contract
+ (Obj_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty);
-- 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
-- considered are:
@@ -103,6 +105,9 @@
-- Effective_Writes
-- Global (single concurrent object)
-- Part_Of
+ --
+ -- Freeze_Id is the entity of a [generic] package body or a [generic]
+ -- subprogram body which "freezes" the contract of Obj_Id.
procedure Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
@@ -123,6 +128,11 @@
-- Initializes
-- Part_Of
+ procedure Analyze_Previous_Contracts (Body_Decl : Node_Id);
+ -- Analyze the contracts of all source constructs found in the declarative
+ -- list which contains entry, package, protected, subprogram, or task body
+ -- denoted by Body_Decl. The analysis stops once Body_Decl is reached.
+
procedure Analyze_Protected_Contract (Prot_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of protected unit
-- Prot_Id if they appeared at the end of a declarative region. Currently
===================================================================
@@ -1294,15 +1294,6 @@
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;
@@ -2988,7 +2979,8 @@
begin
-- A [generic] subprogram body "freezes" the contract of the nearest
- -- enclosing package body:
+ -- enclosing package body and all other contracts encountered in the
+ -- same declarative part upto and excluding the subprogram body:
-- package body Nearest_Enclosing_Package
-- with Refined_State => (State => Constit)
@@ -3009,7 +3001,7 @@
-- Original_Node.
if Comes_From_Source (Original_Node (N)) then
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
end if;
-- Generic subprograms are handled separately. They always have a
@@ -3787,14 +3779,6 @@
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