a-tigeli.adb (Get_Line): Always set Last prior to returning.

2016-05-02  Yannick Moy  <moy@adacore.com>

	* a-tigeli.adb (Get_Line): Always set Last prior to returning.

2016-05-02  Yannick Moy  <moy@adacore.com>

	* lib-xref.adb: Minor style fix in whitespace of declarations.
	* put_spark_xrefs.adb (Put_SPARK_Xrefs): printing of strings
	refactored without loops.
	* put_spark_xrefs.ads (Write_Info_Str): new formal argument of
	generic procedure.
	* spark_xrefs.adb (Write_Info_Str): new actual in instantiation
	of generic procedure.

From-SVN: r235728

6 files changed, 118 insertions, 145 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 10d30a4..fe60f30 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2016-05-02  Yannick Moy  <moy@adacore.com>
+
+	* a-tigeli.adb (Get_Line): Always set Last prior to returning.
+
+2016-05-02  Yannick Moy  <moy@adacore.com>
+
+	* lib-xref.adb: Minor style fix in whitespace of declarations.
+	* put_spark_xrefs.adb (Put_SPARK_Xrefs): printing of strings
+	refactored without loops.
+	* put_spark_xrefs.ads (Write_Info_Str): new formal argument of
+	generic procedure.
+	* spark_xrefs.adb (Write_Info_Str): new actual in instantiation
+	of generic procedure.
+
 2016-05-02  Arnaud Charlet  <charlet@adacore.com>
 
 	* lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope.
diff --git a/gcc/ada/a-tigeli.adb b/gcc/ada/a-tigeli.adb
index 9894e01..f7cb533 100644
--- a/gcc/ada/a-tigeli.adb
+++ b/gcc/ada/a-tigeli.adb
@@ -150,6 +150,12 @@ is
 begin
    FIO.Check_Read_Status (AP (File));
 
+   --  Set Last to Item'First - 1 when no characters are read, as mandated by
+   --  Ada RM. In the case where Item'First is negative or null, this results
+   --  in Constraint_Error being raised.
+
+   Last := Item'First - 1;
+
    --  Immediate exit for null string, this is a case in which we do not
    --  need to test for end of file and we do not skip a line mark under
    --  any circumstances.
@@ -160,8 +166,6 @@ begin
 
    N := Item'Last - Item'First + 1;
 
-   Last := Item'First - 1;
-
    --  Here we have at least one character, if we are immediately before
    --  a line mark, then we will just skip past it storing no characters.
 
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index 3b489e5..ef4acb5 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -191,8 +191,7 @@ package body Lib.Xref is
 
          Set_Has_Xref_Entry (Key.Ent);
 
-      --  It was already in Xref_Set, so throw away the tentatively-added
-      --  entry.
+      --  It was already in Xref_Set, so throw away the tentatively-added entry
 
       else
          Xrefs.Decrement_Last;
@@ -373,16 +372,16 @@ package body Lib.Xref is
       Set_Ref : Boolean   := True;
       Force   : Boolean   := False)
    is
-      Actual_Typ     : Character := Typ;
-      Call           : Node_Id;
-      Def            : Source_Ptr;
-      Ent            : Entity_Id;
-      Ent_Scope      : Entity_Id;
-      Formal         : Entity_Id;
-      Kind           : Entity_Kind;
-      Nod            : Node_Id;
-      Ref            : Source_Ptr;
-      Ref_Scope      : Entity_Id;
+      Actual_Typ : Character := Typ;
+      Call       : Node_Id;
+      Def        : Source_Ptr;
+      Ent        : Entity_Id;
+      Ent_Scope  : Entity_Id;
+      Formal     : Entity_Id;
+      Kind       : Entity_Kind;
+      Nod        : Node_Id;
+      Ref        : Source_Ptr;
+      Ref_Scope  : Entity_Id;
 
       function Get_Through_Renamings (E : Entity_Id) return Entity_Id;
       --  Get the enclosing entity through renamings, which may come from
diff --git a/gcc/ada/put_spark_xrefs.adb b/gcc/ada/put_spark_xrefs.adb
index f200e21..0c6ba2f 100644
--- a/gcc/ada/put_spark_xrefs.adb
+++ b/gcc/ada/put_spark_xrefs.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2011-2013, 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- --
@@ -31,47 +31,30 @@ begin
 
    for J in 1 .. SPARK_File_Table.Last loop
       declare
-         F     : SPARK_File_Record renames SPARK_File_Table.Table (J);
-         Start : Scope_Index;
-         Stop  : Scope_Index;
+         F : SPARK_File_Record renames SPARK_File_Table.Table (J);
 
       begin
-         Start := F.From_Scope;
-         Stop  := F.To_Scope;
-
          Write_Info_Initiate ('F');
          Write_Info_Char ('D');
          Write_Info_Char (' ');
          Write_Info_Nat (F.File_Num);
          Write_Info_Char (' ');
 
