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

	* spark_xrefs.ads Description of the spark cross-references
	clarified; small style fixes.
	* lib-xref-spark_specific.adb (Add_SPARK_Scope,
	Detect_And_Add_SPARK_Scope): consider protected types and bodies
	as yet another scopes.
	(Enclosing_Subprogram_Or_Library_Package): refactored using
	Hristian's suggestions; added support for scopes of protected
	types and bodies; fix for entries to return the scope of the
	enclosing concurrent type, which is consistent with what is
	returned for protected subprograms.
	* sem_intr.adb: Minor style fix in comment.

From-SVN: r235731

4 files changed, 79 insertions, 77 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ee9f265..eaab1b7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2016-05-02  Arnaud Charlet  <charlet@adacore.com>
+
+	* spark_xrefs.ads Description of the spark cross-references
+	clarified; small style fixes.
+	* lib-xref-spark_specific.adb (Add_SPARK_Scope,
+	Detect_And_Add_SPARK_Scope): consider protected types and bodies
+	as yet another scopes.
+	(Enclosing_Subprogram_Or_Library_Package): refactored using
+	Hristian's suggestions; added support for scopes of protected
+	types and bodies; fix for entries to return the scope of the
+	enclosing concurrent type, which is consistent with what is
+	returned for protected subprograms.
+	* sem_intr.adb: Minor style fix in comment.
+
 2016-05-02  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* lib-xref.ads, lib-xref-spark_specific.adb, get_spark_xrefs.adb,
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 10d1a05..46f7b3a 100644
--- 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_Protected_Type
             | E_Task_Type
          =>
             Typ := Xref_Entity_Letters (Ekind (E));
@@ -284,7 +285,11 @@ package body SPARK_Specific is
                Typ := Xref_Entity_Letters (Ekind (E));
             end if;
 
-         when E_Package_Body | E_Subprogram_Body | E_Task_Body =>
+         when E_Package_Body
+            | E_Protected_Body
+            | E_Subprogram_Body
+            | E_Task_Body
+         =>
             Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
 
          when E_Void =>
@@ -1029,6 +1034,10 @@ package body SPARK_Specific is
                       N_Package_Body_Stub,
                       N_Package_Declaration)
            or else
+         Nkind_In (N, N_Protected_Body,         --  protected objects
+                      N_Protected_Body_Stub,
+                      N_Protected_Type_Declaration)
+           or else
          Nkind_In (N, N_Subprogram_Body,        --  subprograms
                       N_Subprogram_Body_Stub,
                       N_Subprogram_Declaration)
@@ -1048,63 +1057,44 @@ package body SPARK_Specific is
    function Enclosing_Subprogram_Or_Library_Package
      (N : Node_Id) return Entity_Id
    is
-      Result : Entity_Id;
+      Context : Entity_Id;
 
    begin
       --  If N is the defining identifier for a subprogram, then return the
       --  enclosing subprogram or package, not this subprogram.
 
       if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
-        and then Nkind (Parent (N)) in N_Subprogram_Specification
+        and then (Ekind (N) in Entry_Kind
+                  or else Ekind (N) = E_Subprogram_Body
+                  or else Ekind (N) in Generic_Subprogram_Kind
+                  or else Ekind (N) in Subprogram_Kind)
       then
-         Result := Parent (Parent (Parent (N)));
+         Context := Parent (Unit_Declaration_Node (N));
 
-         --  If this was a library-level subprogram then replace Result with
+         --  If this was a library-level subprogram then replace Context with
          --  its Unit, which points to N_Subprogram_* node.
 
-         if Nkind (Result) = N_Compilation_Unit then
-            Result := Unit (Result);
+         if Nkind (Context) = N_Compilation_Unit then
+            Context := Unit (Context);
          end if;
       else
-         Result := N;
+         Context := N;
       end if;
 
-      while Present (Result) loop
-         case Nkind (Result) is
-            when N_Package_Specification =>
+      while Present (Context) loop
+         case Nkind (Context) is
+            when N_Package_Body          |
+                 N_Package_Specification =>
 
                --  Only return a library-level package
 
-               if Is_Library_Level_Entity (Defining_Entity (Result)) then
-                  Result := Defining_Entity (Result);
+               if Is_Library_Level_Entity (Defining_Entity (Context)) then
+                  Context := Defining_Entity (Context);
                   exit;
                else
-                  Result := Parent (Result);
+                  Context := Parent (Context);
                end if;
 
-            when N_Package_Body =>
-
-               --  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;
-
-            when N_Subprogram_Declaration =>
-               Result := Defining_Unit_Name (Specification (Result));
-               exit;
-
-            when N_Subprogram_Body =>
-               Result := Defining_Unit_Name (Specification (Result));
-               exit;
-
             when N_Pragma =>
 
                --  The enclosing subprogram for a precondition, postcondition,
