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
40with Get_SPARK_Xrefs;
41with Put_SPARK_Xrefs;
42
43with SPARK_Xrefs;           use SPARK_Xrefs;
44with Types;                 use Types;
45
46with Ada.Command_Line;      use Ada.Command_Line;
47with Ada.Streams;           use Ada.Streams;
48with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
49with Ada.Text_IO;
50
51with GNAT.OS_Lib;           use GNAT.OS_Lib;
52
53procedure 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
69begin
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
318exception
319   when Stop =>
320      null;
321end SPARK_Xrefs_Test;
322