-         for N in F.File_Name'Range loop
-            Write_Info_Char (F.File_Name (N));
-         end loop;
+         Write_Info_Str (F.File_Name.all);
 
          --  If file is a subunit, print the file name for the unit
 
          if F.Unit_File_Name /= null then
-            Write_Info_Char (' ');
-            Write_Info_Char ('-');
-            Write_Info_Char ('>');
-            Write_Info_Char (' ');
-
-            for N in F.Unit_File_Name'Range loop
-               Write_Info_Char (F.Unit_File_Name (N));
-            end loop;
+            Write_Info_Str (" -> " & F.Unit_File_Name.all);
          end if;
 
          Write_Info_Terminate;
 
          --  Loop through scope entries for this file
 
-         loop
-            exit when Start = Stop + 1;
-            pragma Assert (Start <= Stop);
-
+         for J in F.From_Scope .. F.To_Scope loop
             declare
-               S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start);
+               S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J);
 
             begin
                Write_Info_Initiate ('F');
@@ -87,15 +70,10 @@ begin
 
                pragma Assert (S.Scope_Name.all /= "");
 
-               for N in S.Scope_Name'Range loop
-                  Write_Info_Char (S.Scope_Name (N));
-               end loop;
+               Write_Info_Str (S.Scope_Name.all);
 
                if S.Spec_File_Num /= 0 then
-                  Write_Info_Char (' ');
-                  Write_Info_Char ('-');
-                  Write_Info_Char ('>');
-                  Write_Info_Char (' ');
+                  Write_Info_Str (" -> ");
                   Write_Info_Nat (S.Spec_File_Num);
                   Write_Info_Char ('.');
                   Write_Info_Nat (S.Spec_Scope_Num);
@@ -103,8 +81,6 @@ begin
 
                Write_Info_Terminate;
             end;
-
-            Start := Start + 1;
          end loop;
       end;
    end loop;
@@ -114,129 +90,103 @@ begin
    for J in 1 .. SPARK_File_Table.Last loop
       declare
          F           : SPARK_File_Record renames SPARK_File_Table.Table (J);
-         Start       : Scope_Index;
-         Stop        : Scope_Index;
          File        : Nat;
          Scope       : Nat;
          Entity_Line : Nat;
          Entity_Col  : Nat;
 
       begin
-         Start := F.From_Scope;
-         Stop  := F.To_Scope;
-
          --  Loop through scope entries for this file
 
-         loop
-            exit when Start = Stop + 1;
-            pragma Assert (Start <= Stop);
-
+         for K in F.From_Scope .. F.To_Scope loop
             Output_One_Scope : declare
-               S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start);
-
-               XStart : Xref_Index;
-               XStop  : Xref_Index;
+               S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K);
 
             begin
-               XStart := S.From_Xref;
-               XStop  := S.To_Xref;
+               --  Write only non-empty tables
+               if S.From_Xref <= S.To_Xref then
 
-               if XStart > XStop then
-                  goto Continue;
-               end if;
+                  Write_Info_Initiate ('F');
+                  Write_Info_Char ('X');
+                  Write_Info_Char (' ');
+                  Write_Info_Nat (F.File_Num);
+                  Write_Info_Char (' ');
 
-               Write_Info_Initiate ('F');
-               Write_Info_Char ('X');
-               Write_Info_Char (' ');
-               Write_Info_Nat (F.File_Num);
-               Write_Info_Char (' ');
+                  Write_Info_Str (F.File_Name.all);
+
+                  Write_Info_Char (' ');
+                  Write_Info_Char ('.');
+                  Write_Info_Nat (S.Scope_Num);
+                  Write_Info_Char (' ');
 
-               for N in F.File_Name'Range loop
-                  Write_Info_Char (F.File_Name (N));
-               end loop;
+                  Write_Info_Str (S.Scope_Name.all);
 
-               Write_Info_Char (' ');
-               Write_Info_Char ('.');
-               Write_Info_Nat (S.Scope_Num);
-               Write_Info_Char (' ');
+                  --  Default value of (0,0) is used for the special __HEAP
+                  --  variable so use another default value.
 
-               for N in S.Scope_Name'Range loop
-                  Write_Info_Char (S.Scope_Name (N));
-               end loop;
+                  Entity_Line := 0;
+                  Entity_Col  := 1;
 
-               --  Default value of (0,0) is used for the special __HEAP
-               --  variable so use another default value.
+                  --  Loop through cross reference entries for this scope
 
-               Entity_Line := 0;
-               Entity_Col  := 1;
+                  for X in S.From_Xref .. S.To_Xref loop
 
-               --  Loop through cross reference entries for this scope
+                     Output_One_Xref : declare
+                        R : SPARK_Xref_Record renames
+                          SPARK_Xref_Table.Table (X);
 
