|
111
|
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;
|
