class interface F_MEMORY_FILE
creation
make (file_name: STRING)
require
ok: file_name /= Void; -- fail if file is not valid and accessible
file_ok:
ensure
done: -- is_alive set if succesful
feature(s) from MEMORY
-- Removal :
dispose
-- Free memory mapped file.
full_collect
-- Force a full collection cycle if garbage collection is
-- enabled; do nothing otherwise.
feature(s) from F_MEMORY
-- Finalisation
close
-- Close memory object (free memory, handled
-- by finalisation if omitted).
require
alive: size /= 0
ensure
done: size = 0
feature(s) from F_MEMORY
-- Copy
copy (other: like Current)
-- Copy other memory block. Other MUST be the same size
-- as Current.
require
other_not_void: other /= Void
ensure
size: size = other.size;
is_equal: is_equal(other)
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object considered equal to
-- current object ?
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal(other) implies Result;
symmetric: Result implies other.is_equal(Current)
feature(s) from F_MEMORY
is_writable: BOOLEAN
-- Memory mapped file read-only.
ensure
mmap_read_only: Result = false
feature(s) from F_MEMORY
-- Size/Index
size: INTEGER
-- Size of the memory block.
offset (offs: INTEGER): INTEGER
-- Convert an offset to a position.
require
valid: offs >= 0 and offs < size
ensure
done: Result = offs + 1
is_index (idx: INTEGER): BOOLEAN
-- Is idx a valid index?
ensure
done: Result = (idx >= 1 and idx <= size)
feature(s) from F_MEMORY
byte (index: INTEGER): INTEGER
-- Get the value of the byte at index position.
require
valid: is_index(index)
ensure
valid_byte: Result >= 0 and Result <= 255
set_byte (index, value: INTEGER)
-- Set the value of the byte at current position.
require
writable: is_writable;
valid_index: is_index(index);
valid_byte: value >= 0 and value <= 255
ensure
done: byte(index) = value
feature(s) from F_MEMORY
-- Subset
subset (start, length: INTEGER): F_MEMORY
-- Get a copy of a subset of the memory
-- block.
require
valid: is_index(start);
length: length > 0;
bounds: is_index(start + length - 1)
ensure
is_copy: Result /= Void
set_subset (idx: INTEGER; sub_set: F_MEMORY)
-- Set a block of memory inside this one.
require
writable: is_writable;
valid: is_index(idx);
length: is_index(idx + sub_set.size - 1)
ensure
done: subset(idx,sub_set.size).is_equal(sub_set)
feature(s) from F_MEMORY
-- Get unsigned 16-bit WORDs.
unsigned_word (idx: INTEGER): INTEGER
-- Convert this memory block to integer, as a
-- machine-order WORD
require
valid: is_index(idx);
word: is_index(idx + 1)
ensure
done: Result < Max_unsigned_word and Result >= 0
little_unsigned_word (idx: INTEGER): INTEGER
-- Like get_word, little endian order.
require
valid: is_index(idx);
word: is_index(idx + 1)
ensure
done: Result < Max_unsigned_word and Result >= 0
big_unsigned_word (idx: INTEGER): INTEGER
-- Like get_word, big endian order.
require
valid: is_index(idx);
word: is_index(idx + 1)
ensure
done: Result < Max_unsigned_word and Result >= 0
feature(s) from F_MEMORY
-- Set unsigned 16-bit WORDs.
set_unsigned_word (idx: INTEGER; value: INTEGER)
require
writable: is_writable;
valid: is_index(idx) and is_index(idx + 1);
value: value < Max_unsigned_word and value >= 0
ensure
done: value = unsigned_word(idx)
set_little_unsigned_word (idx: INTEGER; value: INTEGER)
require
writable: is_writable;
valid: is_index(idx) and is_index(idx + 1);
value: value < Max_unsigned_word and value >= 0
ensure
done: value = little_unsigned_word(idx)
set_big_unsigned_word (idx: INTEGER; value: INTEGER)
require
writable: is_writable;
valid: is_index(idx) and is_index(idx + 1);
value: value < Max_unsigned_word and value >= 0
ensure
done: value = big_unsigned_word(idx)
feature(s) from F_MEMORY
-- Signed WORD (16 bits, 2 bytes).
word (idx: INTEGER): INTEGER
-- Convert the two bytes at idx to integer as
-- a machine unsigned_word.
require
valid: is_index(idx);
word: is_index(idx + 1)
ensure
done: Result < Max_word and Result > - Max_word
little_word (idx: INTEGER): INTEGER
-- Little endian signed word.
require
valid: is_index(idx);
word: is_index(idx + 1)
ensure
done: Result < Max_word and Result > - Max_word
big_word (idx: INTEGER): INTEGER
-- Big endian signed word.
require
valid: is_index(idx);
word: is_index(idx + 1)
ensure
done: Result < Max_word and Result > - Max_word
feature(s) from F_MEMORY
-- Set 16-bit unsigned WORD.
set_word (idx: INTEGER; value: INTEGER)
require
writable: is_writable;
valid: is_index(idx) and is_index(idx + 1);
value: value < Max_word and value > - Max_word
ensure
done: value = word(idx)
set_little_word (idx: INTEGER; value: INTEGER)
require
writable: is_writable;
valid: is_index(idx) and is_index(idx + 1);
value: value < Max_word and value > - Max_word
ensure
done: value = little_word(idx)
set_big_word (idx: INTEGER; value: INTEGER)
require
writable: is_writable;
valid: is_index(idx) and is_index(idx + 1);
value: value < Max_word and value > - Max_word
ensure
done: value = big_word(idx)
feature(s) from F_MEMORY
-- DWORD
double_word (idx: INTEGER): INTEGER
-- Get (signed) 32-bit integer starting atidx,
-- machine byte order.
require
valid: is_index(idx);
dword: is_index(idx + 3)
little_double_word (idx: INTEGER): INTEGER
-- Get little endian (signed) 32-bit integer.
require
valid: is_index(idx);
dword: is_index(idx + 3)
big_double_word (idx: INTEGER): INTEGER
-- Get big endian (signed) 32-bit integer.
require
valid: is_index(idx);
dword: is_index(idx + 3)
feature(s) from F_MEMORY
-- Set DWORD
set_double_word (idx: INTEGER; value: INTEGER)
-- Set (signed) 32-bit integer at idx.
-- Machine byte order.
require
writable: is_writable;
valid: is_index(idx);
dword: is_index(idx + 3)
ensure
done: double_word(idx) = value
set_little_double_word (idx: INTEGER; value: INTEGER)
-- Set little endian (signed) 32-bit integer at idx.
require
writable: is_writable;
valid: is_index(idx);
dword: is_index(idx + 3)
ensure
done: little_double_word(idx) = value
set_big_double_word (idx: INTEGER; value: INTEGER)
-- Set big endian (signed) 32-bit integer at idx.
require
writable: is_writable;
valid: is_index(idx);
dword: is_index(idx + 3)
ensure
done: big_double_word(idx) = value
feature(s) from F_MEMORY
-- C String
cstring (idx, length: INTEGER): STRING
-- Read system dependent string, character width is
-- the same as the system's CHARACTER. Scanning
-- terminates at first 0 or length whichever happens
-- first. NOTE: length is in bytes.
require
valid_index: is_index(idx);
valid_length: length > 0;
valid_end: is_index(idx + length - 1)
byte_cstring (idx, length: INTEGER): STRING
-- Read string with 8-bit characters, up to
-- a zero byte or length.
require
valid_index: is_index(idx);
valid_length: length > 0;
valid_end: is_index(idx + length - 1)
set_cstring (idx, length: INTEGER; str: STRING)
require
writable: is_writable;
valid_index: is_index(idx);
valid_length: length > 0;
valid_end: is_index(idx + length - 1);
valid_str: str /= Void
ensure
done: cstring(idx,length).is_equal(str)
set_byte_cstring (idx, length: INTEGER; str: STRING)
-- Write string with one byte per characters,
-- bytes between str.count + 1 and length are
-- set to zero.
require
writable: is_writable;
valid_index: is_index(idx);
valid_length: length > 0;
valid_end: is_index(idx + length - 1);
valid_str: str /= Void
ensure
done: byte_cstring(idx,length).is_equal(str)
feature(s) from F_MEMORY
-- Bit operations
bit_and (a, b: INTEGER): INTEGER
-- Bitwise AND (like C '&')
bit_or (a, b: INTEGER): INTEGER
-- Bitwise OR (like C '|')
bit_xor (a, b: INTEGER): INTEGER
-- Bitwise XOR (like C '^')
feature(s) from F_MEMORY
-- Constants
Max_word: INTEGER
-- 2^15
Max_unsigned_word: INTEGER
-- 2^16
feature(s) from F_MEMORY_FILE
is_alive: BOOLEAN
-- Is this memory mapped file working?
ensure
size_ok: is_alive implies size > 0
invariant
implementation: -- ? Integer_bits >= 32
end of F_MEMORY_FILE