class BINARY_FILE_READ
Summary
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
Inherit list: BINARY_INPUT_STREAM, FILE_STREAM, TERMINAL_INPUT_STREAM
Insert list: PLATFORM
Class invariant
Overview
Creation features
{ANY}
Features
{ANY}
{FILTER}
{FILTER_INPUT_STREAM}
{}
{ANY}
{FILTER_INPUT_STREAM}
{FILTER}
{ANY}
{}
{ANY}
{}
{STREAM_HANDLER}
{ANY}
{}
{RECYCLING_POOL}
  • recycle
    Do whatever needs to be done to free resources or recycle other objects when recycling this one
{}
  • dispose
    Action to be executed just before garbage collection reclaims an object.
{}
{ANY}
Skipping separators:
{ANY}
To read one number at a time:
{ANY}
To read one line or one word at a time:
{ANY}
Other features:
{ANY}
{}
{FILTER}
{ANY}
  • path: STRING
    Not Void when connected to the corresponding file on the disk.
{}
Maximum:
{}
Minimum:
{}
Bits:
{}
connect_to (new_path: ABSTRACT_STRING)
effective procedure
{ANY}
Open binary file for reading.
The stream is positioned at the beginning of the file.
See also make, with_buffer_size.
require
  • not is_connected
  • not_malformed_path: not new_path.is_empty
ensure
disconnect
effective procedure
{ANY}
Try to disconnect the stream.
Note that it *does not* ensure that the stream will effectively be disconnected (some terminal streams, for instance, are always connected) but the feature can be used to "shake off" filters.
require
      • is_connected
      • can_disconnect
      • is_connected
      • can_disconnect
      • is_connected
      • can_disconnect
      • is_connected
      • can_disconnect
    • is_connected
    • can_disconnect
ensure
  • not is_filtered
can_unread_character: BOOLEAN
effective function
{ANY}
require
    • is_connected
    • valid_last_character
    • is_connected
    • valid_last_character
read_byte
effective procedure
{ANY}
Read a byte and assign it to last_byte.
require
  • is_connected
  • not is_filtered
  • can_read_character
last_byte: INTEGER_32
effective function
{ANY}
Last byte read with read_byte.
require
  • is_connected
  • not end_of_input
  • not is_filtered
ensure
read_integer_16_native_endian
effective procedure
{ANY}
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 is_filtered
  • can_read_character
read_integer_16_big_endian
effective procedure
{ANY}
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 is_filtered
  • can_read_character
read_integer_16_little_endian
effective procedure
{ANY}
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 is_filtered
  • can_read_character
last_integer_16: INTEGER_32
writable attribute
{ANY}
Last byte read with read_integer_16_*.
require
  • is_connected
  • not end_of_input
  • not is_filtered
read_integer_32_native_endian
effective procedure
{ANY}
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
read_integer_32_big_endian
effective procedure
{ANY}
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 is_filtered
  • can_read_character
read_integer_32_little_endian
effective procedure
{ANY}
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 is_filtered
  • can_read_character
last_integer_32: INTEGER_32
writable attribute
{ANY}
require
  • is_connected
  • not end_of_input
  • not is_filtered
end_of_input: BOOLEAN
writable attribute
{ANY}
end_of_input means the previous attempt in character reading failed because the end has been reached.
So last_character is not valid and you are not allowed to do any read attempt anymore.
Notes:
  • Just after a successful connect, end_of_input is always False because you did not yet read anything).
  • Once the end of input has been reached, this is definitive in that no more characters will ever be provided (but of course you can still come back if can_unread_character; end_of_input will be changed if you unread_character). In that, it is different from can_read_character which is only a temporary state.
Please refer to the Liberty Eiffel FAQ or tutorial/io examples.
seek (new_offset: INTEGER_64)
effective procedure
{ANY}
Next read will start at position new_offset, counted from the beginning of the file.
See also offset.
require ensure
offset: INTEGER_64
effective function
{ANY}
The offset that will be used for the next read.
See also seek.
require
terminal_settings: TERMINAL_SETTINGS
effective function
{ANY}
ensure
  • valid: Result /= Void
  • associated: Result.associated_stream = Current
