[multiple changes]

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.

From-SVN: r229338

gcc/ada/ChangeLog

 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.
+
+2015-10-26  Yannick Moy  <moy@adacore.com>
+
 	* lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Use character 'r' to
 	denote a reference to a constant which may have variable input, and
 	thus may be treated as a variable in GNATprove, instead of the

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 --
    -----------------------------

gcc/ada/sem_prag.adb

@@ -14058,9 +14058,14 @@ package body Sem_Prag is
             Subp_Decl :=
               Find_Related_Declaration_Or_Body (N, Do_Checks => True);
 
+            --  Abstract subprogram declaration
+
+            if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then
+               null;
+
             --  Generic subprogram declaration
 
-            if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+            elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
                null;
 
             --  Body acts as spec