@@ -1112,51 +1102,46 @@ package body SPARK_Specific is
                --  pragma (skipping any other pragmas between this pragma and
                --  this declaration.
 
-               while Nkind (Result) = N_Pragma
-                 and then Is_List_Member (Result)
-                 and then Present (Prev (Result))
+               while Nkind (Context) = N_Pragma
+                 and then Is_List_Member (Context)
+                 and then Present (Prev (Context))
                loop
-                  Result := Prev (Result);
+                  Context := Prev (Context);
                end loop;
 
-               if Nkind (Result) = N_Pragma then
-                  Result := Parent (Result);
+               if Nkind (Context) = N_Pragma then
+                  Context := Parent (Context);
                end if;
 
-            when N_Entry_Body =>
-               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);
+            when N_Entry_Body                 |
+                 N_Entry_Declaration          |
+                 N_Protected_Type_Declaration |
+                 N_Subprogram_Body            |
+                 N_Subprogram_Declaration     |
+                 N_Subprogram_Specification   |
+                 N_Task_Body                  |
+                 N_Task_Type_Declaration      =>
+               Context := Defining_Entity (Context);
                exit;
 
             when others =>
-               Result := Parent (Result);
+               Context := Parent (Context);
          end case;
       end loop;
 
-      if Nkind (Result) = N_Defining_Program_Unit_Name then
-         Result := Defining_Identifier (Result);
+      if Nkind (Context) = N_Defining_Program_Unit_Name then
+         Context := Defining_Identifier (Context);
       end if;
 
       --  Do not return a scope without a proper location
 
-      if Present (Result)
-        and then Sloc (Result) = No_Location
+      if Present (Context)
+        and then Sloc (Context) = No_Location
       then
          return Empty;
       end if;
 
-      return Result;
+      return Context;
    end Enclosing_Subprogram_Or_Library_Package;
 
    -----------------
diff --git a/gcc/ada/sem_intr.adb b/gcc/ada/sem_intr.adb
index e25ebb7..a15e95c 100644
--- a/gcc/ada/sem_intr.adb
+++ b/gcc/ada/sem_intr.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-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- --
@@ -59,7 +59,7 @@ package body Sem_Intr is
    procedure Check_Shift (E : Entity_Id; N : Node_Id);
    --  Check intrinsic shift subprogram, the two arguments are the same
    --  as for Check_Intrinsic_Subprogram (i.e. the entity of the subprogram
-   --  declaration, and the node for the pragma argument, used for messages)
+   --  declaration, and the node for the pragma argument, used for messages).
 
    procedure Errint (Msg : String; S : Node_Id; N : Node_Id);
    --  Post error message for bad intrinsic, the message itself is posted
@@ -340,7 +340,7 @@ package body Sem_Intr is
       then
          null;
 
-      --  Exception  functions
+      --  Exception functions
 
       elsif Nam_In (Nam, Name_Exception_Information,
                          Name_Exception_Message,
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index f3bf1a3..fa958cf 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -36,7 +36,7 @@ package SPARK_Xrefs is
 
    --  SPARK cross-reference information can exist in one of two forms. In
    --  the ALI file, it is represented using a text format that is described
-   --  in this specification. Internally it is stored using three tables
+   --  in this specification. Internally it is stored using three tables:
    --  SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are
    --  also defined in this unit.
 
@@ -56,21 +56,21 @@ package SPARK_Xrefs is
 
    --  SPARK cross-reference information is generated on a unit-by-unit basis
    --  in the ALI file, using lines that start with the identifying character F
-   --  ("Formal"). These lines are generated if Frame_Condition_Mode is True.
+   --  ("Formal"). These lines are generated if GNATprove_Mode is True.
 
    --  The SPARK cross-reference information comes after the shared
-   --  cross-reference information, so it needs not be read by tools like
-   --  gnatbind, gnatmake etc.
+   --  cross-reference information, so it can be ignored by tools like
+   --  gnatbind, gnatmake, etc.
 
    --  -------------------
    --  -- Scope Section --
    --  -------------------
 
    --  A first section defines the scopes in which entities are defined and
-   --  referenced. A scope is a package/subprogram declaration/body. Note that
-   --  a package declaration and body define two different scopes. Similarly, a
-   --  subprogram declaration and body, when both present, define two different
-   --  scopes.
+   --  referenced. A scope is a package/subprogram/protected_type/task_type
+   --  declaration/body. Note that a package declaration and body define two
+   --  different scopes. Similarly, a subprogram, protected type and task type
+   --  declaration and body, when both present, define two different scopes.
 
    --    FD dependency-number filename (-> unit-filename)?
 
@@ -135,8 +135,11 @@ package SPARK_Xrefs is
 
    --      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.
+   --      entity-number and entity identify a scope in FS lines
+   --      for the file previously identified file.
+
+   --      (filename and entity are just a textual representations of
+   --       dependency-number and entity-number)
 
    --    F line typ col entity ref*
 
@@ -192,7 +195,7 @@ package SPARK_Xrefs is
    --  -- Generated Globals Section --
    --  -------------------------------
 
-   --  The Generated Globals section is located at the end of the ALI file.
+   --  The Generated Globals section is located at the end of the ALI file
 
    --  All lines introducing information related to the Generated Globals
    --  have the string "GG" appearing in the beginning. This string ("GG")