filtered_descriptor: INTEGER_32
effective function
Find the descriptor of the terminal stream...
Filters do not have descriptors of their own
require
      • is_connected
      • filtered_has_descriptor
      • is_connected
      • filtered_has_descriptor
      • is_connected
      • filtered_has_descriptor
      • is_connected
      • filtered_has_descriptor
    • is_connected
    • filtered_has_descriptor
filtered_has_descriptor: BOOLEAN
is True
constant attribute
True if the underlying terminal stream has a descriptor
require
      • is_connected
      • is_connected
      • is_connected
      • is_connected
    • is_connected
filtered_stream_pointer: POINTER
writable attribute
Find the pointer of the terminal stream...
Filters do not have pointers of their own
require
      • is_connected
      • filtered_has_stream_pointer
      • is_connected
      • filtered_has_stream_pointer
      • is_connected
      • filtered_has_stream_pointer
      • is_connected
      • filtered_has_stream_pointer
    • is_connected
    • filtered_has_stream_pointer
filtered_has_stream_pointer: BOOLEAN
is True
constant attribute
True if the underlying terminal stream has a pointer
require
      • is_connected
      • is_connected
      • is_connected
      • is_connected
    • is_connected
filtered_read_character
effective procedure
require
    • is_connected
    • can_read_character
    • is_connected
    • can_read_character
filtered_unread_character
effective procedure
require
    • is_connected
    • can_unread_character
    • is_connected
    • can_unread_character
filtered_last_character: CHARACTER
writable attribute
require
    • is_connected
    • valid_last_character
    • is_connected
    • valid_last_character
writable attribute
{}
buffer_position: INTEGER_32
writable attribute
{}
buffer_size: INTEGER_32
writable attribute
{}
capacity: INTEGER_32
writable attribute
{}
the_terminal_settings: TERMINAL_SETTINGS
writable attribute
{}
fill_buffer
effective procedure
{}
make
effective procedure
{}
The new created object is not connected.
(See also connect_to.)
ensure
with_buffer_size (buffer_capacity: INTEGER_32)
effective procedure
{}
binary_file_read_open (path_pointer: POINTER): POINTER
{}
io_fclose (stream: POINTER)
{}
io_fseek (path_pointer: POINTER, new_offset: INTEGER_64): INTEGER_32
{}
ensure
  • Result = 0
    failure otherwise

io_ftell (path_pointer: POINTER): INTEGER_64
{}
ensure
  • Result >= 0
    failure otherwise

as_16_ne (c1: CHARACTER, c2: CHARACTER): INTEGER_16
{}
as_32_ne (i1: INTEGER_16, i2: INTEGER_16): INTEGER_32
{}
read_character
effective procedure
{ANY}
If read_character fail, end_of_input is set.
Else, use last_character. Read tutorial or io cluster documentation to learn the read_character usage pattern.
require
  • is_connected
  • not is_filtered and then can_read_character
ensure
read_line_in (buffer: STRING)
effective procedure
{ANY}
Same job as read_line but storage is directly done in buffer.
Read tutorial or io cluster documentation to learn the read_line usage pattern.
require
  • is_connected
  • not is_filtered and then can_read_line
  • buffer /= Void
read_available_in (buffer: STRING, limit: INTEGER_32)
effective procedure
{ANY}
Same job as read_available but storage is directly done in buffer.
The usage pattern is the same as for read_line.
require
  • is_connected
  • not is_filtered
  • buffer /= Void
  • limit > 0
unread_character
effective procedure
{ANY}
require
  • is_connected
  • not is_filtered and then can_unread_character
ensure
last_character: CHARACTER
effective function
{ANY}
require
  • is_connected
  • not end_of_input
  • not is_filtered and then valid_last_character
ensure
detach
effective procedure
{ANY}
Shake off the filter.
ensure
  • not is_filtered
filtered_read_available_in (buffer: STRING, limit: INTEGER_32)
effective procedure
require
filtered_read_line_in (buffer: STRING)
effective procedure
require
writable attribute
The filter that uses this stream as backend
event_can_read: EVENT_DESCRIPTOR
effective function
{ANY}
writable attribute
{}
new_url: URL
effective function
{}
ensure
  • Result /= Void
