06b599fd62
2013-04-24 Yannick Moy <moy@adacore.com> * adabkend.adb, ali-util.adb, ali.adb, debug.adb, errout.adb, errout.ads, erroutc.adb, exp_ch3.adb, exp_ch4.adb, exp_ch6.adb, exp_ch7.adb, exp_dbug.adb, exp_util.adb, expander.adb, freeze.adb, gnat1drv.adb, lib-writ.adb, lib-writ.ads, lib-xref.adb, lib-xref.ads, opt.adb, opt.ads, restrict.adb, sem_aggr.adb, sem_attr.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_eval.adb, sem_prag.adb, sem_res.adb, sem_util.adb: Everything with name 'Alfa' renamed in 'SPARK'. Update comments. Renaming of units with name 'Alfa', renamed with 'SPARK' instead. * exp_alfa.adb: renamed exp_spark.adb. * exp_alfa.ads: renamed exp_spark.ads. * get_alfa.adb: renamed get_spark_xrefs.adb. * get_alfa.ads: renamed get_spark_xrefs.ads. * lib-xref-alfa.adb: renamed lib-xref-spark_specific.adb. * put_alfa.adb: renamed put_spark_xrefs.adb. * put_alfa.ads: renamed put_spark_xrefs.ads. * alfa.adb: renamed spark_xrefs.adb. * alfa.ads: renamed spark_xrefs.ads. * alfa_test.adb: renamed spark_xrefs_test.adb. From-SVN: r198234
322 lines
9.4 KiB
Ada
322 lines
9.4 KiB
Ada
------------------------------------------------------------------------------
|
|
-- --
|
|
-- 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;
|