Cross references for GNATprove on SPARK code should not use local packages
as valid scopes, but instead the enclosing subprogram, which is the
meaningful scope to distinguish between local and global variables.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-05-21 Yannick Moy <m...@adacore.com>
* lib-xref-spark_specific.adb, lib-xref.ads, lib-xref.adb
(Enclosing_Subprogram_Or_Package): Only return a library-level
package.
Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb (revision 210697)
+++ lib-xref-spark_specific.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2011-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -23,10 +23,9 @@
-- --
------------------------------------------------------------------------------
-with SPARK_Xrefs; use SPARK_Xrefs;
-with Einfo; use Einfo;
-with Nmake; use Nmake;
-with Put_SPARK_Xrefs;
+with SPARK_Xrefs; use SPARK_Xrefs;
+with Einfo; use Einfo;
+with Nmake; use Nmake;
with GNAT.HTable;
@@ -972,7 +971,9 @@
-- Enclosing_Subprogram_Or_Package --
-------------------------------------
- function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
+ function Enclosing_Subprogram_Or_Library_Package
+ (N : Node_Id) return Entity_Id
+ is
Result : Entity_Id;
begin
@@ -990,13 +991,27 @@
while Present (Result) loop
case Nkind (Result) is
when N_Package_Specification =>
- Result := Defining_Unit_Name (Result);
- exit;
+ -- Only return a library-level package
+
+ if Is_Library_Level_Entity (Defining_Entity (Result)) then
+ Result := Defining_Entity (Result);
+ exit;
+ else
+ Result := Parent (Result);
+ end if;
+
when N_Package_Body =>
- Result := Defining_Unit_Name (Result);
- exit;
+ -- Only return a library-level package
+
+ if Is_Library_Level_Entity (Defining_Entity (Result)) then
+ Result := Defining_Entity (Result);
+ exit;
+ else
+ Result := Parent (Result);
+ end if;
+
when N_Subprogram_Specification =>
Result := Defining_Unit_Name (Result);
exit;
@@ -1045,7 +1060,7 @@
end if;
return Result;
- end Enclosing_Subprogram_Or_Package;
+ end Enclosing_Subprogram_Or_Library_Package;
-----------------
-- Entity_Hash --
@@ -1107,7 +1122,7 @@
Create_Heap;
end if;
- Ref_Scope := Enclosing_Subprogram_Or_Package (N);
+ Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
Deref.Ent := Heap;
Deref.Loc := Loc;
Index: lib-xref.ads
===================================================================
--- lib-xref.ads (revision 210697)
+++ lib-xref.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 1998-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1998-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -624,8 +624,12 @@
package SPARK_Specific is
- function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
- -- Return the closest enclosing subprogram of package
+ function Enclosing_Subprogram_Or_Library_Package
+ (N : Node_Id) return Entity_Id;
+ -- Return the closest enclosing subprogram of package. Only return a
+ -- library level package. If the package is enclosed in a subprogram,
+ -- return the subprogram. This ensures that GNATprove can distinguish
+ -- local variables from global variables.
procedure Generate_Dereference
(N : Node_Id;
Index: lib-xref.adb
===================================================================
--- lib-xref.adb (revision 210697)
+++ lib-xref.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1998-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1998-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -1029,8 +1029,10 @@
Ref := Sloc (Nod);
Def := Sloc (Ent);
- Ref_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Nod);
- Ent_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Ent);
+ Ref_Scope :=
+ SPARK_Specific.Enclosing_Subprogram_Or_Library_Package (Nod);
+ Ent_Scope :=
+ SPARK_Specific.Enclosing_Subprogram_Or_Library_Package (Ent);
-- Since we are reaching through renamings in SPARK mode, we may
-- end up with standard constants. Ignore those.
