2015-10-26 Yannick Moy <moy@adacore.com>

	* lib-xref-spark_specific.adb (Traverse_Protected_Declaration): New
	procedure for traversal.
	(Add_SPARK_Xrefs): Remove debugging code.
	(Traverse_Declaration_Or_Statement): Call the new traversal
	procedure.

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Pragma
	Extensions_Visible can now appear on an abstract subprogram
	declaration.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@229338 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 22 insertions, 37 deletions

diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index a53942d59f9..631c87b1d81 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -124,10 +124,6 @@ package body SPARK_Specific is
      (N            : Node_Id;
       Process      : Node_Processing;
       Inside_Stubs : Boolean);
-   procedure Traverse_Package_Declaration
-     (N            : Node_Id;
-      Process      : Node_Processing;
-      Inside_Stubs : Boolean);
    procedure Traverse_Subprogram_Body
      (N            : Node_Id;
       Process      : Node_Processing;
@@ -483,12 +479,7 @@ package body SPARK_Specific is
          begin
             for Index in SPARK_Scope_Table.First .. S - 1 loop
                if SPARK_Scope_Table.Table (Index).Scope_Entity = E then
-                  declare
-                     Dummy : constant SPARK_Scope_Record :=
-                               SPARK_Scope_Table.Table (Index);
-                  begin
-                     return True;
-                  end;
+                  return True;
                end if;
             end loop;
 
@@ -523,13 +514,13 @@ package body SPARK_Specific is
       is
       begin
          --  The only references of interest on callable entities are calls. On
-         --  non-callable entities, the only references of interest are reads
-         --  and writes.
+         --  uncallable entities, the only references of interest are reads and
+         --  writes.
 
          if Ekind (E) in Overloadable_Kind then
             return Typ = 's';
 
-         --  Objects of Task type or protected type are not SPARK references
+         --  Objects of task or protected types are not SPARK references
 
          elsif Present (Etype (E))
            and then Ekind (Etype (E)) in Concurrent_Kind
@@ -1254,7 +1245,14 @@ package body SPARK_Specific is
    begin
       case Nkind (N) is
          when N_Package_Declaration =>
-            Traverse_Package_Declaration (N, Process, Inside_Stubs);
+            declare
+               Spec : constant Node_Id := Specification (N);
+            begin
+               Traverse_Declarations_Or_Statements
+                 (Visible_Declarations (Spec), Process, Inside_Stubs);
+               Traverse_Declarations_Or_Statements
+                 (Private_Declarations (Spec), Process, Inside_Stubs);
+            end;
 
          when N_Package_Body =>
             if Ekind (Defining_Entity (N)) /= E_Generic_Package then
@@ -1297,12 +1295,6 @@ package body SPARK_Specific is
                end;
             end if;
 
-         when N_Protected_Definition =>
-            Traverse_Declarations_Or_Statements
-              (Visible_Declarations (N), Process, Inside_Stubs);
-            Traverse_Declarations_Or_Statements
-              (Private_Declarations (N), Process, Inside_Stubs);
-
          when N_Protected_Body =>
             Traverse_Protected_Body (N, Process, Inside_Stubs);
 
@@ -1318,6 +1310,16 @@ package body SPARK_Specific is
                end;
             end if;
 
+         when N_Protected_Type_Declaration | N_Single_Protected_Declaration =>
+            declare
+               Def : constant Node_Id := Protected_Definition (N);
+            begin
+               Traverse_Declarations_Or_Statements
+                 (Visible_Declarations (Def), Process, Inside_Stubs);
+               Traverse_Declarations_Or_Statements
+                 (Private_Declarations (Def), Process, Inside_Stubs);
+            end;
+
          when N_Task_Definition =>
             Traverse_Declarations_Or_Statements
               (Visible_Declarations (N), Process, Inside_Stubs);
@@ -1481,23 +1483,6 @@ package body SPARK_Specific is
         (Handled_Statement_Sequence (N), Process, Inside_Stubs);
    end Traverse_Package_Body;
 
-   ----------------------------------
-   -- Traverse_Package_Declaration --
-   ----------------------------------
-
-   procedure Traverse_Package_Declaration
-     (N            : Node_Id;
-      Process      : Node_Processing;
-      Inside_Stubs : Boolean)
-   is
-      Spec : constant Node_Id := Specification (N);
-   begin
-      Traverse_Declarations_Or_Statements
-        (Visible_Declarations (Spec), Process, Inside_Stubs);
-      Traverse_Declarations_Or_Statements
-        (Private_Declarations (Spec), Process, Inside_Stubs);
-   end Traverse_Package_Declaration;
-
    -----------------------------
    -- Traverse_Protected_Body --
    -----------------------------