lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope.

2016-05-02  Arnaud Charlet  <charlet@adacore.com>

	* lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope.
	(Detect_And_Add_SPARK_Scope): detect and add task type scope.
	(Enclosing_Subprogram_Or_Package): Respect boundaries of task
	and entry declarations.
	* spark_xrefs.ads: minor typo in comment.

From-SVN: r235726

gcc/ada/ChangeLog

 2016-05-02  Arnaud Charlet  <charlet@adacore.com>
 
+	* lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope.
+	(Detect_And_Add_SPARK_Scope): detect and add task type scope.
+	(Enclosing_Subprogram_Or_Package): Respect boundaries of task
+	and entry declarations.
+	* spark_xrefs.ads: minor typo in comment.
+
+2016-05-02  Arnaud Charlet  <charlet@adacore.com>
+
 	* make.adb: Minor: avoid an exception when calling gnatmake with
 	no argument and gnatmake is built with checks on.
 	* lib-xref-spark_specific.adb: Minor code cleanup.

gcc/ada/lib-xref-spark_specific.adb

@@ -265,6 +265,7 @@ package body SPARK_Specific is
             | E_Generic_Package
             | E_Generic_Procedure
             | E_Package
+            | E_Task_Type
          =>
             Typ := Xref_Entity_Letters (Ekind (E));
 
@@ -382,7 +383,7 @@ package body SPARK_Specific is
          Key        => Entity_Id,
          Hash       => Entity_Hash,
          Equal      => "=");
-      --  Package used to build a correspondance between entities and scope
+      --  Package used to build a correspondence between entities and scope
       --  numbers used in SPARK cross references.
 
       Nrefs : Nat := Xrefs.Last;
@@ -1033,7 +1034,8 @@ package body SPARK_Specific is
                       N_Subprogram_Declaration)
            or else
          Nkind_In (N, N_Task_Body,              --  tasks
-                      N_Task_Body_Stub)
+                      N_Task_Body_Stub,
+                      N_Task_Type_Declaration)
       then
          Add_SPARK_Scope (N);
       end if;
@@ -1125,10 +1127,18 @@ package body SPARK_Specific is
                Result := Defining_Identifier (Result);
                exit;
 
+            when N_Entry_Declaration =>
+               Result := Defining_Identifier (Result);
+               exit;
+
             when N_Task_Body =>
                Result := Defining_Identifier (Result);
                exit;
 
+            when N_Task_Type_Declaration =>
+               Result := Defining_Identifier (Result);
+               exit;
+
             when others =>
                Result := Parent (Result);
          end case;

gcc/ada/spark_xrefs.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2011-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2011-2016, 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- --
@@ -133,7 +133,7 @@ package SPARK_Xrefs is
 
    --    FX dependency-number filename . entity-number entity
 
-   --      dependency-number and filename identity a file in FD lines
+   --      dependency-number and filename identify a file in FD lines
 
    --      entity-number and identity identify a scope entity in FS lines for
    --      the file previously identified.