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-2015, 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 297 -- Scan out scope entity name 298 299 Skip_Spaces; 300 Get_Name; 301 Skip_Spaces; 302 303 if Nextc = '-' then 304 Skipc; 305 Check ('>'); 306 Skip_Spaces; 307 Spec_File := Get_Nat; 308 Check ('.'); 309 Spec_Scope := Get_Nat; 310 311 else 312 Spec_File := 0; 313 Spec_Scope := 0; 314 end if; 315 316 -- Make new scope table entry (will fill in From_Xref and 317 -- To_Xref later). Initial range (From_Xref .. To_Xref) is 318 -- empty for scopes without entities. 319 320 SPARK_Scope_Table.Append ( 321 (Scope_Entity => Empty, 322 Scope_Name => new String'(Name_Str (1 .. Name_Len)), 323 File_Num => Cur_File, 324 Scope_Num => Cur_Scope, 325 Spec_File_Num => Spec_File, 326 Spec_Scope_Num => Spec_Scope, 327 Line => Line, 328 Stype => Typ, 329 Col => Col, 330 From_Xref => 1, 331 To_Xref => 0)); 332 end; 333 334 -- Update counter for scopes 335 336 Cur_Scope := Cur_Scope + 1; 337 338 -- Header entry for cross-ref section 339 340 when 'X' => 341 342 -- Scan out dependency number and file name (ignored) 343 344 Skip_Spaces; 345 Cur_File := Get_Nat; 346 Skip_Spaces; 347 Get_Name; 348 349 -- Update component From_Xref of current file if first reference 350 -- in this file. 351 352 while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File 353 loop 354 Cur_File_Idx := Cur_File_Idx + 1; 355 end loop; 356 357 -- Scan out scope entity number and entity name (ignored) 358 359 Skip_Spaces; 360 Check ('.'); 361 Cur_Scope := Get_Nat; 362 Skip_Spaces; 363 Get_Name; 364 365 -- Update component To_Xref of previous scope 366 367 if Cur_Scope_Idx /= 0 then 368 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := 369 SPARK_Xref_Table.Last; 370 end if; 371 372 -- Update component From_Xref of current scope 373 374 Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope; 375 376 while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /= 377 Cur_Scope 378 loop 379 Cur_Scope_Idx := Cur_Scope_Idx + 1; 380 end loop; 381 382 SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref := 383 SPARK_Xref_Table.Last + 1; 384 385 -- Cross reference entry 386 387 when ' ' => 388 declare 389 XR_Entity : String_Ptr; 390 XR_Entity_Line : Nat; 391 XR_Entity_Col : Nat; 392 XR_Entity_Typ : Character; 393 394 XR_File : Nat; 395 -- Keeps track of the current file (changed by nn|) 396 397 XR_Scope : Nat; 398 -- Keeps track of the current scope (changed by nn:) 399 400 begin 401 XR_File := Cur_File; 402 XR_Scope := Cur_Scope; 403 404 XR_Entity_Line := Get_Nat; 405 XR_Entity_Typ := Getc; 406 XR_Entity_Col := Get_Nat; 407 408 Skip_Spaces; 409 Get_Name; 410 XR_Entity := new String'(Name_Str (1 .. Name_Len)); 411 412 -- Initialize to scan items on one line 413 414 Skip_Spaces; 415 416 -- Loop through cross-references for this entity 417 418 loop 419 420 declare 421 Line : Nat; 422 Col : Nat; 423 N : Nat; 424 Rtype : Character; 425 426 begin 427 Skip_Spaces; 428 429 if At_EOL then 430 Skip_EOL; 431 exit when Nextc /= '.'; 432 Skipc; 433 Skip_Spaces; 434 end if; 435 436 if Nextc = '.' then 437 Skipc; 438 XR_Scope := Get_Nat; 439 Check (':'); 440 441 else 442 N := Get_Nat; 443 444 if Nextc = '|' then 445 XR_File := N; 446 Skipc; 447 448 else 449 Line := N; 450 Rtype := Getc; 451 Col := Get_Nat; 452 453 pragma Assert 454 (Rtype = 'r' or else 455 Rtype = 'c' or else 456 Rtype = 'm' or else 457 Rtype = 's'); 458 459 SPARK_Xref_Table.Append ( 460 (Entity_Name => XR_Entity, 461 Entity_Line => XR_Entity_Line, 462 Etype => XR_Entity_Typ, 463 Entity_Col => XR_Entity_Col, 464 File_Num => XR_File, 465 Scope_Num => XR_Scope, 466 Line => Line, 467 Rtype => Rtype, 468 Col => Col)); 469 end if; 470 end if; 471 end; 472 end loop; 473 end; 474 475 -- No other SPARK lines are possible 476 477 when others => 478 raise Data_Error; 479 end case; 480 481 -- For cross reference lines, the EOL character has been skipped already 482 483 if C /= ' ' then 484 Skip_EOL; 485 end if; 486 end loop; 487 488 -- Here with all Xrefs stored, complete last entries in File/Scope tables 489 490 if SPARK_File_Table.Last /= 0 then 491 SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope := 492 SPARK_Scope_Table.Last; 493 end if; 494 495 if Cur_Scope_Idx /= 0 then 496 SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last; 497 end if; 498end Get_SPARK_Xrefs; 499