class BINARY_FILE_READ

All features

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.

Direct parents

conformant parents

FILE

Summary

creation features

exported features

Details

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_malformed_path: not new_path.is_empty

ensure

  • is_connected implies not end_of_input
  • is_connected implies path.same_as(new_path)

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_malformed_path: not new_path.is_empty

ensure

  • is_connected implies not end_of_input
  • is_connected implies path.same_as(new_path)

disconnect

Disconnect from any file.

require

  • is_connected

ensure

  • not is_connected

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

read_integer_32_native_endian

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

require

  • is_connected
  • not end_of_input

read_integer_32_big_endian

Read a big endian value is the file. If 32-bits value is available, it's assigned to last_integer_32.

require

  • is_connected
  • not end_of_input

read_integer_32_little_endian

Read a little endian value is the file. If a 32-bits value is available, it's assigned to last_integer_32.

require

  • is_connected
  • not end_of_input

last_integer_32: INTEGER
end_of_input: BOOLEAN

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

buffer: NATIVE_ARRAY [E_][CHARACTER]
buffer_position: INTEGER
buffer_size: INTEGER
capacity: INTEGER
input_stream: POINTER
fill_buffer
make

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

ensure

  • not is_connected

binary_file_read_open (path_pointer: POINTER): POINTER
io_fread (buf: NATIVE_ARRAY [E_][CHARACTER], size: INTEGER, stream_pointer: POINTER): INTEGER

return size read or 0 if end of input (-1 on error => exception ?)

io_fclose (stream_pointer: POINTER)
as_16_ne (c1: CHARACTER, c2: CHARACTER): INTEGER_16
as_32_ne (i1: INTEGER_16, i2: INTEGER_16): INTEGER
path: STRING

Not Void when connected to the corresponding file on the disk.

is_connected: BOOLEAN

Is this file connected to some file of the operating system?

ensure

  • definition: Result = (path /= Void)