diff mbox

[Ada] Update SPARK cross references for local packages

Message ID 20140521125613.GA23520@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet May 21, 2014, 12:56 p.m. UTC 
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  <moy@adacore.com>

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

Patch

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.