[Ada] Pre/Postconditions on generic subprograms

[Arnaud Charlet]

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  <schonberg@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.

-------------- next part --------------
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