This patch corrects the propagation of various SPARK aspects from a generic
template to an instance.
------------
-- Source --
------------
-- values.ads
package Values is
In_1 : Integer := 1234;
end Values;
-- gen.ads
with Values; use Values;
generic
package Gen
with Abstract_State => State,
Initializes => Out_1,
Initial_Condition => (Out_1 = 5678)
is
Out_1 : Integer := 5678;
procedure Proc (In_2 : Integer; Out_2 : out Integer)
with Global => (Input => In_1,
In_Out => State,
Output => Out_1),
Depends => ((Out_1, Out_2, State) => (In_1, In_2, State));
end Gen;
-- gen.adb
package body Gen
with Refined_State => (State => (In_3, Out_3))
is
In_3 : Integer := 1;
Out_3 : Integer := 2;
procedure Proc (In_2 : Integer; Out_2 : out Integer)
with Refined_Global => (Input => (In_1, In_3),
Output => (Out_1, Out_3)),
Refined_Depends => ((Out_1, Out_2, Out_3) => (In_1, In_2, In_3))
is begin null; end Proc;
end Gen;
-- inst.ads
with Gen;
package Inst is new Gen;
-----------------
-- Compilation --
-----------------
$ gcc -c inst.ads
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-20 Hristian Kirtchev <kirtc...@adacore.com>
* aspects.adb (Exchange_Aspects): New routine.
* aspects.ads (Exchange_Aspects): New routine.
* atree.adb (Rewrite): Do not check whether the save node has
aspects as it never will, instead check the node about to be clobbered.
* einfo.adb (Write_Field25_Name): Abstract_States can appear in
entities of generic packages.
* sem_ch6.adb (Analyze_Expression_Function): Fix the parent
pointer of an aspect specification list after rewriting takes place.
* sem_ch7.adb (Analyze_Package_Body_Helper): Swap the aspect
specifications of the generic template and the copy used for analysis.
* sem_ch12.adb (Analyze_Generic_Package_Declaration): Swap
the aspect specifications of the generic template and the
copy used for analysis.
(Analyze_Package_Instantiation): Propagate the aspect specifications
from the generic template to the instantiation.
(Build_Instance_Compilation_Unit_Nodes): Propagate the aspect
specifications from the generic template to the instantiation.
* sem_ch13.adb (Analyze_Aspect_Specifications): Handle aspects
Abstract_State, Initializes and Initial_Condition when they
apply to a package instantiation.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 207879)
+++ sem_ch7.adb (working copy)
@@ -327,6 +327,11 @@
New_N := Copy_Generic_Node (N, Empty, Instantiating => False);
Rewrite (N, New_N);
+ -- Once the contents of the generic copy and the template are
+ -- swapped, do the same for their respective aspect specifications.
+
+ Exchange_Aspects (N, New_N);
+
-- Update Body_Id to point to the copied node for the remainder of
-- the processing.
Index: einfo.adb
===================================================================
--- einfo.adb (revision 207879)
+++ einfo.adb (working copy)
@@ -9290,7 +9290,8 @@
procedure Write_Field25_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
- when E_Package =>
+ when E_Generic_Package |
+ E_Package =>
Write_Str ("Abstract_States");
when E_Variable =>
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 207942)
+++ sem_ch12.adb (working copy)
@@ -3019,6 +3019,11 @@
New_N := Copy_Generic_Node (N, Empty, Instantiating => False);
Set_Parent_Spec (New_N, Save_Parent);
Rewrite (N, New_N);
+
+ -- Once the contents of the generic copy and the template are swapped,
+ -- do the same for their respective aspect specifications.
+
+ Exchange_Aspects (N, New_N);
Id := Defining_Entity (N);
Generate_Definition (Id);
@@ -3088,7 +3093,6 @@
Check_References (Id);
end if;
end if;
-
end Analyze_Generic_Package_Declaration;
--------------------------------------------
@@ -3598,7 +3602,7 @@
Make_Package_Renaming_Declaration (Loc,
Defining_Unit_Name =>
Make_Defining_Identifier (Loc, Chars (Gen_Unit)),
- Name => New_Occurrence_Of (Act_Decl_Id, Loc));
+ Name => New_Occurrence_Of (Act_Decl_Id, Loc));
Append (Unit_Renaming, Renaming_List);
@@ -3616,6 +3620,14 @@
Make_Package_Declaration (Loc,
Specification => Act_Spec);
+ -- Propagate the aspect specifications from the package declaration
+ -- template to the instantiated version of the package declaration.
+
+ if Has_Aspects (Act_Tree) then
+ Set_Aspect_Specifications (Act_Decl,
+ New_Copy_List_Tree (Aspect_Specifications (Act_Tree)));
+ end if;
+
-- Save the instantiation node, for subsequent instantiation of the
-- body, if there is one and we are generating code for the current
-- unit. Mark unit as having a body (avoids premature error message).
@@ -5007,7 +5019,7 @@
Unit => Act_Decl,
Aux_Decls_Node => Make_Compilation_Unit_Aux (Sloc (N)));
- Set_Parent_Spec (Act_Decl, Parent_Spec (N));
+ Set_Parent_Spec (Act_Decl, Parent_Spec (N));
-- The new compilation unit is linked to its body, but both share the
-- same file, so we do not set Body_Required on the new unit so as not
@@ -5018,6 +5030,15 @@
-- compilation unit of the instance, since this is the main unit.
Rewrite (N, Act_Body);
+
+ -- Propagate the aspect specifications from the package body template to
+ -- the instantiated version of the package body.
+
+ if Has_Aspects (Act_Body) then
+ Set_Aspect_Specifications
+ (N, New_Copy_List_Tree (Aspect_Specifications (Act_Body)));
+ end if;
+
Body_Cunit := Parent (N);
-- The two compilation unit nodes are linked by the Library_Unit field
Index: aspects.adb
===================================================================
--- aspects.adb (revision 207881)
+++ aspects.adb (working copy)
@@ -174,6 +174,31 @@
return True;
end Aspects_On_Body_Or_Stub_OK;
+ ----------------------
+ -- Exchange_Aspects --
+ ----------------------
+
+ procedure Exchange_Aspects (N1 : Node_Id; N2 : Node_Id) is
+ begin
+ pragma Assert
+ (Permits_Aspect_Specifications (N1)
+ and then Permits_Aspect_Specifications (N2));
+
+ -- Perform the exchange only when both nodes have lists to be swapped
+
+ if Has_Aspects (N1) and then Has_Aspects (N2) then
+ declare
+ L1 : constant List_Id := Aspect_Specifications (N1);
+ L2 : constant List_Id := Aspect_Specifications (N2);
+ begin
+ Set_Parent (L1, N2);
+ Set_Parent (L2, N1);
+ Aspect_Specifications_Hash_Table.Set (N1, L2);
+ Aspect_Specifications_Hash_Table.Set (N2, L1);
+ end;
+ end if;
+ end Exchange_Aspects;
+
-----------------
-- Find_Aspect --
-----------------
Index: aspects.ads
===================================================================
--- aspects.ads (revision 207881)
+++ aspects.ads (working copy)
@@ -786,6 +786,11 @@
-- N denotes a body [stub] with aspects. Determine whether all aspects of N
-- are allowed to appear on a body [stub].
+ procedure Exchange_Aspects (N1 : Node_Id; N2 : Node_Id);
+ -- Exchange the aspect specifications of two nodes. If either node lacks an
+ -- aspect specification list, the routine has no effect. It is assumed that
+ -- both nodes can support aspects.
+
function Find_Aspect (Id : Entity_Id; A : Aspect_Id) return Node_Id;
-- Find the aspect specification of aspect A associated with entity I.
-- Return Empty if Id does not have the requested aspect.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 207942)
+++ sem_ch6.adb (working copy)
@@ -374,6 +374,13 @@
Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
Rewrite (N, New_Body);
+ -- Correct the parent pointer of the aspect specification list to
+ -- reference the rewritten node.
+
+ if Has_Aspects (N) then
+ Set_Parent (Aspect_Specifications (N), N);
+ end if;
+
-- Propagate any pragmas that apply to the expression function to the
-- proper body when the expression function acts as a completion.
-- Aspects are automatically transfered because of node rewriting.
@@ -429,6 +436,14 @@
Make_Subprogram_Declaration (Loc, Specification => Spec);
Rewrite (N, New_Decl);
+
+ -- Correct the parent pointer of the aspect specification list to
+ -- reference the rewritten node.
+
+ if Has_Aspects (N) then
+ Set_Parent (Aspect_Specifications (N), N);
+ end if;
+
Analyze (N);
Set_Is_Inlined (Defining_Entity (New_Decl));
Index: atree.adb
===================================================================
--- atree.adb (revision 207879)
+++ atree.adb (working copy)
@@ -1870,8 +1870,7 @@
-- Both the old and new copies of the node will share the same list
-- of aspect specifications if aspect specifications are present.
- if Has_Aspects (Sav_Node) then
- Set_Has_Aspects (Sav_Node, False);
+ if Old_Has_Aspects then
Set_Aspect_Specifications
(Sav_Node, Aspect_Specifications (Old_Node));
end if;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 207942)
+++ sem_ch13.adb (working copy)
@@ -2008,13 +2008,22 @@
-- immediately.
when Aspect_Abstract_State => Abstract_State : declare
- Decls : List_Id;
+ Context : Node_Id := N;
+ Decls : List_Id;
begin
- if Nkind_In (N, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ -- When aspect Abstract_State appears on a generic package,
+ -- it is propageted to the package instance. The context in
+ -- this case is the instance spec.
+
+ if Nkind (Context) = N_Package_Instantiation then
+ Context := Instance_Spec (Context);
+ end if;
+
+ if Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
- Decls := Visible_Declarations (Specification (N));
+ Decls := Visible_Declarations (Specification (Context));
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
@@ -2025,7 +2034,7 @@
if No (Decls) then
Decls := New_List;
- Set_Visible_Declarations (N, Decls);
+ Set_Visible_Declarations (Context, Decls);
end if;
Prepend_To (Decls, Aitem);
@@ -2084,13 +2093,22 @@
-- it must be evaluated at the end of the said declarations.
when Aspect_Initial_Condition => Initial_Condition : declare
- Decls : List_Id;
+ Context : Node_Id := N;
+ Decls : List_Id;
begin
- if Nkind_In (N, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ -- When aspect Abstract_State appears on a generic package,
+ -- it is propageted to the package instance. The context in
+ -- this case is the instance spec.
+
+ if Nkind (Context) = N_Package_Instantiation then
+ Context := Instance_Spec (Context);
+ end if;
+
+ if Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
- Decls := Visible_Declarations (Specification (N));
+ Decls := Visible_Declarations (Specification (Context));
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
@@ -2104,7 +2122,7 @@
if No (Decls) then
Decls := New_List;
- Set_Visible_Declarations (N, Decls);
+ Set_Visible_Declarations (Context, Decls);
end if;
Prepend_To (Decls, Aitem);
@@ -2125,13 +2143,22 @@
-- said declarations.
when Aspect_Initializes => Initializes : declare
- Decls : List_Id;
+ Context : Node_Id := N;
+ Decls : List_Id;
begin
- if Nkind_In (N, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ -- When aspect Abstract_State appears on a generic package,
+ -- it is propageted to the package instance. The context in
+ -- this case is the instance spec.
+
+ if Nkind (Context) = N_Package_Instantiation then
+ Context := Instance_Spec (Context);
+ end if;
+
+ if Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
- Decls := Visible_Declarations (Specification (N));
+ Decls := Visible_Declarations (Specification (Context));
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
@@ -2144,7 +2171,7 @@
if No (Decls) then
Decls := New_List;
- Set_Visible_Declarations (N, Decls);
+ Set_Visible_Declarations (Context, Decls);
end if;
Prepend_To (Decls, Aitem);
