[Ada] Correct ALFA xrefs for separates and pre/post

[Arnaud Charlet]

The ALFA cross references generated for formal verification were missing
for separates and incorrect inside pre/post. Now corrected.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-05  Yannick Moy  <moy@adacore.com>

	* lib-xref-alfa.adb (Collect_ALFA): generate the proper relation
	between body and spec for stub.
	(Detect_And_Add_ALFA_Scope): take into account subprogram stub
	* lib-xref.adb (Enclosing_Subprogram_Or_Package): in the case of a
	pragma precondition or postcondition, for which the enclosing
	subprogram or package in the AST is not the desired one, return empty.

-------------- next part --------------
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb	(revision 177448)
+++ lib-xref-alfa.adb	(working copy)
@@ -845,6 +845,9 @@
                if Present (Body_Entity) then
                   if Nkind (Body_Entity) = N_Defining_Program_Unit_Name then
                      Body_Entity := Parent (Body_Entity);
+                  elsif Nkind (Body_Entity) = N_Subprogram_Body_Stub then
+                     Body_Entity :=
+                       Proper_Body (Unit (Library_Unit (Body_Entity)));
                   end if;
 
                   Spec_Entity := Corresponding_Spec (Body_Entity);
@@ -874,10 +877,12 @@
 
    procedure Detect_And_Add_ALFA_Scope (N : Node_Id) is
    begin
-      if Nkind_In (N, N_Subprogram_Declaration,
-                      N_Subprogram_Body,
-                      N_Package_Declaration,
-                      N_Package_Body)
+      if Nkind_In (N,
+                   N_Subprogram_Declaration,
+                   N_Subprogram_Body,
+                   N_Subprogram_Body_Stub,
+                   N_Package_Declaration,
+                   N_Package_Body)
       then
          Add_ALFA_Scope (N);
       end if;
Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 177448)
+++ lib-xref.adb	(working copy)
@@ -129,7 +129,7 @@
    -------------------------------------
 
    function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
-      Result         : Entity_Id;
+      Result : Entity_Id;
 
    begin
       --  If N is the defining identifier for a subprogram, then return the
@@ -167,6 +167,20 @@
                Result := Defining_Unit_Name (Specification (Result));
                exit;
 
+            --  The enclosing subprogram for a pre- or postconditions should be
+            --  the subprogram to which the pragma is attached. This is not
+            --  always the case in the AST, as the pragma may be declared after
+            --  the declaration of the subprogram. Return Empty in this case.
+
+            when N_Pragma =>
+               if Get_Pragma_Id (Result) = Pragma_Precondition
+                 or else Get_Pragma_Id (Result) = Pragma_Postcondition
+               then
+                  return Empty;
+               else
+                  Result := Parent (Result);
+               end if;
+
             when others =>
                Result := Parent (Result);
          end case;