1---------------------------------------------------------------- 2-- IRONSIDES - DNS SERVER 3-- 4-- By: Martin C. Carlisle and Barry S. Fagin 5-- Department of Computer Science 6-- United States Air Force Academy 7-- 8-- This is free software; you can redistribute it and/or 9-- modify without restriction. We do ask that you please keep 10-- the original author information, and clearly indicate if the 11-- software has been modified. 12-- 13-- This software is distributed in the hope that it will be useful, 14-- but WITHOUT ANY WARRANTY; without even the implied warranty 15-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 16---------------------------------------------------------------- 17 18with Text_IO; 19with Unchecked_Deallocation; 20 21 22package body Protected_Spark_Io_05 is 23 --# hide Protected_SPARK_IO_05; 24 25 type File_System is 26 record 27 Standard_Input : File_Type; 28 Standard_Output : File_Type; 29 end record; 30 File_System_Standard_Input : aliased File_Descriptor := 31 File_Descriptor'(File_Ref => Text_IO.Standard_Input); 32 File_System_Standard_Output : aliased File_Descriptor := 33 File_Descriptor'(File_Ref => Text_IO.Standard_Output); 34 35 File_Sys : constant File_System := 36 File_System'(Standard_Input => File_System_Standard_Input'access, 37 Standard_Output => File_System_Standard_Output'access); 38 39 package Integer_IO is new Text_IO.Integer_IO (Integer); 40 package Real_IO is new Text_IO.Float_IO (Float); 41 42 43 procedure Dispose is new Unchecked_Deallocation 44 (File_Descriptor, File_Type); 45 46 47 ------------------------------------------------------------------------------- 48 -- (C) Altran Praxis Limited 49 ------------------------------------------------------------------------------- 50 -- 51 -- The SPARK toolset is free software; you can redistribute it and/or modify it 52 -- under terms of the GNU General Public License as published by the Free 53 -- Software Foundation; either version 3, or (at your option) any later 54 -- version. The SPARK toolset is distributed in the hope that it will be 55 -- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of 56 -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General 57 -- Public License for more details. You should have received a copy of the GNU 58 -- General Public License distributed with the SPARK toolset; see file 59 -- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of 60 -- the license. 61 -- 62 --============================================================================= 63 64 protected body SPARK_IO_05 65 is 66 --# hide SPARK_IO_05; 67 68 -- File Management 69 70 71 72 function Standard_Input return File_Type 73 is 74 begin 75 return File_Sys.Standard_Input; 76 end Standard_Input; 77 78 function Standard_Output return File_Type 79 is 80 begin 81 return File_Sys.Standard_Output; 82 end Standard_Output; 83 84 procedure Create (File : out File_Type; 85 Name_Of_File : in String; 86 Form_Of_File : in String; 87 Status : out File_Status) 88 is 89 begin 90 Create_Flex (File => File, 91 Name_Length => Name_Of_File'Length, 92 Name_Of_File => Name_Of_File, 93 Form_Of_File => Form_Of_File, 94 Status => Status); 95 end Create; 96 97 procedure Create_Flex (File : out File_Type; 98 Name_Length : in Natural; 99 Name_Of_File : in String; 100 Form_Of_File : in String; 101 Status : out File_Status) 102 is 103 begin 104 File := new File_Descriptor; 105 Text_IO.Create (File.File_Ref, 106 Text_IO.Out_File, 107 Name_Of_File (Name_Of_File'First .. Name_Length), 108 Form_Of_File); 109 Status := Ok; 110 exception 111 when Text_IO.Status_Error => 112 Status := Status_Error; 113 Dispose (File); 114 when Text_IO.Name_Error => 115 Status := Name_Error; 116 Dispose (File); 117 when Text_IO.Use_Error => 118 Status := Use_Error; 119 Dispose (File); 120 when Text_IO.Device_Error => 121 Status := Device_Error; 122 Dispose (File); 123 when Standard.Storage_Error => 124 Status := Storage_Error; 125 Dispose (File); 126 when Standard.Program_Error => 127 Status := Program_Error; 128 Dispose (File); 129 end Create_Flex; 130 131 procedure Open (File : out File_Type; 132 Mode_Of_File : in File_Mode; 133 Name_Of_File : in String; 134 Form_Of_File : in String; 135 Status : out File_Status) 136 is 137 begin 138 Open_Flex (File => File, 139 Mode_Of_File => Mode_Of_File, 140 Name_Length => Name_Of_File'Length, 141 Name_Of_File => Name_Of_File, 142 Form_Of_File => Form_Of_File, 143 Status => Status); 144 end Open; 145 146 procedure Open_Flex (File : out File_Type; 147 Mode_Of_File : in File_Mode; 148 Name_Length : in Natural; 149 Name_Of_File : in String; 150 Form_Of_File : in String; 151 Status : out File_Status) 152 is 153 F_Mode : Text_IO.File_Mode; 154 begin 155 File := new File_Descriptor; 156 case Mode_Of_File is 157 when In_File => F_Mode := Text_IO.In_File; 158 when Out_File => F_Mode := Text_IO.Out_File; 159 when Append_File => F_Mode := Text_IO.Append_File; 160 end case; 161 Text_IO.Open (File.File_Ref, 162 F_Mode, 163 Name_Of_File (Name_Of_File'First .. Name_Length), 164 Form_Of_File); 165 Status := Ok; 166 exception 167 when Text_IO.Status_Error => 168 Status := Status_Error; 169 Dispose (File); 170 when Text_IO.Name_Error => 171 Status := Name_Error; 172 Dispose (File); 173 when Text_IO.Use_Error => 174 Status := Use_Error; 175 Dispose (File); 176 when Text_IO.Device_Error => 177 Status := Device_Error; 178 Dispose (File); 179 when Standard.Storage_Error => 180 Status := Storage_Error; 181 Dispose (File); 182 when Standard.Program_Error => 183 Status := Program_Error; 184 Dispose (File); 185 end Open_Flex; 186 187 procedure Close (File : in out File_Type; 188 Status : out File_Status) 189 is 190 begin 191 if File = null then 192 Status := Status_Error; 193 else 194 Text_IO.Close (File.File_Ref); 195 Dispose (File); 196 Status := Ok; 197 end if; 198 exception 199 when Text_IO.Status_Error => 200 Status := Status_Error; 201 Dispose (File); 202 when Text_IO.Device_Error => 203 Status := Device_Error; 204 Dispose (File); 205 when Constraint_Error => 206 Status := Use_Error; 207 Dispose (File); 208 when Standard.Storage_Error => 209 Status := Storage_Error; 210 Dispose (File); 211 when Standard.Program_Error => 212 Status := Program_Error; 213 Dispose (File); 214 end Close; 215 216 procedure Delete (File : in out File_Type; 217 Status : out File_Status) 218 is 219 begin 220 if File = null then 221 Status := Status_Error; 222 else 223 Text_IO.Delete (File.File_Ref); 224 Dispose (File); 225 Status := Ok; 226 end if; 227 exception 228 when Text_IO.Status_Error => 229 Status := Status_Error; 230 Dispose (File); 231 when Text_IO.Use_Error => 232 Status := Use_Error; 233 Dispose (File); 234 when Text_IO.Device_Error => 235 Status := Device_Error; 236 Dispose (File); 237 when Constraint_Error => 238 Status := Use_Error; 239 Dispose (File); 240 when Standard.Storage_Error => 241 Status := Storage_Error; 242 Dispose (File); 243 when Standard.Program_Error => 244 Status := Program_Error; 245 Dispose (File); 246 end Delete; 247 248 procedure Reset (File : in out File_Type; 249 Mode_Of_File : in File_Mode; 250 Status : out File_Status) 251 is 252 F_Mode : Text_IO.File_Mode; 253 begin 254 if File = null then 255 Status := Status_Error; 256 else 257 case Mode_Of_File is 258 when In_File => F_Mode := Text_IO.In_File; 259 when Out_File => F_Mode := Text_IO.Out_File; 260 when Append_File => F_Mode := Text_IO.Append_File; 261 end case; 262 Text_IO.Reset (File.File_Ref, 263 F_Mode); 264 Status := Ok; 265 end if; 266 exception 267 when Text_IO.Status_Error => 268 Status := Status_Error; 269 Dispose (File); 270 when Text_IO.Use_Error => 271 Status := Use_Error; 272 Dispose (File); 273 when Text_IO.Device_Error => 274 Status := Device_Error; 275 Dispose (File); 276 when Standard.Storage_Error => 277 Status := Storage_Error; 278 Dispose (File); 279 when Standard.Program_Error => 280 Status := Program_Error; 281 Dispose (File); 282 end Reset; 283 284 function Valid_File (File : File_Type) return Boolean 285 is 286 begin 287 return File /= null; 288 end Valid_File; 289 290 function Is_Open (File : File_Type) return Boolean 291 is 292 begin 293 return Valid_File (File) and then 294 Text_IO.Is_Open (File.File_Ref); 295 end Is_Open; 296 297 function Mode (File : File_Type) return File_Mode 298 is 299 F_Mode : File_Mode; 300 begin 301 if Is_Open (File) and then 302 Text_IO.Is_Open (File.File_Ref) then 303 case Text_IO.Mode (File.File_Ref) is 304 when Text_IO.In_File => 305 F_Mode := In_File; 306 when Text_IO.Out_File => 307 F_Mode := Out_File; 308 when Text_IO.Append_File => 309 F_Mode := Append_File; 310 end case; 311 else 312 F_Mode := In_File; 313 end if; 314 return F_Mode; 315 end Mode; 316 317 function Is_In (File : File_Type) return Boolean; 318 319 function Is_In (File : File_Type) return Boolean 320 is 321 begin 322 return Is_Open (File) and then Mode (File) = In_File; 323 end Is_In; 324 325 function Is_Out (File : File_Type) return Boolean; 326 327 function Is_Out (File : File_Type) return Boolean 328 is 329 begin 330 return Is_Open (File) and then (Mode (File) = Out_File or 331 Mode (File) = Append_File); 332 end Is_Out; 333 334 procedure Name (File : in File_Type; 335 Name_Of_File : out String; 336 Stop : out Natural) 337 is 338 begin 339 if Is_Open (File) then 340 declare 341 FN : constant String := Text_IO.Name (File.File_Ref); 342 begin 343 if Name_Of_File'Length >= FN'Length then 344 Name_Of_File (FN'range) := FN; 345 Stop := FN'Length; 346 else 347 Name_Of_File := FN (Name_Of_File'range); 348 Stop := Name_Of_File'Length; 349 end if; 350 end; 351 else 352 Stop := Name_Of_File'First - 1; 353 end if; 354 exception 355 when others => Stop := Name_Of_File'First - 1; 356 end Name; 357 358 procedure Form (File : in File_Type; 359 Form_Of_File : out String; 360 Stop : out Natural) 361 is 362 begin 363 if Is_Open (File) then 364 declare 365 FM : constant String := Text_IO.Form (File.File_Ref); 366 begin 367 if Form_Of_File'Length >= FM'Length then 368 Form_Of_File (FM'range) := FM; 369 Stop := FM'Length; 370 else 371 Form_Of_File := FM (Form_Of_File'range); 372 Stop := Form_Of_File'Length; 373 end if; 374 end; 375 else 376 Stop := Form_Of_File'First - 1; 377 end if; 378 exception 379 when others => Stop := Form_Of_File'First - 1; 380 end Form; 381 382 -- Line and file terminator control 383 384 function P_To_PC (P : Positive) return Text_IO.Positive_Count; 385 386 function P_To_PC (P : Positive) return Text_IO.Positive_Count 387 is 388 begin 389 return Text_IO.Positive_Count (P); 390 end P_To_PC; 391 392 function PC_To_P (PC : Text_IO.Positive_Count) return Positive; 393 394 function PC_To_P (PC : Text_IO.Positive_Count) return Positive 395 is 396 begin 397 return Positive (PC); 398 end PC_To_P; 399 400 procedure New_Line (File : in File_Type; 401 Spacing : in Positive) 402 is 403 Gap : Text_IO.Positive_Count; 404 begin 405 if Is_Out (File) then 406 Gap := P_To_PC (Spacing); 407 Text_IO.New_Line (File.File_Ref, Gap); 408 end if; 409 exception 410 when others => null; 411 end New_Line; 412 413 procedure Skip_Line (File : in File_Type; 414 Spacing : in Positive) 415 is 416 Gap : Text_IO.Positive_Count; 417 begin 418 if Is_In (File) then 419 Gap := P_To_PC (Spacing); 420 Text_IO.Skip_Line (File.File_Ref, Gap); 421 end if; 422 exception 423 when others => null; 424 end Skip_Line; 425 426 procedure New_Page (File : in File_Type) 427 is 428 begin 429 if Is_Out (File) then 430 Text_IO.New_Page (File.File_Ref); 431 end if; 432 exception 433 when others => null; 434 end New_Page; 435 436 function End_Of_Line (File : File_Type) return Boolean 437 is 438 EOLN : Boolean; 439 begin 440 if Is_In (File) then 441 EOLN := Text_IO.End_Of_Line (File.File_Ref); 442 else 443 EOLN := False; 444 end if; 445 return EOLN; 446 end End_Of_Line; 447 448 function End_Of_File (File : File_Type) return Boolean 449 is 450 EOF : Boolean; 451 begin 452 if Is_In (File) then 453 EOF := Text_IO.End_Of_File (File.File_Ref); 454 else 455 EOF := True; 456 end if; 457 return EOF; 458 end End_Of_File; 459 460 procedure Set_Col (File : in File_Type; 461 Posn : in Positive); 462 463 procedure Set_Col (File : in File_Type; 464 Posn : in Positive) 465 is 466 Col : Text_IO.Positive_Count; 467 begin 468 if Is_Open (File) then 469 Col := P_To_PC (Posn); 470 Text_IO.Set_Col (File.File_Ref, Col); 471 end if; 472 exception 473 when others => null; 474 end Set_Col; 475 476 procedure Set_In_File_Col (File : in File_Type; 477 Posn : in Positive) 478 is 479 begin 480 if Is_In (File) then 481 Set_Col (File, Posn); 482 end if; 483 end Set_In_File_Col; 484 485 procedure Set_Out_File_Col (File : in File_Type; 486 Posn : in Positive) 487 is 488 begin 489 if Is_Out (File) then 490 Set_Col (File, Posn); 491 end if; 492 end Set_Out_File_Col; 493 494 function Col (File : File_Type) return Positive; 495 496 function Col (File : File_Type) return Positive 497 is 498 Posn : Positive; 499 Col : Text_IO.Positive_Count; 500 begin 501 if Is_Open (File) then 502 Col := Text_IO.Col (File.File_Ref); 503 Posn := PC_To_P (Col); 504 else 505 Posn := 1; 506 end if; 507 return Posn; 508 exception 509 when Text_IO.Status_Error => return 1; 510 when Text_IO.Layout_Error => return PC_To_P (Text_IO.Count'Last); 511 when Text_IO.Device_Error => return 1; 512 when Standard.Storage_Error => return 1; 513 when Standard.Program_Error => return 1; 514 end Col; 515 516 function In_File_Col (File : File_Type) return Positive 517 is 518 begin 519 if Is_In (File) then 520 return Col (File); 521 else 522 return 1; 523 end if; 524 end In_File_Col; 525 526 function Out_File_Col (File : File_Type) return Positive 527 is 528 begin 529 if Is_Out (File) then 530 return Col (File); 531 else 532 return 1; 533 end if; 534 end Out_File_Col; 535 536 function Line (File : File_Type) return Positive; 537 538 function Line (File : File_Type) return Positive 539 is 540 Posn : Positive; 541 Line : Text_IO.Positive_Count; 542 begin 543 if Is_Open (File) then 544 Line := Text_IO.Line (File.File_Ref); 545 Posn := PC_To_P (Line); 546 else 547 Posn := 1; 548 end if; 549 return Posn; 550 exception 551 when Text_IO.Status_Error => return 1; 552 when Text_IO.Layout_Error => return PC_To_P (Text_IO.Count'Last); 553 when Text_IO.Device_Error => return 1; 554 when Standard.Storage_Error => return 1; 555 when Standard.Program_Error => return 1; 556 end Line; 557 558 function In_File_Line (File : File_Type) return Positive 559 is 560 begin 561 if Is_In (File) then 562 return Line (File); 563 else 564 return 1; 565 end if; 566 end In_File_Line; 567 568 function Out_File_Line (File : File_Type) return Positive 569 is 570 begin 571 if Is_Out (File) then 572 return Line (File); 573 else 574 return 1; 575 end if; 576 end Out_File_Line; 577 578 -- Character IO 579 580 procedure Get_Char (File : in File_Type; 581 Item : out Character) 582 is 583 begin 584 if Is_In (File) then 585 Text_IO.Get (File.File_Ref, Item); 586 else 587 Item := Character'First; 588 end if; 589 exception 590 when others => null; 591 end Get_Char; 592 593 procedure Put_Char (File : in File_Type; 594 Item : in Character) 595 is 596 begin 597 if Is_Out (File) then 598 Text_IO.Put (File.File_Ref, Item); 599 end if; 600 exception 601 when others => null; 602 end Put_Char; 603 604 procedure Get_Char_Immediate (File : in File_Type; 605 Item : out Character; 606 Status : out File_Status) 607 is 608 begin 609 if Is_In (File) then 610 Text_IO.Get_Immediate (File.File_Ref, Item); 611 Status := Ok; 612 else 613 Item := Character'First; 614 Status := Mode_Error; 615 end if; 616 exception 617 when others => 618 Item := Character'First; 619 Status := End_Error; 620 end Get_Char_Immediate; 621 622 -- String IO 623 624 procedure Get_String (File : in File_Type; 625 Item : out String; 626 Stop : out Natural) 627 is 628 LSTP : Natural; 629 begin 630 if Is_In (File) then 631 LSTP := Item'First - 1; 632 loop 633 exit when End_Of_File (File); 634 LSTP := LSTP + 1; 635 Get_Char (File, Item (LSTP)); 636 exit when LSTP = Item'Last; 637 end loop; 638 Stop := LSTP; 639 else 640 Stop := Item'First - 1; 641 end if; 642 end Get_String; 643 644 -- CFR 718 The behaviour of Put_String is now as follows: 645 -- If Stop is 0 then all characters in Item are output. 646 -- If Stop <= Item'Last then output Item(Item'First .. Stop). 647 -- If Stop > Item'Last then output all characters in Item, then pad with 648 -- spaces to width specified by Stop. 649 procedure Put_String (File : in File_Type; 650 Item : in String; 651 Stop : in Natural) 652 is 653 Pad : Natural; 654 begin 655 if Is_Out (File) then 656 if Stop = 0 then 657 Text_IO.Put (File.File_Ref, Item); 658 elsif Stop <= Item'Last then 659 Text_IO.Put (File.File_Ref, Item (Item'First .. Stop)); 660 else 661 Pad := Stop - Item'Last; 662 Text_IO.Put (File.File_Ref, Item); 663 while Pad > 0 loop 664 Text_IO.Put (File.File_Ref, ' '); 665 Pad := Pad - 1; 666 end loop; 667 end if; 668 end if; 669 exception 670 when others => null; 671 end Put_String; 672 673 procedure Get_Line (File : in File_Type; 674 Item : out String; 675 Stop : out Natural) 676 is 677 begin 678 if Is_In (File) then 679 Text_IO.Get_Line (File.File_Ref, Item, Stop); 680 else 681 Stop := Item'First - 1; 682 end if; 683 exception 684 when others => Stop := Item'First - 1; 685 end Get_Line; 686 687 procedure Put_Line (File : in File_Type; 688 Item : in String; 689 Stop : in Natural) 690 is 691 ES : Positive; 692 begin 693 if Stop = 0 then 694 ES := Item'Last; 695 else 696 ES := Stop; 697 end if; 698 if Is_Out (File) then 699 Text_IO.Put_Line (File.File_Ref, Item (Item'First .. ES)); 700 end if; 701 exception 702 when others => null; 703 end Put_Line; 704 705 706 -- Integer IO 707 708 procedure Get_Integer (File : in File_Type; 709 Item : out Integer; 710 Width : in Natural; 711 Read : out Boolean) 712 is 713 begin 714 if Is_In (File) then 715 Integer_IO.Get (File.File_Ref, Item, Width); 716 Read := True; 717 else 718 Read := False; 719 end if; 720 exception 721 when others => Read := False; 722 end Get_Integer; 723 724 procedure Put_Integer (File : in File_Type; 725 Item : in Integer; 726 Width : in Natural; 727 Base : in Number_Base) 728 is 729 begin 730 if Is_Out (File) then 731 Integer_IO.Put (File.File_Ref, Item, Width, Base); 732 end if; 733 exception 734 when others => null; 735 end Put_Integer; 736 737 procedure Get_Int_From_String (Source : in String; 738 Item : out Integer; 739 Start_Pos : in Positive; 740 Stop : out Natural) 741 is 742 begin 743 Integer_IO.Get (Source (Start_Pos .. Source'Last), Item, Stop); 744 exception 745 when others => Stop := Start_Pos - 1; 746 end Get_Int_From_String; 747 748 procedure Put_Int_To_String (Dest : in out String; 749 Item : in Integer; 750 Start_Pos : in Positive; 751 Base : in Number_Base) 752 is 753 begin 754 Integer_IO.Put (Dest (Start_Pos .. Dest'Last), Item, Base); 755 exception 756 when others => null; 757 end Put_Int_To_String; 758 759 760 -- Float IO 761 762 procedure Get_Float (File : in File_Type; 763 Item : out Float; 764 Width : in Natural; 765 Read : out Boolean) 766 is 767 begin 768 if Is_In (File) then 769 Real_IO.Get (File.File_Ref, Item, Width); 770 Read := True; 771 else 772 Read := False; 773 end if; 774 exception 775 when others => Read := False; 776 end Get_Float; 777 778 procedure Put_Float (File : in File_Type; 779 Item : in Float; 780 Fore : in Natural; 781 Aft : in Natural; 782 Exp : in Natural) 783 is 784 begin 785 if Is_Out (File) then 786 Real_IO.Put (File.File_Ref, Item, Fore, Aft, Exp); 787 end if; 788 exception 789 when others => null; 790 end Put_Float; 791 792 procedure Get_Float_From_String (Source : in String; 793 Item : out Float; 794 Start_Pos : in Positive; 795 Stop : out Natural) 796 is 797 begin 798 Real_IO.Get (Source (Start_Pos .. Source'Last), Item, Stop); 799 exception 800 when others => Stop := Start_Pos - 1; 801 end Get_Float_From_String; 802 803 procedure Put_Float_To_String (Dest : in out String; 804 Item : in Float; 805 Start_Pos : in Positive; 806 Aft : in Natural; 807 Exp : in Natural) 808 is 809 begin 810 Real_IO.Put (Dest (Start_Pos .. Dest'Last), Item, Aft, Exp); 811 exception 812 when others => null; 813 end Put_Float_To_String; 814 815 end SPARK_IO_05; 816end Protected_Spark_Io_05; 817 818