aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/lib-xref.ads
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2014-05-21 12:56:05 +0000
committerArnaud Charlet <charlet@gcc.gnu.org>2014-05-21 14:56:05 +0200
commit63b5225b44626f58396430f11b1592f3b7f155f4 (patch)
tree56db786687dc97722095edb5588d9fc21cf0651a /gcc/ada/lib-xref.ads
parenta8a89b743d7f22120969402642b2375537c67243 (diff)
downloadgcc-63b5225b44626f58396430f11b1592f3b7f155f4.zip
gcc-63b5225b44626f58396430f11b1592f3b7f155f4.tar.gz
gcc-63b5225b44626f58396430f11b1592f3b7f155f4.tar.bz2
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
Diffstat (limited to 'gcc/ada/lib-xref.ads')
-rw-r--r--gcc/ada/lib-xref.ads10
1 files changed, 7 insertions, 3 deletions
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index 7f397a8..17733a0 100644
--- 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;