------------------------------------------------------------------------------ -- -- -- GNAT COMPILER COMPONENTS -- -- -- -- G E T _ S P A R K _ X R E F S -- -- -- -- 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. -- -- -- ------------------------------------------------------------------------------ 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 Val : Nat; C : Character; begin C := Nextc; Val := 0; 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 : Integer; begin N := 0; 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); pragma Assert (Typ = 'K' or else Typ = 'V' or else Typ = 'U'); -- 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;