From ef25192beef53daf8cecb32384b1d69d1cfddac9 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 2 May 2016 09:50:45 +0000 Subject: [PATCH] a-tigeli.adb (Get_Line): Always set Last prior to returning. 2016-05-02 Yannick Moy * a-tigeli.adb (Get_Line): Always set Last prior to returning. 2016-05-02 Yannick Moy * 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 --- gcc/ada/ChangeLog | 14 +++ gcc/ada/a-tigeli.adb | 8 +- gcc/ada/lib-xref.adb | 23 +++-- gcc/ada/put_spark_xrefs.adb | 206 +++++++++++++++++--------------------------- gcc/ada/put_spark_xrefs.ads | 5 +- gcc/ada/spark_xrefs.adb | 7 +- 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 + + * a-tigeli.adb (Get_Line): Always set Last prior to returning. + +2016-05-02 Yannick Moy + + * 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 * 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; - <> - 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 -- 2.7.4