is_connected: BOOLEAN
deferred function
{ANY}
True if the stream is connected.
Only in that case can data be transferred via this stream.
descriptor: INTEGER_32
effective function
{ANY}
Some OS-dependent descriptor.
Mainly used by the sequencer library (see READY_CONDITION).
require
has_descriptor: BOOLEAN
effective function
{ANY}
True if that stream can be associated to some OS-meaningful descriptor.
require
can_disconnect: BOOLEAN
deferred function
{ANY}
True if the stream can be safely disconnected (without data loss, etc.)
require
url: URL
frozen
effective function
{ANY}
The URL to this stream as resource
ensure
  • not_void: Result /= Void
  • always_the_same: Result = url
url_memory: URL
writable attribute
{}
stream_pointer: POINTER
effective function
Some Back-end-dependent pointer (FILE* in C, InputStream or OutputStream in Java)
has_stream_pointer: BOOLEAN
effective function
True if that stream can be associated to some Back-end-meaningful stream pointer.
require
event_exception: EVENT_DESCRIPTOR
effective function
{ANY}
stream_exception: STREAM_EXCEPTION
writable attribute
{}
recycle
effective procedure
Do whatever needs to be done to free resources or recycle other objects when recycling this one
dispose
effective procedure
{}
Action to be executed just before garbage collection reclaims an object.
sequencer_descriptor (file: POINTER): INTEGER_32
{}
can_read_character: BOOLEAN
deferred function
{ANY}
Note that this state is usually temporary.
Usually it is called until either it becomes True or the stream is disconnected:
 from
 until
    stream.can_read_character or else not stream.is_connected
 loop
    -- some "still waiting..." code, maybe a sandglass?
 end
 if stream.is_connected then
    stream.read_character
 end
See also: is_connected, end_of_input
require ensure
can_read_line: BOOLEAN
deferred function
{ANY}
require
valid_last_character: BOOLEAN
deferred function
{ANY}
require
is_filtered: BOOLEAN
deferred function
{ANY}
skip_separators
effective procedure
{ANY}
Skip all separators (see is_separator of class CHARACTER) and make the first non-separator available in last_character.
This non-separator character is pushed back into the stream (see unread_character) to be available one more time (the next read_character will consider this non-separator). When end_of_input occurs, this process is automatically stopped.
require
skip_separators_using (separators: STRING)
effective procedure
{ANY}
Same job as skip_separators using the separators set.
require
skip_remainder_of_line
effective procedure
{ANY}
Skip all the remainder of the line including the end of line delimiter itself.
read_integer
effective procedure
{ANY}
Read an integer according to the Eiffel syntax.
 Make result available in last_integer.  Heading
separators are automatically skipped using is_separator of class CHARACTER.  Trailing separators
are not skipped.
require ensure
last_integer: INTEGER_32
writable attribute
{ANY}
Last integer read using read_integer.
valid_last_integer: BOOLEAN
writable attribute
{ANY}
Was the last call to read_integer successful ?
last_real: REAL_64
writable attribute
{ANY}
Last real read with read_real.
valid_last_real: BOOLEAN
writable attribute
{ANY}
Was the last call to read_real successful ?
read_real
effective procedure
{ANY}
Read a REAL and make the result available in last_real.
require ensure
last_string: STRING
once function
{ANY}
Access to the unique common buffer to get for example the result computed by read_line, read_word, newline, etc.
This is a once function (the same common buffer is used for all streams).
read_line
effective procedure
{ANY}
Read a complete line ended by '%N' or end_of_input.%
% Make the result available in last_string common buffer. The end of line character (usually '%N') is not added in the last_string buffer. Read tutorial or io cluster documentation to learn the read_line usage pattern.
See also read_line_in.
require
read_available (limit: INTEGER_32)
effective procedure
{ANY}
Read as many characters as possible, as long as the stream does not block and up to the given limit.
read_word
effective procedure
{ANY}
Read a word using is_separator of class CHARACTER.
The result is available in the last_string common buffer. Heading separators are automatically skipped. Trailing separators are not skipped (last_character is left on the first one). If end_of_input is encountered, Result can be the empty string.
require
newline
effective procedure
{ANY}
Consume input until newline ('%N') is found.
% The corresponding STRING is stored in last_string common buffer.
require
reach_and_skip (keyword: STRING)
effective procedure
{ANY}
Try to skip enough characters in order to reach the keyword which is skipped too.
If the keyword is not in the remainder of this stream, the process is stopped as soon as end_of_input occurs.
require ensure
read_word_using (separators: STRING)
effective procedure
{ANY}
Same job as read_word using separators.
require
read_tail_in (str: STRING)
effective procedure
{ANY}
Read all remaining character of the stream in str.
require ensure
io_getc (stream: POINTER): INTEGER_32
{}
io_ungetc (byte: CHARACTER, stream: POINTER)
{}
io_fread (buf: NATIVE_ARRAY[CHARACTER], size: INTEGER_32, stream: POINTER): INTEGER_32
{}
return size read or 0 if end of input (-1 on error => exception ?)
{}
set_filter (a_filter: FILTER)
effective procedure
Used by the filter itself to get attached
require
  • a_filter /= Void
