Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/spark_xrefs_test.adb @ 111:04ced10e8804

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children
comparison
equal deleted inserted replaced
68:561a7518be6b 111:04ced10e8804
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;