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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 90628591ebf4aa1afe2e885cfdf2d8b300975924..10d30a44731d31f7b2fabe7d8f9d5110e7a30c5d 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+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

diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index e575150d2b50e591bfc55ad51429d272de39f06d..d0321dbfa0d3cdfe8ab9866c217ffec2e9453146 100644 (file)
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/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;

diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index f02234f9d14a3cc380e17dfc684c34f747eadddc..f3bf1a38f76e05212ecff78a1b49a019377d59be 100644 (file)
--- a/gcc/ada/spark_xrefs.ads
+++ b/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.