*******************************************************
                           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--------------------------------------------------