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 <[email protected]>
* 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)
