From patchwork Wed Nov 18 13:54:11 2015 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 546008 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 7CC0D141468 for ; Thu, 19 Nov 2015 00:54:30 +1100 (AEDT) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=obuZAg4P; dkim-atps=neutral DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=Cs1UvnYx3QUMuA3ZSUe5u2rjkOq5tXKfnM7+eKR1NUcSAyrv6q tme/4v/pXYM8sjY2n0LaWmFIq2++XwSlFGMSpgrE8A+cngCqF87QxZGj3WghfS0f qts89PxCZpIFOWvKrtrAYKel0E71qIUKsLpYUYDUSpNBJnBlEOF5N8xjg= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=kZxQlgmmuGDs768UZGdb/OqaUqA=; b=obuZAg4Psx3jIbHsi2cQ wBffk6aveNw5jg7owWQ8+U4EzQ78wXRYfgpBvlDMTyyVDLlcvwcPlH++iG9xz0hk PsHtQgJ+dHn3lA8ENc/+4vk/l3NSl4Z/VhpaaS2Gsl5ksWdjhdWtUwmK0z4GqrBU Op4PwEnaa4xwJo0806jq2lY= Received: (qmail 121684 invoked by alias); 18 Nov 2015 13:54:19 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 121666 invoked by uid 89); 18 Nov 2015 13:54:19 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=4.8 required=5.0 tests=BAYES_99, BAYES_999, KAM_ASCII_DIVIDERS, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_LOW, T_FILL_THIS_FORM_SHORT autolearn=no version=3.3.2 X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with (AES256-SHA encrypted) ESMTPS; Wed, 18 Nov 2015 13:54:13 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 7C0982957F; Wed, 18 Nov 2015 08:54:11 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id xFpbA9EcY4NV; Wed, 18 Nov 2015 08:54:11 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id 5A99329469; Wed, 18 Nov 2015 08:54:11 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4192) id 54E3F1A5; Wed, 18 Nov 2015 08:54:11 -0500 (EST) Date: Wed, 18 Nov 2015 08:54:11 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Freezing of contracts, Part_Of and current instance of a concurrent type Message-ID: <20151118135411.GA38679@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch addresses several areas: The freezing of contracts has been enhanced. A body continues to freeze the contract of the nearest enclosing package and now freezes the contracts of all eligible constructs in the same declarative list that precede the body. A concurrent constituent is no longer considered a visible state of a package body because it is already part of a single protected/task type. The current instance of a concurrent type now correctly includes single protected/task types. As a result, the current instance of such a type will appear as an implicit formal parameter of a protected subprogram or a single task type as per SPARK RM 6.1.4. ------------ -- Source -- ------------ -- subprogram_freezing.ads package Subprogram_Freezing with SPARK_Mode is procedure Force_Freeze; end Subprogram_Freezing; -- subprogram_freezing.adb package body Subprogram_Freezing with SPARK_Mode is function Func (Formal : Integer) return Integer with Contract_Cases => (Var + Formal = 1 => Var + Func'Result = 0, -- Error others => Var - Func'Result = 1), -- Error Pre => (Var > 2), -- Error Post => (Var + Func'Result = 100); -- Error procedure Force_Freeze is begin null; end Force_Freeze; Var : Integer := 1; function Func (Formal : Integer) return Integer is begin return Formal; end Func; end Subprogram_Freezing; -- variable_freezing.ads package Variable_Freezing with SPARK_Mode is procedure Force_Freeze; end Variable_Freezing; -- variable_freezing.adb package body Variable_Freezing with SPARK_Mode is Error_1 : Integer := 1 with Part_Of => Prot; -- Error procedure Force_Freeze is begin null; end Force_Freeze; protected Prot is end Prot; protected body Prot is end Prot; end Variable_Freezing; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c subprogram_freezing.adb $ gcc -c variable_freezing.adb subprogram_freezing.adb:2:13: body "Force_Freeze" declared at line 9 freezes the contract of "Func" subprogram_freezing.adb:2:13: all contractual items must be declared before body at line 9 subprogram_freezing.adb:6:30: "Var" is undefined (more references follow) variable_freezing.adb:2:04: body "Force_Freeze" declared at line 4 freezes the contract of "Error_1" variable_freezing.adb:2:04: all contractual items must be declared before body at line 4 variable_freezing.adb:2:43: "Prot" is undefined Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-18 Hristian Kirtchev * contracts.adb (Analyze_Contracts): New routine. (Analyze_Enclosing_Package_Body_Contract): Removed. (Analyze_Entry_Or_Subprogram_Contract): Add formal parameter Freeze_Id. Propagate the entity of the freezing body to vaious analysis routines. (Analyze_Initial_Declaration_Contract): Removed. (Analyze_Object_Contract): Add formal parameter Freeze_Id. Propagate the entity of the freezing body to vaious analysis routines. (Analyze_Previous_Contracts): New routine. * contracts.ads (Analyze_Enclosing_Package_Body_Contract): Removed. (Analyze_Contracts): New routine. (Analyze_Entry_Or_Subprogram_Contract): Add formal parameter Freeze_Id and update the comment on usage. (Analyze_Initial_Declaration_Contract): Removed. (Analyze_Object_Contract): Add formal parameter Freeze_Id and update the comment on usage. (Analyze_Previous_Contracts): New routine. * sem_ch3.adb (Analyze_Declarations): Use Analyze_Contracts to analyze all contracts of eligible constructs. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): A body no longer freezes the contract of its initial declaration. This effect is achieved through different means. (Analyze_Subprogram_Body_Helper): A body now freezes the contracts of all eligible constructs that precede it. A body no longer freezes the contract of its initial declaration. This effect is achieved through different means. * sem_ch7.adb (Analyze_Package_Body_Helper): A body now freezes the contracts of all eligible constructs that precede it. A body no longer freezes the contract of its initial declaration. This effect is achieved through different means. * sem_ch9.adb (Analyze_Entry_Body): A body now freezes the contracts of all eligible constructs that precede it. A body no longer freezes the contract of its initial declaration. This effect is achieved through different means. (Analyze_Protected_Body): A body now freezes the contracts of all eligible constructs that precede it. A body no longer freezes the contract of its initial declaration. This effect is achieved through different means. (Analyze_Task_Body): A body now freezes the contracts of all eligible constructs that precede it. A body no longer freezes the contract of its initial declaration. This effect is achieved through different means. * sem_prag.adb (Add_Item_To_Name_Buffer): Single protected/task objects now output their respective current instance of xxx type messages. (Analyze_Contract_Cases_In_Decl_Part): Add formal parameter Freeze_Id. Emit a clarification message when an undefined entity may the byproduct of contract freezing. (Analyze_Part_Of_In_Decl_Part): Add formal parameter Freeze_Id. Emit a clarification message when an undefined entity may the byproduct of contract freezing. (Analyze_Pre_Post_Condition_In_Decl_Part): Add formal parameter Freeze_Id. Emit a clarification message when an undefined entity may the byproduct of contract freezing. (Analyze_Refined_State_In_Decl_Part): Do not report unused body states as constituents of single protected/task types may not bave been identified yet. (Collect_Subprogram_Inputs_Outputs): Reimplemented. (Contract_Freeze_Error): New routine. (Process_Overloadable): Use predicate Is_Single_Task_Object. * sem_prag.ads (Analyze_Contract_Cases_In_Decl_Part): Add formal parameter Freeze_Id and update the comment on usage. (Analyze_Part_Of_In_Decl_Part): Add formal parameter Freeze_Id and update the comment on usage. (Analyze_Pre_Post_Condition_In_Decl_Part): Add formal parameter Freeze_Id and update the comment on usage. * sem_util.adb (Check_Unused_Body_States): Remove global variable Legal_Constits. The routine now reports unused body states regardless of whether constituents are legal or not. (Collect_Body_States): A constituent of a single protected/task type is not a visible state of a package body. (Collect_Visible_States): A constituent of a single protected/task type is not a visible state of a package body. (Has_Undefined_Reference): New routine. (Is_Single_Concurrent_Object): Reimplemented. (Is_Single_Protected_Object): New routine. (Is_Single_Task_Object): New routine. (Is_Visible_Object): New routine. (Report_Unused_Body_States): Moved to Check_Unused_Body_States. * sem_util.ads (Check_Unused_Body_States): Update the comment on usage. (Has_Undefined_Reference): New routine. (Is_Single_Protected_Object): New routine. (Is_Single_Task_Object): New routine. (Report_Unused_Body_States): Moved to Check_Unused_Body_States. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 230524) +++ sem_ch3.adb (working copy) @@ -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 Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 230529) +++ sem_ch7.adb (working copy) @@ -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)); Index: sem_ch9.adb =================================================================== --- sem_ch9.adb (revision 230522) +++ sem_ch9.adb (working copy) @@ -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); Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 230540) +++ sem_prag.adb (working copy) @@ -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 -- --------------------------------- Index: sem_prag.ads =================================================================== --- sem_prag.ads (revision 230522) +++ sem_prag.ads (working copy) @@ -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 Index: sem_util.adb =================================================================== --- sem_util.adb (revision 230540) +++ sem_util.adb (working copy) @@ -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 -- -------------------- Index: sem_util.ads =================================================================== --- sem_util.ads (revision 230540) +++ sem_util.ads (working copy) @@ -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 Index: contracts.adb =================================================================== --- contracts.adb (revision 230540) +++ contracts.adb (working copy) @@ -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 -- -------------------------------- Index: contracts.ads =================================================================== --- contracts.ads (revision 230536) +++ contracts.ads (working copy) @@ -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 Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 230533) +++ sem_ch6.adb (working copy) @@ -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