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

gcc/ada/ChangeLog

+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

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;

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.

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;