This patch ensures that contract of subprogram body stubs are analyzed in timely fashion.
------------ -- Source -- ------------ -- pack.ads package Pack with SPARK_Mode, Abstract_State => State, Initializes => (Var_1, State) is Var_1 : Integer := 0; procedure Double with Global => (In_Out => (State, Var_1)); procedure Error_1 with Global => (In_Out => State); end Pack; -- pack-double.adb separate (Pack) procedure Double with SPARK_Mode is begin Var_1 := Var_1 * 2; end Double; -- pack-double_a.adb separate (Pack) procedure Double_A with SPARK_Mode is begin Var_2 := Var_2 * 2; end Double_A; -- pack-error_1.adb separate (Pack) procedure Error_1 with SPARK_Mode is begin null; end Error_1; -- pack-error_2.adb separate (Pack) procedure Error_2 with SPARK_Mode is begin null; end Error_2; -- pack.adb package body Pack with SPARK_Mode, Refined_State => (State => Var_2) is Var_2 : Integer := 0; procedure Double is separate with Refined_Global => (In_Out => (Var_1, Var_2)); procedure Double_A is separate with Global => (In_Out => Var_2); procedure Error_1 is separate with Refined_Global => (In_Out => Junk_1); procedure Error_2 is separate with Global => (In_Out => Junk_2); end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb pack.adb:14:40: "Junk_1" is undefined pack.adb:17:32: "Junk_2" is undefined Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-11 Hristian Kirtchev <kirtc...@adacore.com> * sem_ch3.adb Add with and use clause for Sem_Ch10. (Analyze_Declarations): Code reformatting. Analyze the contract of a subprogram body stub at the end of the declarative region. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Spec_Id is now a variable. Do not process the body if its contract is not available. Account for subprogram body stubs when extracting the corresponding spec. * sem_ch6.ads (Analyze_Subprogram_Contract): Update the comment on usage. * sem_ch10.ads, sem_ch10.adb (Analyze_Subprogram_Body_Stub_Contract): New routine. * sem_prag.adb (Analyze_Depends_In_Decl_Part): Account for subprogram body stubs when extracting the corresponding spec. (Analyze_Global_In_Decl_List): Account for subprogram body stubs when extracting the corresponding spec. (Analyze_Refined_Depends_In_Decl_Part): Use Find_Related_Subprogram_Or_Body to retrieve the declaration of the related body. Spec_Is now a variable. Account for subprogram body stubs when extracting the corresponding spec. (Analyze_Refined_Global_In_Decl_Part): Use Find_Related_Subprogram_Or_Body to retrieve the declaration of the related body. Spec_Is now a variable. Account for subprogram body stubs when extracting the corresponding spec. (Collect_Subprogram_Inputs_Output): Account for subprogram body stubs when extracting the corresponding spec.
Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 211448) +++ sem_ch3.adb (working copy) @@ -57,6 +57,7 @@ with Sem_Ch6; use Sem_Ch6; with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; +with Sem_Ch10; use Sem_Ch10; with Sem_Ch13; use Sem_Ch13; with Sem_Dim; use Sem_Dim; with Sem_Disp; use Sem_Disp; @@ -2371,13 +2372,16 @@ if Nkind (Decl) = N_Object_Declaration then Analyze_Object_Contract (Defining_Entity (Decl)); + elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, + N_Subprogram_Declaration) + then + Analyze_Subprogram_Contract (Defining_Entity (Decl)); + elsif Nkind (Decl) = N_Subprogram_Body then Analyze_Subprogram_Body_Contract (Defining_Entity (Decl)); - elsif Nkind_In (Decl, N_Subprogram_Declaration, - N_Abstract_Subprogram_Declaration) - then - Analyze_Subprogram_Contract (Defining_Entity (Decl)); + elsif Nkind (Decl) = N_Subprogram_Body_Stub then + Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl)); end if; Next (Decl); Index: sem_ch10.adb =================================================================== --- sem_ch10.adb (revision 211445) +++ sem_ch10.adb (working copy) @@ -1879,6 +1879,39 @@ end if; end Analyze_Protected_Body_Stub; + ------------------------------------------- + -- Analyze_Subprogram_Body_Stub_Contract -- + ------------------------------------------- + + procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is + Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); + + begin + -- A subprogram body stub may act as its own spec or as the completion + -- of a previous declaration. Depending on the context, the contract of + -- the stub may contain two sets of pragmas. + + -- The stub is a completion, the applicable pragmas are: + -- Contract_Cases + -- Depends + -- Global + -- Postcondition + -- Precondition + -- Test_Case + + if Present (Spec_Id) then + Analyze_Subprogram_Body_Contract (Stub_Id); + + -- The stub acts as its own spec, the applicable pragmas are: + -- Refined_Depends + -- Refined_Global + + else + Analyze_Subprogram_Contract (Stub_Id); + end if; + end Analyze_Subprogram_Body_Stub_Contract; + ---------------------------------- -- Analyze_Subprogram_Body_Stub -- ---------------------------------- Index: sem_ch10.ads =================================================================== --- sem_ch10.ads (revision 211445) +++ sem_ch10.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -33,6 +33,19 @@ procedure Analyze_Protected_Body_Stub (N : Node_Id); procedure Analyze_Subunit (N : Node_Id); + procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id); + -- Analyze all delayed aspects chained on the contract of a subprogram body + -- stub Stub_Id as if they appeared at the end of a declarative region. The + -- aspects in question are: + -- Contract_Cases + -- Depends + -- Global + -- Postcondition + -- Precondition + -- Refined_Depends + -- Refined_Global + -- Test_Case + procedure Install_Context (N : Node_Id); -- Installs the entities from the context clause of the given compilation -- unit into the visibility chains. This is done before analyzing a unit. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 211448) +++ sem_prag.adb (working copy) @@ -1700,11 +1700,13 @@ -- Refined_Depends. if Nkind (Subp_Decl) = N_Subprogram_Body - and then not Acts_As_Spec (Subp_Decl) + and then Present (Corresponding_Spec (Subp_Decl)) then Spec_Id := Corresponding_Spec (Subp_Decl); - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub then + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + then Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); else @@ -2327,11 +2329,13 @@ -- Refined_Global. if Nkind (Subp_Decl) = N_Subprogram_Body - and then not Acts_As_Spec (Subp_Decl) + and then Present (Corresponding_Spec (Subp_Decl)) then Spec_Id := Corresponding_Spec (Subp_Decl); - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub then + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + then Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); else @@ -22623,7 +22627,7 @@ -- Local variables - Body_Decl : constant Node_Id := Parent (N); + Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Errors : constant Nat := Serious_Errors_Detected; Refs : constant Node_Id := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); @@ -22641,7 +22645,12 @@ return; end if; - Spec_Id := Corresponding_Spec (Body_Decl); + if Nkind (Body_Decl) = N_Subprogram_Body_Stub then + Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + else + Spec_Id := Corresponding_Spec (Body_Decl); + end if; + Depends := Get_Pragma (Spec_Id, Pragma_Depends); -- Subprogram declarations lacks pragma Depends. Refined_Depends is @@ -23390,11 +23399,11 @@ -- Local variables - Body_Decl : constant Node_Id := Parent (N); + Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Errors : constant Nat := Serious_Errors_Detected; Items : constant Node_Id := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); - Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + Spec_Id : Entity_Id; -- Start of processing for Analyze_Refined_Global_In_Decl_Part @@ -23407,6 +23416,12 @@ return; end if; + if Nkind (Body_Decl) = N_Subprogram_Body_Stub then + Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + else + Spec_Id := Corresponding_Spec (Body_Decl); + end if; + Global := Get_Pragma (Spec_Id, Pragma_Global); -- The subprogram declaration lacks pragma Global. This renders @@ -25323,10 +25338,11 @@ -- Local variables - Formal : Entity_Id; - Global : Node_Id; - List : Node_Id; - Spec_Id : Entity_Id; + Subp_Decl : constant Node_Id := Parent (Parent (Subp_Id)); + Formal : Entity_Id; + Global : Node_Id; + List : Node_Id; + Spec_Id : Entity_Id; -- Start of processing for Collect_Subprogram_Inputs_Outputs @@ -25335,8 +25351,16 @@ -- Find the entity of the corresponding spec when processing a body - if Ekind (Subp_Id) = E_Subprogram_Body then - Spec_Id := Corresponding_Spec (Parent (Parent (Subp_Id))); + if Nkind (Subp_Decl) = N_Subprogram_Body + and then Present (Corresponding_Spec (Subp_Decl)) + then + Spec_Id := Corresponding_Spec (Subp_Decl); + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); + else Spec_Id := Subp_Id; end if; Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 211448) +++ sem_ch6.adb (working copy) @@ -2031,21 +2031,27 @@ -------------------------------------- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is - Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); - Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl); + Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); Prag : Node_Id; Ref_Depends : Node_Id := Empty; Ref_Global : Node_Id := Empty; + Spec_Id : Entity_Id; begin -- When a subprogram body declaration is illegal, its defining entity is -- left unanalyzed. There is nothing left to do in this case because the -- body lacks a contract. - if not Analyzed (Body_Id) then + if No (Contract (Body_Id)) then return; end if; + if Nkind (Body_Decl) = N_Subprogram_Body_Stub then + Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + else + Spec_Id := Corresponding_Spec (Body_Decl); + end if; + -- Locate and store pragmas Refined_Depends and Refined_Global since -- their order of analysis matters. Index: sem_ch6.ads =================================================================== --- sem_ch6.ads (revision 211445) +++ sem_ch6.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -57,6 +57,8 @@ -- as if they appeared at the end of a declarative region. The aspects in -- question are: -- Contract_Cases + -- Depends + -- Global -- Postcondition -- Precondition -- Test_Case