class interface BINARY_FILE_READ
   -- This class allow to read a file on the disk as a binary file 
   -- (ie. file containing bytes). If you need to read a file which 
   -- contain text, then consider using TEXT_FILE_READ.

creation
   make
      -- The new created object is not connected. (See also connect_to.)

      ensure
         not is_connected

   connect_to (new_path: STRING)
      -- Open binary file for reading. The stream is positioned at the
      -- beginning of the file.

      require
         not is_connected;
         not new_path.is_empty

feature(s) from FILE   is_connected: BOOLEAN
      -- Is this file connected to some file of the operating system?

      ensure
         definition: Result = (path /= Void)

   connect_to (new_path: STRING)
      -- Open binary file for reading. The stream is positioned at the
      -- beginning of the file.

      require
         not is_connected;
         not new_path.is_empty

   disconnect
      -- Disconnect from any file.

      require
         is_connected
      ensure
         not is_connected

feature(s) from BINARY_FILE_READ   path: STRING
      -- Not Void when connected to the corresponding file on the disk.


   read_byte
      -- Read a byte and assign it to last_byte.

      require
         is_connected;
         not end_of_input

   last_byte: INTEGER
      -- Last byte read with read_byte.


   read_integer_16_native_endian
      -- Read in the same order as the machine running this code. If a 
      -- 16-bits value is available, it's assigned to last_integer_16.
      -- The result is machine dependant.

      require
         is_connected;
         not end_of_input

   read_integer_16_big_endian
      -- Read a big endian value is the file. If a 16-bits value
      -- is available, it's assigned to last_integer_16.

      require
         is_connected;
         not end_of_input

   read_integer_16_little_endian
      -- Read a little endian value is the file. If a 16-bits value
      -- is available, it's assigned to last_integer_16.

      require
         is_connected;
         not end_of_input

   last_integer_16: INTEGER
      -- Last byte read with read_integer_16_*.


   end_of_input: BOOLEAN
      -- Has end-of-input been reached ?
      -- True when the last character has been read.




end of BINARY_FILE_READ