ensure
path: STRING
writable attribute
{ANY}
Not Void when connected to the corresponding file on the disk.
set_path (new_path: ABSTRACT_STRING)
effective procedure
{}
ensure
  • path.same_as(new_path.out)
Maximum_character_code: INTEGER_16
{}
Largest supported code for CHARACTER values.
ensure
  • meaningful: Result >= 127
Maximum_integer_8: INTEGER_8
is 127
constant attribute
{}
Largest supported value of type INTEGER_8.
Maximum_integer_16: INTEGER_16
is 32767
constant attribute
{}
Largest supported value of type INTEGER_16.
Maximum_integer: INTEGER_32
is 2147483647
constant attribute
{}
Largest supported value of type INTEGER/INTEGER_32.
Maximum_integer_32: INTEGER_32
is 2147483647
constant attribute
{}
Largest supported value of type INTEGER/INTEGER_32.
Maximum_integer_64: INTEGER_64
is 9223372036854775807
constant attribute
{}
Largest supported value of type INTEGER_64.
Maximum_real_32: REAL_32
is {REAL_32 3.4028234663852885981170418348451692544e+38}
constant attribute
{}
Largest non-special (no NaNs nor infinity) supported value of type REAL_32.
Maximum_real: REAL_64
{}
Largest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: 1.79769313486231570....e+308
Maximum_real_64: REAL_64
{}
Largest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: 1.79769313486231570....e+308
Maximum_real_80: REAL_EXTENDED
{}
Largest supported value of type REAL_80.
ensure
Minimum_character_code: INTEGER_16
{}
Smallest supported code for CHARACTER values.
ensure
  • meaningful: Result <= 0
Minimum_integer_8: INTEGER_8
is -128
constant attribute
{}
Smallest supported value of type INTEGER_8.
Minimum_integer_16: INTEGER_16
is -32768
constant attribute
{}
Smallest supported value of type INTEGER_16.
Minimum_integer: INTEGER_32
is -2147483648
constant attribute
{}
Smallest supported value of type INTEGER/INTEGER_32.
Minimum_integer_32: INTEGER_32
is -2147483648
constant attribute
{}
Smallest supported value of type INTEGER/INTEGER_32.
Minimum_integer_64: INTEGER_64
is -9223372036854775808
constant attribute
{}
Smallest supported value of type INTEGER_64.
Minimum_real_32: REAL_32
is {REAL_32 -3.40282346638528859811704183484516925440e+38}
constant attribute
{}
Smallest non-special (no NaNs nor infinity) supported value of type REAL_32.
Minimum_real: REAL_64
{}
Smallest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: -1.79769313486231570....e+308
Minimum_real_64: REAL_64
{}
Smallest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: -1.79769313486231570....e+308
Minimum_real_80: REAL_64
{}
Smallest supported value of type REAL_80.
ensure
  • meaningful: Result <= 0.0
Boolean_bits: INTEGER_32
{}
Number of bits in a value of type BOOLEAN.
ensure
  • meaningful: Result >= 1
Character_bits: INTEGER_32
{}
Number of bits in a value of type CHARACTER.
ensure
Integer_bits: INTEGER_32
{}
Number of bits in a value of type INTEGER.
ensure
  • integer_definition: Result = 32
Real_bits: INTEGER_32
is 64
constant attribute
{}
Number of bits in a value of type REAL.
Pointer_bits: INTEGER_32
{}
Number of bits in a value of type POINTER.