Commit ef25192b by Yannick Moy Committed by Arnaud Charlet

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
parent ebae28e9
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> 2016-05-02 Arnaud Charlet <charlet@adacore.com>
* lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope. * lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope.
......
...@@ -150,6 +150,12 @@ is ...@@ -150,6 +150,12 @@ is
begin begin
FIO.Check_Read_Status (AP (File)); 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 -- 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 -- need to test for end of file and we do not skip a line mark under
-- any circumstances. -- any circumstances.
...@@ -160,8 +166,6 @@ begin ...@@ -160,8 +166,6 @@ begin
N := Item'Last - Item'First + 1; N := Item'Last - Item'First + 1;
Last := Item'First - 1;
-- Here we have at least one character, if we are immediately before -- 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. -- a line mark, then we will just skip past it storing no characters.
......
...@@ -191,8 +191,7 @@ package body Lib.Xref is ...@@ -191,8 +191,7 @@ package body Lib.Xref is
Set_Has_Xref_Entry (Key.Ent); Set_Has_Xref_Entry (Key.Ent);
-- It was already in Xref_Set, so throw away the tentatively-added -- It was already in Xref_Set, so throw away the tentatively-added entry
-- entry.
else else
Xrefs.Decrement_Last; Xrefs.Decrement_Last;
...@@ -373,16 +372,16 @@ package body Lib.Xref is ...@@ -373,16 +372,16 @@ package body Lib.Xref is
Set_Ref : Boolean := True; Set_Ref : Boolean := True;
Force : Boolean := False) Force : Boolean := False)
is is
Actual_Typ : Character := Typ; Actual_Typ : Character := Typ;
Call : Node_Id; Call : Node_Id;
Def : Source_Ptr; Def : Source_Ptr;
Ent : Entity_Id; Ent : Entity_Id;
Ent_Scope : Entity_Id; Ent_Scope : Entity_Id;
Formal : Entity_Id; Formal : Entity_Id;
Kind : Entity_Kind; Kind : Entity_Kind;
Nod : Node_Id; Nod : Node_Id;
Ref : Source_Ptr; Ref : Source_Ptr;
Ref_Scope : Entity_Id; Ref_Scope : Entity_Id;
function Get_Through_Renamings (E : Entity_Id) return Entity_Id; function Get_Through_Renamings (E : Entity_Id) return Entity_Id;
-- Get the enclosing entity through renamings, which may come from -- Get the enclosing entity through renamings, which may come from
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- 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 -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -31,47 +31,30 @@ begin ...@@ -31,47 +31,30 @@ begin
for J in 1 .. SPARK_File_Table.Last loop for J in 1 .. SPARK_File_Table.Last loop
declare declare
F : SPARK_File_Record renames SPARK_File_Table.Table (J); F : SPARK_File_Record renames SPARK_File_Table.Table (J);
Start : Scope_Index;
Stop : Scope_Index;
begin begin
Start := F.From_Scope;
Stop := F.To_Scope;
Write_Info_Initiate ('F'); Write_Info_Initiate ('F');
Write_Info_Char ('D'); Write_Info_Char ('D');
Write_Info_Char (' '); Write_Info_Char (' ');
Write_Info_Nat (F.File_Num); Write_Info_Nat (F.File_Num);
Write_Info_Char (' '); Write_Info_Char (' ');
for N in F.File_Name'Range loop Write_Info_Str (F.File_Name.all);
Write_Info_Char (F.File_Name (N));
end loop;
-- If file is a subunit, print the file name for the unit -- If file is a subunit, print the file name for the unit
if F.Unit_File_Name /= null then if F.Unit_File_Name /= null then
Write_Info_Char (' '); Write_Info_Str (" -> " & F.Unit_File_Name.all);
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;
end if; end if;
Write_Info_Terminate; Write_Info_Terminate;
-- Loop through scope entries for this file -- Loop through scope entries for this file
loop for J in F.From_Scope .. F.To_Scope loop
exit when Start = Stop + 1;
pragma Assert (Start <= Stop);
declare declare
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start); S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J);
begin begin
Write_Info_Initiate ('F'); Write_Info_Initiate ('F');
...@@ -87,15 +70,10 @@ begin ...@@ -87,15 +70,10 @@ begin
pragma Assert (S.Scope_Name.all /= ""); pragma Assert (S.Scope_Name.all /= "");
for N in S.Scope_Name'Range loop Write_Info_Str (S.Scope_Name.all);
Write_Info_Char (S.Scope_Name (N));
end loop;
if S.Spec_File_Num /= 0 then if S.Spec_File_Num /= 0 then
Write_Info_Char (' '); Write_Info_Str (" -> ");
Write_Info_Char ('-');
Write_Info_Char ('>');
Write_Info_Char (' ');
Write_Info_Nat (S.Spec_File_Num); Write_Info_Nat (S.Spec_File_Num);
Write_Info_Char ('.'); Write_Info_Char ('.');
Write_Info_Nat (S.Spec_Scope_Num); Write_Info_Nat (S.Spec_Scope_Num);
...@@ -103,8 +81,6 @@ begin ...@@ -103,8 +81,6 @@ begin
Write_Info_Terminate; Write_Info_Terminate;
end; end;
Start := Start + 1;
end loop; end loop;
end; end;
end loop; end loop;
...@@ -114,129 +90,103 @@ begin ...@@ -114,129 +90,103 @@ begin
for J in 1 .. SPARK_File_Table.Last loop for J in 1 .. SPARK_File_Table.Last loop
declare declare
F : SPARK_File_Record renames SPARK_File_Table.Table (J); F : SPARK_File_Record renames SPARK_File_Table.Table (J);
Start : Scope_Index;
Stop : Scope_Index;
File : Nat; File : Nat;
Scope : Nat; Scope : Nat;
Entity_Line : Nat; Entity_Line : Nat;
Entity_Col : Nat; Entity_Col : Nat;
begin begin
Start := F.From_Scope;
Stop := F.To_Scope;
-- Loop through scope entries for this file -- Loop through scope entries for this file
loop for K in F.From_Scope .. F.To_Scope loop
exit when Start = Stop + 1;
pragma Assert (Start <= Stop);
Output_One_Scope : declare Output_One_Scope : declare
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Start); S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K);
XStart : Xref_Index;
XStop : Xref_Index;
begin begin
XStart := S.From_Xref; -- Write only non-empty tables
XStop := S.To_Xref; if S.From_Xref <= S.To_Xref then
if XStart > XStop then Write_Info_Initiate ('F');
goto Continue; Write_Info_Char ('X');
end if; Write_Info_Char (' ');
Write_Info_Nat (F.File_Num);
Write_Info_Char (' ');
Write_Info_Initiate ('F'); Write_Info_Str (F.File_Name.all);
Write_Info_Char ('X');
Write_Info_Char (' '); Write_Info_Char (' ');
Write_Info_Nat (F.File_Num); 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_Str (S.Scope_Name.all);
Write_Info_Char (F.File_Name (N));
end loop;
Write_Info_Char (' '); -- Default value of (0,0) is used for the special __HEAP
Write_Info_Char ('.'); -- variable so use another default value.
Write_Info_Nat (S.Scope_Num);
Write_Info_Char (' ');
for N in S.Scope_Name'Range loop Entity_Line := 0;
Write_Info_Char (S.Scope_Name (N)); Entity_Col := 1;
end loop;
-- Default value of (0,0) is used for the special __HEAP -- Loop through cross reference entries for this scope
-- variable so use another default value.
Entity_Line := 0; for X in S.From_Xref .. S.To_Xref loop
Entity_Col := 1;
-- Loop through cross reference entries for this scope Output_One_Xref : declare
R : SPARK_Xref_Record renames
SPARK_Xref_Table.Table (X);
loop begin
exit when XStart = XStop + 1; if R.Entity_Line /= Entity_Line
pragma Assert (XStart <= XStop); or else R.Entity_Col /= Entity_Col
then
Write_Info_Terminate;
Output_One_Xref : declare Write_Info_Initiate ('F');
R : SPARK_Xref_Record renames Write_Info_Char (' ');
SPARK_Xref_Table.Table (XStart); Write_Info_Nat (R.Entity_Line);
Write_Info_Char (R.Etype);
Write_Info_Nat (R.Entity_Col);
Write_Info_Char (' ');
begin Write_Info_Str (R.Entity_Name.all);
if R.Entity_Line /= Entity_Line
or else R.Entity_Col /= Entity_Col Entity_Line := R.Entity_Line;
then Entity_Col := R.Entity_Col;
Write_Info_Terminate; 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 (' '); Write_Info_Char (' ');
for N in R.Entity_Name'Range loop if R.File_Num /= File then
Write_Info_Char (R.Entity_Name (N)); Write_Info_Nat (R.File_Num);
end loop; Write_Info_Char ('|');
File := R.File_Num;
Entity_Line := R.Entity_Line; Scope := 0;
Entity_Col := R.Entity_Col; end if;
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;
Write_Info_Terminate; if R.Scope_Num /= Scope then
end Output_One_Scope; Write_Info_Char ('.');
Write_Info_Nat (R.Scope_Num);
Write_Info_Char (':');
Scope := R.Scope_Num;
end if;
<<Continue>> Write_Info_Nat (R.Line);
Start := Start + 1; 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 loop;
end; end;
end loop; end loop;
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- 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 -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -43,6 +43,9 @@ generic ...@@ -43,6 +43,9 @@ generic
with procedure Write_Info_Char (C : Character) is <>; with procedure Write_Info_Char (C : Character) is <>;
-- Output one character -- 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 <>; with procedure Write_Info_Initiate (Key : Character) is <>;
-- Initiate write of new line to output file, the parameter is the -- Initiate write of new line to output file, the parameter is the
-- keyword character for the line. -- keyword character for the line.
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- 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 -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -160,7 +160,10 @@ package body SPARK_Xrefs is ...@@ -160,7 +160,10 @@ package body SPARK_Xrefs is
procedure pspark is procedure pspark is
procedure Write_Info_Char (C : Character) renames Write_Char; 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; function Write_Info_Col return Positive;
-- Return next column for writing -- Return next column for writing
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment