2014-05-21 Yannick Moy <moy@adacore.com>

	* lib-xref-spark_specific.adb, lib-xref.ads, lib-xref.adb
	(Enclosing_Subprogram_Or_Package): Only return a library-level
	package.

From-SVN: r210700

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9c47f98ad7d0dd1bc2e973fdf075d16bc5697334..0091301dacfb415d48557cf4410f3c0efb1d61e2 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2014-05-21  Yannick Moy  <moy@adacore.com>
+
+       * lib-xref-spark_specific.adb, lib-xref.ads, lib-xref.adb
+       (Enclosing_Subprogram_Or_Package): Only return a library-level
+       package.
+
 2014-05-21  Javier Miranda  <miranda@adacore.com>
 
        * sem_ch3.adb (Build_Derived_Record_Type): Initialize Parent_Base

diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 0b32aada218b97f51ccb86418b0959cde2458103..aea8b2cfee88a85950e9ced7fa4ada93159fdffb 100644 (file)
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -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 @@ package body SPARK_Specific is
    -- 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,12 +991,26 @@ package body SPARK_Specific is
       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);
@@ -1045,7 +1060,7 @@ package body SPARK_Specific is
       end if;
 
       return Result;
-   end Enclosing_Subprogram_Or_Package;
+   end Enclosing_Subprogram_Or_Library_Package;
 
    -----------------
    -- Entity_Hash --
@@ -1107,7 +1122,7 @@ package body SPARK_Specific is
                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;

diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index 28c5dbbd3939d938931a8c73fb5a33e680556411..ed1138927cf30b123b62c4a26dc2fabdda2c2bd0 100644 (file)
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -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 @@ package body Lib.Xref is
             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.

diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index 7f397a868a5f0820b37ac4e023e6c12b1c6798a9..17733a0c93038b1d17a28691c8052a7cf20f7ffd 100644 (file)
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -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 Lib.Xref is
 
    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;