class BINARY_FILE_WRITE

Features exported to ANY

This class allow to write a file on the disk as a binary file (ie. file containing bytes). If you need to write text in a file, then consider using TEXT_FILE_WRITE.

Direct parents

conformant parents

DISPOSABLE, FILE

Summary

creation features

exported features

Details

make

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

ensure

  • not is_connected

connect_to (new_path: STRING)

Truncate file to zero length or create binary file for writing. 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 path.same_as(new_path)

connect_for_appending_to (new_path: STRING)

Truncate file to zero length or create binary file for writing. The stream is positioned at the beginning of the file.

require

  • not is_connected
  • not new_path.is_empty

connect_to (new_path: STRING)

Truncate file to zero length or create binary file for writing. 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 path.same_as(new_path)

connect_for_appending_to (new_path: STRING)

Truncate file to zero length or create binary file for writing. The stream is positioned at the beginning of the file.

require

  • not is_connected
  • not new_path.is_empty

flush

forces a write of unwritten character (write my have been delayed, flush writes buffered characters)

disconnect

Disconnect from any file.

require

  • is_connected

ensure

  • not is_connected

put_byte (byte: INTEGER)

require

  • is_connected

put_integer_16_native_endian (i: INTEGER_16)

Write in the same order as the machine running this code. The result is machine dependant.

require

  • is_connected

put_integer_16_big_endian (i: INTEGER_16)

Write i in big endian mode. The result is machine independant.

require

  • is_connected

put_integer_16_little_endian (i: INTEGER_16)

Write i in little endian mode. The result is machine independant.

require

  • is_connected

put_integer_32_native_endian (i: INTEGER)

Write in the same order as the machine running this code. The result is machine dependant.

require

  • is_connected

put_integer_32_big_endian (i: INTEGER)

Write i in big endian mode. The result is machine independant.

require

  • is_connected

put_integer_32_little_endian (i: INTEGER)

Write i in little endian mode. The result is machine independant.

require

  • is_connected

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)