gcc/ada/spark_xrefs_test.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                          GNAT SYSTEM UTILITIES                           --
   4 --                                                                          --
   5 --                     S P A R K _ X R E F S _ T E S T                      --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2011-2013, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
  17 -- for  more details.  You should have  received  a copy of the GNU General --
  18 -- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
  19 -- http://www.gnu.org/licenses for a complete copy of the license.          --
  20 --                                                                          --
  21 -- GNAT was originally developed  by the GNAT team at  New York University. --
  22 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  23 --                                                                          --
  24 ------------------------------------------------------------------------------
  25
  26 --  This utility program is used to test proper operation of the
  27 --  Get_SPARK_Xrefs and Put_SPARK_Xrefs units. To run it, compile any source
  28 --  file with switch -gnatd.E or -gnatd.F to get an ALI file file.ALI
  29 --  containing SPARK information. Then run this utility using:
  30
  31 --     spark_xrefs_test file.ali
  32
  33 --  This test will read the SPARK cross-reference information from the ALI
  34 --  file, and use Get_SPARK_Xrefs to store this in binary form in the internal
  35 --  tables in SPARK_Xrefs. Then Put_SPARK_Xrefs is used to write the
  36 --  information from these tables back into text form. This output is compared
  37 --  with the original SPARK cross-reference information in the ALI file and the
  38 --  two should be identical. If not an error message is output.
  39
  40 with Get_SPARK_Xrefs;
  41 with Put_SPARK_Xrefs;
  42
  43 with SPARK_Xrefs;           use SPARK_Xrefs;
  44 with Types;                 use Types;
  45
  46 with Ada.Command_Line;      use Ada.Command_Line;
  47 with Ada.Streams;           use Ada.Streams;
  48 with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
  49 with Ada.Text_IO;
  50
  51 with GNAT.OS_Lib;           use GNAT.OS_Lib;
  52
  53 procedure SPARK_Xrefs_Test is
  54    Infile    : File_Type;
  55    Name1     : String_Access;
  56    Outfile_1 : File_Type;
  57    Name2     : String_Access;
  58    Outfile_2 : File_Type;
  59    C         : Character;
  60
  61    Stop : exception;
  62    --  Terminate execution
  63
  64    Diff_Exec   : constant String_Access := Locate_Exec_On_Path ("diff");
  65    Diff_Result : Integer;
  66
  67    use ASCII;
  68
  69 begin
  70    if Argument_Count /= 1 then
  71       Ada.Text_IO.Put_Line ("Usage: spark_xrefs_test FILE.ali");
  72       raise Stop;
  73    end if;
  74
  75    Name1 := new String'(Argument (1) & ".1");
  76    Name2 := new String'(Argument (1) & ".2");
  77
  78    Open   (Infile,    In_File,  Argument (1));
  79    Create (Outfile_1, Out_File, Name1.all);
  80    Create (Outfile_2, Out_File, Name2.all);
  81
  82    --  Read input file till we get to first 'F' line
  83
  84    Process : declare
  85       Output_Col : Positive := 1;
  86
  87       function Get_Char (F : File_Type) return Character;
  88       --  Read one character from specified  file
  89
  90       procedure Put_Char (F : File_Type; C : Character);
  91       --  Write one character to specified file
  92
  93       function Get_Output_Col return Positive;
  94       --  Return current column in output file, where each line starts at
  95       --  column 1 and terminate with LF, and HT is at columns 1, 9, etc.
  96       --  All output is supposed to be carried through Put_Char.
  97
  98       --------------
  99       -- Get_Char --
 100       --------------
 101
 102       function Get_Char (F : File_Type) return Character is
 103          Item : Stream_Element_Array (1 .. 1);
 104          Last : Stream_Element_Offset;
 105
 106       begin
 107          Read (F, Item, Last);
 108
 109          if Last /= 1 then
 110             return Types.EOF;
 111          else
 112             return Character'Val (Item (1));
 113          end if;
 114       end Get_Char;
 115
 116       --------------------
 117       -- Get_Output_Col --
 118       --------------------
 119
 120       function Get_Output_Col return Positive is
 121       begin
 122          return Output_Col;
 123       end Get_Output_Col;
 124
 125       --------------
 126       -- Put_Char --
 127       --------------
 128
 129       procedure Put_Char (F : File_Type; C : Character) is
 130          Item : Stream_Element_Array (1 .. 1);
 131
 132       begin
 133          if C /= CR and then C /= EOF then
 134             if C = LF then
 135                Output_Col := 1;
 136             elsif C = HT then
 137                Output_Col := ((Output_Col + 6) / 8) * 8 + 1;
 138             else
 139                Output_Col := Output_Col + 1;
 140             end if;
 141
 142             Item (1) := Character'Pos (C);
 143             Write (F, Item);
 144          end if;
 145       end Put_Char;
 146
 147       --  Subprograms used by Get_SPARK_Xrefs (these also copy the output to
 148       --  Outfile_1 for later comparison with the output generated by
 149       --  Put_SPARK_Xrefs).
 150
 151       function  Getc  return Character;
 152       function  Nextc return Character;
 153       procedure Skipc;
 154
 155       ----------
 156       -- Getc --
 157       ----------
 158
 159       function Getc  return Character is
 160          C : Character;
 161       begin
 162          C := Get_Char (Infile);
 163          Put_Char (Outfile_1, C);
 164          return C;
 165       end Getc;
 166
 167       -----------
 168       -- Nextc --
 169       -----------
 170
 171       function Nextc return Character is
 172          C : Character;
 173
 174       begin
 175          C := Get_Char (Infile);
 176
 177          if C /= EOF then
 178             Set_Index (Infile, Index (Infile) - 1);
 179          end if;
 180
 181          return C;
 182       end Nextc;
 183
 184       -----------
 185       -- Skipc --
 186       -----------
 187
 188       procedure Skipc is
 189          C : Character;
 190          pragma Unreferenced (C);
 191       begin
 192          C := Getc;
 193       end Skipc;
 194
 195       --  Subprograms used by Put_SPARK_Xrefs, which write information to
 196       --  Outfile_2.
 197
 198       function Write_Info_Col return Positive;
 199       procedure Write_Info_Char (C : Character);
 200       procedure Write_Info_Initiate (Key : Character);
 201       procedure Write_Info_Nat (N : Nat);
 202       procedure Write_Info_Terminate;
 203
 204       --------------------
 205       -- Write_Info_Col --
 206       --------------------
 207
 208       function Write_Info_Col return Positive is
 209       begin
 210          return Get_Output_Col;
 211       end Write_Info_Col;
 212
 213       ---------------------
 214       -- Write_Info_Char --
 215       ---------------------
 216
 217       procedure Write_Info_Char (C : Character) is
 218       begin
 219          Put_Char (Outfile_2, C);
 220       end Write_Info_Char;
 221
 222       -------------------------
 223       -- Write_Info_Initiate --
 224       -------------------------
 225
 226       procedure Write_Info_Initiate (Key : Character) is
 227       begin
 228          Write_Info_Char (Key);
 229       end Write_Info_Initiate;
 230
 231       --------------------
 232       -- Write_Info_Nat --
 233       --------------------
 234
 235       procedure Write_Info_Nat (N : Nat) is
 236       begin
 237          if N > 9 then
 238             Write_Info_Nat (N / 10);
 239          end if;
 240
 241          Write_Info_Char (Character'Val (48 + N mod 10));
 242       end Write_Info_Nat;
 243
 244       --------------------------
 245       -- Write_Info_Terminate --
 246       --------------------------
 247
 248       procedure Write_Info_Terminate is
 249       begin
 250          Write_Info_Char (LF);
 251       end Write_Info_Terminate;
 252
 253       --  Local instantiations of Put_SPARK_Xrefs and Get_SPARK_Xrefs
 254
 255       procedure Get_SPARK_Xrefs_Info is new Get_SPARK_Xrefs;
 256       procedure Put_SPARK_Xrefs_Info is new Put_SPARK_Xrefs;
 257
 258    --  Start of processing for Process
 259
 260    begin
 261       --  Loop to skip till first 'F' line
 262
 263       loop
 264          C := Get_Char (Infile);
 265
 266          if C = EOF then
 267             raise Stop;
 268
 269          elsif C = LF or else C = CR then
 270             loop
 271                C := Get_Char (Infile);
 272                exit when C /= LF and then C /= CR;
 273             end loop;
 274
 275             exit when C = 'F';
 276          end if;
 277       end loop;
 278
 279       --  Position back to initial 'F' of first 'F' line
 280
 281       Set_Index (Infile, Index (Infile) - 1);
 282
 283       --  Read SPARK cross-reference information to internal SPARK tables, also
 284       --  copying SPARK xrefs info to Outfile_1.
 285
 286       Initialize_SPARK_Tables;
 287       Get_SPARK_Xrefs_Info;
 288
 289       --  Write SPARK cross-reference information from internal SPARK tables to
 290       --  Outfile_2.
 291
 292       Put_SPARK_Xrefs_Info;
 293
 294       --  Junk blank line (see comment at end of Lib.Writ)
 295
 296       Write_Info_Terminate;
 297
 298       --  Flush to disk
 299
 300       Close (Outfile_1);
 301       Close (Outfile_2);
 302
 303       --  Now Outfile_1 and Outfile_2 should be identical
 304
 305       Diff_Result :=
 306         Spawn (Diff_Exec.all,
 307                Argument_String_To_List
 308                  ("-u " & Name1.all & " " & Name2.all).all);
 309
 310       if Diff_Result /= 0 then
 311          Ada.Text_IO.Put_Line ("diff(1) exit status" & Diff_Result'Img);
 312       end if;
 313
 314       OS_Exit (Diff_Result);
 315
 316    end Process;
 317
 318 exception
 319    when Stop =>
 320       null;
 321 end SPARK_Xrefs_Test;