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