This patch corrects the diagnostics related to elaboration requirements of instantiations imposed on a unit. In addition, the patch updates two key routines to handle compilation unit instances.
------------ -- Source -- ------------ -- gnat.adc pragma SPARK_Mode (On); -- gen_pack.ads generic package Gen_Pack is generic package Nested is procedure Proc; end Nested; end Gen_Pack; -- gen_pack.adb with Ada.Text_IO; use Ada.Text_IO; package body Gen_Pack is package body Nested is procedure Proc is begin Put_Line ("Proc"); end Proc; end Nested; end Gen_Pack; -- gen_proc.ads generic procedure Gen_Proc; -- gen_proc.adb with Ada.Text_IO; use Ada.Text_IO; procedure Gen_Proc is begin Put_Line ("Gen_Proc"); end Gen_Proc; -- inst_proc.ads with Gen_Proc; pragma Elaborate (Gen_Proc); procedure Inst_Proc is new Gen_Proc; -- inst_proc2.ads with Gen_Proc; procedure Inst_Proc2 is new Gen_Proc; -- inst_pack.ads with Gen_Pack; pragma Elaborate_All (Gen_Pack); package Inst_Pack is new Gen_Pack; -- inst_pack2.ads with Gen_Pack; package Inst_Pack2 is new Gen_Pack; -- inst_nested.ads with Inst_Pack; pragma Elaborate_All (Inst_Pack); package Inst_Nested is new Inst_Pack.Nested; -- inst_nested2.ads with Inst_Pack; package Inst_Nested2 is new Inst_Pack.Nested; -- call_proc.ads package Call_Proc is procedure Force_Body; end Call_Proc; -- call_proc.adb with Inst_Proc; pragma Elaborate_All (Inst_Proc); package body Call_Proc is procedure Force_Body is begin null; end Force_Body; begin Inst_Proc; end Call_Proc; -- call_proc2.ads package Call_Proc2 is procedure Force_Body; end Call_Proc2; -- call_proc2.adb with Inst_Proc2; package body Call_Proc2 is procedure Force_Body is begin null; end Force_Body; begin Inst_Proc2; end Call_Proc2; -- call_nested_proc.ads package Call_Nested_Proc is procedure Force_Body; end Call_Nested_Proc; -- call_nested_proc.adb with Inst_Nested; pragma Elaborate_All (Inst_Nested); package body Call_Nested_Proc is procedure Force_Body is begin null; end Force_Body; begin Inst_Nested.Proc; end Call_Nested_Proc; -- call_nested_proc2.ads package Call_Nested_Proc2 is procedure Force_Body; end Call_Nested_Proc2; -- call_nested_proc2.adb with Inst_Nested2; package body Call_Nested_Proc2 is procedure Force_Body is begin null; end Force_Body; begin Inst_Nested2.Proc; end Call_Nested_Proc2; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnatd.v inst_proc.ads $ gcc -c -gnatd.v inst_pack.ads $ gcc -c -gnatd.v inst_nested.ads $ gcc -c -gnatd.v call_proc.adb $ gcc -c -gnatd.v call_nested_proc.adb $ gcc -c -gnatd.v inst_proc2.ads $ gcc -c -gnatd.v inst_pack2.ads $ gcc -c -gnatd.v inst_nested2.ads $ gcc -c -gnatd.v call_proc2.adb $ gcc -c -gnatd.v call_nested_proc2.adb inst_proc2.ads:3:01: instantiation of "Gen_Proc" during elaboration in SPARK inst_proc2.ads:3:01: unit "Inst_Proc2" requires pragma "Elaborate" for "Gen_Proc" inst_proc2.ads:3:01: body of unit "Inst_Proc2" elaborated inst_proc2.ads:3:01: procedure "Gen_Proc" instantiated as "Inst_Proc2" at line 3 inst_pack2.ads:3:01: instantiation of "Gen_Pack" during elaboration in SPARK inst_pack2.ads:3:01: unit "Inst_Pack2" requires pragma "Elaborate_All" for "Gen_Pack" inst_pack2.ads:3:01: spec of unit "Inst_Pack2" elaborated inst_pack2.ads:3:01: package "Gen_Pack" instantiated as "Inst_Pack2" at line 3 inst_nested2.ads:3:01: instantiation of "Nested" during elaboration in SPARK inst_nested2.ads:3:01: unit "Inst_Nested2" requires pragma "Elaborate_All" for "Inst_Pack" inst_nested2.ads:3:01: spec of unit "Inst_Nested2" elaborated inst_nested2.ads:3:01: package "Nested" instantiated as "Inst_Nested2" at line 3 call_proc2.adb:6:04: call to "Inst_Proc2" during elaboration in SPARK call_proc2.adb:6:04: unit "Call_Proc2" requires pragma "Elaborate_All" for "Inst_Proc2" call_proc2.adb:6:04: body of unit "Call_Proc2" elaborated call_proc2.adb:6:04: procedure "Inst_Proc2" called at line 6 call_nested_proc2.adb:6:16: call to "Proc" during elaboration in SPARK call_nested_proc2.adb:6:16: unit "Call_Nested_Proc2" requires pragma "Elaborate_All" for "Inst_Nested2" call_nested_proc2.adb:6:16: body of unit "Call_Nested_Proc2" elaborated call_nested_proc2.adb:6:16: procedure "Proc" called at line 6 Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-19 Hristian Kirtchev <kirtc...@adacore.com> * sem_elab.adb (Compilation_Unit): Handle the case of a subprogram instantiation that acts as a compilation unit. (Find_Code_Unit): Reimplemented. (Find_Top_Unit): Reimplemented. (Find_Unit_Entity): New routine. (Process_Instantiation_SPARK): Correct the elaboration requirement a package instantiation imposes on a unit.
Index: sem_elab.adb =================================================================== --- sem_elab.adb (revision 253913) +++ sem_elab.adb (working copy) @@ -159,7 +159,7 @@ -- -- - Instantiations -- - -- - References to variables + -- - Reads of variables -- -- - Task activation -- @@ -175,7 +175,7 @@ -- -- - For instantiations, the target is the generic template -- - -- - For references to variables, the target is the variable + -- - For reads of variables, the target is the variable -- -- - For task activation, the target is the task body -- @@ -883,6 +883,10 @@ -- is obtained by logically unwinding instantiations and subunits when N -- resides within one. + function Find_Unit_Entity (N : Node_Id) return Entity_Id; + pragma Inline (Find_Unit_Entity); + -- Return the entity of unit N + function First_Formal_Type (Subp_Id : Entity_Id) return Entity_Id; pragma Inline (First_Formal_Type); -- Return the type of subprogram Subp_Id's first formal parameter. If the @@ -1904,7 +1908,20 @@ Comp_Unit := Parent (Unit_Declaration_Node (Unit_Id)); end if; - if Nkind (Comp_Unit) = N_Subunit then + -- Handle the case where a subprogram instantiation which acts as a + -- compilation unit is expanded into an anonymous package that wraps + -- the instantiated subprogram. + + if Nkind (Comp_Unit) = N_Package_Specification + and then Nkind_In (Original_Node (Parent (Comp_Unit)), + N_Function_Instantiation, + N_Procedure_Instantiation) + then + Comp_Unit := Parent (Parent (Comp_Unit)); + + -- Handle the case where the compilation unit is a subunit + + elsif Nkind (Comp_Unit) = N_Subunit then Comp_Unit := Parent (Comp_Unit); end if; @@ -2933,10 +2950,8 @@ -------------------- function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id is - N_Unit : constant Node_Id := Unit (Cunit (Get_Code_Unit (N))); - begin - return Defining_Entity (N_Unit, Concurrent_Subunit => True); + return Find_Unit_Entity (Unit (Cunit (Get_Code_Unit (N)))); end Find_Code_Unit; --------------------------- @@ -3405,12 +3420,47 @@ ------------------- function Find_Top_Unit (N : Node_Or_Entity_Id) return Entity_Id is - N_Unit : constant Node_Id := Unit (Cunit (Get_Top_Level_Code_Unit (N))); - begin - return Defining_Entity (N_Unit, Concurrent_Subunit => True); + return Find_Unit_Entity (Unit (Cunit (Get_Top_Level_Code_Unit (N)))); end Find_Top_Unit; + ---------------------- + -- Find_Unit_Entity -- + ---------------------- + + function Find_Unit_Entity (N : Node_Id) return Entity_Id is + Context : constant Node_Id := Parent (N); + Orig_N : constant Node_Id := Original_Node (N); + + begin + -- The unit denotes a package body of an instantiation which acts as + -- a compilation unit. The proper entity is that of the package spec. + + if Nkind (N) = N_Package_Body + and then Nkind (Orig_N) = N_Package_Instantiation + and then Nkind (Context) = N_Compilation_Unit + then + return Corresponding_Spec (N); + + -- The unit denotes an anonymous package created to wrap a subprogram + -- instantiation which acts as a compilation unit. The proper entity is + -- that of the "related instance". + + elsif Nkind (N) = N_Package_Declaration + and then Nkind_In (Orig_N, N_Function_Instantiation, + N_Procedure_Instantiation) + and then Nkind (Context) = N_Compilation_Unit + then + return + Related_Instance (Defining_Entity (N, Concurrent_Subunit => True)); + + -- Otherwise the proper entity is the defining entity + + else + return Defining_Entity (N, Concurrent_Subunit => True); + end if; + end Find_Unit_Entity; + ----------------------- -- First_Formal_Type -- ----------------------- @@ -5335,8 +5385,8 @@ -- in a great number of contexts. To determine whether a reference is -- a read, it is more practical to find out whether it is a write. - -- A reference is a write when appearing immediately on the left-hand - -- side of an assignment. + -- A reference is a write when it appears immediately on the left- + -- hand side of an assignment. if Nkind (Context) = N_Assignment_Statement and then Name (Context) = Ref @@ -7796,9 +7846,9 @@ -- ABE ramifications of the instantiation. if Nkind (Inst) = N_Package_Instantiation then + Req_Nam := Name_Elaborate_All; + else Req_Nam := Name_Elaborate; - else - Req_Nam := Name_Elaborate_All; end if; Meet_Elaboration_Requirement @@ -8155,10 +8205,10 @@ -- listed below are not considered. The categories are: -- 'Access for entries, operators, and subprograms + -- Assignments to variables -- Calls (includes task activation) -- Instantiations - -- Variable assignments - -- Variable references + -- Reads of variables elsif Is_Suitable_Access (N) or else Is_Suitable_Variable_Assignment (N)