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 <m...@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.
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;
