This patch is a partial implementation of pre/postconditions that apply to
generic subprograms and are inherited by the corresponding instantiations.
This implementation does not defer the analysis of the corresponding aspects
to a later point, and therefore is restricted to conditions that only depend
on the formals and the generic formals of the unit.
The following must compile and execute quietly:
gnatmake -gnat12 -gnata try_list
try_list
---
with T; use T;
procedure Try_List is
Short_List : Lists.List;
function Inc (X : integer) return integer is
begin
return X + 1;
end Inc;
procedure Map_Inc is new Map_F (Inc);
begin
Short_List.Append (15);
Map_Inc (Short_List);
end;
---
with Ada.Containers.Doubly_Linked_Lists;
package T is
package Lists is new Ada.Containers.Doubly_Linked_Lists (Integer);
use Lists;
generic
with function F (E : Integer) return Integer;
procedure Map_F (L : in out List) with
Pre => (for all Cu in L => Element (Cu) /= F (Element (Cu)));
end T;
---
package body T is
procedure Map_F (L : in out List) is
Current : Cursor := First (L);
begin
while Current /= No_Element loop
Replace_Element (L, Current, F (Element (Current)));
Next (Current);
end loop;
end Map_F;
end T;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-02 Ed Schonberg <schonb...@adacore.com>
* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): copy properly
the aspect declarations and attach them to the generic copy for
subsequent analysis.
(Analyze_Subprogram_Instantiation): copy explicitly the aspect
declarations of the generic tree to the new subprogram declarations.
* sem_attr.adb (Check_Precondition_Postcondition): recognize
conditions that apply to a subprogram instance.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 177147)
+++ sem_prag.adb (working copy)
@@ -1738,8 +1738,19 @@
-- Skip stuff not coming from source
elsif not Comes_From_Source (PO) then
- null;
+ -- The condition may apply to a subprogram instantiation.
+
+ if Nkind (PO) = N_Subprogram_Declaration
+ and then Present (Generic_Parent (Specification (PO)))
+ then
+ Chain_PPC (PO);
+ return;
+
+ else
+ null;
+ end if;
+
-- Only remaining possibility is subprogram declaration
else
@@ -7554,6 +7565,7 @@
then
Set_Elaborate_Present (Citem, True);
Set_Unit_Name (Get_Pragma_Arg (Arg), Name (Citem));
+ Generate_Reference (Entity (Name (Citem)), Citem);
-- With the pragma present, elaboration calls on
-- subprograms from the named unit need no further
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 177144)
+++ sem_ch12.adb (working copy)
@@ -2794,6 +2794,20 @@
Set_Parent_Spec (New_N, Save_Parent);
Rewrite (N, New_N);
+ -- The aspect specifications are not attached to the tree, and must
+ -- be copied and attached to the generic copy explicitly.
+
+ if Present (Aspect_Specifications (New_N)) then
+ declare
+ Aspects : constant List_Id := Aspect_Specifications (N);
+ begin
+ Set_Has_Aspects (N, False);
+ Move_Aspects (New_N, N);
+ Set_Has_Aspects (Original_Node (N), False);
+ Set_Aspect_Specifications (Original_Node (N), Aspects);
+ end;
+ end if;
+
Spec := Specification (N);
Id := Defining_Entity (Spec);
Generate_Definition (Id);
@@ -2888,16 +2902,42 @@
Save_Global_References (Original_Node (N));
+ -- To capture global references, analyze the expressions of aspects,
+ -- and propagate information to original tree. Note that in this case
+ -- analysis of attributes is not delayed until the freeze point.
+ -- It seems very hard to recreate the proper visibility of the generic
+ -- subprogram at a later point because the analysis of an aspect may
+ -- create pragmas after the generic copies have been made ???
+
+ if Has_Aspects (N) then
+ declare
+ Aspect : Node_Id;
+
+ begin
+ Aspect := First (Aspect_Specifications (N));
+ while Present (Aspect) loop
+ if Get_Aspect_Id (Chars (Identifier (Aspect)))
+ /= Aspect_Warnings
+ then
+ Analyze (Expression (Aspect));
+ end if;
+ Next (Aspect);
+ end loop;
+
+ Aspect := First (Aspect_Specifications (Original_Node (N)));
+ while Present (Aspect) loop
+ Save_Global_References (Expression (Aspect));
+ Next (Aspect);
+ end loop;
+ end;
+ end if;
+
End_Generic;
End_Scope;
Exit_Generic_Scope (Id);
Generate_Reference_To_Formals (Id);
List_Inherited_Pre_Post_Aspects (Id);
-
- if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Id);
- end if;
end Analyze_Generic_Subprogram_Declaration;
-----------------------------------
@@ -4262,6 +4302,12 @@
Make_Subprogram_Declaration (Sloc (Act_Spec),
Specification => Act_Spec);
+ -- The aspects have been copied previously, but they have to be
+ -- linked explicitly to the new subprogram declaration.
+ -- Explicit pre/postconditions on the instance are analyzed below,
+ -- in a separate step.
+
+ Move_Aspects (Act_Tree, Act_Decl);
Set_Categorization_From_Pragmas (Act_Decl);
if Parent_Installed then
