1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- G E T _ S P A R K _ X R E F S -- 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 26with SPARK_Xrefs; use SPARK_Xrefs; 27with Types; use Types; 28 29with Ada.IO_Exceptions; use Ada.IO_Exceptions; 30 31procedure Get_SPARK_Xrefs is 32 C : Character; 33 34 use ASCII; 35 -- For CR/LF 36 37 Cur_File : Nat; 38 -- Dependency number for the current file 39 40 Cur_Scope : Nat; 41 -- Scope number for the current scope entity 42 43 Cur_File_Idx : File_Index; 44 -- Index in SPARK_File_Table of the current file 45 46 Cur_Scope_Idx : Scope_Index; 47 -- Index in SPARK_Scope_Table of the current scope 48 49 Name_Str : String (1 .. 32768); 50 Name_Len : Natural := 0; 51 -- Local string used to store name of File/entity scanned as 52 -- Name_Str (1 .. Name_Len). 53 54 File_Name : String_Ptr; 55 Unit_File_Name : String_Ptr; 56 57 ----------------------- 58 -- Local Subprograms -- 59 ----------------------- 60 61 function At_EOL return Boolean; 62 -- Skips any spaces, then checks if at the end of a line. If so, returns 63 -- True (but does not skip the EOL sequence). If not, then returns False. 64 65 procedure Check (C : Character); 66 -- Checks that file is positioned at given character, and if so skips past 67 -- it, If not, raises Data_Error. 68 69 function Get_Nat return Nat; 70 -- On entry the file is positioned to a digit. On return, the file is 71 -- positioned past the last digit, and the returned result is the decimal 72 -- value read. Data_Error is raised for overflow (value greater than 73 -- Int'Last), or if the initial character is not a digit. 74 75 procedure Get_Name; 76 -- On entry the file is positioned to a name. On return, the file is 77 -- positioned past the last character, and the name scanned is returned 78 -- in Name_Str (1 .. Name_Len). 79 80 procedure Skip_EOL; 81 -- Called with the current character about to be read being LF or CR. Skips 82 -- past CR/LF characters until either a non-CR/LF character is found, or 83 -- the end of file is encountered. 84 85 procedure Skip_Spaces; 86 -- Skips zero or more spaces at the current position, leaving the file 87 -- positioned at the first non-blank character (or Types.EOF). 88 89 ------------ 90 -- At_EOL -- 91 ------------ 92 93 function At_EOL return Boolean is 94 begin 95 Skip_Spaces; 96 return Nextc = CR or else Nextc = LF; 97 end At_EOL; 98 99 ----------- 100 -- Check -- 101 ----------- 102 103 procedure Check (C : Character) is 104 begin 105 if Nextc = C then 106 Skipc; 107 else 108 raise Data_Error; 109 end if; 110 end Check; 111 112 ------------- 113 -- Get_Nat -- 114 ------------- 115 116 function Get_Nat return Nat is 117 Val : Nat; 118 C : Character; 119 120 begin 121 C := Nextc; 122 Val := 0; 123 124 if C not in '0' .. '9' then 125 raise Data_Error; 126 end if; 127 128 -- Loop to read digits of integer value 129 130 loop 131 declare 132 pragma Unsuppress (Overflow_Check); 133 begin 134 Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0')); 135 end; 136 137 Skipc; 138 C := Nextc; 139 140 exit when C not in '0' .. '9'; 141 end loop; 142 143 return Val; 144 145 exception 146 when Constraint_Error => 147 raise Data_Error; 148 end Get_Nat; 149 150 -------------- 151 -- Get_Name -- 152 -------------- 153 154 procedure Get_Name is 155 N : Integer; 156 157 begin 158 N := 0; 159 while Nextc > ' ' loop 160 N := N + 1; 161 Name_Str (N) := Getc; 162 end loop; 163 164 Name_Len := N; 165 end Get_Name; 166 167 -------------- 168 -- Skip_EOL -- 169 -------------- 170 171 procedure Skip_EOL is 172 C : Character; 173 174 begin 175 loop 176 Skipc; 177 C := Nextc; 178 exit when C /= LF and then C /= CR; 179 180 if C = ' ' then 181 Skip_Spaces; 182 C := Nextc; 183 exit when C /= LF and then C /= CR; 184 end if; 185 end loop; 186 end Skip_EOL; 187 188 ----------------- 189 -- Skip_Spaces -- 190 ----------------- 191 192 procedure Skip_Spaces is 193 begin 194 while Nextc = ' ' loop 195 Skipc; 196 end loop; 197 end Skip_Spaces; 198 199-- Start of processing for Get_SPARK_Xrefs 200 201begin 202 Initialize_SPARK_Tables; 203 204 Cur_File := 0; 205 Cur_Scope := 0; 206 Cur_File_Idx := 1; 207 Cur_Scope_Idx := 0; 208 209 -- Loop through lines of SPARK cross-reference information 210 211 while Nextc = 'F' loop 212 Skipc; 213 214 C := Getc; 215 216 -- Make sure first line is a File line 217 218 if SPARK_File_Table.Last = 0 and then C /= 'D' then 219 raise Data_Error; 220 end if; 221 222 -- Otherwise dispatch on type of line 223 224 case C is 225 226 -- Header entry for scope section 227 228 when 'D' => 229 230 -- Complete previous entry if any 231 232 if SPARK_File_Table.Last /= 0 then 233 SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope := 234 SPARK_Scope_Table.Last; 235 end if; 236 237 -- Scan out dependency number and file name 238 239 Skip_Spaces; 240 Cur_File := Get_Nat; 241 Skip_Spaces; 242 243 Get_Name; 244 File_Name := new String'(Name_Str (1 .. Name_Len)); 245 Skip_Spaces; 246 247 -- Scan out unit file name when present (for subunits) 248 249 if Nextc = '-' then 250 Skipc; 251 Check ('>'); 252 Skip_Spaces; 253 Get_Name; 254 Unit_File_Name := new String'(Name_Str (1 .. Name_Len)); 255 256 else 257 Unit_File_Name := null; 258 end if; 259 260 -- Make new File table entry (will fill in To_Scope later) 261 262 SPARK_File_Table.Append ( 263 (File_Name => File_Name, 264 Unit_File_Name => Unit_File_Name, 265 File_Num => Cur_File, 266 From_Scope => SPARK_Scope_Table.Last + 1, 267 To_Scope => 0)); 268 269 -- Initialize counter for scopes 270 271 Cur_Scope := 1; 272 273 -- Scope entry 274 275 when 'S' => 276 declare 277 Spec_File : Nat; 278 Spec_Scope : Nat; 279 Scope : Nat; 280 Line : Nat; 281 Col : Nat; 282 Typ : Character; 283 284 begin 285 -- Scan out location 286 287 Skip_Spaces; 288 Check ('.'); 289 Scope := Get_Nat; 290 Check (' '); 291 Line := Get_Nat; 292 Typ := Getc; 293 Col := Get_Nat; 294 295 pragma Assert (Scope = Cur_Scope); 296 pragma Assert (Typ = 'K' 297 or else Typ = 'V' 298 or else Typ = 'U'); 299 300 -- Scan out scope entity name 301 302 Skip_Spaces; 303 Get_Name; 304 Skip_Spaces; 305 306 if Nextc = '-' then 307 Skipc; 308 Check ('>'); 309 Skip_Spaces; 310 Spec_File := Get_Nat; 311 Check ('.'); 312 Spec_Scope := Get_Nat; 313 314 else 315 Spec_File := 0; 316 Spec_Scope := 0; 317 end if; 318 319 -- Make new scope table entry (will fill in From_Xref and 320 -- To_Xref later). Initial range (From_Xref .. To_Xref) is 321 -- empty for scopes without entities. 322 323 SPARK_Scope_Table.Append ( 324 (Scope_Entity => Empty, 325 Scope_Name => new String'(Name_Str (1 .. Name_Len)), 326 File_Num => Cur_File, 327 Scope_Num => Cur_Scope, 328 Spec_File_Num => Spec_File, 329 Spec_Scope_Num => Spec_Scope, 330 Line => Line, 331 Stype => Typ, 332 Col => Col, 333 From_Xref => 1, 334 To_Xref => 0)); 335 end; 336 337 -- Update counter for scopes 338 339 Cur_Scope := Cur_Scope + 1; 340 341 -- Header entry for cross-ref section 342 343 when 'X' => 344 345 -- Scan out dependency number and file name (ignored) 346 347 Skip_Spaces; 348 Cur_File := Get_Nat; 349 Skip_Spaces; 350 Get_Name; 351 352 -- Update component From_Xref of current file if first reference 353 -- in this file. 354 355 while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File 356 loop 357 Cur_File_Idx := Cur_File_Idx + 1; 358 end loop; 359 360 -- Scan out scope entity number and entity name (ignored) 361 362 Skip_Spaces; 363 Check ('.'); 364 Cur_Scope := Get_Nat; 365 Skip_Spaces; 366 Get_Name; 367 368 -- Update component To_Xref of previous scope 369 370 if Cur_Scope_Idx /= 0 then 371 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := 372 SPARK_Xref_Table.Last; 373 end if; 374 375 -- Update component From_Xref of current scope 376 377 Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope; 378 379 while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /= 380 Cur_Scope 381 loop 382 Cur_Scope_Idx := Cur_Scope_Idx + 1; 383 end loop; 384 385 SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref := 386 SPARK_Xref_Table.Last + 1; 387 388 -- Cross reference entry 389 390 when ' ' => 391 declare 392 XR_Entity : String_Ptr; 393 XR_Entity_Line : Nat; 394 XR_Entity_Col : Nat; 395 XR_Entity_Typ : Character; 396 397 XR_File : Nat; 398 -- Keeps track of the current file (changed by nn|) 399 400 XR_Scope : Nat; 401 -- Keeps track of the current scope (changed by nn:) 402 403 begin 404 XR_File := Cur_File; 405 XR_Scope := Cur_Scope; 406 407 XR_Entity_Line := Get_Nat; 408 XR_Entity_Typ := Getc; 409 XR_Entity_Col := Get_Nat; 410 411 Skip_Spaces; 412 Get_Name; 413 XR_Entity := new String'(Name_Str (1 .. Name_Len)); 414 415 -- Initialize to scan items on one line 416 417 Skip_Spaces; 418 419 -- Loop through cross-references for this entity 420 421 loop 422 423 declare 424 Line : Nat; 425 Col : Nat; 426 N : Nat; 427 Rtype : Character; 428 429 begin 430 Skip_Spaces; 431 432 if At_EOL then 433 Skip_EOL; 434 exit when Nextc /= '.'; 435 Skipc; 436 Skip_Spaces; 437 end if; 438 439 if Nextc = '.' then 440 Skipc; 441 XR_Scope := Get_Nat; 442 Check (':'); 443 444 else 445 N := Get_Nat; 446 447 if Nextc = '|' then 448 XR_File := N; 449 Skipc; 450 451 else 452 Line := N; 453 Rtype := Getc; 454 Col := Get_Nat; 455 456 pragma Assert 457 (Rtype = 'r' or else 458 Rtype = 'c' or else 459 Rtype = 'm' or else 460 Rtype = 's'); 461 462 SPARK_Xref_Table.Append ( 463 (Entity_Name => XR_Entity, 464 Entity_Line => XR_Entity_Line, 465 Etype => XR_Entity_Typ, 466 Entity_Col => XR_Entity_Col, 467 File_Num => XR_File, 468 Scope_Num => XR_Scope, 469 Line => Line, 470 Rtype => Rtype, 471 Col => Col)); 472 end if; 473 end if; 474 end; 475 end loop; 476 end; 477 478 -- No other SPARK lines are possible 479 480 when others => 481 raise Data_Error; 482 end case; 483 484 -- For cross reference lines, the EOL character has been skipped already 485 486 if C /= ' ' then 487 Skip_EOL; 488 end if; 489 end loop; 490 491 -- Here with all Xrefs stored, complete last entries in File/Scope tables 492 493 if SPARK_File_Table.Last /= 0 then 494 SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope := 495 SPARK_Scope_Table.Last; 496 end if; 497 498 if Cur_Scope_Idx /= 0 then 499 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last; 500 end if; 501end Get_SPARK_Xrefs; 502