-               loop
-                  exit when XStart = XStop + 1;
-                  pragma Assert (XStart <= XStop);
+                     begin
+                        if R.Entity_Line /= Entity_Line
+                          or else R.Entity_Col /= Entity_Col
+                        then
+                           Write_Info_Terminate;
 
-                  Output_One_Xref : declare
-                     R : SPARK_Xref_Record renames
-                           SPARK_Xref_Table.Table (XStart);
+                           Write_Info_Initiate ('F');
+                           Write_Info_Char (' ');
+                           Write_Info_Nat (R.Entity_Line);
+                           Write_Info_Char (R.Etype);
+                           Write_Info_Nat (R.Entity_Col);
+                           Write_Info_Char (' ');
 
-                  begin
-                     if R.Entity_Line /= Entity_Line
-                       or else R.Entity_Col /= Entity_Col
-                     then
-                        Write_Info_Terminate;
+                           Write_Info_Str (R.Entity_Name.all);
+
+                           Entity_Line := R.Entity_Line;
+                           Entity_Col  := R.Entity_Col;
+                           File        := F.File_Num;
+                           Scope       := S.Scope_Num;
+                        end if;
+
+                        if Write_Info_Col > 72 then
+                           Write_Info_Terminate;
+                           Write_Info_Initiate ('.');
+                        end if;
 
-                        Write_Info_Initiate ('F');
-                        Write_Info_Char (' ');
-                        Write_Info_Nat (R.Entity_Line);
-                        Write_Info_Char (R.Etype);
-                        Write_Info_Nat (R.Entity_Col);
                         Write_Info_Char (' ');
 
-                        for N in R.Entity_Name'Range loop
-                           Write_Info_Char (R.Entity_Name (N));
-                        end loop;
-
-                        Entity_Line := R.Entity_Line;
-                        Entity_Col  := R.Entity_Col;
-                        File        := F.File_Num;
-                        Scope       := S.Scope_Num;
-                     end if;
-
-                     if Write_Info_Col > 72 then
-                        Write_Info_Terminate;
-                        Write_Info_Initiate ('.');
-                     end if;
-
-                     Write_Info_Char (' ');
-
-                     if R.File_Num /= File then
-                        Write_Info_Nat (R.File_Num);
-                        Write_Info_Char ('|');
-                        File  := R.File_Num;
-                        Scope := 0;
-                     end if;
-
-                     if R.Scope_Num /= Scope then
-                        Write_Info_Char ('.');
-                        Write_Info_Nat (R.Scope_Num);
-                        Write_Info_Char (':');
-                        Scope := R.Scope_Num;
-                     end if;
-
-                     Write_Info_Nat (R.Line);
-                     Write_Info_Char (R.Rtype);
-                     Write_Info_Nat (R.Col);
-                  end Output_One_Xref;
-
-                  XStart := XStart + 1;
-               end loop;
+                        if R.File_Num /= File then
+                           Write_Info_Nat (R.File_Num);
+                           Write_Info_Char ('|');
+                           File  := R.File_Num;
+                           Scope := 0;
+                        end if;
 
-               Write_Info_Terminate;
-            end Output_One_Scope;
+                        if R.Scope_Num /= Scope then
+                           Write_Info_Char ('.');
+                           Write_Info_Nat (R.Scope_Num);
+                           Write_Info_Char (':');
+                           Scope := R.Scope_Num;
+                        end if;
 
-         <<Continue>>
-            Start := Start + 1;
+                        Write_Info_Nat (R.Line);
+                        Write_Info_Char (R.Rtype);
+                        Write_Info_Nat (R.Col);
+                     end Output_One_Xref;
+
+                  end loop;
+
+                  Write_Info_Terminate;
+               end if;
+            end Output_One_Scope;
          end loop;
       end;
    end loop;
diff --git a/gcc/ada/put_spark_xrefs.ads b/gcc/ada/put_spark_xrefs.ads
index fa0b81c..fa4a4bc 100644
--- a/gcc/ada/put_spark_xrefs.ads
+++ b/gcc/ada/put_spark_xrefs.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2011-2013, 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- --
@@ -43,6 +43,9 @@ generic
    with procedure Write_Info_Char (C : Character) is <>;
    --  Output one character
 
+   with procedure Write_Info_Str (Val : String) is <>;
+   --  Output string stored in string pointer
+
    with procedure Write_Info_Initiate (Key : Character) is <>;
    --  Initiate write of new line to output file, the parameter is the
    --  keyword character for the line.
diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb
index 8049c7e..8fab555 100644
--- a/gcc/ada/spark_xrefs.adb
+++ b/gcc/ada/spark_xrefs.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2011-2013, 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- --
@@ -160,7 +160,10 @@ package body SPARK_Xrefs is
    procedure pspark is
 
       procedure Write_Info_Char (C : Character) renames Write_Char;
-      --  Write one character;
+      --  Write one character
+
+      procedure Write_Info_Str (Val : String) renames Write_Str;
+      --  Write string
 
       function Write_Info_Col return Positive;
       --  Return next column for writing