gcc/ada/libgnat/a-tifiio.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                 A D A . T E X T _ I O . F I X E D _ I O                  --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 -- This specification is derived from the Ada Reference Manual for use with --
  10 -- GNAT.  In accordance with the copyright of that document, you can freely --
  11 -- copy and modify this specification,  provided that if you redistribute a --
  12 -- modified version,  any changes that you have made are clearly indicated. --
  13 --                                                                          --
  14 ------------------------------------------------------------------------------
  15
  16 --  In Ada 95, the package Ada.Text_IO.Fixed_IO is a subpackage of Text_IO.
  17 --  This is for compatibility with Ada 83. In GNAT we make it a child package
  18 --  to avoid loading the necessary code if Fixed_IO is not instantiated. See
  19 --  routine Rtsfind.Check_Text_IO_Special_Unit for a description of how we
  20 --  patch up the difference in semantics so that it is invisible to the Ada
  21 --  programmer.
  22
  23 private generic
  24    type Num is delta <>;
  25
  26 package Ada.Text_IO.Fixed_IO with
  27   SPARK_Mode => On,
  28   Always_Terminates
  29 is
  30
  31    Default_Fore : Field := Num'Fore;
  32    Default_Aft  : Field := Num'Aft;
  33    Default_Exp  : Field := 0;
  34
  35    procedure Get
  36      (File  : File_Type;
  37       Item  : out Num;
  38       Width : Field := 0)
  39    with
  40      Pre               => Is_Open (File) and then Mode (File) = In_File,
  41      Global            => (In_Out => File_System),
  42      Exceptional_Cases => (Data_Error | End_Error => Standard.True);
  43
  44    procedure Get
  45      (Item  : out Num;
  46       Width : Field := 0)
  47    with
  48      Post              =>
  49        Line_Length'Old = Line_Length
  50        and Page_Length'Old = Page_Length,
  51      Global            => (In_Out => File_System),
  52      Exceptional_Cases => (Data_Error | End_Error => Standard.True);
  53
  54    procedure Put
  55      (File : File_Type;
  56       Item : Num;
  57       Fore : Field := Default_Fore;
  58       Aft  : Field := Default_Aft;
  59       Exp  : Field := Default_Exp)
  60    with
  61      Pre               => Is_Open (File) and then Mode (File) /= In_File,
  62      Post              =>
  63        Line_Length (File)'Old = Line_Length (File)
  64        and Page_Length (File)'Old = Page_Length (File),
  65      Global            => (In_Out => File_System),
  66      Exceptional_Cases => (Layout_Error => Line_Length (File) /= 0);
  67
  68    procedure Put
  69      (Item : Num;
  70       Fore : Field := Default_Fore;
  71       Aft  : Field := Default_Aft;
  72       Exp  : Field := Default_Exp)
  73    with
  74      Post              =>
  75        Line_Length'Old = Line_Length
  76        and Page_Length'Old = Page_Length,
  77      Global            => (In_Out => File_System),
  78      Exceptional_Cases => (Layout_Error => Ada.Text_IO.Line_Length /= 0);
  79
  80    procedure Get
  81      (From : String;
  82       Item : out Num;
  83       Last : out Positive)
  84    with
  85      Global            => null,
  86      Exceptional_Cases => (Data_Error => Standard.True);
  87
  88    procedure Put
  89      (To   : out String;
  90       Item : Num;
  91       Aft  : Field := Default_Aft;
  92       Exp  : Field := Default_Exp)
  93    with
  94      Global            => null,
  95      Exceptional_Cases => (Layout_Error => Standard.True);
  96
  97 private
  98    pragma Inline (Get);
  99    pragma Inline (Put);
 100
 101 end Ada.Text_IO.Fixed_IO;