GNATprove relied on frontend writing cross-references data into the ALI
files to synthesize Global contracts. Now this is done by the GNATprove
itself. This patch deconstructs the frontend code, that is no longer needed.
No test, as only dead code removed.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-08 Piotr Trojanek <troja...@adacore.com>
* lib-xref-spark_specific.adb (Add_SPARK_Scope): Remove detection of
protected operations.
(Add_SPARK_Xrefs): Simplify detection of empty entities.
* get_spark_xrefs.ads, get_spark_xrefs.adb, put_spark_xrefs.ads,
put_spark_xrefs.adb, spark_xrefs_test.adb: Remove code for writing,
reading and testing SPARK cross-references stored in the ALI files.
* lib-xref.ads (Output_SPARK_Xrefs): Remove.
* lib-writ.adb (Write_ALI): Do not write SPARK cross-references to the
ALI file.
* spark_xrefs.ads, spark_xrefs.adb (pspark): Remove, together
with description of the SPARK xrefs ALI format.
* gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Remove get_spark_refs.o
and put_spark_refs.o.
Index: get_spark_xrefs.adb
===================================================================
--- get_spark_xrefs.adb (revision 254523)
+++ get_spark_xrefs.adb (working copy)
@@ -1,493 +0,0 @@
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- G E T _ S P A R K _ X R E F S --
--- --
--- B o d y --
--- --
--- 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
-with SPARK_Xrefs; use SPARK_Xrefs;
-with Types; use Types;
-
-with Ada.IO_Exceptions; use Ada.IO_Exceptions;
-
-procedure Get_SPARK_Xrefs is
- C : Character;
-
- use ASCII;
- -- For CR/LF
-
- Cur_File : Nat;
- -- Dependency number for the current file
-
- Cur_Scope : Nat;
- -- Scope number for the current scope entity
-
- Cur_File_Idx : File_Index;
- -- Index in SPARK_File_Table of the current file
-
- Cur_Scope_Idx : Scope_Index;
- -- Index in SPARK_Scope_Table of the current scope
-
- Name_Str : String (1 .. 32768);
- Name_Len : Natural := 0;
- -- Local string used to store name of File/entity scanned as
- -- Name_Str (1 .. Name_Len).
-
- File_Name : String_Ptr;
- Unit_File_Name : String_Ptr;
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- function At_EOL return Boolean;
- -- Skips any spaces, then checks if at the end of a line. If so, returns
- -- True (but does not skip the EOL sequence). If not, then returns False.
-
- procedure Check (C : Character);
- -- Checks that file is positioned at given character, and if so skips past
- -- it, If not, raises Data_Error.
-
- function Get_Nat return Nat;
- -- On entry the file is positioned to a digit. On return, the file is
- -- positioned past the last digit, and the returned result is the decimal
- -- value read. Data_Error is raised for overflow (value greater than
- -- Int'Last), or if the initial character is not a digit.
-
- procedure Get_Name;
- -- On entry the file is positioned to a name. On return, the file is
- -- positioned past the last character, and the name scanned is returned
- -- in Name_Str (1 .. Name_Len).
-
- procedure Skip_EOL;
- -- Called with the current character about to be read being LF or CR. Skips
- -- past CR/LF characters until either a non-CR/LF character is found, or
- -- the end of file is encountered.
-
- procedure Skip_Spaces;
- -- Skips zero or more spaces at the current position, leaving the file
- -- positioned at the first non-blank character (or Types.EOF).
-
- ------------
- -- At_EOL --
- ------------
-
- function At_EOL return Boolean is
- begin
- Skip_Spaces;
- return Nextc = CR or else Nextc = LF;
- end At_EOL;
-
- -----------
- -- Check --
- -----------
-
- procedure Check (C : Character) is
- begin
- if Nextc = C then
- Skipc;
- else
- raise Data_Error;
- end if;
- end Check;
-
- -------------
- -- Get_Nat --
- -------------
-
- function Get_Nat return Nat is
- C : Character := Nextc;
- Val : Nat := 0;
-
- begin
- if C not in '0' .. '9' then
- raise Data_Error;
- end if;
-
- -- Loop to read digits of integer value
-
- loop
- declare
- pragma Unsuppress (Overflow_Check);
- begin
- Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0'));
- end;
-
- Skipc;
- C := Nextc;
-
- exit when C not in '0' .. '9';
- end loop;
-
- return Val;
-
- exception
- when Constraint_Error =>
- raise Data_Error;
- end Get_Nat;
-
- --------------
- -- Get_Name --
- --------------
-
- procedure Get_Name is
- N : Natural := 0;
-
- begin
- while Nextc > ' ' loop
- N := N + 1;
- Name_Str (N) := Getc;
- end loop;
-
- Name_Len := N;
- end Get_Name;
-
- --------------
- -- Skip_EOL --
- --------------
-
- procedure Skip_EOL is
- C : Character;
-
- begin
- loop
- Skipc;
- C := Nextc;
- exit when C /= LF and then C /= CR;
-
- if C = ' ' then
- Skip_Spaces;
- C := Nextc;
- exit when C /= LF and then C /= CR;
- end if;
- end loop;
- end Skip_EOL;
-
- -----------------
- -- Skip_Spaces --
- -----------------
-
- procedure Skip_Spaces is
- begin
- while Nextc = ' ' loop
- Skipc;
- end loop;
- end Skip_Spaces;
-
--- Start of processing for Get_SPARK_Xrefs
-
-begin
- Initialize_SPARK_Tables;
-
- Cur_File := 0;
- Cur_Scope := 0;
- Cur_File_Idx := 1;
- Cur_Scope_Idx := 0;
-
- -- Loop through lines of SPARK cross-reference information
-
- while Nextc = 'F' loop
- Skipc;
-
- C := Getc;
-
- -- Make sure first line is a File line
-
- if SPARK_File_Table.Last = 0 and then C /= 'D' then
- raise Data_Error;
- end if;
-
- -- Otherwise dispatch on type of line
-
- case C is
-
- -- Header entry for scope section
-
- when 'D' =>
-
- -- Complete previous entry if any
-
- if SPARK_File_Table.Last /= 0 then
- SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
- SPARK_Scope_Table.Last;
- end if;
-
- -- Scan out dependency number and file name
-
- Skip_Spaces;
- Cur_File := Get_Nat;
- Skip_Spaces;
-
- Get_Name;
- File_Name := new String'(Name_Str (1 .. Name_Len));
- Skip_Spaces;
-
- -- Scan out unit file name when present (for subunits)
-
- if Nextc = '-' then
- Skipc;
- Check ('>');
- Skip_Spaces;
- Get_Name;
- Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
-
- else
- Unit_File_Name := null;
- end if;
-
- -- Make new File table entry (will fill in To_Scope later)
-
- SPARK_File_Table.Append (
- (File_Name => File_Name,
- Unit_File_Name => Unit_File_Name,
- File_Num => Cur_File,
- From_Scope => SPARK_Scope_Table.Last + 1,
- To_Scope => 0));
-
- -- Initialize counter for scopes
-
- Cur_Scope := 1;
-
- -- Scope entry
-
- when 'S' =>
- declare
- Spec_File : Nat;
- Spec_Scope : Nat;
- Scope : Nat;
- Line : Nat;
- Col : Nat;
- Typ : Character;
-
- begin
- -- Scan out location
-
- Skip_Spaces;
- Check ('.');
- Scope := Get_Nat;
- Check (' ');
- Line := Get_Nat;
- Typ := Getc;
- Col := Get_Nat;
-
- pragma Assert (Scope = Cur_Scope);
-
- -- Scan out scope entity name
-
- Skip_Spaces;
- Get_Name;
- Skip_Spaces;
-
- if Nextc = '-' then
- Skipc;
- Check ('>');
- Skip_Spaces;
- Spec_File := Get_Nat;
- Check ('.');
- Spec_Scope := Get_Nat;
-
- else
- Spec_File := 0;
- Spec_Scope := 0;
- end if;
-
- -- Make new scope table entry (will fill in From_Xref and
- -- To_Xref later). Initial range (From_Xref .. To_Xref) is
- -- empty for scopes without entities.
-
- SPARK_Scope_Table.Append (
- (Scope_Entity => Empty,
- Scope_Name => new String'(Name_Str (1 .. Name_Len)),
- File_Num => Cur_File,
- Scope_Num => Cur_Scope,
- Spec_File_Num => Spec_File,
- Spec_Scope_Num => Spec_Scope,
- Line => Line,
- Stype => Typ,
- Col => Col,
- From_Xref => 1,
- To_Xref => 0));
- end;
-
- -- Update counter for scopes
-
- Cur_Scope := Cur_Scope + 1;
-
- -- Header entry for cross-ref section
-
- when 'X' =>
-
- -- Scan out dependency number and file name (ignored)
-
- Skip_Spaces;
- Cur_File := Get_Nat;
- Skip_Spaces;
- Get_Name;
-
- -- Update component From_Xref of current file if first reference
- -- in this file.
-
- while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
- loop
- Cur_File_Idx := Cur_File_Idx + 1;
- end loop;
-
- -- Scan out scope entity number and entity name (ignored)
-
- Skip_Spaces;
- Check ('.');
- Cur_Scope := Get_Nat;
- Skip_Spaces;
- Get_Name;
-
- -- Update component To_Xref of previous scope
-
- if Cur_Scope_Idx /= 0 then
- SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
- SPARK_Xref_Table.Last;
- end if;
-
- -- Update component From_Xref of current scope
-
- Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope;
-
- while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /=
- Cur_Scope
- loop
- Cur_Scope_Idx := Cur_Scope_Idx + 1;
- end loop;
-
- SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
- SPARK_Xref_Table.Last + 1;
-
- -- Cross reference entry
-
- when ' ' =>
- declare
- XR_Entity : String_Ptr;
- XR_Entity_Line : Nat;
- XR_Entity_Col : Nat;
- XR_Entity_Typ : Character;
-
- XR_File : Nat;
- -- Keeps track of the current file (changed by nn|)
-
- XR_Scope : Nat;
- -- Keeps track of the current scope (changed by nn:)
-
- begin
- XR_File := Cur_File;
- XR_Scope := Cur_Scope;
-
- XR_Entity_Line := Get_Nat;
- XR_Entity_Typ := Getc;
- XR_Entity_Col := Get_Nat;
-
- Skip_Spaces;
- Get_Name;
- XR_Entity := new String'(Name_Str (1 .. Name_Len));
-
- -- Initialize to scan items on one line
-
- Skip_Spaces;
-
- -- Loop through cross-references for this entity
-
- loop
- declare
- Line : Nat;
- Col : Nat;
- N : Nat;
- Rtype : Character;
-
- begin
- Skip_Spaces;
-
- if At_EOL then
- Skip_EOL;
- exit when Nextc /= '.';
- Skipc;
- Skip_Spaces;
- end if;
-
- if Nextc = '.' then
- Skipc;
- XR_Scope := Get_Nat;
- Check (':');
-
- else
- N := Get_Nat;
-
- if Nextc = '|' then
- XR_File := N;
- Skipc;
-
- else
- Line := N;
- Rtype := Getc;
- Col := Get_Nat;
-
- pragma Assert
- (Rtype = 'r' or else
- Rtype = 'c' or else
- Rtype = 'm' or else
- Rtype = 's');
-
- SPARK_Xref_Table.Append (
- (Entity_Name => XR_Entity,
- Entity_Line => XR_Entity_Line,
- Etype => XR_Entity_Typ,
- Entity_Col => XR_Entity_Col,
- File_Num => XR_File,
- Scope_Num => XR_Scope,
- Line => Line,
- Rtype => Rtype,
- Col => Col));
- end if;
- end if;
- end;
- end loop;
- end;
-
- -- No other SPARK lines are possible
-
- when others =>
- raise Data_Error;
- end case;
-
- -- For cross reference lines, the EOL character has been skipped already
-
- if C /= ' ' then
- Skip_EOL;
- end if;
- end loop;
-
- -- Here with all Xrefs stored, complete last entries in File/Scope tables
-
- if SPARK_File_Table.Last /= 0 then
- SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
- SPARK_Scope_Table.Last;
- end if;
-
- if Cur_Scope_Idx /= 0 then
- SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
- end if;
-end Get_SPARK_Xrefs;
Index: get_spark_xrefs.ads
===================================================================
--- get_spark_xrefs.ads (revision 254523)
+++ get_spark_xrefs.ads (working copy)
@@ -1,60 +0,0 @@
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- G E T _ S P A R K _ X R E F S --
--- --
--- S p e c --
--- --
--- Copyright (C) 2011-2013, 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This package contains the function used to read SPARK cross-reference
--- information from an ALI file and populate the tables defined in package
--- SPARK_Xrefs with the result.
-
-generic
- -- These subprograms provide access to the ALI file. Locating, opening and
- -- providing access to the ALI file is the callers' responsibility.
-
- with function Getc return Character is <>;
- -- Get next character, positioning the ALI file ready to read the following
- -- character (equivalent to calling Nextc, then Skipc). If the end of file
- -- is encountered, the value Types.EOF is returned.
-
- with function Nextc return Character is <>;
- -- Look at the next character, and return it, leaving the position of the
- -- file unchanged, so that a subsequent call to Getc or Nextc will return
- -- this same character. If the file is positioned at the end of file, then
- -- Types.EOF is returned.
-
- with procedure Skipc is <>;
- -- Skip past the current character (which typically was read with Nextc),
- -- and position to the next character, which will be returned by the next
- -- call to Getc or Nextc.
-
-procedure Get_SPARK_Xrefs;
--- Load SPARK cross-reference information from ALI file text format into
--- internal SPARK tables (SPARK_Xrefs.SPARK_Xref_Table,
--- SPARK_Xrefs.SPARK_Scope_Table and SPARK_Xrefs.SPARK_File_Table). On entry
--- the input file is positioned to the initial 'F' of the first SPARK specific
--- line in the ALI file. On return, the file is positioned either to the end
--- of file, or to the first character of the line following the SPARK specific
--- information (which will never start with an 'F').
---
--- If a format error is detected in the input, then an exception is raised
--- (Ada.IO_Exceptions.Data_Error), with the file positioned to the error.
Index: lib-writ.adb
===================================================================
--- lib-writ.adb (revision 254523)
+++ lib-writ.adb (working copy)
@@ -1572,7 +1572,6 @@
if Opt.Xref_Active and then GNATprove_Mode then
SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
Num_Sdep => Num_Sdep);
- SPARK_Specific.Output_SPARK_Xrefs;
end if;
-- Output final blank line and we are done. This final blank line is
Index: lib-xref.adb
===================================================================
--- lib-xref.adb (revision 254523)
+++ lib-xref.adb (working copy)
@@ -27,6 +27,7 @@
with Csets; use Csets;
with Elists; use Elists;
with Errout; use Errout;
+with Lib.Util; use Lib.Util;
with Nlists; use Nlists;
with Opt; use Opt;
with Restrict; use Restrict;
Index: lib-xref.ads
===================================================================
--- lib-xref.ads (revision 254523)
+++ lib-xref.ads (working copy)
@@ -26,9 +26,7 @@
-- This package contains for collecting and outputting cross-reference
-- information.
-with Einfo; use Einfo;
-with Lib.Util; use Lib.Util;
-with Put_SPARK_Xrefs;
+with Einfo; use Einfo;
package Lib.Xref is
@@ -647,11 +645,6 @@
-- files and scopes) and from shared cross-references. Fill in the
-- tables in library package called SPARK_Xrefs.
- procedure Output_SPARK_Xrefs is new Put_SPARK_Xrefs;
- -- Output SPARK cross-reference information to the ALI files, based on
- -- the information collected in the tables in library package called
- -- SPARK_Xrefs, and using routines in Lib.Util.
-
generic
with procedure Process (N : Node_Id) is <>;
procedure Traverse_Compilation_Unit
Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb (revision 254523)
+++ lib-xref-spark_specific.adb (working copy)
@@ -139,30 +139,17 @@
case Ekind (E) is
when E_Entry
| E_Entry_Family
+ | E_Function
| E_Generic_Function
| E_Generic_Package
| E_Generic_Procedure
| E_Package
+ | E_Procedure
| E_Protected_Type
| E_Task_Type
=>
Typ := Xref_Entity_Letters (Ekind (E));
- when E_Function
- | E_Procedure
- =>
- -- In SPARK we need to distinguish protected functions and
- -- procedures from ordinary subprograms, but there are no
- -- special Xref letters for them. Since this distiction is
- -- only needed to detect protected calls, we pretend that
- -- such calls are entry calls.
-
- if Ekind (Scope (E)) = E_Protected_Type then
- Typ := Xref_Entity_Letters (E_Entry);
- else
- Typ := Xref_Entity_Letters (Ekind (E));
- end if;
-
when E_Package_Body
| E_Protected_Body
| E_Subprogram_Body
@@ -670,7 +657,6 @@
Prev_Loc : Source_Ptr;
Prev_Typ : Character;
Ref_Count : Nat;
- Ref_Id : Entity_Id;
Ref_Name : String_Ptr;
Scope_Id : Scope_Index;
@@ -795,7 +781,6 @@
return;
end if;
- Ref_Id := Empty;
Scope_Id := 1;
From_Index := 1;
@@ -833,7 +818,7 @@
pragma Assert (Scope_Id <= SPARK_Scope_Table.Last);
end loop;
- if Ref.Ent /= Ref_Id then
+ if Present (Ref.Ent) then
Ref_Name := new String'(Unique_Name (Ref.Ent));
end if;
Index: put_spark_xrefs.adb
===================================================================
--- put_spark_xrefs.adb (revision 254523)
+++ put_spark_xrefs.adb (working copy)
@@ -1,194 +0,0 @@
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- P U T _ S P A R K _ X R E F S --
--- --
--- B o d y --
--- --
--- 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
-with SPARK_Xrefs; use SPARK_Xrefs;
-
-procedure Put_SPARK_Xrefs is
-begin
- -- Loop through entries in SPARK_File_Table
-
- for J in 1 .. SPARK_File_Table.Last loop
- declare
- F : SPARK_File_Record renames SPARK_File_Table.Table (J);
-
- begin
- Write_Info_Initiate ('F');
- Write_Info_Char ('D');
- Write_Info_Char (' ');
- Write_Info_Nat (F.File_Num);
- Write_Info_Char (' ');
-
- 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_Str (" -> " & F.Unit_File_Name.all);
- end if;
-
- Write_Info_Terminate;
-
- -- Loop through scope entries for this file
-
- for J in F.From_Scope .. F.To_Scope loop
- declare
- S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (J);
-
- begin
- Write_Info_Initiate ('F');
- Write_Info_Char ('S');
- Write_Info_Char (' ');
- Write_Info_Char ('.');
- Write_Info_Nat (S.Scope_Num);
- Write_Info_Char (' ');
- Write_Info_Nat (S.Line);
- Write_Info_Char (S.Stype);
- Write_Info_Nat (S.Col);
- Write_Info_Char (' ');
-
- pragma Assert (S.Scope_Name.all /= "");
-
- Write_Info_Str (S.Scope_Name.all);
-
- if S.Spec_File_Num /= 0 then
- Write_Info_Str (" -> ");
- Write_Info_Nat (S.Spec_File_Num);
- Write_Info_Char ('.');
- Write_Info_Nat (S.Spec_Scope_Num);
- end if;
-
- Write_Info_Terminate;
- end;
- end loop;
- end;
- end loop;
-
- -- Loop through entries in SPARK_File_Table
-
- for J in 1 .. SPARK_File_Table.Last loop
- declare
- F : SPARK_File_Record renames SPARK_File_Table.Table (J);
- File : Nat;
- Scope : Nat;
- Entity_Line : Nat;
- Entity_Col : Nat;
-
- begin
- -- Loop through scope entries for this file
-
- for K in F.From_Scope .. F.To_Scope loop
- Output_One_Scope : declare
- S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (K);
-
- begin
- -- Write only non-empty tables
-
- if S.From_Xref <= S.To_Xref then
-
- 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 (' ');
-
- Write_Info_Str (S.Scope_Name.all);
-
- -- Default value of (0,0) is used for the special __HEAP
- -- variable so use another default value.
-
- Entity_Line := 0;
- Entity_Col := 1;
-
- -- Loop through cross reference entries for this scope
-
- for X in S.From_Xref .. S.To_Xref loop
-
- Output_One_Xref : declare
- R : SPARK_Xref_Record renames
- SPARK_Xref_Table.Table (X);
-
- begin
- if R.Entity_Line /= Entity_Line
- or else R.Entity_Col /= Entity_Col
- then
- Write_Info_Terminate;
-
- 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_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_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;
-
- end loop;
-
- Write_Info_Terminate;
- end if;
- end Output_One_Scope;
- end loop;
- end;
- end loop;
-end Put_SPARK_Xrefs;
Index: put_spark_xrefs.ads
===================================================================
--- put_spark_xrefs.ads (revision 254523)
+++ put_spark_xrefs.ads (working copy)
@@ -1,62 +0,0 @@
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- P U T _ S P A R K _ X R E F S --
--- --
--- S p e c --
--- --
--- 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This package contains the function used to read SPARK cross-reference
--- information from the internal tables defined in package SPARK_Xrefs, and
--- output text information for the ALI file. The interface allows control over
--- the destination of the output, so that this routine can also be used for
--- debugging purposes.
-
-with Types; use Types;
-
-generic
- -- The following procedures are used to output text information. The
- -- destination of the text information is thus under control of the
- -- particular instantiation. In particular, this procedure is used to
- -- write output to the ALI file, and also for debugging output.
-
- with function Write_Info_Col return Positive is <>;
- -- Return the column in which the next character will be written
-
- 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.
-
- with procedure Write_Info_Nat (N : Nat) is <>;
- -- Write image of N to output file with no leading or trailing blanks
-
- with procedure Write_Info_Terminate is <>;
- -- Terminate current info line and output lines built in Info_Buffer
-
-procedure Put_SPARK_Xrefs;
--- Read information from SPARK tables (SPARK_Xrefs.SPARK_Xref_Table,
--- SPARK_Xrefs.SPARK_Scope_Table and SPARK_Xrefs.SPARK_File_Table) and output
--- corresponding information in ALI format using the Write_Info procedures.
Index: spark_xrefs.adb
===================================================================
--- spark_xrefs.adb (revision 254523)
+++ spark_xrefs.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2017, 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- --
@@ -23,8 +23,7 @@
-- --
------------------------------------------------------------------------------
-with Output; use Output;
-with Put_SPARK_Xrefs;
+with Output; use Output;
package body SPARK_Xrefs is
@@ -153,54 +152,4 @@
SPARK_Xref_Table.Init;
end Initialize_SPARK_Tables;
- ------------
- -- pspark --
- ------------
-
- procedure pspark is
-
- procedure Write_Info_Char (C : Character) renames Write_Char;
- -- 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
-
- procedure Write_Info_Initiate (Key : Character) renames Write_Char;
- -- Start new one and write one character;
-
- procedure Write_Info_Nat (N : Nat);
- -- Write value of N
-
- procedure Write_Info_Terminate renames Write_Eol;
- -- Terminate current line
-
- --------------------
- -- Write_Info_Col --
- --------------------
-
- function Write_Info_Col return Positive is
- begin
- return Positive (Column);
- end Write_Info_Col;
-
- --------------------
- -- Write_Info_Nat --
- --------------------
-
- procedure Write_Info_Nat (N : Nat) is
- begin
- Write_Int (N);
- end Write_Info_Nat;
-
- procedure Debug_Put_SPARK_Xrefs is new Put_SPARK_Xrefs;
-
- -- Start of processing for pspark
-
- begin
- Debug_Put_SPARK_Xrefs;
- end pspark;
-
end SPARK_Xrefs;
Index: spark_xrefs.ads
===================================================================
--- spark_xrefs.ads (revision 254523)
+++ spark_xrefs.ads (working copy)
@@ -25,173 +25,21 @@
-- This package defines tables used to store information needed for the SPARK
-- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the
--- SPARK-specific cross-reference information before writing it to the ALI
--- file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read/write the textual
--- representation that is stored in the ALI file.
+-- SPARK-specific cross-reference information.
with Table;
-with Types; use Types;
+with Types; use Types;
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:
- -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are
- -- also defined in this unit.
+ -- SPARK cross-reference information is stored internally using three
+ -- tables: SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which
+ -- are defined in this unit.
-- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK
-- cross-reference information from the complete set of cross-references
-- generated during compilation.
- -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the
- -- internal tables with corresponding information.
-
- -- Put_SPARK_Xrefs reads the internal tables and generates text lines in
- -- the ALI format.
-
- ----------------------------
- -- SPARK Xrefs ALI Format --
- ----------------------------
-
- -- 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 GNATprove_Mode is True.
-
- -- The SPARK cross-reference information comes after the shared
- -- 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/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)?
-
- -- This header precedes scope information for the unit identified by
- -- dependency number and file name. The dependency number is the index
- -- into the generated D lines and is ones-origin (e.g. 2 = reference to
- -- second generated D line).
-
- -- The list of FD lines should match the list of D lines defined in the
- -- ALI file, in the same order.
-
- -- Note that the filename here will reflect the original name if a
- -- Source_Reference pragma was encountered (since all line number
- -- references will be with respect to the original file).
-
- -- Note: the filename is redundant in that it could be deduced from the
- -- corresponding D line, but it is convenient at least for human
- -- reading of the SPARK cross-reference information, and means that
- -- the SPARK cross-reference information can stand on its own without
- -- needing other parts of the ALI file.
-
- -- The optional unit filename is given only for subunits.
-
- -- FS . scope line type col entity (-> spec-file . spec-scope)?
-
- -- (The ? mark stands for an optional entry in the syntax)
-
- -- scope is the ones-origin scope number for the current file (e.g. 2 =
- -- reference to the second FS line in this FD block).
-
- -- line is the line number of the scope entity. The name of the entity
- -- starts in column col. Columns are numbered from one, and if
- -- horizontal tab characters are present, the column number is computed
- -- assuming standard 1,9,17,.. tab stops. For example, if the entity is
- -- the first token on the line, and is preceded by space-HT-space, then
- -- the column would be column 10.
-
- -- type is a single letter identifying the type of the entity, using
- -- the same code as in cross-references:
-
- -- K = package (k = generic package)
- -- V = function (v = generic function)
- -- U = procedure (u = generic procedure)
- -- Y = entry
-
- -- col is the column number of the scope entity
-
- -- entity is the name of the scope entity, with casing in the canonical
- -- casing for the source file where it is defined.
-
- -- spec-file and spec-scope are respectively the file and scope for the
- -- spec corresponding to the current body scope, when they differ.
-
- -- ------------------
- -- -- Xref Section --
- -- ------------------
-
- -- A second section defines cross-references useful for computing global
- -- variables read/written in each subprogram/package/protected_type/
- -- task_type.
-
- -- FX dependency-number filename . entity-number entity
-
- -- dependency-number and filename identify a file in FD lines
-
- -- entity-number and entity identify a scope in FS lines
- -- for the previously identified file.
-
- -- (filename and entity are just a textual representations of
- -- dependency-number and entity-number)
-
- -- F line typ col entity ref*
-
- -- line is the line number of the referenced entity
-
- -- typ is the type of the referenced entity, using a code similar to
- -- the one used for cross-references:
-
- -- > = IN parameter
- -- < = OUT parameter
- -- = = IN OUT parameter
- -- * = all other cases
-
- -- col is the column number of the referenced entity
-
- -- entity is the name of the referenced entity as written in the source
- -- file where it is defined.
-
- -- There may be zero or more ref entries on each line
-
- -- (file |)? ((. scope :)? line type col)*
-
- -- file is the dependency number of the file with the reference. It and
- -- the following vertical bar are omitted if the file is the same as
- -- the previous ref, and the refs for the current file are first (and
- -- do not need a bar).
-
- -- scope is the scope number of the scope with the reference. It and
- -- the following colon are omitted if the scope is the same as the
- -- previous ref, and the refs for the current scope are first (and do
- -- not need a colon).
-
- -- line is the line number of the reference
-
- -- col is the column number of the reference
-
- -- type is one of the following, using the same code as in
- -- cross-references:
-
- -- m = modification
- -- r = reference
- -- c = reference to constant object
- -- s = subprogram reference in a static call
-
- -- Special entries for reads and writes to memory reference a special
- -- variable called "__HEAP". These special entries are present in every
- -- scope where reads and writes to memory are present. Line and column for
- -- this special variable are always 0.
-
- -- Examples: ??? add examples here
-
-- -------------------------------
-- -- Generated Globals Section --
-- -------------------------------
@@ -389,8 +237,4 @@
-- Debug routine to dump internal SPARK cross-reference tables. This is a
-- raw format dump showing exactly what the tables contain.
- procedure pspark;
- -- Debugging procedure to output contents of SPARK cross-reference binary
- -- tables in the format in which they appear in an ALI file.
-
end SPARK_Xrefs;
Index: spark_xrefs_test.adb
===================================================================
--- spark_xrefs_test.adb (revision 254523)
+++ spark_xrefs_test.adb (working copy)
@@ -1,321 +0,0 @@
-------------------------------------------------------------------------------
--- --
--- GNAT SYSTEM UTILITIES --
--- --
--- S P A R K _ X R E F S _ T E S T --
--- --
--- B o d y --
--- --
--- Copyright (C) 2011-2013, 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
--- for more details. You should have received a copy of the GNU General --
--- Public License distributed with GNAT; see file COPYING3. If not, go to --
--- http://www.gnu.org/licenses for a complete copy of the license. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This utility program is used to test proper operation of the
--- Get_SPARK_Xrefs and Put_SPARK_Xrefs units. To run it, compile any source
--- file with switch -gnatd.E or -gnatd.F to get an ALI file file.ALI
--- containing SPARK information. Then run this utility using:
-
--- spark_xrefs_test file.ali
-
--- This test will read the SPARK cross-reference information from the ALI
--- file, and use Get_SPARK_Xrefs to store this in binary form in the internal
--- tables in SPARK_Xrefs. Then Put_SPARK_Xrefs is used to write the
--- information from these tables back into text form. This output is compared
--- with the original SPARK cross-reference information in the ALI file and the
--- two should be identical. If not an error message is output.
-
-with Get_SPARK_Xrefs;
-with Put_SPARK_Xrefs;
-
-with SPARK_Xrefs; use SPARK_Xrefs;
-with Types; use Types;
-
-with Ada.Command_Line; use Ada.Command_Line;
-with Ada.Streams; use Ada.Streams;
-with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
-with Ada.Text_IO;
-
-with GNAT.OS_Lib; use GNAT.OS_Lib;
-
-procedure SPARK_Xrefs_Test is
- Infile : File_Type;
- Name1 : String_Access;
- Outfile_1 : File_Type;
- Name2 : String_Access;
- Outfile_2 : File_Type;
- C : Character;
-
- Stop : exception;
- -- Terminate execution
-
- Diff_Exec : constant String_Access := Locate_Exec_On_Path ("diff");
- Diff_Result : Integer;
-
- use ASCII;
-
-begin
- if Argument_Count /= 1 then
- Ada.Text_IO.Put_Line ("Usage: spark_xrefs_test FILE.ali");
- raise Stop;
- end if;
-
- Name1 := new String'(Argument (1) & ".1");
- Name2 := new String'(Argument (1) & ".2");
-
- Open (Infile, In_File, Argument (1));
- Create (Outfile_1, Out_File, Name1.all);
- Create (Outfile_2, Out_File, Name2.all);
-
- -- Read input file till we get to first 'F' line
-
- Process : declare
- Output_Col : Positive := 1;
-
- function Get_Char (F : File_Type) return Character;
- -- Read one character from specified file
-
- procedure Put_Char (F : File_Type; C : Character);
- -- Write one character to specified file
-
- function Get_Output_Col return Positive;
- -- Return current column in output file, where each line starts at
- -- column 1 and terminate with LF, and HT is at columns 1, 9, etc.
- -- All output is supposed to be carried through Put_Char.
-
- --------------
- -- Get_Char --
- --------------
-
- function Get_Char (F : File_Type) return Character is
- Item : Stream_Element_Array (1 .. 1);
- Last : Stream_Element_Offset;
-
- begin
- Read (F, Item, Last);
-
- if Last /= 1 then
- return Types.EOF;
- else
- return Character'Val (Item (1));
- end if;
- end Get_Char;
-
- --------------------
- -- Get_Output_Col --
- --------------------
-
- function Get_Output_Col return Positive is
- begin
- return Output_Col;
- end Get_Output_Col;
-
- --------------
- -- Put_Char --
- --------------
-
- procedure Put_Char (F : File_Type; C : Character) is
- Item : Stream_Element_Array (1 .. 1);
-
- begin
- if C /= CR and then C /= EOF then
- if C = LF then
- Output_Col := 1;
- elsif C = HT then
- Output_Col := ((Output_Col + 6) / 8) * 8 + 1;
- else
- Output_Col := Output_Col + 1;
- end if;
-
- Item (1) := Character'Pos (C);
- Write (F, Item);
- end if;
- end Put_Char;
-
- -- Subprograms used by Get_SPARK_Xrefs (these also copy the output to
- -- Outfile_1 for later comparison with the output generated by
- -- Put_SPARK_Xrefs).
-
- function Getc return Character;
- function Nextc return Character;
- procedure Skipc;
-
- ----------
- -- Getc --
- ----------
-
- function Getc return Character is
- C : Character;
- begin
- C := Get_Char (Infile);
- Put_Char (Outfile_1, C);
- return C;
- end Getc;
-
- -----------
- -- Nextc --
- -----------
-
- function Nextc return Character is
- C : Character;
-
- begin
- C := Get_Char (Infile);
-
- if C /= EOF then
- Set_Index (Infile, Index (Infile) - 1);
- end if;
-
- return C;
- end Nextc;
-
- -----------
- -- Skipc --
- -----------
-
- procedure Skipc is
- C : Character;
- pragma Unreferenced (C);
- begin
- C := Getc;
- end Skipc;
-
- -- Subprograms used by Put_SPARK_Xrefs, which write information to
- -- Outfile_2.
-
- function Write_Info_Col return Positive;
- procedure Write_Info_Char (C : Character);
- procedure Write_Info_Initiate (Key : Character);
- procedure Write_Info_Nat (N : Nat);
- procedure Write_Info_Terminate;
-
- --------------------
- -- Write_Info_Col --
- --------------------
-
- function Write_Info_Col return Positive is
- begin
- return Get_Output_Col;
- end Write_Info_Col;
-
- ---------------------
- -- Write_Info_Char --
- ---------------------
-
- procedure Write_Info_Char (C : Character) is
- begin
- Put_Char (Outfile_2, C);
- end Write_Info_Char;
-
- -------------------------
- -- Write_Info_Initiate --
- -------------------------
-
- procedure Write_Info_Initiate (Key : Character) is
- begin
- Write_Info_Char (Key);
- end Write_Info_Initiate;
-
- --------------------
- -- Write_Info_Nat --
- --------------------
-
- procedure Write_Info_Nat (N : Nat) is
- begin
- if N > 9 then
- Write_Info_Nat (N / 10);
- end if;
-
- Write_Info_Char (Character'Val (48 + N mod 10));
- end Write_Info_Nat;
-
- --------------------------
- -- Write_Info_Terminate --
- --------------------------
-
- procedure Write_Info_Terminate is
- begin
- Write_Info_Char (LF);
- end Write_Info_Terminate;
-
- -- Local instantiations of Put_SPARK_Xrefs and Get_SPARK_Xrefs
-
- procedure Get_SPARK_Xrefs_Info is new Get_SPARK_Xrefs;
- procedure Put_SPARK_Xrefs_Info is new Put_SPARK_Xrefs;
-
- -- Start of processing for Process
-
- begin
- -- Loop to skip till first 'F' line
-
- loop
- C := Get_Char (Infile);
-
- if C = EOF then
- raise Stop;
-
- elsif C = LF or else C = CR then
- loop
- C := Get_Char (Infile);
- exit when C /= LF and then C /= CR;
- end loop;
-
- exit when C = 'F';
- end if;
- end loop;
-
- -- Position back to initial 'F' of first 'F' line
-
- Set_Index (Infile, Index (Infile) - 1);
-
- -- Read SPARK cross-reference information to internal SPARK tables, also
- -- copying SPARK xrefs info to Outfile_1.
-
- Initialize_SPARK_Tables;
- Get_SPARK_Xrefs_Info;
-
- -- Write SPARK cross-reference information from internal SPARK tables to
- -- Outfile_2.
-
- Put_SPARK_Xrefs_Info;
-
- -- Junk blank line (see comment at end of Lib.Writ)
-
- Write_Info_Terminate;
-
- -- Flush to disk
-
- Close (Outfile_1);
- Close (Outfile_2);
-
- -- Now Outfile_1 and Outfile_2 should be identical
-
- Diff_Result :=
- Spawn (Diff_Exec.all,
- Argument_String_To_List
- ("-u " & Name1.all & " " & Name2.all).all);
-
- if Diff_Result /= 0 then
- Ada.Text_IO.Put_Line ("diff(1) exit status" & Diff_Result'Img);
- end if;
-
- OS_Exit (Diff_Result);
-
- end Process;
-
-exception
- when Stop =>
- null;
-end SPARK_Xrefs_Test;
Index: gcc-interface/Make-lang.in
===================================================================
--- gcc-interface/Make-lang.in (revision 254523)
+++ gcc-interface/Make-lang.in (working copy)
@@ -322,7 +322,6 @@
ada/libgnat/g-spchge.o \
ada/libgnat/g-speche.o \
ada/libgnat/g-u3spch.o \
- ada/get_spark_xrefs.o \
ada/get_targ.o \
ada/ghost.o \
ada/libgnat/gnat.o \
@@ -352,7 +351,6 @@
ada/par_sco.o \
ada/prep.o \
ada/prepcomp.o \
- ada/put_spark_xrefs.o \
ada/put_scos.o \
ada/repinfo.o \
ada/restrict.o \
