gnatprove_11.2.3_f7ece6d3/share/examples/spark/ipstack/src/support.native/aip-io.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
------------------------------------------------------------------------------
--                            IPSTACK COMPONENTS                            --
--          Copyright (C) 2012-2017, Free Software Foundation, Inc.         --
------------------------------------------------------------------------------

with Ada.Text_IO;

package body AIP.IO with
  SPARK_Mode => Off
is

   Last : Integer := 0;

   procedure Put (S : String) renames Ada.Text_IO.Put;
   procedure Put_Line (S : String) renames Ada.Text_IO.Put_Line;

   function Line_Available return Boolean is
      Available : Boolean;
   begin
      Ada.Text_IO.Get_Immediate (Line (Last + 1), Available);
      if not Available then
         return False;
      end if;
      Last := Last + 1;
      return Line (Last) = ASCII.LF;
   end Line_Available;

   function Get_Last return Integer is
      R_Last : constant Integer := Last;
   begin
      Last := 0;
      return R_Last - 1;
   end Get_Last;

end AIP.IO;