******************************************************* Listing of SPARK Text SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06 Demonstration Version ******************************************************* DATE : 28-FEB-2010 12:06:45.99 Line 1 -- $Id: spark95_io.adb,v 1.4 2004/07/22 14:55:14 spark Exp $ 2 -------------------------------------------------------------------------------- 3 --(C) 1990-2000 Praxis Critical Systems Limited 4 -- 5 --The material contained herein is the subject of copyright and all rights in it 6 --are reserved. It may not be copied, in whole or in part, without the written 7 --consent of Program Validation Limited. Under law copying includes translating 8 --into another language or format. 9 -------------------------------------------------------------------------------- 10 --Module File Name : SPARKIO.ADS 11 --Used as part of : Spark_IO package for SPARK95 12 --Module Function : Spark IO package body 13 --Uses Library Units : Ada.Text_IO 14 --Author : JRG 15 16 --Modification History (one line per CFR) : 17 --Date CFR Details of modifications 18 --15-Jan-90 000 Adoption of source code. 19 --31-Oct-96 539 Avoidance of predefined FDL indentifiers 20 --26-Feb-97 614 Changes for Spark95 21 --18-Nov-99 718 Change to behaviour of Put_String plus new exceptions 22 --13-Jul-00 New exception added to Close and Delete. Mode of Reset altered 23 -- as well (MJW) 24 --22-Jul-04 1396 Add Get_Char_Immediate 25 ------------------------------------------------------------------------------ 26 27 package body Spark_IO 28 is 29 --# hide Spark_IO 30 31 -- File Management 32 33 procedure Create( File : out File_Type; 34 Name_Of_File : in String; 35 Form_Of_File : in String; 36 Status : out File_Status) 37 is 38 begin 39 Status := Ok; 40 File.File := new Ada.Text_IO.File_Type; 41 Ada.Text_IO.Create ( File.File.all, Ada.Text_IO.Out_File, 42 Name_Of_File, Form_Of_File); 43 exception 44 when Ada.Text_IO.Status_Error => Status := Status_Error; 45 when Ada.Text_IO.Name_Error => Status := Name_Error; 46 when Ada.Text_IO.Use_Error => Status := Use_Error; 47 when Ada.Text_IO.Device_Error => Status := Device_Error; 48 when Standard.Storage_Error => Status := Storage_Error; 49 when Standard.Program_Error => Status := Program_Error; 50 end Create; 51 52 procedure Open( File : out File_Type; 53 Mode_Of_File : in File_Mode; 54 Name_Of_File : in String; 55 Form_Of_File : in String; 56 Status : out File_Status) 57 is 58 Fmode : Ada.Text_IO.File_Mode; 59 begin 60 case Mode_Of_File is 61 when In_File => Fmode := Ada.Text_IO.In_File; 62 when Out_File => Fmode := Ada.Text_IO.Out_File; 63 when Append_File => Fmode := Ada.Text_IO.Append_File; 64 end case; 65 Status := Ok; 66 File.File := new Ada.Text_IO.File_Type; 67 Ada.Text_IO.Open( File.File.all, Fmode, Name_Of_File, Form_Of_File); 68 exception 69 when Ada.Text_IO.Status_Error => Status := Status_Error; 70 when Ada.Text_IO.Name_Error => Status := Name_Error; 71 when Ada.Text_IO.Use_Error => Status := Use_Error; 72 when Ada.Text_IO.Device_Error => Status := Device_Error; 73 when Standard.Storage_Error => Status := Storage_Error; 74 when Standard.Program_Error => Status := Program_Error; 75 end Open; 76 77 procedure Close( File : in File_Type; 78 Status : out File_Status) 79 is 80 begin 81 Ada.Text_IO.Close( File.File.all); 82 Status := Ok; 83 exception 84 when Constraint_Error => Status := Use_Error; 85 when Ada.Text_IO.Status_Error => Status := Status_Error; 86 when Ada.Text_IO.Device_Error => Status := Device_Error; 87 when Standard.Storage_Error => Status := Storage_Error; 88 when Standard.Program_Error => Status := Program_Error; 89 end Close; 90 91 procedure Delete( File : in File_Type; 92 Status : out File_Status) 93 is 94 begin 95 Ada.Text_IO.Delete( File.File.all); 96 Status := Ok; 97 exception 98 when Ada.Text_IO.Status_Error => Status := Status_Error; 99 when Ada.Text_IO.Use_Error => Status := Use_Error; 100 when Constraint_Error => Status := Use_Error; 101 when Ada.Text_IO.Device_Error => Status := Device_Error; 102 when Standard.Storage_Error => Status := Storage_Error; 103 when Standard.Program_Error => Status := Program_Error; 104 end Delete; 105 106 procedure Reset( File : in out File_Type; 107 Mode_Of_File : in File_Mode; 108 Status : out File_Status) 109 is 110 Fmode : Ada.Text_IO.File_Mode; 111 begin 112 case Mode_Of_File is 113 when In_File => Fmode := Ada.Text_IO.In_File; 114 when Out_File => Fmode := Ada.Text_IO.Out_File; 115 when Append_File => Fmode := Ada.Text_IO.Append_File; 116 end case; 117 Ada.Text_IO.Reset( File.File.all, Fmode); 118 Status := Ok; 119 exception 120 when Ada.Text_IO.Status_Error => Status := Status_Error; 121 when Ada.Text_IO.Use_Error => Status := Use_Error; 122 when Ada.Text_IO.Device_Error => Status := Device_Error; 123 when Standard.Storage_Error => Status := Storage_Error; 124 when Standard.Program_Error => Status := Program_Error; 125 end Reset; 126 127 function Valid_File( File : File_Type) return Boolean 128 is 129 Valid : Boolean; 130 begin 131 case File.IO_Sort is 132 when Stdin => Valid := True; 133 when Stdout => Valid := True; 134 when NamedFile => Valid := (File.File /= null); 135 end case; 136 return Valid; 137 end Valid_File; 138 139 function File_Ref( File : File_Type) return Ada.Text_IO.File_Type 140 is 141 begin 142 case File.IO_Sort is 143 when Stdin => return Ada.Text_IO.Standard_Input; 144 when Stdout => return Ada.Text_IO.Standard_Output; 145 when NamedFile => return File.File.all; 146 end case; 147 end File_Ref; 148 149 function Is_Open( File : File_Type) return Boolean 150 is 151 begin 152 return Valid_File( File) and then 153 Ada.Text_IO.Is_Open( File_Ref( File)); 154 end Is_Open; 155 156 function Mode( File : File_Type) return File_Mode 157 is 158 Fmode : File_Mode; 159 begin 160 if Is_Open( File) and then 161 Ada.Text_IO.Is_Open( File_Ref( File)) then 162 case Ada.Text_IO.Mode( File_Ref( File)) is 163 when Ada.Text_IO.In_File => Fmode := In_File; 164 when Ada.Text_IO.Out_File => Fmode := Out_File; 165 when Ada.Text_IO.Append_File => Fmode := Append_File; 166 end case; 167 else 168 Fmode := In_File; 169 end if; 170 return Fmode; 171 end Mode; 172 173 function Is_In( File : File_Type) return Boolean 174 is 175 begin 176 return Is_Open( File) and then Mode( File) = In_File; 177 end Is_In; 178 179 function Is_Out( File : File_Type) return Boolean 180 is 181 begin 182 return Is_Open( File) and then (Mode( File) = Out_File or 183 Mode( File) = Append_File); 184 end Is_Out; 185 186 procedure Name( File : in File_Type; 187 Name_Of_File : out String; 188 Stop : out Natural) 189 is 190 begin 191 if Is_Open( File) then 192 declare 193 Fn : constant String := Ada.Text_IO.Name( File_Ref( File)); 194 begin 195 if Name_Of_File'Length >= Fn'Length then 196 Name_Of_File( Fn'Range) := Fn; 197 Stop := Fn'Length; 198 else 199 Name_Of_File := Fn(Name_Of_File'Range); 200 Stop := Name_Of_File'Length; 201 end if; 202 end; 203 else 204 Stop := Name_Of_File'First - 1; 205 end if; 206 exception 207 when others => Stop := Name_Of_File'First - 1; 208 end Name; 209 210 procedure Form( File : in File_Type; 211 Form_Of_File : out String; 212 Stop : out Natural) 213 is 214 begin 215 if Is_Open( File) then 216 declare 217 Fm : constant string := Ada.Text_IO.Form( File_Ref( File)); 218 begin 219 if Form_Of_File'Length >= Fm'Length then 220 Form_Of_File( Fm'Range) := Fm; 221 Stop := Fm'Length; 222 else 223 Form_Of_File := Fm( Form_Of_File'Range); 224 Stop := Form_Of_File'Length; 225 end if; 226 end; 227 else 228 Stop := Form_Of_File'First - 1; 229 end if; 230 exception 231 when others => Stop := Form_Of_File'First - 1; 232 end Form; 233 234 -- Line and file terminator control 235 236 function P_To_PC( P : Positive) return Ada.Text_IO.Positive_Count 237 is 238 PC : Ada.Text_IO.Positive_Count; 239 begin 240 if P > Positive( Ada.Text_IO.Positive_Count'Last) then 241 PC := Ada.Text_IO.Positive_Count'Last; 242 else 243 PC := Ada.Text_IO.Positive_Count( P); 244 end if; 245 return PC; 246 end; 247 248 function PC_To_P( PC : Ada.Text_IO.Positive_Count) return Positive 249 is 250 begin 251 return Positive( PC); 252 end; 253 254 procedure New_Line( File : in File_Type; 255 Spacing : in Positive) 256 is 257 Gap : Ada.Text_IO.Positive_Count; 258 begin 259 if Is_Out( File) then 260 Gap := P_To_PC( Spacing); 261 Ada.Text_IO.New_Line( File_Ref( File), Gap); 262 end if; 263 exception 264 when others => null; 265 end New_Line; 266 267 procedure Skip_Line( File : in File_Type; 268 Spacing : in Positive) 269 is 270 Gap : Ada.Text_IO.Positive_Count; 271 begin 272 if Is_In( File) then 273 Gap := P_To_PC( Spacing); 274 Ada.Text_IO.Skip_Line( File_Ref( File), Gap); 275 end if; 276 exception 277 when others => null; 278 end Skip_Line; 279 280 procedure New_Page ( File : in File_Type) 281 is 282 begin 283 if Is_Out( File) then 284 Ada.Text_IO.New_Page( File_Ref( File)); 285 end if; 286 exception 287 when others => null; 288 end New_Page; 289 290 function End_Of_Line( File : File_Type) return Boolean 291 is 292 EOLN : Boolean; 293 begin 294 if Is_In( File) then 295 EOLN := Ada.Text_IO.End_Of_Line( File_Ref( File)); 296 else 297 EOLN := False; 298 end if; 299 return EOLN; 300 end End_Of_Line; 301 302 function End_Of_File( File : File_Type) return Boolean 303 is 304 EOF : Boolean; 305 begin 306 if Is_In( File) then 307 EOF := Ada.Text_IO.End_Of_File( File_Ref( File)); 308 else 309 EOF := True; 310 end if; 311 return EOF; 312 end End_Of_File; 313 314 procedure Set_Col( File : in File_Type; 315 Posn : in Positive) 316 is 317 Col : Ada.Text_IO.Positive_Count; 318 begin 319 if Is_Open( File) then 320 Col := P_To_PC( Posn); 321 Ada.Text_IO.Set_Col( File_Ref( File), Col); 322 end if; 323 exception 324 when others => null; 325 end Set_Col; 326 327 procedure Set_In_File_Col( File : in File_Type; 328 Posn : in Positive) 329 is 330 begin 331 if Is_In( File ) then 332 Set_Col( File, Posn); 333 end if; 334 end Set_In_File_Col; 335 336 procedure Set_Out_File_Col( File : in File_Type; 337 Posn : in Positive) 338 is 339 begin 340 if Is_Out( File ) then 341 Set_Col( File, Posn); 342 end if; 343 end Set_Out_File_Col; 344 345 function Col( File : File_Type) return Positive 346 is 347 Posn : Positive; 348 Col : Ada.Text_IO.Positive_Count; 349 begin 350 if Is_Open( File) then 351 Col := Ada.Text_IO.Col( File_Ref( File)); 352 Posn := Pc_To_P( Col); 353 else 354 Posn := 1; 355 end if; 356 return Posn; 357 exception 358 when Ada.Text_IO.Status_Error => return 1; 359 when Ada.Text_IO.Layout_Error => return PC_To_P( Ada.Text_IO.Count'Last); 360 when Ada.Text_IO.Device_Error => return 1; 361 when Standard.Storage_Error => return 1; 362 when Standard.Program_Error => return 1; 363 end Col; 364 365 function In_File_Col( File : File_Type) return Positive 366 is 367 begin 368 if Is_In (File) then 369 return Col (File); 370 else 371 return 1; 372 end if; 373 end In_File_Col; 374 375 function Out_File_Col( File : File_Type) return Positive 376 is 377 begin 378 if Is_Out (File) then 379 return Col (File); 380 else 381 return 1; 382 end if; 383 end Out_File_Col; 384 385 function Line( File : File_Type) return Positive 386 is 387 Posn : Positive; 388 Line : Ada.Text_IO.Positive_Count; 389 begin 390 if Is_Open( File) then 391 Line := Ada.Text_IO.Line( File_Ref( File)); 392 Posn := PC_To_P( Line); 393 else 394 Posn := 1; 395 end if; 396 return Posn; 397 exception 398 when Ada.Text_IO.Status_Error => return 1; 399 when Ada.Text_IO.Layout_Error => return PC_To_P( Ada.Text_IO.Count'Last); 400 when Ada.Text_IO.Device_Error => return 1; 401 when Standard.Storage_Error => return 1; 402 when Standard.Program_Error => return 1; 403 end Line; 404 405 function In_File_Line(File : File_Type) return Positive 406 is 407 begin 408 if Is_In (File) then 409 return Line (File); 410 else 411 return 1; 412 end if; 413 end In_File_Line; 414 415 function Out_File_Line( File : File_Type) return Positive 416 is 417 begin 418 if Is_Out (File) then 419 return Line (File); 420 else 421 return 1; 422 end if; 423 end Out_File_Line; 424 425 426 -- Character IO 427 428 procedure Get_Char( File : in File_Type; 429 Item : out Character) 430 is 431 begin 432 if Is_In( File) then 433 Ada.Text_IO.Get( File_Ref( File), Item); 434 else 435 Item := Character'First; 436 end if; 437 exception 438 when others => null; 439 end Get_Char; 440 441 procedure Put_Char( File : in File_Type; 442 Item : in Character) 443 is 444 begin 445 if Is_Out( File) then 446 Ada.Text_IO.Put( File_Ref( File), Item); 447 end if; 448 exception 449 when others => null; 450 end Put_Char; 451 452 procedure Get_Char_Immediate (File : in File_Type; 453 Item : out Character; 454 Status : out File_Status) 455 is 456 begin 457 if Is_In( File) then 458 Ada.Text_IO.Get_Immediate( File_Ref( File), Item); 459 Status := Ok; 460 else 461 Item := Character'First; 462 Status := Mode_Error; 463 end if; 464 exception 465 when others => 466 Item := Character'First; 467 Status := End_Error; 468 469 end Get_Char_Immediate; 470 471 -- String IO 472 473 procedure Get_String( File : in File_Type; 474 Item : out String; 475 Stop : out Natural) 476 is 477 LSTP : Natural; 478 begin 479 if Is_In( File) then 480 LSTP := Item'First - 1; 481 loop 482 exit when End_Of_File( File); 483 LSTP := LSTP + 1; 484 Get_Char( File, Item(LSTP)); 485 exit when LSTP = Item'Last; 486 end loop; 487 Stop := LSTP; 488 else 489 Stop := Item'First - 1; 490 end if; 491 end Get_String; 492 493 -- CFR 718 The behaviour of Put_String is now as follows: 494 -- If Stop is 0 then all characters in Item are output. 495 -- If Stop <= Item'Last then output Item(Item'First .. Stop). 496 -- If Stop > Item'Last then output all characters in Item, then pad with 497 -- spaces to width specified by Stop. 498 procedure Put_String( File : in File_Type; 499 Item : in String; 500 Stop : in Natural) 501 is 502 Pad : Natural; 503 begin 504 505 if Is_Out( File) then 506 507 if Stop = 0 then 508 Ada.Text_IO.Put( File_Ref( File), Item); 509 elsif Stop <= Item'Last then 510 Ada.Text_IO.Put( File_Ref( File), Item( Item'First .. Stop)); 511 else 512 Pad := Stop - Item'Last; 513 Ada.Text_IO.Put( File_Ref( File), Item); 514 while Pad > 0 loop 515 Ada.Text_IO.Put( File_Ref( File), ' '); 516 Pad := Pad - 1; 517 end loop; 518 end if; 519 520 end if; 521 522 exception 523 when others => null; 524 end Put_String; 525 526 procedure Get_Line( File : in File_Type; 527 Item : out String; 528 Stop : out Natural) 529 is 530 begin 531 if Is_In( File) then 532 Ada.Text_IO.Get_Line( File_Ref( File), Item, Stop); 533 else 534 Stop := Item'First - 1; 535 end if; 536 exception 537 when others => Stop := Item'First - 1; 538 end Get_Line; 539 540 procedure Put_Line( File : in File_Type; 541 Item : in String; 542 Stop : in Natural) 543 is 544 ES : Positive; 545 begin 546 if Stop = 0 then 547 ES := Item'Last; 548 else 549 ES := Stop; 550 end if; 551 if Is_Out( File) then 552 Ada.Text_IO.Put_Line( File_Ref( File), Item( Item'First .. ES)); 553 end if; 554 exception 555 when others => null; 556 end Put_Line; 557 558 559 -- Integer IO 560 561 package Integer_IO is new Ada.Text_IO.Integer_IO( Integer); 562 563 procedure Get_Integer( File : in File_Type; 564 Item : out Integer; 565 Width : in Natural; 566 Read : out Boolean) 567 is 568 begin 569 if Is_In( File) then 570 Integer_IO.Get( File_Ref( File), Item, Width); 571 Read := True; 572 else 573 Read := False; 574 end if; 575 exception 576 when others => Read := False; 577 end Get_Integer; 578 579 procedure Put_Integer( File : in File_Type; 580 Item : in Integer; 581 Width : in Natural; 582 Base : in Number_Base) 583 is 584 begin 585 if Is_Out( File) then 586 Integer_IO.Put( File_Ref( File), Item, Width, Base); 587 end if; 588 exception 589 when others => null; 590 end Put_Integer; 591 592 procedure Get_Int_From_String( Source : in String; 593 Item : out Integer; 594 Start_Pos : in Positive; 595 Stop : out Natural) 596 is 597 begin 598 Integer_IO.Get( Source( Start_Pos..Source'Last), Item, Stop); 599 exception 600 when others => Stop := Start_Pos - 1; 601 end Get_Int_From_String; 602 603 procedure Put_Int_To_String( Dest : in out String; 604 Item : in Integer; 605 Start_Pos : in Positive; 606 Base : in Number_Base) 607 is 608 begin 609 Integer_IO.Put( Dest( Start_Pos..Dest'Last), Item, Base); 610 exception 611 when others => null; 612 end Put_Int_To_String; 613 614 615 -- Float IO 616 617 package Real_IO is new Ada.Text_IO.Float_IO( Float); 618 619 procedure Get_Float( File : in File_Type; 620 Item : out Float; 621 Width : in Natural; 622 Read : out Boolean) 623 is 624 begin 625 if Is_In( File) then 626 Real_IO.Get( File_Ref( File), Item, Width); 627 Read := True; 628 else 629 Read := False; 630 end if; 631 exception 632 when others => Read := False; 633 end Get_Float; 634 635 procedure Put_Float( File : in File_Type; 636 Item : in Float; 637 Fore : in Natural; 638 Aft : in Natural; 639 Exp : in Natural) 640 is 641 begin 642 if Is_Out( File) then 643 Real_IO.Put( File_Ref( File), Item, Fore, Aft, Exp); 644 end if; 645 exception 646 when others => null; 647 end Put_Float; 648 649 procedure Get_Float_From_String( Source : in String; 650 Item : out Float; 651 Start_Pos : in Positive; 652 Stop : out Natural) 653 is 654 begin 655 Real_IO.Get( Source( Start_Pos..Source'Last), Item, Stop); 656 exception 657 when others => Stop := Start_Pos - 1; 658 end Get_Float_From_String; 659 660 procedure Put_Float_To_String( Dest : in out String; 661 Item : in Float; 662 Start_Pos : in Positive; 663 Aft : in Natural; 664 Exp : in Natural) 665 is 666 begin 667 Real_IO.Put( Dest( Start_Pos..Dest'Last), Item, Aft, Exp); 668 exception 669 when others => null; 670 end Put_Float_To_String; 671 672 end Spark_IO; --- ( 1) Warning : 10: The body of package Spark_IO is hidden - hidden text is ignored by the SPARK Examiner [Explanatory note: Issued when a --# hide XXX annotation is used. (warning control file keyword: hidden_parts)]. --End of file--------------------------------------------------